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

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

Revision: 1566
          http://toss.svn.sourceforge.net/toss/?rev=1566&view=rev
Author:   lukstafi
Date:     2011-09-13 17:47:33 +0000 (Tue, 13 Sep 2011)
Log Message:
-----------
GDL translation: transforming original state terms without fluent paths into relations; adding new state terms (therefore elements) with a single coordinate path in case of missing subterms.

Modified Paths:
--------------
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-09-12 22:25:10 UTC (rev 1565)
+++ trunk/Toss/GGP/GDL.ml	2011-09-13 17:47:33 UTC (rev 1566)
@@ -28,6 +28,12 @@
 
 module Terms = Set.Make (
   struct type t = term let compare = Pervasives.compare end)
+let add_terms nvs vs =
+  List.fold_left (fun vs nv -> Terms.add nv vs) vs nvs
+let terms_of_list nvs =
+  add_terms nvs Terms.empty
+
+
 module Atoms = Set.Make (
   struct type t = rel_atom let compare = Pervasives.compare end)
 
@@ -480,6 +486,10 @@
     Tuples.mem tup (Aux.StrMap.find rel graph)
   with Not_found -> false
 
+let gdl_rel_graph rel graph =
+  try Tuples.elements (Aux.StrMap.find rel graph)
+  with Not_found -> []
+
 let instantiate_one tot_base cur_base irules =
   Aux.concat_map (function
     | (hrel, hargs as head), [], neg_body ->
@@ -829,6 +839,7 @@
       cls)
     program
 
+
 (* ************************************************************ *)
 (* ************************************************************ *)
 (** {3 Transformations of GDL clauses: inlining, negation.} *)

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-09-12 22:25:10 UTC (rev 1565)
+++ trunk/Toss/GGP/GDL.mli	2011-09-13 17:47:33 UTC (rev 1566)
@@ -46,6 +46,10 @@
   (** game ends here: match id, actions on previous step *)
 
 
+module Terms : Set.S with type elt = term
+val add_terms : term list -> Terms.t -> Terms.t
+val terms_of_list : term list -> Terms.t
+
 val atoms_of_body : literal list -> atom list
 val rel_of_atom : atom -> rel_atom
 
@@ -80,7 +84,10 @@
 module Tuples : Set.S with type elt = term array
 type graph = Tuples.t Aux.StrMap.t
 val graph_mem : string -> term array -> graph -> bool
+val merge_graphs : graph -> graph -> graph
+val build_graph : rel_atom list -> graph  
 val graph_to_atoms : graph -> rel_atom list
+val gdl_rel_graph : string -> graph -> term array list
 (** Saturation currently exposed for testing purposes. *)
 val saturate : graph -> gdl_rule list -> graph
 

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-09-12 22:25:10 UTC (rev 1565)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-09-13 17:47:33 UTC (rev 1566)
@@ -18,12 +18,6 @@
     occur in the structure)
 
     TODO: filter out legal tuples that are not statically satisfiable
-
-    TODO: after detecting that some state terms do not have any fluent
-    paths in them, eliminate these state terms by performing a GDL
-    source-level transformation into relations (i.e. erase the "init"
-    and "true" wrappers, and their "next" clauses, which are frame
-    clauses)
     
     TODO: perform the argument-path analysis for all GDL relations,
     not only future defined relations; if fact-only GDL relations have
@@ -234,7 +228,7 @@
   (* Turns out the saturation-based solver is sometimes far better for
      performing aggregate playout, which is very much
      saturation-like. *)
-  let static_rel_defs, nonstatic_rel_defs,
+  let _, _,
     static_base, init_state, (agg_actions, agg_states, terminal_state) =
     playout_satur ~aggregate:true players !playout_horizon rules in
   (* *)
@@ -273,6 +267,51 @@
          (List.map GDL.path_str (GDL.paths_to_list f_paths)))
   );
   (* }}} *)
