[Toss-devel-svn] SF.net SVN: toss:[1574] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1574] trunk/Toss
|
From: <luk...@us...> - 2011-09-27 09:44:04
|
Revision: 1574
http://toss.svn.sourceforge.net/toss/?rev=1574&view=rev
Author: lukstafi
Date: 2011-09-27 09:43:50 +0000 (Tue, 27 Sep 2011)
Log Message:
-----------
GDL translation: major overhaul due to extending compact argument passing from defined relations to all relations; removed constant argument elimination, instead fluent-discriminating information is passed to relations using additional (val_X) elements introduced recently.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/GDL.mli
trunk/Toss/GGP/GDLTest.ml
trunk/Toss/GGP/TranslateFormula.ml
trunk/Toss/GGP/TranslateFormula.mli
trunk/Toss/GGP/TranslateFormulaTest.ml
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/GGP/TranslateGameTest.ml
trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss
trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
trunk/Toss/GGP/tests/breakthrough-raw.toss
trunk/Toss/GGP/tests/breakthrough-simpl.toss
trunk/Toss/GGP/tests/connect4-raw.toss
trunk/Toss/GGP/tests/connect4-simpl.toss
trunk/Toss/GGP/tests/connect5-raw.toss
trunk/Toss/GGP/tests/connect5-simpl.toss
trunk/Toss/GGP/tests/tictactoe-raw.toss
trunk/Toss/GGP/tests/tictactoe-simpl.toss
trunk/Toss/www/reference/reference.tex
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/Formula/Aux.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -342,11 +342,11 @@
x :: unique eq (List.filter (fun y -> not (eq y x)) xs)
let not_unique xs =
- let rec aux left = function
+ let rec aux = function
| [] -> false
- | x :: xs when List.mem x left || List.mem x xs -> true
- | x :: xs -> aux (x::left) xs in
- aux [] xs
+ | x :: xs when List.mem x xs -> true
+ | x :: xs -> aux xs in
+ aux xs
let take_n n l =
let rec aux n acc = function
@@ -545,6 +545,8 @@
let neg f x = not (f x)
+let is_right = function Right _ -> true | Left _ -> false
+
let partition_choice l =
let rec split laux raux = function
| [] -> List.rev laux, List.rev raux
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/Formula/Aux.mli 2011-09-27 09:43:50 UTC (rev 1574)
@@ -267,6 +267,8 @@
(** [neg f x = not (f x)] *)
val neg : ('a -> bool) -> 'a -> bool
+val is_right : ('a, 'b) choice -> bool
+
(** Partition a list of tagged elements into the [Left] and
[Right]-tagged elements. *)
val partition_choice : ('a, 'b) choice list -> 'a list * 'b list
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/GDL.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -221,7 +221,7 @@
stratify (stratum::strata) (more_rules @ rules)
(* Topological-like sort w.r.t. the call-graph. *)
-let topsort_callgraph clauses for_rels =
+let topsort_callgraph (*for_rels*) clauses =
let defs = defs_of_rules (Aux.concat_map rules_of_clause clauses) in
(* building incidence list *)
let defs = List.map
@@ -232,7 +232,7 @@
defs in
let defs = List.map
(fun (rel, drels) ->
- rel, Aux.strings_of_list (Aux.list_inter drels for_rels)) defs in
+ rel, Aux.strings_of_list (*Aux.list_inter for_rels*) drels) defs in
let rec aux strata defs =
if defs = [] then List.flatten (List.rev strata)
else
@@ -247,7 +247,7 @@
let defs = List.map
(fun (r,calls) -> r, Aux.Strings.diff calls visited) defs in
aux (stratum::strata) defs in
- aux [] (List.filter (fun (r,_) -> List.mem r for_rels) defs)
+ aux [] (*List.filter (fun (r,_) -> List.mem r for_rels)*) defs
let rec subst_one (x, term as sb) = function
| Var y when x=y -> term
@@ -444,6 +444,9 @@
| Disj disjs ->
"(or "^String.concat " " (List.map literal_str disjs)^")"
+let literals_str lits =
+ String.concat " " (List.map literal_str lits)
+
let clause_str (head, body) =
"(<= "^rel_atom_str head^"\n "^String.concat "\n "
(List.map literal_str body)^")"
@@ -1050,29 +1053,69 @@
Aux.concat_map (elim_ground_arg_in_body rel arg grounding)
(renamed_brs @ clauses)
-let elim_ground_args rels clauses =
- let new_rels = ref [] and all_rels = ref [] in
- let rec aux clauses = function
+let elim_ground_args rels1 rels2 clauses =
+ let new_rels1 = ref [] and all_rels1 = ref [] in
+ let new_rels2 = ref [] and all_rels2 = ref [] in
+ let rec aux new_rels all_rels clauses = function
| [] -> clauses
| rel::rels ->
(let try arg = find_ground_arg rel clauses in
- aux (elim_ground_arg new_rels rel arg clauses) rels
+ let clauses = elim_ground_arg new_rels rel arg clauses in
+ aux new_rels all_rels clauses rels
with Not_found ->
- all_rels := rel:: !all_rels; aux clauses rels) in
+ all_rels := rel:: !all_rels;
+ aux new_rels all_rels clauses rels) in
let rec fix clauses =
- all_rels := !new_rels @ !all_rels;
- new_rels := [];
- let clauses = aux clauses rels in
- if !new_rels <> []
+ all_rels1 := !new_rels1 @ !all_rels1;
+ new_rels1 := [];
+ let clauses = aux new_rels1 all_rels1 clauses rels1 in
+ all_rels2 := !new_rels2 @ !all_rels2;
+ new_rels2 := [];
+ let clauses = aux new_rels2 all_rels2 clauses rels2 in
+ if !new_rels1 <> [] || !new_rels2 <> []
then fix clauses
else
- let all_rels = List.filter
+ let all_rels1 = List.filter
(fun r->List.exists
(function ((rel,_),_) when r=rel -> true | _ -> false) clauses)
- (Aux.unique_sorted !all_rels) in
- all_rels, clauses in
+ (Aux.unique_sorted !all_rels1) in
+ let all_rels2 = List.filter
+ (fun r->List.exists
+ (function ((rel,_),_) when r=rel -> true | _ -> false) clauses)
+ (Aux.unique_sorted !all_rels2) in
+ all_rels1, all_rels2, clauses in
fix clauses
+let elim_ground_distinct clauses =
+ let rec filter_disj = function
+ | Pos (Distinct ts) when Aux.Strings.is_empty (terms_vars ts) ->
+ if Aux.not_unique (Array.to_list ts)
+ then None
+ else raise Not_found (* disjunction is true *)
+ | Neg (Distinct ts) when Aux.Strings.is_empty (terms_vars ts) ->
+ if Aux.not_unique (Array.to_list ts)
+ then raise Not_found (* disjunction is true *)
+ else None
+ | Disj d -> Some (Disj (Aux.map_some filter_disj d))
+ | lit -> Some lit in
+ let filter_conj = function
+ | Pos (Distinct ts) when Aux.Strings.is_empty (terms_vars ts) ->
+ if Aux.not_unique (Array.to_list ts)
+ then raise Not_found
+ else None
+ | Neg (Distinct ts) when Aux.Strings.is_empty (terms_vars ts) ->
+ if Aux.not_unique (Array.to_list ts)
+ then None
+ else raise Not_found
+ | Disj d ->
+ (try Some (Disj (Aux.map_some filter_disj d)) with Not_found -> None)
+ | lit -> Some lit in
+ Aux.map_try
+ (fun (h, body) ->
+ h, Aux.map_some filter_conj body)
+ clauses
+
+
let state_cls terms =
List.map (fun t -> ("true", [|t|]), []) terms
@@ -1765,7 +1808,9 @@
List.fold_left (fun acc (p, s) -> subst_past_blank arities p s acc)
blank path_subts
with Not_found ->
- invalid_arg "blank_outside_subterms: conflicting paths"
+ invalid_arg
+ ("blank_outside_subterms: conflicting paths "^
+ (String.concat "; "(List.map (fun (p,_)->path_str p) path_subts)))
(* If some path points only to bigger than one (i.e. non-leaf)
@@ -1889,3 +1934,13 @@
(* }}} *)
let res = aux terms paths in
res
+
+(* The integers should be all-distinct and in {0..N-1}. *)
+type argpaths = (path * int) list list
+
+
+let find_rel_arg sterms args apset =
+ List.find
+ (fun s -> List.for_all (fun (p,i) ->
+ try at_path s p = args.(i) with Not_found -> false) apset)
+ sterms
Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/GDL.mli 2011-09-27 09:43:50 UTC (rev 1574)
@@ -151,8 +151,11 @@
defining clause. Return the new clauses, and also the new
relation set. *)
val elim_ground_args :
- string list -> clause list -> string list * clause list
+ string list -> string list -> clause list ->
+ string list * string list * clause list
+val elim_ground_distinct : clause list -> clause list
+
val state_cls : term list -> clause list
(** {3 GDL translation helpers.} *)
@@ -171,9 +174,11 @@
val rel_atom_str : rel_atom -> string
val def_str : string * def_branch list -> string
val literal_str : literal -> string
+val literals_str : literal list -> string
val clause_str : clause -> string
+val sb_str : (string * term) list -> string
-val topsort_callgraph : clause list -> string list -> string list
+val topsort_callgraph : (* string list -> *) clause list -> string list
(** {3 GDL whole-game operations.}
@@ -286,3 +291,8 @@
in terms. *)
val refine_paths_avoiding :
path_set -> (term -> bool) -> (term -> bool) -> term list -> path_set
+
+(** The integers should be all-distinct and in {0..N-1}. *)
+type argpaths = (path * int) list list
+
+val find_rel_arg : term list -> term array -> (path * int) list -> term
Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/GDLTest.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -338,8 +338,8 @@
(nextcol ?d ?e)
(true (cell ?x ?e o)))
" in
- let defined_rels, result =
- elim_ground_args ["conn5"; "col"; "row"] descr in
+ let _, defined_rels, result =
+ elim_ground_args [] ["conn5"; "col"; "row"] descr in
let res_s =
(String.concat "\n" (List.map GDL.clause_str result)) in
assert_equal ~printer:(fun x->x)
Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/TranslateFormula.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -4,6 +4,21 @@
let debug_level = ref 0
+type transl_data = {
+ f_paths : path_set; (* fluent paths *)
+ c_paths : path_set; (* coordinate paths *)
+ all_paths : path_set; (* sum of f_paths and c_paths *)
+ root_reps : term list; (* coordinate root terms *)
+ counters : string list;
+ num_functions : (string * Formula.real_expr) list;
+ defined_rels : string list;
+ argpaths : (string * (path list array, argpaths) Aux.choice) list;
+ (* [Left argpaths] are coordinating relation argument paths, [Right
+ argpaths] is fact relation argument partition. *)
+ term_arities : (string * int) list;
+}
+
+
let rel_atoms body =
Aux.map_some (function Rel (rel, args) -> Some (rel, args)
| _ -> None) (atoms_of_body body)
@@ -61,22 +76,6 @@
| _ -> assert false
) state_terms in
other, pos_terms, neg_terms) disj
-
-type defrel_argpaths = (GDL.path * int) list list
-
-type transl_data = {
- f_paths : path_set; (* fluent paths *)
- c_paths : path_set; (* coordinate paths *)
- all_paths : path_set; (* sum of f_paths and c_paths *)
- root_reps : term list; (* coordinate root terms *)
- counters : string list;
- num_functions : (string * Formula.real_expr) list;
- defined_rels : string list;
- mutable defrel_argpaths : (string * defrel_argpaths) list;
- (* late binding to store $ArgMode# data *)
- term_arities : (string * int) list;
- rel_default_path : (string * path option array) list;
-}
let empty_transl_data = {
f_paths = empty_path_set;
@@ -86,9 +85,8 @@
num_functions = [];
counters = [];
defined_rels = [];
- defrel_argpaths = [];
+ argpaths = [];
term_arities = [];
- rel_default_path = [];
}
let blank_out data t =
@@ -106,27 +104,26 @@
(term_to_name (blank_outside_subterms data.term_arities path_subts))
-let find_defrel_arg sterms args apset =
+let find_rel_arg sterms args apset =
List.find
(fun s -> List.for_all (fun (p,i) ->
try at_path s p = args.(i) with Not_found -> false) apset)
sterms
-let translate_defrel data sterms sign rel args =
+let translate_factrel data sterms sign rel args partition =
(* {{{ log entry *)
if !debug_level > 2 then (
- Printf.printf "translate_defrel: phi=%s, sign=%b\n"
+ Printf.printf "translate_factrel: phi=%s, sign=%b\n"
(rel_atom_str (rel, args)) sign
);
(* }}} *)
- let partition = List.assoc rel data.defrel_argpaths in
let s_l =
- try List.map (find_defrel_arg sterms args) partition
+ try List.map (find_rel_arg sterms args) partition
with Not_found -> failwith
- ("could not build arguments for defined relation "^rel) in
+ ("could not build arguments for relation "^rel) in
let vtup = Array.of_list (List.map (var_of_term data) s_l) in
- let defrel_phi = Formula.Rel (rel, vtup) in
- if sign then defrel_phi else Formula.Not defrel_phi
+ let rel_phi = Formula.Rel (rel, vtup) in
+ if sign then rel_phi else Formula.Not rel_phi
let minus a b = Formula.Plus (a, Formula.Times (Formula.Const (-1.), b))
let counter_v = `FO counter_n
@@ -149,7 +146,13 @@
);
(* }}} *)
let s_subterms = Aux.collect s_subterms in
- let transl_rel sign rel args =
+ let transl_coordrel sign rel args =
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "transl_coordrel: sign=%B; atom=%s\n%!"
+ sign (rel_atom_str (rel, args))
+ );
+ (* }}} *)
(let try stuples =
List.map (fun arg -> List.assoc arg s_subterms)
(Array.to_list args) in
@@ -167,17 +170,18 @@
if rel = "EQ_" && vartup.(0) = vartup.(1)
then None
else
- let fact_rel = rel_on_paths rel (List.map snd stup) in
- Some (Formula.Rel (fact_rel, vartup)))
+ let rname = rel_on_paths rel (List.map snd stup) in
+ Some (Formula.Rel (rname, vartup)))
stuples in
if sign then atoms
else List.map (fun a -> Formula.Not a) atoms
- with Not_found -> []) in
- let transl_posdefrel sign rel args =
- if List.mem rel data.defined_rels
- then
- [translate_defrel data sterms_all sign rel args]
- else transl_rel sign rel args in
+ with Not_found -> assert false) in
+ let transl_rel sign rel args =
+ match List.assoc rel data.argpaths with
+ | Aux.Left _ ->
+ transl_coordrel sign rel args
+ | Aux.Right partition ->
+ [translate_factrel data sterms_all sign rel args partition] in
let transl_c = function
| Const v when
(try ignore (float_of_string v); true with _ -> false) ->
@@ -218,8 +222,8 @@
(try ignore [transl_c t1; transl_c t2]; true
with Not_found -> false) ->
transl_numfun_rel false rel t1 t2
- | Pos (Rel (rel, args)) -> transl_posdefrel true rel args
- | Neg (Rel (rel, args)) -> transl_posdefrel false rel args
+ | Pos (Rel (rel, args)) -> transl_rel true rel args
+ | Neg (Rel (rel, args)) -> transl_rel false rel args
| Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
[]
| Pos (Distinct ts) ->
@@ -372,171 +376,19 @@
else res
(* **************************************** *)
-(* {3 Build and use defined relations.} *)
+(* {3 Build defined relations.} *)
-let select_defrel_argpaths drel data clauses =
- let atoms_sterms = List.map
- (fun ((rel,args), body) ->
- let r_atoms = if rel = drel then [args] else [] in
- let r_atoms = r_atoms @ Aux.map_some
- (function Rel (rel, args) when rel = drel -> Some args
- | _ -> None)
- (atoms_of_body body) in
- r_atoms, state_terms body
- (* we take all state terms to have more compact partition *)
- (*Aux.map_some
- (function Pos (True s) -> Some s | _ -> None) body*))
- clauses in
- let check_path args p s_p =
- let inds = Aux.array_argfind_all (fun r -> r=s_p) args in
- List.map (fun i->p,i) inds in
- let sterm_path_sets args s =
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "sterm_path_sets: rel=%s args={%s} sterm=%s\n%!"
- drel
- (String.concat ", " (Array.to_list (Array.map term_str args)))
- (term_str s)
- );
- (* }}} *)
- let psets = map_paths (check_path args) data.c_paths s in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "sterm_path_sets: psets=%s\n%!"
- (String.concat "; "(List.map (fun pset->"["^
- String.concat ", " (List.map (fun (p,i)->
- path_str p^":"^string_of_int i) pset)^"]") psets))
- );
- (* }}} *)
- let ptups = Aux.product (Aux.list_remove [] psets) in
- (* distinct [p] in a tuple is already ensured *)
- List.filter (fun tup ->
- not (Aux.not_unique (List.map snd tup))) ptups in
- let argpath_sets = Aux.concat_map
- (fun (atoms, sterms) -> Aux.concat_map
- (fun args -> Aux.concat_map (sterm_path_sets args) sterms)
- atoms)
- atoms_sterms in
- let argpath_sets =
- Aux.map_reduce (fun pset -> pset, 1) (+) 0 argpath_sets in
- let argpath_sets = List.sort Pervasives.compare
- (List.map (* lexicographic comparison *)
- (fun (pset,count) -> List.length pset, count, pset)
- argpath_sets) in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf
- "select_defrel_argpaths: drel=%s; argpath_sets=\n%!" drel;
- List.iter (fun (len, count, pset) ->
- Printf.printf "len=%d; count=%d; pset=%s\n%!" len count
- (String.concat ", "
- (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
- argpath_sets
- );
- (* }}} *)
- let argpath_sets = List.map Aux.trd3 (List.rev argpath_sets) in
- (* now greedily -- by traversing the ordering -- select covering *)
- let apsets_cover = List.fold_left
- (fun cover apset ->
- if List.exists
- (fun (_,i) -> not (List.exists (fun cov_apset ->
- List.exists (fun (_,j)->i=j) cov_apset) cover)) apset
- then apset::cover else cover)
- [] argpath_sets in
- (* eliminating multiple points -- starting with best apsets so
- they're unchanged *)
- let partition = List.fold_left
- (fun partition apset ->
- let apset = List.filter (fun (_,i) ->
- not (List.exists (fun cov_apset ->
- List.exists (fun (_,j)->i=j) cov_apset) partition)) apset in
- if apset = [] then partition else apset::partition)
- [] apsets_cover in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf
- "select_defrel_argpaths: drel=%s; partition=\n%!" drel;
- List.iter (fun pset ->
- Printf.printf "pset=%s\n%!"
- (String.concat ", "
- (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
- partition
- );
- (* }}} *)
- (* filling-in missing paths from precomputed defaults *)
- let arity = Array.length
- (List.hd (fst (List.find (fun (atoms,_) -> atoms<>[])
- atoms_sterms))) in
- let argpaths = Array.init arity
- (fun i ->
- try List.find (List.exists (fun (_,j)->i=j)) partition
- with Not_found ->
- try
- match (List.assoc drel data.rel_default_path).(i) with
- | Some p -> [p, i]
- | None -> raise Not_found
- with Not_found ->
- failwith
- (Printf.sprintf
- "TranslateFormula.build_defrels: could not \
- determine path for relation %s argument %d" drel i)
- ) in
- let res = Aux.unique (=) (Array.to_list argpaths) in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf
- "select_defrel_argpaths: drel=%s; result=\n%!" drel;
- List.iter (fun pset ->
- Printf.printf "pset=%s\n%!"
- (String.concat ", "
- (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
- res
- );
- (* }}} *)
- res
-
-
-let defrel_transform drel partition data ((h_rel,h_args as h),body as cl) =
- (* adding "true" atoms to clauses for missing argpath state terms *)
- let r_atoms = if h_rel = drel then [h_args] else [] in
- let r_atoms = r_atoms @ Aux.map_some
- (function Rel (rel, args) when rel = drel -> Some args
- | _ -> None)
- (atoms_of_body body) in
- let sterms = Aux.map_some
- (function Pos (True s) -> Some s | _ -> None) body in
- let sterm_arg_for_atom args apset =
- try ignore (find_defrel_arg sterms args apset); None
- with Not_found ->
- let path_subts = List.map (fun (p,i)->p, args.(i)) apset in
- Some (blank_outside_subterms data.term_arities path_subts) in
- let add_sterms = Aux.concat_map
- (fun args -> Aux.map_some (sterm_arg_for_atom args) partition)
- r_atoms in
- (* {{{ log entry *)
- if !debug_level > 2 && add_sterms <> [] then (
- Printf.printf
- "defrel_transform: add_sterms=%s; clause=\n%s\n\n%!"
- (String.concat ", " (List.map term_str add_sterms))
- (clause_str cl)
- );
- (* }}} *)
- h, Aux.map_rev_prepend body (fun s -> Pos (True s)) add_sterms
-
-
let build_defrels data clauses =
- let defined_rels_ord =
- topsort_callgraph clauses data.defined_rels in
- let process_drel clauses drel =
- let partition =
- select_defrel_argpaths drel data clauses in
- data.defrel_argpaths <- (drel, partition)::data.defrel_argpaths;
- List.map (defrel_transform drel partition data) clauses in
- (* first arguments processed first -- fold_left *)
- let clauses = List.fold_left process_drel clauses defined_rels_ord in
let build_defrel drel =
- (* now building the translation *)
- let partition = List.assoc drel data.defrel_argpaths in
+ (* {{{ log entry *)
+ if !debug_level > 1 then (
+ Printf.printf "build_defrel: %s\n%!" drel
+ );
+ (* }}} *)
+ let partition =
+ match List.assoc drel data.argpaths with
+ | Aux.Right partition -> partition
+ | Aux.Left _ -> assert false in
let r_clauses = Aux.map_some
(fun ((rel,args),body) ->
if rel=drel then Some (args,body) else None) clauses in
@@ -546,7 +398,7 @@
let tr_def_r (args, body) =
let sterms = Aux.map_some
(function Pos (True s) -> Some s | _ -> None) body in
- let s_l = List.map (find_defrel_arg sterms args) partition in
+ let s_l = List.map (find_rel_arg sterms args) partition in
let v_l = List.map (var_of_term data) s_l in
let eqs = List.map2
(fun v sv -> Formula.Eq (`FO v, sv))
@@ -558,5 +410,5 @@
Formula.And (eqs @ [def_phi])) in
drel, (Array.to_list defvars,
Formula.Or (List.map tr_def_r r_clauses)) in
- clauses, List.map build_defrel defined_rels_ord
+ List.map build_defrel data.defined_rels
Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/TranslateFormula.mli 2011-09-27 09:43:50 UTC (rev 1574)
@@ -1,7 +1,5 @@
val debug_level : int ref
-type defrel_argpaths = (GDL.path * int) list list
-
type transl_data = {
f_paths : GDL.path_set; (** fluent paths *)
c_paths : GDL.path_set; (** coordinate paths *)
@@ -10,10 +8,10 @@
counters : string list;
num_functions : (string * Formula.real_expr) list;
defined_rels : string list;
- mutable defrel_argpaths : (string * defrel_argpaths) list;
- (** late binding to store argument paths data *)
+ argpaths : (string * (GDL.path list array, GDL.argpaths) Aux.choice) list;
+ (** [Left argpaths] are coordinating relation argument paths, [Right
+ argpaths] is fact relation argument partition. *)
term_arities : (string * int) list;
- rel_default_path : (string * GDL.path option array) list;
}
val blank_out : transl_data -> GDL.term -> GDL.term
@@ -31,4 +29,4 @@
val build_defrels :
transl_data -> GDL.clause list ->
- GDL.clause list * (string * (string list * Formula.formula)) list
+ (string * (string list * Formula.formula)) list
Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -29,49 +29,6 @@
(Lexing.from_channel f) in
descr
-let connect5_data =
- let term_arities =
- ["control", 1; "cell", 3; "x", 0; "o", 0; "b", 0; "mark", 2;
- "a", 0; "b", 0; "c", 0; "d", 0; "e", 0; "f", 0; "g", 0; "h", 0] in
- let arities f = List.assoc f term_arities in
- let f_paths = [["cell", 2]; ["control", 0]] in
- let ground_flu = [GDL.Const "x"; GDL.Const "o"; GDL.Const "b"] in
- let ground_at_f_paths = List.map (fun f -> f, ground_flu) f_paths in
- let f_paths = List.fold_right (GDL.add_path arities)
- f_paths GDL.empty_path_set in
- let c_paths = List.fold_right (GDL.add_path arities)
- [["cell", 0]; ["cell", 1]] GDL.empty_path_set in
- let all_paths = GDL.paths_union f_paths c_paths in
- let root_reps =
- [GDL.Func ("control", [|GDL.blank|]);
- GDL.Func ("cell", [|GDL.blank; GDL.blank; GDL.blank|])] in
- let exp_defrel_arities = [
- "adjacent_cell", 4;
- "col__x", 0; "col__o", 0; "col__b", 0;
- "conn5__x", 0; "conn5__o", 0; "conn5__b", 0;
- "diag1__x", 0; "diag1__o", 0; "diag1__b", 0;
- "diag2__x", 0; "diag2__o", 0; "diag2__b", 0;
- "exists_empty_cell", 0; "exists_line_of_five", 0;
- "row__x", 0; "row__o", 0; "row__b", 0] in
- let defined_rels =
- ["adjacent_cell"; "col"; "conn5"; "diag1"; "diag2";
- "exists_empty_cell"; "exists_line_of_five"; "row"] in
- let default_path = Some ["cell", 0] in
- let rel_default_path = List.map
- (fun (rel, ar) -> rel, Array.make ar default_path) exp_defrel_arities in
- ground_at_f_paths,
- {
- f_paths = f_paths;
- c_paths = c_paths;
- all_paths = all_paths;
- root_reps = root_reps;
- counters = [];
- num_functions = [];
- defined_rels = defined_rels;
- defrel_argpaths = [];
- term_arities = term_arities;
- rel_default_path = rel_default_path;
- }
let tests = "TranslateFormula" >::: [
@@ -140,86 +97,7 @@
(String.concat "\n" (Array.to_list (str_res disj)));
);
-
- "defined relations connect5" >::
- (fun () ->
- let descr = load_rules ("./GGP/examples/connect5.gdl") in
- let ground_at_f_paths, transl_data = connect5_data in
- let clauses = GDL.expand_players descr in
- let prepare_lits ((h_rel, h_args), body) =
- if h_rel = "next" then (GDL.Pos (GDL.True h_args.(0))::body)
- else if h_rel = "frame next"
- then Aux.list_remove (GDL.Pos (GDL.True h_args.(0))) body
- else body in
- let clauses =
- GDL.ground_vars_at_paths prepare_lits ground_at_f_paths clauses in
- let defined_rels, clauses =
- GDL.elim_ground_args transl_data.defined_rels clauses in
- let transl_data = {transl_data with defined_rels = defined_rels} in
- let clauses, defined_rels =
- TranslateFormula.build_defrels transl_data clauses in
- (* {{{ log entry *)
- if !TranslateFormula.debug_level > 2 then (
- Printf.printf
- "defined relations connect5: transformed clauses =\n%s\n%!"
- (String.concat "\n" (List.map GDL.clause_str clauses))
- );
- (* }}} *)
- let result drel =
- let args, body = List.assoc drel defined_rels in
- drel^"("^String.concat ", " args^
- ") = "^Formula.str (FormulaOps.simplify body) in
- assert_equal ~msg:"adjacent_cell defined relation translation"
- ~printer:(fun x->x)
- "adjacent_cell(v0, v1) ="
- (result "adjacent_cell");
- assert_equal ~msg:"conn5__o defined relation translation"
- ~printer:(fun x->x)
- "conn5__o() = col__o() or diag1__o() or diag2__o() or row__o()"
- (result "conn5__o");
-
- assert_equal ~msg:"col__x defined relation translation"
- ~printer:(fun x->x)
- "col__x() = ex cell_x_a__BLANK_, cell_x_b__BLANK_, cell_x_c__BLANK_, cell_x_d__BLANK_,
- cell_x_e__BLANK_
- (cell__BLANK___BLANK___BLANK_(cell_x_a__BLANK_) and
- cell_2x(cell_x_a__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_x_b__BLANK_) and
- cell_2x(cell_x_b__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_x_c__BLANK_) and
- cell_2x(cell_x_c__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_x_d__BLANK_) and
- cell_2x(cell_x_d__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_x_e__BLANK_) and
- cell_2x(cell_x_e__BLANK_) and nextcol__cell_1__cell_1(cell_x_a__BLANK_,
- cell_x_b__BLANK_) and nextcol__cell_1__cell_1(cell_x_b__BLANK_,
- cell_x_c__BLANK_) and nextcol__cell_1__cell_1(cell_x_c__BLANK_,
- cell_x_d__BLANK_) and nextcol__cell_1__cell_1(cell_x_d__BLANK_,
- cell_x_e__BLANK_) and EQ___cell_0__cell_0(cell_x_a__BLANK_,
- cell_x_b__BLANK_) and EQ___cell_0__cell_0(cell_x_a__BLANK_,
- cell_x_c__BLANK_) and EQ___cell_0__cell_0(cell_x_a__BLANK_,
- cell_x_d__BLANK_) and EQ___cell_0__cell_0(cell_x_a__BLANK_,
- cell_x_e__BLANK_) and EQ___cell_0__cell_0(cell_x_b__BLANK_,
- cell_x_a__BLANK_) and EQ___cell_0__cell_0(cell_x_b__BLANK_,
- cell_x_c__BLANK_) and EQ___cell_0__cell_0(cell_x_b__BLANK_,
- cell_x_d__BLANK_) and EQ___cell_0__cell_0(cell_x_b__BLANK_,
- cell_x_e__BLANK_) and EQ___cell_0__cell_0(cell_x_c__BLANK_,
- cell_x_a__BLANK_) and EQ___cell_0__cell_0(cell_x_c__BLANK_,
- cell_x_b__BLANK_) and EQ___cell_0__cell_0(cell_x_c__BLANK_,
- cell_x_d__BLANK_) and EQ___cell_0__cell_0(cell_x_c__BLANK_,
- cell_x_e__BLANK_) and EQ___cell_0__cell_0(cell_x_d__BLANK_,
- cell_x_a__BLANK_) and EQ___cell_0__cell_0(cell_x_d__BLANK_,
- cell_x_b__BLANK_) and EQ___cell_0__cell_0(cell_x_d__BLANK_,
- cell_x_c__BLANK_) and EQ___cell_0__cell_0(cell_x_d__BLANK_,
- cell_x_e__BLANK_) and EQ___cell_0__cell_0(cell_x_e__BLANK_,
- cell_x_a__BLANK_) and EQ___cell_0__cell_0(cell_x_e__BLANK_,
- cell_x_b__BLANK_) and EQ___cell_0__cell_0(cell_x_e__BLANK_,
- cell_x_c__BLANK_) and EQ___cell_0__cell_0(cell_x_e__BLANK_,
- cell_x_d__BLANK_))"
- (result "col__x");
- );
-
]
let a () =
Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml 2011-09-26 00:10:41 UTC (rev 1573)
+++ trunk/Toss/GGP/TranslateGame.ml 2011-09-27 09:43:50 UTC (rev 1574)
@@ -18,13 +18,17 @@
occur in the structure)
TODO: filter out legal tuples that are not statically satisfiable
-
- TODO: perform the argument-path analysis for all GDL relations,
- not only future defined relations; if fact-only GDL relations have
- no conflicting paths (i.e. each argument is only used with a
- specific path), translate them using the mechanism of defined
- relations, but as stable (structure) relations, called
- "materialized defined relations".
+
+ TODO: perform "fluent path prediate inversion" by transforming
+ single-argument state terms into two arguments of a "value" state
+ term.
+
+ TODO-FIXME: add "preserved fluents" check, make rewrite rules
+ remove fluents that are not covered by any frame clause. (Erasure
+ clauses are only built from frame clauses, i.e. they handle only
+ fluents that are preserved elsewhere.) Unfortunately it cannot be
+ assumed that an element holding a non-preserved fluent is
+ different from an element where the fluent is to be added!
*)
open GDL
@@ -61,8 +65,8 @@
with arity smaller than three; or, select relations that have ground
defining clauses (i.e. defining clauses with empty bodies). *)
type as_defined_rels =
- Many_by_arity | Few_by_ground_def | Fewer_by_all_ground
-let as_defined_rels = ref Few_by_ground_def
+ By_arity | By_const_param | By_ground_def | By_all_ground
+let as_defined_rels = ref By_ground_def
(** When translating as turn-based, filter-out moves composed only of
actions such that each is a "noop" action of some player at some
@@ -211,6 +215,14 @@
| (p, _)::_ -> add_path arities p f_paths in
let f_paths =
List.fold_left find_cl_fluent empty_path_set move_cls in
+ (* {{{ log entry *)
+if !debug_level > 3 then (
+ Printf.printf "frame clauses:\n%s\n"
+ (String.concat "\n"
+ (List.map (fun (h,body)->term_str h^" <== "^literals_str body)
+ frame_cls))
+);
+(* }}} *)
frame_cls, move_cls, f_paths
@@ -219,17 +231,12 @@
| Func (f,args) -> Aux.array_existsi (fun _ -> contains_blank) args
| _ -> false
+let val_path = ["val_", 0]
-(* Expand role variables, find fluent and coordinate paths, generate the
- initial structure. Encode frame clauses by using the unique
- relation name "frame next". *)
-let create_init_struc program ~playout_states clauses =
- let players =
- Aux.map_some (function
- | ("role", [|player|]), _ -> Some player
- | _ -> None
- ) clauses in
- let players = Array.of_list players in
+(* Expand role variables, find fluent and coordinate paths, lift
+ unused state terms into relations and add state terms / elements
+ for missing subterms. *)
+let prepare_paths_and_elems players_wo_env program ~playout_states clauses =
let rules = Aux.concat_map rules_of_clause clauses in
let static_rels, nonstatic_rels =
static_rels (defs_of_rules rules) in
@@ -238,7 +245,7 @@
saturation-like. *)
let _, _,
static_base, init_state, (agg_actions, agg_states, terminal_state) =
- playout_satur ~aggregate:true players !playout_horizon rules in
+ playout_satur ~aggregate:true players_wo_env !playout_horizon rules in
(* *)
(*
let program = preprocess_program clauses in
@@ -268,6 +275,8 @@
let frame_clauses, move_clauses, f_paths =
fluent_paths_and_frames term_arities program playout_states
ground_state_terms clauses in
+ let clauses =
+ List.filter (fun ((rel,_),_) -> rel <> "next") clauses in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf
@@ -315,12 +324,17 @@
when Aux.Strings.mem f unused_roots -> Neg (Rel (f, args))
| Disj disj -> Disj (List.map lift_to_rel disj)
| l -> l in
- let clauses = List.map
+ let clauses = Aux.map_some
(function
| ("init", [|Func (f, args)|]), body
when Aux.Strings.mem f unused_roots ->
- (f, args), List.map lift_to_rel body
- | h, body -> h, List.map lift_to_rel body) clauses in
+ Some ((f, args), List.map lift_to_rel body)
+ | ("next", [|Func (f, args)|]), body
+ when Aux.Strings.mem f unused_roots -> None
+ | h, body -> Some (h, List.map lift_to_rel body)) clauses in
+ let static_rels =
+ if List.exists (fun ((r,_),_) -> r="init") clauses
+ then static_rels else Aux.list_remove "init" static_rels in
let element_reps =
Aux.unique_sorted (List.map (fun t ->
simult_subst f_paths blank t) ground_state_terms) in
@@ -353,8 +367,8 @@
(String.concat "; "
(List.map GDL.path_str (GDL.paths_to_list res)))
);
- (* }}} *)
- res
+ (* }}} *)
+ res
) else c_paths in
let root_reps =
Aux.unique_sorted (List.map (fun t ->
@@ -371,8 +385,17 @@
Aux.concat_map Array.to_list
(gdl_rel_graph r static_base))
static_rels) Terms.empty in
+ (* TODO: we also need players? *)
+ (*let needed_coords =
+ add_terms (Array.to_list players_wo_env) needed_coords in*)
+ (* TODO: we do need fluents sometimes... but not always! *)
+ (*let needed_coords = List.fold_right add_terms
+ (List.map (at_paths f_paths) ground_state_terms) needed_coords in*)
let missing_coords =
- Terms.elements (Terms.diff needed_coords coord_subterms) in
+ Terms.diff needed_coords coord_subterms in
+ let missing_coords = List.fold_right add_terms
+ (List.map (at_paths f_paths) ground_state_terms) missing_coords in
+ let missing_coords = Terms.elements missing_coords in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "create_init_struc: missing_coords=%s\n%!"
@@ -381,14 +404,14 @@
(* }}} *)
let val_elems = List.map
(fun subt -> Func ("val_", [|subt|])) missing_coords in
- let val_path = ["val_", 0] in
let term_arities =
- if val_elems = [] then term_arities
- else ("val_", 1)::term_arities in
+ if val_elems = [] then term_arities
+ else ("val_", 1)::term_arities in
let c_paths =
if val_elems = [] then c_paths
else add_path (fun f->List.assoc f term_arities) val_path c_paths in
let element_reps = val_elems @ element_reps in
+ let ground_state_terms = val_elems @ ground_state_terms in
(* let gorund_state_terms = val_elems @ ground_state_terms in *)
let root_reps =
if val_elems = [] then root_reps
@@ -400,31 +423,422 @@
(String.concat ", " (List.map term_str root_reps))
);
(* }}} *)
+ static_base, init_state, c_paths, f_paths, element_reps, root_reps,
+ ground_state_terms, arities, term_arities, static_rels, nonstatic_rels,
+ frame_clauses, move_clauses, clauses
+
+
+let default_argpaths rel ar init_state program ground_at_c_paths =
+ if ground_at_c_paths = [] then Array.make ar None
+ else
+ let program =
+ replace_rel_in_program "true" (state_cls init_state) program in
+ let vtup = Array.init ar (fun i -> Var ("v"^string_of_int i)) in
+ let rel_graph = List.map snd
+ (run_prolog_atom (rel, vtup) program) in
+ match rel_graph with
+ (* empty graph, take any path *)
+ | [] -> Array.make ar None
+ | tup::tups ->
+ let projs =
+ List.fold_left
+ (fun agg_tup tup ->
+ Aux.array_map2 (fun x y->x::y) tup agg_tup)
+ (Array.map (fun t->[t]) tup) tups in
+ let intersects = Array.map
+ (fun rel_proj ->
+ let rel_proj = Aux.unique_sorted rel_proj in
+ List.sort (fun (i,_) (j,_) -> j-i) (
+ List.map
+ (fun (p, pts) ->
+ List.length (Aux.list_inter rel_proj pts), p)
+ ground_at_c_paths)) projs in
+ Array.map (function (_, p)::_ -> Some p | [] -> None)
+ intersects
+
+
+let select_argpaths static_rels init_state program c_paths f_paths
+ ground_at_c_paths clauses rel =
+ let atoms_sterms = List.map
+ (fun ((r, args), body) ->
+ let r_atoms = if r = rel then [args] else [] in
+ let r_atoms = r_atoms @ Aux.map_some
+ (function Rel (r, args) when r = rel -> Some args
+ | _ -> None)
+ (atoms_of_body body) in
+ r_atoms, state_terms body)
+ clauses in
+ let check_path args p s_p =
+ let inds = Aux.array_argfind_all (fun r -> r=s_p) args in
+ List.map (fun i->p,i) inds in
+ let sterm_path_sets args s =
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "sterm_path_sets: rel=%s args={%s} sterm=%s\n%!"
+ rel
+ (String.concat ", " (Array.to_list (Array.map term_str args)))
+ (term_str s)
+ );
+ (* }}} *)
+ let c_psets = map_paths (check_path args) c_paths s in
+ let f_psets = map_paths (check_path args) f_paths s in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "sterm_path_sets: c_psets=%s; f_psets=%s\n%!"
+ (String.concat "; "(List.map (fun pset->"["^
+ String.concat ", " (List.map (fun (p,i)->
+ path_str p^":"^string_of_int i) pset)^"]") c_psets))
+ (String.concat "; "(List.map (fun pset->"["^
+ String.concat ", " (List.map (fun (p,i)->
+ path_str p^":"^string_of_int i) pset)^"]") f_psets))
+ );
+ (* }}} *)
+ let c_ptups = Aux.product (Aux.list_remove [] c_psets) in
+ let f_ptups = Aux.concat_map
+ (fun pset -> List.map (fun (_,i) -> [val_path, i]) pset)
+ f_psets in
+ let ptups = f_ptups @ c_ptups in
+ (* distinct [p] in a tuple is already ensured *)
+ List.filter (fun tup ->
+ not (Aux.not_unique (List.map snd tup))) ptups in
+ let argpath_sets = Aux.concat_map
+ (fun (atoms, sterms) -> Aux.concat_map
+ (fun args -> Aux.concat_map (sterm_path_sets args) sterms)
+ atoms)
+ atoms_sterms in
+ let argpath_sets =
+ Aux.map_reduce (fun pset -> pset, 1) (+) 0 argpath_sets in
+ let argpath_sets = List.sort Pervasives.compare
+ (List.map (* lexicographic comparison *)
+ (fun (pset,count) -> List.length pset, count, pset)
+ argpath_sets) in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf
+ "select_argpaths: rel=%s; argpath_sets=\n%!" rel;
+ List.iter (fun (len, count, pset) ->
+ Printf.printf "len=%d; count=%d; pset=%s\n%!" len count
+ (String.concat ", "
+ (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+ argpath_sets
+ );
+ (* }}} *)
+ let len, count = match argpath_sets with
+ | (len,count,_)::_ -> len, count | [] -> 0, 0 in
+ let argpath_sets = List.map Aux.trd3 (List.rev argpath_sets) in
+ (* check if it is a coordinating relation *)
+ let is_coordin = List.mem rel static_rels &&
+ List.for_all (function [] | [_] -> true | _ -> false) argpath_sets &&
+ Aux.not_unique (Aux.concat_map (List.map snd) argpath_sets) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf
+ "select_argpaths: %s is_coordin=%B because not composite: %B, conflicting=%B {%s}\n%!"
+ rel is_coordin
+ (List.for_all (function [] | [_] -> true | _ -> false) argpath_sets)
+ (Aux.not_unique (Aux.concat_map (List.map snd) argpath_sets))
+ (String.concat ", "
+ (List.map string_of_int
+ (Aux.concat_map (List.map snd) argpath_sets)))
+ );
+ (* }}} *)
+ (* now greedily -- by traversing the ordering -- select covering *)
+ let apsets_cover = List.fold_left
+ (fun cover apset ->
+ if List.exists
+ (fun (_,i) -> not (List.exists (fun cov_apset ->
+ List.exists (fun (_,j)->i=j) cov_apset) cover)) apset
+ then apset::cover else cover)
+ [] argpath_sets in
+ (* eliminating multiple points -- starting with best apsets so
+ they're unchanged *)
+ let partition = List.fold_left
+ (fun partition apset ->
+ let apset = List.filter (fun (_,i) ->
+ not (List.exists (fun cov_apset ->
+ List.exists (fun (_,j)->i=j) cov_apset) partition)) apset in
+ if apset = [] then partition else apset::partition)
+ [] apsets_cover in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf
+ "select_argpaths: rel=%s; partition=\n%!" rel;
+ List.iter (fun pset ->
+ Printf.printf "pset=%s\n%!"
+ (String.concat ", "
+ (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+ partition
+ );
+ (* }}} *)
+ (* filling-in missing paths from precomputed defaults *)
+ let arity = Array.length
+ (List.hd (fst (List.find (fun (atoms,_) -> atoms<>[])
+ atoms_sterms))) in
+ let default_paths =
+ default_argpaths rel arity init_state program ground_at_c_paths in
+ if is_coordin
+ then (* discard some work above... *)
+ let argpaths = Aux.map_some
+ (function [p, i] -> Some (i, p) | [] -> None
+ | _ -> assert false) argpath_sets in
+ let argpaths = Array.init arity
+ (fun i ->
+ let ps = Aux.assoc_all i argpaths in
+ if ps <> [] then ps else
+ match default_paths.(i) with
+ | Some p -> [p]
+ | None ->
+ failwith
+ (Printf.sprintf
+ "select_argpaths: could not \
+ determine path for coordinating relation %s argument %d" rel i)
+ ) in
+ (* let res = argpaths
+ List.map Array.of_list (Aux.product (Array.to_list argpaths)) in *)
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf
+ "select_argpaths: coordinating rel=%s; result=\n%s%!" rel
+ (String.concat " -- " (List.map (fun ps ->
+ (String.concat " | " (List.map path_str ps)))
+ (Array.to_list argpaths)))
+ );
+ (* }}} *)
+ len, count, (rel, Aux.Left argpaths)
+
+ else
+ let argpaths = Array.init arity
+ (fun i ->
+ try List.find (List.exists (fun (_,j)->i=j)) partition
+ with Not_found ->
+ try
+ match default_paths.(i) with
+ | Some p -> [p, i]
+ | None -> raise Not_found
+ with Not_found ->
+ failwith
+ (Printf.sprintf
+ "select_argpaths: could not \
+ determine path for relation %s argument %d" rel i)
+ ) in
+ let res = Aux.unique (=) (Array.to_list argpaths) in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf
+ "select_argpaths: rel=%s; result=\n%!" rel;
+ List.iter (fun pset ->
+ Printf.printf "pset=%s\n%!"
+ (String.concat ", "
+ (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+ res
+ );
+ (* }}} *)
+ len, count, (rel, Aux.Right res)
+
+let has_term_arg_avoid rel lits t =
+ let check = function
+ | Rel (r, args) when r <> rel -> Aux.array_mem t args
+ | _ -> false in
+ let rec map = function
+ | Pos a | Neg a -> check a
+ | Disj d -> List.exists map d in
+ List.exists map lits
+
+(* Adding "true" atoms to clauses for missing argpath state terms *)
+let call_transform term_arities ground_at_c_paths
+ rel partition ((h_rel,h_args as h),body as cl) =
+ let r_atoms = if h_rel = rel then [h_args] else [] in
+ let r_atoms = r_atoms @ Aux.map_some
+ (function Rel (r, args) when r = rel -> Some args
+ | Distinct args when rel = "distinct" && h_rel <> "frame next"
+ -> Some args
+ | _ -> None)
+ (atoms_of_body body) in
+ let sterms = Aux.map_some
+ (function Pos (True s) -> Some s | _ -> None) body in
+ let sterm_arg_for_atom_fact args apset =
+ try ignore (find_rel_arg sterms args apset); None
+ with Not_found ->
+ let path_subts = List.map (fun (p,i)->p, args.(i)) apset in
+ Some (blank_outside_subterms term_arities path_subts) in
+ let sterm_arg_for_atom_coordin arg ps =
+ let find_rel_arg =
+ List.exists
+ (fun s -> List.exists (fun p ->
+ try at_path s p = arg with Not_found -> false) ps)
+ sterms in
+ if find_rel_arg then None
+ else
+ Some (blank_outside_subterm term_arities (List.hd ps) arg) in
+ let sterm_arg_for_distinct arg =
+ if has_term_arg_avoid "distinct"
+ (Pos (Rel (h_rel, h_args))::body) arg then None
+ else
+ let path =
+ try fst (List.find
+ (fun (_,ts) -> List.mem arg ts) ground_at_c_paths)
+ with Not_found -> failwith
+ ("in clause "^h_rel^", alien <distinct> argument "^term_str arg) in
+ Some (blank_outside_subterm term_arities path arg) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf
+ "call_transform: rel=%s; clause=\n%s\n\n%!"
+ rel (clause_str cl)
+ );
+ (* }}} *)
+ let add_sterms = Aux.concat_map
+ (fun args ->
+ if rel = "distinct" && h_rel <> "frame next" then
+ Aux.map_some (fun x->x)
+ (Array.to_list (Array.map sterm_arg_for_distinct args))
+ else if rel = "distinct" then []
+ else match partition with
+ | Aux.Left argpaths ->
+ Aux.map_some (fun x->x)
+ (Array.to_list (
+ Aux.array_map2 sterm_arg_for_atom_coordin args
+ argpaths))
+ | Aux.Right partition ->
+ Aux.map_some (sterm_arg_for_atom_fact args) partition)
+ r_atoms in
+ (* {{{ log entry *)
+ if !debug_level > 2 && add_sterms <> [] then (
+ Printf.printf
+ "call_transform: rel=%s; add_sterms=%s; clause=\n%s\n\n%!"
+ rel
+ (String.concat ", " (List.map term_str add_sterms))
+ (clause_str cl)
+ );
+ (* }}} *)
+ h, Aux.map_rev_prepend body (fun s -> Pos (True s)) add_sterms
+
+let not_callable =
+ ["goal"; "next"; "rule clause"; "update clause";"legal"]
+
+let prepare_rels static_rels nonstatic_rels init_state c_paths f_paths
+ ground_at_c_paths term_arities counters clauses =
+ let ord_rels =
+ topsort_callgraph (*(static_rels @ nonstatic_rels)*) clauses in
+ let all_rels = Aux.list_diff ord_rels (not_callable @ counters) in
let c_pathl = paths_to_list c_paths in
- let f_pathl = paths_to_list f_paths in
- (* adding subterm equality relations and fact relations *)
- let struc_rels, defined_rels = List.partition
+ (* program is only used to find default argpaths *)
+ let program = preprocess_program clauses in
+ let is_strucrel rel = List.mem rel static_rels &&
+ if !as_defined_rels = By_const_param
+ then List.exists
+ (fun ((rc,args),_) -> rel=rc &&
+ Aux.array_existsi
+ (fun _ -> function Var _ -> false | _ -> true) args)
+ clauses
+ else if !as_defined_rels = By_ground_def
+ then List.exists
+ (fun ((rc,args),body) -> rel=rc && body = []) clauses
+ else if !as_defined_rels = By_all_ground
+ then List.for_all
+ (fun ((rc,args),body) -> rel=rc && body = []) clauses
+ else assert false in
+ let struc_rels, defined_rels = ref [], ref [] in
+ (if !as_defined_rels <> By_arity then
+ let as_struc, as_defined =
+ List.partition is_strucrel static_rels in
+ struc_rels := as_struc;
+ defined_rels := as_defined @ nonstatic_rels);
+
+ (* first pass *)
+ let fstpass_clauses = List.fold_left
+ (fun clauses rel ->
+ let _, _, (_, partition) =
+ select_argpaths static_rels init_state program c_paths f_paths
+ ground_at_c_paths clauses rel in
+ List.map (call_transform term_arities ground_at_c_paths rel
+ partition) clauses)
+ clauses all_rels in
+
+ (* second pass -- but update clauses from originals *)
+ let argpaths = List.map
+ (select_argpaths static_rels init_state program c_paths f_paths
+ ground_at_c_paths fstpass_clauses)
+ all_rels in
+ let argpaths =
+ List.map Aux.trd3 (List.rev (List.sort Pervasives.compare argpaths)) in
+ let nthpass_clauses = List.fold_left
+ (fun clauses (rel, partition) ->
+ List.map (call_transform term_arities ground_at_c_paths rel
+ partition) clauses)
+ clauses argpaths in
+
+ (* third pass -- but update clauses from originals *)
+ let argpaths = List.map
+ (select_argpaths static_rels init_state program c_paths f_paths
+ ground_at_c_paths nthpass_clauses)
+ all_rels in
+ let argpaths =
+ List.map Aux.trd3 (List.rev (List.sort Pervasives.compare argpaths)) in
+ let nthpass_clauses = List.fold_left
+ (fun clauses (rel, partition) ->
+ List.map (call_transform term_arities ground_at_c_paths rel
+ partition) clauses)
+ clauses argpaths in
+ (* TODO: a proper fixpoint instead of four passes? *)
+
+ (* last pass -- but update clauses from originals *)
+ let argpaths = List.map
+ (select_argpaths static_rels init_state program c_paths f_paths
+ ground_at_c_paths nthpass_clauses)
+ all_rels in
+ let argpaths =
+ List.map Aux.trd3 (List.rev (List.sort Pervasives.compare argpaths)) in
+ let argpaths =
+ (* actually, arity mismatch for "distinct" is captured in
+ call_transform *)
+ ("distinct", Aux.Left (Array.make 2 c_pathl))::argpaths in
+ let clauses = List.fold_left
+ (fun clauses (rel, partition) ->
+ List.map (call_transform term_arities ground_at_c_paths rel
+ partition) clauses)
+ clauses argpaths in
+
+ let is_strucrel rel = List.mem rel static_rels &&
+ try
+ let def_arity =
+ match List.assoc rel argpaths with
+ | Aux.Left argpaths -> Array.length argpaths
+ | Aux.Right partition -> List.length partition in
+ def_arity >= 3
+ with Not_found -> false in
+ (if !as_defined_rels = By_arity then
+ let as_struc, as_defined =
+ List.partition is_strucrel static_rels in
+ struc_rels := as_struc;
+ defined_rels := as_defined @ nonstatic_rels);
+ let defined_rels = List.filter
(fun rel ->
- if !as_defined_rels = Few_by_ground_def
- then List.exists
- (fun ((rc,args),body) -> rel=rc && body = []) clauses
- else if !as_defined_rels = Fewer_by_all_ground
- then List.for_all
- (fun ((rc,args),body) -> rel=rc && body = []) clauses
- else List.assoc rel arities < 3)
- static_rels in
- let struc_rels = "EQ_"::struc_rels in
- let defined_rels = defined_rels @ nonstatic_rels in
+ try match List.assoc rel argpaths with
+ | Aux.Left _ -> false | Aux.Right _ -> true
+ with Not_found -> true)
+ !defined_rels in
+ let struc_rels = "EQ_":: !struc_rels in
(* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf "create_init_struc: struc_rels=%s; defined_rels=%s\n%!"
+ if !debug_level > 3 then (
+ Printf.printf
+ "prepare_rels: struc_rels=%s; defined_rels= %s\n%!"
(String.concat ", " struc_rels) (String.concat ", " defined_rels)
);
(* }}} *)
+ struc_rels, defined_rels,
+ ("EQ_", Aux.Left (Array.make 2 c_pathl)) :: argpaths, clauses
+
+
+let process_frame_clauses clauses frame_clauses =
(* we need to expand frame clauses so that later local variables will get
eliminated from erasure clauses *)
+ let expand_rels = Aux.unique_sorted (List.map (fst -| fst) clauses) in
+ let expand_rels = List.filter
+ (fun r -> List.for_all (fun ((h_r, _),body) -> h_r<>r || body<>[])
+ clauses) expand_rels in
let defs = List.filter
- (fun ((rel,_),_) -> List.mem rel defined_rels) clauses in
+ (fun ((rel,_),_) -> List.mem rel expand_rels) clauses in
let defs = defs_of_rules (Aux.concat_map rules_of_clause defs) in
let frame_clauses = List.map
(fun (h,body)->("next",[|h|]),body) frame_clauses in
@@ -441,29 +855,69 @@
List.map (fun a->pos (atom_of_rel a)) body @
List.map (fun a->neg (atom_of_rel a)) neg_body)
frame_defs in
+ frame_clauses
+
+
+(* Generate the initial structure. *)
+let create_init_struc ground_state_terms c_paths f_paths
+ element_reps root_reps
+ arities struc_rels defined_rels
+ argpaths static_base init_state =
+ let c_pathl = paths_to_list c_paths in
+ let f_pathl = paths_to_list f_paths in
+ (* adding subterm equality relations and fact relations *)
let stable_rels = ref Aux.Strings.empty in
- (* TODO: OPTIMIZE!!! *)
+ (* TODO: optimize by iterating over static_base or results of
+ prolog_query instead of creating all tuples *)
let struc =
List.fold_left (fun struc rel ->
- let arity = List.assoc rel arities in
- let elem_tups = Aux.all_ntuples element_reps arity in
- let path_tups = Aux.all_ntuples c_pathl arity in
- List.fold_left (fun struc ptup ->
- let fact_rel = rel_on_paths rel ptup in
- Aux.fold_left_try (fun struc etup ->
- let tup = Array.of_list (List.map2 at_path etup ptup) in
- if rel = "EQ_" && arity = 2 && tup.(0) = tup.(1) ||
- rel <> "EQ_" && graph_mem rel tup static_base
- (* rel <> "EQ_" && run_prolog_check_atom (rel, tup) program *)
- then (
- stable_rels := Aux.Strings.add fact_rel !stable_rels;
- Structure.add_rel_named_elems struc fact_rel
- (* we add the element repr. tuple if subterms at ptup
- are in relation *)
- (Aux.array_map_of_list term_to_name etup))
- else struc
- ) struc elem_tups
- ) struc path_tups
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "create_init_struc: adding relation %s\n%!" rel
+ );
+ (* }}} *)
+ match List.assoc rel argpaths with
+ | Aux.Left argpaths ->
+ let arity = List.assoc rel arities in
+ let elem_tups = Aux.all_ntuples element_reps arity in
+ let path_tups =
+ Aux.product (Array.to_list argpaths) in
+ List.fold_left (fun struc ptup ->
+ Aux.fold_left_try (fun struc etup ->
+ let rname = rel_on_paths rel ptup in
+ let tup = Array.of_list (List.map2 at_path etup ptup) in
+ if rel = "EQ_" && arity = 2 && tup.(0) = tup.(1) ||
+ rel <> "EQ_" && graph_mem rel tup static_base
+ (* rel <> "EQ_" && run_prolog_check_atom (rel, tup) program *)
+ then (
+ stable_rels := Aux.Strings.add rname !stable_rels;
+ Structure.add_rel_named_elems struc rname
+ (* we add the element repr. tuple if subterms at ptup
+ are in relation *)
+ (Aux.array_map_of_list term_to_name etup))
+ else struc
+ ) struc elem_tups
+ ) struc path_tups
+ | Aux.Right partition ->
+ let arity = List.length partition in
+ let elem_tups = Aux.all_ntuples element_reps arity in
+ Aux.fold_left_try (fun struc etup ->
+ let tup = List.map2
+ (fun e pset ->
+ List.map (fun (p,i) -> i, at_path e p) pset)
+ etup partition in
+ let tup = Aux.array_from_assoc (List.concat tup) in
+ if graph_mem rel tup static_base
+ (* run_prolog_check_atom (rel, tup) program *)
+ then (
+ stable_rels := Aux.Strings.add rel !stable_rels;
+ Structure.add_rel_named_elems struc rel
+ (* we add the element repr. tuple if subterms, perhaps
+ several coming from a single element repr., are in
+ relation *)
+ (Aux.array_map_of_list term_to_name etup))
+ else struc
+ ) struc elem_tups
) (Structure.empty_structure ()) struc_rels in
(* adding coordinate and fluent predicates *)
let add_pred sig_only rels struc paths elements =
@@ -505,6 +959,68 @@
(Structure.str struc)
);
(* }}} *)
+ Aux.Strings.elements !stable_rels, Aux.Strings.elements !fluents, struc
+
+
+(* Expand goal value variables using values it could possibly have in
+ the game. *)
+let ground_goal_values ground_state_terms clauses =
+ (* the un-grounded goals, and remaining clauses *)
+ let goal_cls, clauses = Aux.partition_map
+ (function ("goal",[|_; Var v|]),_ as cl -> Aux.Left (v, cl)
+ | cl -> Aux.Right cl) clauses in
+ let rec neg_true = function
+ | Neg (True _) | Neg (Rel ("true",_)) -> true
+ | Disj disj -> List.exists neg_true disj
+ | _ -> false in
+ let pos_clauses = List.map
+ (fun (head, body) -> head, List.filter (Aux.neg neg_true) body)
+ clauses in
+ let pos_clauses =
+ List.map (fun t-> ("true",[|t|]),[]) ground_state_terms @
+ pos_clauses in
+ (* TODO: saturation-like memoization in the Prolog interpreter
+ might be needed because many "true" facts and removed negative
+ literals can lead to explosion of the amount of derivations. *)
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf
+ "traslate_game: all clauses for instantiating goals\n%s\n\n%!"
+ (String.concat "\n"(List.map clause_str pos_clauses));
+ );
+ (* }}} *)
+ let program = preprocess_program pos_clauses in
+ let expand (v, (_,body as g_cl)) =
+ let sbs = run_prolog_goal body program in
+ let v_sbs = Aux.unique_sorted
+ (List.map (fun sb-> [v, List.assoc v sb]) sbs) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "ground_goal_values: grounding var %s goal %s:\n%s\n%!"
+ v (String.concat " " (List.map literal_str body))
+ (String.concat " -sb- " (List.map sb_str sbs))
+ );
+ (* }}} *)
+ List.map (fun sb->subst_clause sb g_cl) v_sbs in
+ Aux.concat_map expand goal_cls @ clauses
+
+let prepare_relations_and_structure
+ ground_state_terms f_paths c_paths element_reps ro...
[truncated message content] |
