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

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

Revision: 1533
          http://toss.svn.sourceforge.net/toss/?rev=1533&view=rev
Author:   lukstafi
Date:     2011-08-10 12:15:33 +0000 (Wed, 10 Aug 2011)

Log Message:
-----------
GDL translation fixing: eliminating ground arguments of relations integrated.

Modified Paths:
--------------
    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

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/GDL.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -555,7 +555,7 @@
         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)
+        sb, (* subst_clause sb *) r_br)
       grounding in
 
   let rec expand_literal emb_lit literal (sb, (head, body) as accu) =
@@ -580,7 +580,7 @@
     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 elim_ground_arg new_rels rel arg clauses =
   let rel_brs, clauses =
     List.partition (fun ((r,_),_) -> r=rel) clauses in
   let grounding = Aux.unique_sorted
@@ -590,24 +590,33 @@
       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
+      new_rels := rname:: !new_rels;
       (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 new_rels = ref [] and all_rels = ref [] 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
+       aux (elim_ground_arg new_rels rel arg clauses) rels
+       with Not_found ->
+         all_rels := rel:: !all_rels; aux clauses rels) in
   let rec fix clauses =
-    modified := false;
+    all_rels := !new_rels @ !all_rels;
+    new_rels := [];
     let clauses = aux clauses rels in
-    if !modified then fix clauses else clauses in
+    if !new_rels <> []
+    then fix clauses
+    else
+      let all_rels = List.filter
+        (fun r->List.exists
+          (function ((rel,_),_) when r=rel -> true | _ -> false) clauses)
+        (Aux.unique_sorted !all_rels) in
+      all_rels, clauses in
   fix clauses
   
 
@@ -799,6 +808,7 @@
 
 let player_vars_of rels =
   Aux.map_some (function
+    | "role", [|Var v|] -> Some v
     | "goal", [|Var v; _|] -> Some v
     | "does", [|Var v; _|] -> Some v
     | "legal", [|Var v; _|] -> Some v

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/GDL.mli	2011-08-10 12:15:33 UTC (rev 1533)
@@ -91,7 +91,11 @@
 
 val func_graph : string -> term list -> term array list
 
-val elim_ground_args : string list -> clause list -> clause list
+(** Eliminate arguments of relations that are constant in each
+    defining clause. Return the new clauses, and also the new
+    relation set. *)
+val elim_ground_args :
+  string list -> clause list -> string list * clause list
 
 (** {3 GDL translation helpers.} *)
 

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/GDLTest.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -218,10 +218,14 @@
 	(nextcol ?d ?e)
     (true (cell ?x ?e o)))
 " in
