[Toss-devel-svn] SF.net SVN: toss:[1532] trunk/Toss

[<luk...@us...>]

Revision: 1532
          http://toss.svn.sourceforge.net/toss/?rev=1532&view=rev
Author:   lukstafi
Date:     2011-08-10 03:31:00 +0000 (Wed, 10 Aug 2011)

Log Message:
-----------
GDL translation: eliminating ground arguments of relations. (TranslateFormula and TranslateGame tests do not pass yet.)

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/TranslateFormulaTest.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/Formula/Aux.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -117,6 +117,11 @@
   match l with
     | [] -> init
     | a::l -> concat_map (f a) (concat_foldr f l init)
+
+let rec concat_foldl f l init =
+  match l with
+    | [] -> init
+    | a::l -> concat_foldl f l (concat_map (f a) init)
   
 
 let list_remove v l = List.filter (fun w->v<>w) l
@@ -394,6 +399,14 @@
   if !i >= n then raise Not_found
   else !i
 
+let array_argfindi f a =
+  let i = ref 0 in
+  let n = Array.length a in
+  while !i < n && not (f !i (Array.unsafe_get a !i)) do
+    incr i done;
+  if !i >= n then raise Not_found
+  else !i
+
 let array_find_all f a =
   let r = ref [] in
   for i = Array.length a - 1 downto 0 do

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/Formula/Aux.mli	2011-08-10 03:31:00 UTC (rev 1532)
@@ -72,6 +72,9 @@
     [concat_foldr f (a::l) init = concat_map (f a) (concat_foldr f l init)] *)
 val concat_foldr : ('a -> 'b -> 'b list) -> 'a list -> 'b list -> 'b list
 
+(** [concat_foldl f (a::l) init = concat_foldl f l (concat_map (f a) init)] *)
+val concat_foldl : ('a -> 'b -> 'b list) -> 'a list -> 'b list -> 'b list
+
 (** Remove all elements equal to the argument, using structural
     inequality. *)
 val list_remove : 'a -> 'a list -> 'a list
@@ -212,6 +215,8 @@
 
 val array_argfind : ('a -> bool) -> 'a array -> int
 
+val array_argfindi : (int -> 'a -> bool) -> 'a array -> int
+
 (** Find all elements for which [f] holds. *)
 val array_find_all : ('a -> bool) -> 'a array -> 'a list
 (** Find all indices for which [f] holds. *)

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/GGP/GDL.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -315,6 +315,18 @@
 let def_str (rel, branches) =
   String.concat "\n" (List.map (branch_str rel) branches)
 
+let atom_str a = rel_atom_str (rel_of_atom a)
+
+let rec literal_str = function
+  | Pos atom -> atom_str atom
+  | Neg atom -> "(not "^atom_str atom^")"
+  | Disj disjs ->
+    "(or "^String.concat " " (List.map literal_str disjs)^")"
+
+let clause_str (head, body) =
+  "(<= "^rel_atom_str head^"\n    "^String.concat "\n    "
+    (List.map literal_str body)^")"
+
 let sb_str sb =
   String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
 
@@ -521,6 +533,84 @@
   ) (flatten_disjs body)
 
 
+let find_ground_arg rel clauses =
+  match Aux.assoc_all rel (List.map fst clauses) with
+    | [] -> raise Not_found
+    | (args::_ as all_args) ->
+      Aux.array_argfindi
+        (fun i _ ->
+          List.for_all (fun args ->
+            Aux.Strings.is_empty (term_vars args.(i))) all_args)
+        args
+
+let elim_ground_arg_in_body rel arg grounding (head, body) =
+
+  let expand_atom args add_lit (sb, (head, body)) =
+    (* [short_args] will be subsituted with [sb] inside [r_br] *)
+    let short_args = Array.init (Array.length args - 1)
+      (fun i -> if i < arg then args.(i) else args.(i+1)) in
+    let inst_arg = subst sb args.(arg) in
+    Aux.map_try
+      (fun ground ->
+        let sb = unify sb [ground] [inst_arg] in
+        let r_gr = rel ^ "__" ^ term_to_name ground in
+        let r_br = head, add_lit (Rel (r_gr, short_args)) body in
+        sb, subst_clause sb r_br)
+      grounding in
+
+  let rec expand_literal emb_lit literal (sb, (head, body) as accu) =
+    match literal with
+      | Pos (Rel (r, args)) when r=rel ->
+        expand_atom args (fun a body -> emb_lit (Pos a) body) accu
+      | Neg (Rel (r, args)) when r=rel ->
+        expand_atom args (fun a body -> emb_lit (Neg a) body) accu
+      | Pos _ | Neg _ -> [sb, (head, emb_lit literal body)]
+      | Disj disjs ->
+        let emb_lit lit body =
+          match body with
+            | Disj disjs::body -> Disj (lit::disjs)::body
+            | _ -> assert false in
+        (* unfortunately only works with one level of disjunctions *)
+        (* TODO: optimization when splitting clause not necessary *)
+        Aux.concat_foldr (expand_literal emb_lit) disjs
+          [sb, (head, Disj []::body)] in
+
+  let init = [[], (head, [])] in
+  let result =
+    Aux.concat_foldr (expand_literal (fun l body-> l::body)) body init in
+  List.map (fun (sb, cl) -> subst_clause sb cl) result
+
+let elim_ground_arg rel arg clauses =
+  let rel_brs, clauses =
+    List.partition (fun ((r,_),_) -> r=rel) clauses in
+  let grounding = Aux.unique_sorted
+    (List.map (fun ((_,args),_) -> args.(arg)) rel_brs) in
+  let renamed_brs = List.map
+    (fun ((_,args), body) ->
+      let short_args = Array.init (Array.length args - 1)
+        (fun i -> if i < arg then args.(i) else args.(i+1)) in
+      let rname = rel ^ "__" ^ term_to_name args.(arg) in
+      (rname, short_args), body)
+    rel_brs in
+  Aux.concat_map (elim_ground_arg_in_body rel arg grounding)
+    (renamed_brs @ clauses)
+
+let elim_ground_args rels clauses =
+  let modified = ref false in
+  let rec aux clauses = function
+    | [] -> clauses
+    | rel::rels ->
+      (let try arg = find_ground_arg rel clauses in
+       modified := true;
+       aux (elim_ground_arg rel arg clauses) rels
+       with Not_found -> aux clauses rels) in
+  let rec fix clauses =
+    modified := false;
+    let clauses = aux clauses rels in
+    if !modified then fix clauses else clauses in
+  fix clauses
+  
+
 (* ************************************************************ *)
 (* ************************************************************ *)
 (** {3 GDL whole-game operations.}

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/GGP/GDL.mli	2011-08-10 03:31:00 UTC (rev 1532)
@@ -91,8 +91,8 @@
 
 val func_graph : string -> term list -> term array list
 
+val elim_ground_args : string list -> clause list -> clause list
 
-
 (** {3 GDL translation helpers.} *)
 
 val blank : term
@@ -105,6 +105,7 @@
 
 val rel_atom_str : rel_atom -> string
 val def_str : string * def_branch list -> string
+val clause_str : clause -> string
 
 (** {3 GDL whole-game operations.}
 

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/GGP/GDLTest.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -171,6 +171,106 @@
         (GDL.def_str ("legal", legal_def));
     );
 
+  "eliminate ground args simple" >::
+    (fun () ->
+      let descr = parse_game_descr
+        "
+(<= (conn5 ?r)
+	(or (col ?r) (row ?r)))
+(<= (row x)
+    (true (cell ?a ?y x))
+	(nextcol ?a ?b)
+    (true (cell ?b ?y x))
+	(nextcol ?b ?c)
+    (true (cell ?c ?y x))
+	(nextcol ?c ?d)
+    (true (cell ?d ?y x))
+	(nextcol ?d ?e)
+    (true (cell ?e ?y x)))
+(<= (col x)
+    (true (cell ?x ?a x))
+	(nextcol ?a ?b)
+    (true (cell ?x ?b x))
+	(nextcol ?b ?c)
+    (true (cell ?x ?c x))
+	(nextcol ?c ?d)
+    (true (cell ?x ?d x))
+	(nextcol ?d ?e)
+    (true (cell ?x ?e x)))
+(<= (row o)
+    (true (cell ?a ?y o))
+	(nextcol ?a ?b)
+    (true (cell ?b ?y o))
+	(nextcol ?b ?c)
+    (true (cell ?c ?y o))
+	(nextcol ?c ?d)
+    (true (cell ?d ?y o))
+	(nextcol ?d ?e)
+    (true (cell ?e ?y o)))
+(<= (col o)
+    (true (cell ?x ?a o))
+	(nextcol ?a ?b)
+    (true (cell ?x ?b o))
+	(nextcol ?b ?c)
+    (true (cell ?x ?c o))
+	(nextcol ?c ?d)
+    (true (cell ?x ?d o))
+	(nextcol ?d ?e)
+    (true (cell ?x ?e o)))
+" in
+      let 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)
+        "(<= (conn5__o )
+    (or (col__o ) (row__o )))
+(<= (conn5__x )
+    (or (col__x ) (row__x )))
+(<= (row__x )
+    (true (cell ?a ?y x))
+    (nextcol ?a ?b)
+    (true (cell ?b ?y x))
+    (nextcol ?b ?c)
+    (true (cell ?c ?y x))
+    (nextcol ?c ?d)
+    (true (cell ?d ?y x))
+    (nextcol ?d ?e)
+    (true (cell ?e ?y x)))
+(<= (row__o )
+    (true (cell ?a ?y o))
+    (nextcol ?a ?b)
+    (true (cell ?b ?y o))
+    (nextcol ?b ?c)
+    (true (cell ?c ?y o))
+    (nextcol ?c ?d)
+    (true (cell ?d ?y o))
+    (nextcol ?d ?e)
+    (true (cell ?e ?y o)))
+(<= (col__x )
+    (true (cell ?x ?a x))
+    (nextcol ?a ?b)
+    (true (cell ?x ?b x))
+    (nextcol ?b ?c)
+    (true (cell ?x ?c x))
+    (nextcol ?c ?d)
+    (true (cell ?x ?d x))
+    (nextcol ?d ?e)
+    (true (cell ?x ?e x)))
+(<= (col__o )
+    (true (cell ?x ?a o))
+    (nextcol ?a ?b)
+    (true (cell ?x ?b o))
+    (nextcol ?b ?c)
+    (true (cell ?x ?c o))
+    (nextcol ?c ?d)
+    (true (cell ?x ?d o))
+    (nextcol ?d ?e)
+    (true (cell ?x ?e o)))"
+        res_s
+    );
+]
+
+let bigtests = "GDLBig" >::: [
   "playout connect5" >::
     (fun () ->
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
@@ -194,4 +294,8 @@
 
 ]
 
+let a () =
+  GDL.debug_level := 5
+
+
 let exec = Aux.run_test_if_target "GDLTest" tests

Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -66,8 +66,10 @@
   "defined relations connect5" >::
     (fun () ->
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
+      let transl_data = connect5_data in
       let clauses = GDL.expand_players descr in
-      let transl_data = connect5_data in
+      let clauses =
+        GDL.elim_ground_args transl_data.defined_rels clauses in
       let defined_rels =
         TranslateFormula.build_defrels transl_data clauses in
       let res = String.concat "\n"

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -1139,6 +1139,9 @@
     ground_vars_at_paths ground_at_f_paths frame_clauses in
   let move_clauses =
     ground_vars_at_paths ground_at_f_paths move_clauses in
+  let defined_rels = Aux.list_diff defined_rels
+    ["goal"; "legal"; "next"; "terminal"] in
+  let clauses = elim_ground_args defined_rels clauses in
   let next_cls =
     List.map (function
       | (_,[|s_C|]),body_C -> s_C, true, body_C

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/Server/Tests.ml	2011-08-10 03:31:00 UTC (rev 1532)
@@ -33,7 +33,7 @@
 
 let ggp_tests = "GGP", [
   "GameSimplTest",  	[GameSimplTest.tests];
-  "GDLTest",        	[GDLTest.tests];
+  "GDLTest",        	[GDLTest.tests; GDLTest.bigtests];
   "TranslateGameTest",  [TranslateGameTest.tests; TranslateGameTest.bigtests];
   "TranslateFormulaTest",  [TranslateFormulaTest.tests];
 ]

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-08-10 02:59:51 UTC (rev 1531)
+++ trunk/Toss/www/reference/reference.tex	2011-08-10 03:31:00 UTC (rev 1532)
@@ -1646,8 +1646,13 @@
 (by virtue of occurring in \texttt{does}, \texttt{legal} or
 \texttt{goal} atoms), by the players of the game.
 
-Before generating Toss formulas we also transform the definition $G$
-by grounding all variables that have occurrences at fluent paths, \ie
+Another form of expansion was the inlining of clauses, used only for
+finding fluent paths. (In particular, \texttt{does} atoms were then
+replaced by appropriately instantiated bodies of \texttt{legal}
+clauses.)
+
+Before generating Toss formulas we transform the definition $G$ by
+grounding all variables that have occurrences at fluent paths, \ie
 eliminating these variables by constants that occur at these paths in
 ground state terms $\calS$.
 


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.