+  (* Lifting state terms that are not operated-on during game
+     evolution into relations. *)
+  let used_roots = Aux.strings_of_list
+    (Aux.map_some (function Func (f,_),_ -> Some f
+      | _ -> None) move_clauses) in
+  let frame_clauses, unused_roots = Aux.partition_map
+    (function
+      | Func (f, args), _ when not (Aux.Strings.mem f used_roots) ->
+        Aux.Right (f, Array.length args)
+      | fr_cl -> Aux.Left fr_cl) frame_clauses in
+  let arities = Aux.unique_sorted unused_roots @ arities in
+  let unused_roots = Aux.strings_of_list (List.map fst unused_roots) in
+  let static_rels = Aux.Strings.elements unused_roots @ static_rels in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "create_init_struc:\nused_roots=%s\nunused_roots=%s\nstatic_rels=%s\n%!"
+      (String.concat ", "(Aux.Strings.elements used_roots))
+      (String.concat ", "(Aux.Strings.elements unused_roots))
+      (String.concat ", " static_rels)
+  );
+  (* }}} *)
+  let ground_state_terms = List.filter
+    (function
+      | Func (f, _) when Aux.Strings.mem f unused_roots -> false
+      | _ -> true) ground_state_terms in
+  let more_base = Aux.map_some
+    (function
+      | [|Func (f, args)|] when Aux.Strings.mem f unused_roots ->
+        Some (f, args)
+      | _ -> None)
+    (gdl_rel_graph "init" static_base) in
+  let static_base = merge_graphs (build_graph more_base) static_base in
+  let rec lift_to_rel = function
+    | Pos (True (Func (f, args)))
+        when Aux.Strings.mem f unused_roots -> Pos (Rel (f, args))
+    | Neg (True (Func (f, args)))
+        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
+    (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
   let element_reps =
     Aux.unique_sorted (List.map (fun t ->
       simult_subst f_paths blank t) ground_state_terms) in
@@ -306,13 +345,47 @@
              (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 ->
       simult_subst c_paths blank t) element_reps) in
+  (* Compute all available subterms to see what subterms are missing
+     among element representants. *)
+  let coord_subterms = List.fold_right add_terms
+    (List.map (at_paths c_paths) element_reps) Terms.empty in
+  (* Now compute what subterms are needed to represent all the
+     relations. *)
+  let needed_coords = List.fold_right add_terms
+    (List.map
+       (fun r-> if r="init" || r="role" then [] else
+           Aux.concat_map Array.to_list
+             (gdl_rel_graph r static_base))
+       static_rels) Terms.empty in
+  let missing_coords =
+    Terms.elements (Terms.diff needed_coords coord_subterms) in
   (* {{{ log entry *)
   if !debug_level > 2 then (
+    Printf.printf "create_init_struc: missing_coords=%s\n%!"
+      (String.concat ", "(List.map term_str missing_coords))
+  );
+  (* }}} *)
+  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
+  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 gorund_state_terms = val_elems @ ground_state_terms in *)
+  let root_reps =
+    if val_elems = [] then root_reps
+    else Func ("val_", [|blank|])::root_reps in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
     Printf.printf
       "create_init_struc: root_reps=\n%s\n%!"
       (String.concat ", " (List.map term_str root_reps))
@@ -333,6 +406,12 @@
     static_rels in
   let struc_rels = "EQ_"::struc_rels in
   let defined_rels = defined_rels @ nonstatic_rels in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "create_init_struc: struc_rels=%s; defined_rels=%s\n%!"
+      (String.concat ", " struc_rels) (String.concat ", " defined_rels)
+  );
+  (* }}} *)
   (* we need to expand frame clauses so that later local variables will get
      eliminated from erasure clauses *)
   let defs = List.filter
@@ -340,8 +419,10 @@
   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
-  let frame_defs = List.assoc "next"
-    (defs_of_rules (Aux.concat_map rules_of_clause frame_clauses)) in
+  let frame_defs =
+    try List.assoc "next"
+          (defs_of_rules (Aux.concat_map rules_of_clause frame_clauses))
+    with Not_found -> [] in
   let frame_defs = expand_definitions defs frame_defs in
   let pos = function Distinct _ as a -> Neg a | a -> Pos a in
   let neg = function Distinct _ as a -> Pos a | a -> Neg a in