-      let 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)
+        "col__o, col__x, conn5__o, conn5__x, row__o, row__x"
+        (String.concat ", " defined_rels);
+      assert_equal ~printer:(fun x->x)
         "(<= (conn5__o )
     (or (col__o ) (row__o )))
 (<= (conn5__x )

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -2,6 +2,8 @@
 
 open GDL
 
+let debug_level = ref 0
+
 let rel_atoms body =
   Aux.map_some (function Rel (rel, args) -> Some (rel, args)
     | _ -> None) (atoms_of_body body)
@@ -226,6 +228,12 @@
   let build_defrel rel =
     (* searching for ArgType = DefSide,S,p *)
     let branches = Aux.assoc_all rel all_branches in
+    (* {{{ log entry *)
+    if !debug_level > 2 then (
+      Printf.printf "build_defrel: rel=%s, no of brs=%d\n%!"
+        rel (List.length branches)
+    );
+    (* }}} *)
     (* first find the common paths, we will find the state terms later *)
     let branch_paths =
       List.map (fun (args, (_, sterms_pos, sterms_neg)) ->
@@ -290,10 +298,13 @@
         match defside, callside with
           | Some p, _ | None, Some p -> p
           | None, None ->
-      (* the ArgType(R,i) = NoSide,p variant is precomputed *)
-            match (List.assoc rel data.rel_default_path).(i) with
-              | Some p -> p
-              | None -> failwith
+            (* the ArgType(R,i) = NoSide,p variant is precomputed *)
+            try
+              match (List.assoc rel data.rel_default_path).(i) with
+                | Some p -> p
+                | None -> raise Not_found
+            with Not_found ->
+              failwith
                 (Printf.sprintf
                    "TranslateFormula.build_defrels: could not \
   determine path for relation %s argument %d" rel i)
@@ -313,7 +324,7 @@
               | None -> assert false in
             Formula.Eq (v, s_i)
           else Formula.Eq (v,
-            var_of_subterm data arg_paths.(i) args.(i)))
+                           var_of_subterm data arg_paths.(i) args.(i)))
         defvars in
       let arg_eqs = Formula.And (Array.to_list arg_eqs) in
       let callside_sterms =

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-08-10 12:15:33 UTC (rev 1533)
@@ -1,3 +1,5 @@
+val debug_level : int ref
+
 (* Whether $i$th argument is a $\mathrm{DefSide}$ or a
    $\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
 type defrel_arg_type = (bool * GDL.path) array

Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -30,15 +30,18 @@
     ["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)
-    [["cell", 2]; ["control", 0]] GDL.empty_path_set in
+    f_paths GDL.empty_path_set in
   let m_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 m_paths in
   let mask_reps =
     [GDL.Func ("control", [|GDL.blank|]);
      GDL.Func ("cell", [|GDL.blank; GDL.blank; GDL.blank|])] in
-  let defrel_arities = [
+  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;
@@ -46,10 +49,13 @@
     "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 = List.map fst defrel_arities 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) defrel_arities in
+    (fun (rel, ar) -> rel, Array.make ar default_path) exp_defrel_arities in
+  ground_at_f_paths,
   {
     f_paths = f_paths;
     m_paths = m_paths;
@@ -66,10 +72,19 @@
   "defined relations connect5" >::
     (fun () ->
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
-      let transl_data = connect5_data in
+      let ground_at_f_paths, transl_data = connect5_data in
       let clauses = GDL.expand_players descr in
       let clauses =
+        GDL.ground_vars_at_paths ground_at_f_paths clauses in
+      let defined_rels, clauses =
         GDL.elim_ground_args transl_data.defined_rels clauses in
+      (* {{{ log entry *)
+      if !TranslateFormula.debug_level > 2 then (
+        Printf.printf "defined relations connect5: clauses =\n%s\n%!"
+          (String.concat "\n" (List.map GDL.clause_str clauses))
+      );
+      (* }}} *)
+      let transl_data = {transl_data with defined_rels = defined_rels} in
       let defined_rels =
         TranslateFormula.build_defrels transl_data clauses in
       let res = String.concat "\n"
@@ -78,9 +93,39 @@
             ") = "^Formula.str body) defined_rels) in
       assert_equal ~msg:"connect5 noop moves by players"
         ~printer:(fun x->x)
-        "" res;
+        "" res
     ); 
 
 ]
 
+let a () =
+  TranslateFormula.debug_level := 5;
+  GDL.debug_level := 2;
+  ()
+
+let a () =
+  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 clauses =
+    GDL.ground_vars_at_paths ground_at_f_paths clauses in
+  let defined_rels, clauses =
+    GDL.elim_ground_args transl_data.defined_rels clauses in
+  (* {{{ log entry *)
+  if !TranslateFormula.debug_level > 2 then (
+    Printf.printf "defined relations connect5: clauses =\n%s\n%!"
+      (String.concat "\n" (List.map GDL.clause_str clauses))
+  );
+  (* }}} *)
+  let transl_data = {transl_data with defined_rels = defined_rels} in
+  let defined_rels =
+    TranslateFormula.build_defrels transl_data clauses in
+  let res = String.concat "\n"
+    (List.map (fun (rel,(args,body)) ->
+      rel^"("^String.concat ", " args^
+        ") = "^Formula.str body) defined_rels) in
+  assert_equal ~msg:"connect5 noop moves by players"
+    ~printer:(fun x->x)
+    "" res
+
 let exec = Aux.run_test_if_target "TranslateFormulaTest" tests

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -231,7 +231,8 @@
 
 
 (* Expand role variables, find fluent and mask paths, generate the
-   initial structure. *)
+   initial structure. Encode frame clauses by using the unique
+   relation name "frame next". *)
 let create_init_struc clauses =
   let players =
     Aux.map_some (function
@@ -389,8 +390,13 @@
   let elem_term_map = Aux.intmap_of_assoc
     (List.map (fun e ->
       Structure.find_elem struc (term_to_name e), e) element_reps) in
+  let clauses =
+    List.filter (fun ((rel,_),_) -> rel <> "next") clauses in
+  let frame_clauses = List.map
+    (fun ((_,args),body) -> ("frame next", args), body) frame_clauses in
   players, rules,
-  frame_clauses, move_clauses, f_paths, m_paths, mask_reps, defined_rels,
+  frame_clauses @ move_clauses @ clauses,
+  f_paths, m_paths, mask_reps, defined_rels,
   Aux.Strings.elements !stable_rels, Aux.Strings.elements !fluents,
   static_base, init_state, struc, ground_state_terms, elem_term_map
 
@@ -1124,7 +1130,7 @@
   let clauses = expand_players clauses in
   let used_vars, clauses = rename_clauses clauses in
   let players, rules,
-    frame_clauses, move_clauses, f_paths, m_paths,
+    clauses, f_paths, m_paths,
     mask_reps, defined_rels, stable_rels, fluents,
     static_base, init_state, struc, ground_state_terms, elem_term_map =
     create_init_struc clauses in
@@ -1135,20 +1141,15 @@
   let ground_at_f_paths = ground_at f_paths in
   let clauses =
     ground_vars_at_paths ground_at_f_paths clauses in
-  let frame_clauses =
-    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
-      | _ -> assert false) frame_clauses
-    @ List.map (function
-      | (_,[|s_C|]),body_C -> s_C, false, body_C
-      | _ -> assert false) move_clauses in
+  let defined_rels, clauses = elim_ground_args defined_rels clauses in
+  let next_cls = Aux.map_some
+    (function
+      | ("frame next",[|s_C|]),body_C -> Some (s_C, true, body_C)
+      | ("next",[|s_C|]),body_C -> Some (s_C, false, body_C)
+      | _ -> None)
+    clauses in
   let turn_data =
     try Some (check_turn_based players rules)
     with Not_turn_based -> None in

Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateGame.mli	2011-08-10 12:15:33 UTC (rev 1533)
@@ -49,7 +49,8 @@
 val empty_gdl_translation : gdl_translation
 
 (* Create the initial structure and assorted data. Exposed for testing
-   purposes. 
+   purposes. Encode frame clauses by using the unique
+   relation name "frame next".
 
    [players, rules, frame_cls, move_cls, f_paths, m_paths, mask_reps,
    defined_rels, stable_rels, fluents, stable_base, init_state,
@@ -57,7 +58,7 @@
 val create_init_struc :
   GDL.clause list ->
   GDL.term array * GDL.gdl_rule list *
-    GDL.clause list * GDL.clause list * GDL.path_set *
+    GDL.clause list * GDL.path_set *
     GDL.path_set * GDL.term list * string list * string list *
     string list * GDL.rel_atom list * GDL.term list *
     Structure.structure * GDL.term list *

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-08-10 03:31:00 UTC (rev 1532)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-08-10 12:15:33 UTC (rev 1533)
@@ -120,7 +120,7 @@
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
       let clauses = GDL.expand_players descr in
       let players, rules,
-        frame_cls, move_cls, f_paths, m_paths, mask_reps, defined_rels,
+        clauses, f_paths, m_paths, mask_reps, defined_rels,
         stable_rels, fluents,
         stable_base, init_state, struc, ground_state_terms, elem_term_map =
         TranslateGame.create_init_struc clauses in


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