@@ -351,14 +432,8 @@
       List.map (fun a->pos (atom_of_rel a)) body @
         List.map (fun a->neg (atom_of_rel a)) neg_body)
     frame_defs in
-  (* {{{ log entry *)
-  if !debug_level > 2 then (
-    Printf.printf
-      "create_init_struc: struc_rels=%s; defined_rels=%s\n%!"
-      (String.concat ", " struc_rels) (String.concat ", " defined_rels)
-  );
-  (* }}} *)
   let stable_rels = ref Aux.Strings.empty in
+  (* TODO: OPTIMIZE!!! *)
   let struc =
     List.fold_left (fun struc rel ->
       let arity = List.assoc rel arities in

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-09-12 22:25:10 UTC (rev 1565)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-09-13 17:47:33 UTC (rev 1566)
@@ -307,20 +307,16 @@
 
 let a () =
   set_debug_level 4;
-      game_test_case ~game_name:"breakthrough" ~player:"white"
-        ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"move_x2_y3_x3_y4_noop"
-        ~loc0_emb:[
-          "cellholds_x2_y3__BLANK_", "cellholds_2_2__BLANK_";
-          "cellholds_x3_y4__BLANK_", "cellholds_1_3__BLANK_";
-          "control__BLANK_", "control__BLANK_"]
-        ~loc0_move:"(move 2 2 1 3)" ~loc0_noop:"noop" ~loc1:1
-        ~loc1_rule_name:"noop_move_x7_y9_x8_y10"
-        ~loc1_emb:[
-          "cellholds_x7_y9__BLANK_", "cellholds_7_7__BLANK_";
-          "cellholds_x8_y10__BLANK_", "cellholds_6_6__BLANK_";
-          "control__BLANK_", "control__BLANK_"]
-        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
+      simult_test_case ~game_name:"2player_normal_form_2010" ~player:"row"
+        ~own_plnum:1 ~opp_plnum:2       (* 0 is environment! *)
+        ~own_rule_name:"m"
+        ~own_emb:["did__BLANK__m", "did__BLANK__r1";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
+        ~own_move:"r1"
+        ~opp_rule_name:"m2"
+        ~opp_emb:["did__BLANK__m2", "did__BLANK__c1";
+                  "reward_r1_c1_90_90", "reward_r1_c1_90_90"]
+        ~opp_move:"c1"
 
 
 let a () =

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-09-12 22:25:10 UTC (rev 1565)
+++ trunk/Toss/www/reference/reference.tex	2011-09-13 17:47:33 UTC (rev 1566)
@@ -2167,12 +2167,13 @@
 (including both the heads $(R \ t^j_1 \ldots t^j_n)$, and inside of
 $b_j$ above) be $\calR=\big\{(R \ r^1_1 \ldots r^1_n),\ldots,(R \
 r^K_1 \ldots r^K_n)\big\}$. Based on $\calR$ we will find a partition
-of argument positions and an assignment of coordinate paths to positions
-$(a_1,p_1),\ldots,(a_n,p_n)$ such that $a_1=1$, $a_{i+1}-a_i \in \{0,1\}$, for any partition $\calI = \{i
-\ | \ a_i = I\}$, the paths $(p_i \ | \ i \in \calI)$ are distinct and
-do not conflict, \ie $(\exists s) (\forall p_i \ | \ i \in \calI) \
-s\tpos_{p_i}$. GDL arguments of a single partition will be passed as a
-single defined relation argument.
+of argument positions and an assignment of coordinate paths to
+positions $(a_1,p_1),\ldots,(a_n,p_n)$ such that $a_1=1$,
+$\{a_1,\ldots,a_n\} = \{1,2,\ldots,\max\{a_1,\ldots,a_n\}\}$, for any
+partition $\calI = \{i \ | \ a_i = I\}$, the paths $(p_i \ | \ i \in
+\calI)$ are distinct and do not conflict, \ie $(\exists s) (\forall
+p_i \ | \ i \in \calI) \ s\tpos_{p_i}$. GDL arguments of a single
+partition will be passed as a single defined relation argument.
 
 To find the paths and the partition, consider a clause body
 $\mathtt{b}$, any occurrence of relation $R$ atom $(R \ r^j_1 \ldots

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