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

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

Revision: 1324
          http://toss.svn.sourceforge.net/toss/?rev=1324&view=rev
Author:   lukstafi
Date:     2011-02-22 01:08:46 +0000 (Tue, 22 Feb 2011)

Log Message:
-----------
GDL translation related major commit. Heuristic adv-ratio separate monotonic and non-monotonic defaults, default effort parameter. All-upper/all-lower case insensitive KIF keywords. List-related helper functions.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/Arena/DiscreteRule.mli
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/AuxTest.ml
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/GGP/KIFLexer.mll
    trunk/Toss/Play/Game.ml
    trunk/Toss/Play/Game.mli
    trunk/Toss/Play/GameTest.ml
    trunk/Toss/Play/Heuristic.ml
    trunk/Toss/Play/Heuristic.mli
    trunk/Toss/Server/Server.ml
    trunk/Toss/Server/ServerTest.ml
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/Solver.mli

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Arena/Arena.ml	2011-02-22 01:08:46 UTC (rev 1324)
@@ -473,6 +473,8 @@
   | GetRuleMatches of string                       (* Get matches of a rule *)
   | ApplyRule of string * (string * string) list * float * (string * float) list
       (* Apply rule at match for given time and with params *)
+  | ApplyRuleInt of string * (int * int) list * float * (string * float) list
+      (* Apply rule at match for given time and with params *)
   | GetRuleNames                                   (* Get names of all rules *)
   | SetTime of float * float                       (* Set time step and time *)
   | GetTime                                        (* Get time step and time *)
@@ -858,6 +860,19 @@
          | None -> (state, "ERR applying "^r_name^", postcondition fails")
        with Not_found -> (state, "ERR applying "^r_name^", rule not found")
       )
+    | ApplyRuleInt (r_name,  mtch, t, p) ->
+      (let try r = List.assoc r_name state.game.rules in
+       match ContinuousRule.rewrite_single struc state.time mtch r t p with
+         | Some (new_struc, new_time, shifts) ->
+           let val_str ((f, e), tl) = 
+	     let ts t = string_of_float (Term.term_val t) in
+         (* we've moved to using element names in Term *)
+	     f ^ ", " ^ e ^ ", " ^ (String.concat ", " (List.map ts tl)) in
+           let shifts_s = String.concat "; " (List.map val_str shifts) in
+           ({state with struc = new_struc; time = new_time}, shifts_s)
+         | None -> (state, "ERR applying "^r_name^", postcondition fails")
+       with Not_found -> (state, "ERR applying "^r_name^", rule not found")
+      )
     | GetRuleNames -> (state, String.concat "; " (fst (List.split state.game.rules)))
     | SetTime (tstep, t) ->
       ContinuousRule.set_time_step tstep;

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Arena/Arena.mli	2011-02-22 01:08:46 UTC (rev 1324)
@@ -174,6 +174,7 @@
   | GetRuleMatches of string                       (** Get matches of a rule *)
   | ApplyRule of string * (string * string) list * float * (string * float) list
       (** Apply rule at match for given time and with params *)
+  | ApplyRuleInt of string * (int * int) list * float * (string * float) list
   | GetRuleNames                                   (** Get names of rules *)
   | SetTime of float * float                       (** Set time step and time *)
   | GetTime                                        (** Get time step and time *)

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Arena/DiscreteRule.ml	2011-02-22 01:08:46 UTC (rev 1324)
@@ -176,7 +176,7 @@
   Solver.M.evaluate model rule_obj.lhs_form_pp
 
 (* Convert assignment to an embedding of the LHS structure. *)
-let assignment_to_embedding rule_obj assgn =
+let assignment_to_embedding rule_obj asgn =
   List.map (fun (var,e) ->
     try
       elem_of_elemvar rule_obj.lhs_elem_names var, e
@@ -184,7 +184,7 @@
       failwith (
         "assignment_to_embedding: inconsistent rule_obj at variable "
                                   ^ var))
-    assgn
+    asgn
 
 (* Choose an arbitrary embedding of a rule from the matchings returned
    by {!find_matchings} for the same structure and rewrite rule. Does
@@ -192,10 +192,10 @@
 let choose_match model rule_obj matches =
   let elem = Structure.Elems.choose model.Structure.elements in
   let default = List.map (fun v->v,elem) rule_obj.lhs_elem_vars in
-  let assgn = AssignmentSet.choose_fo default matches in
-  assignment_to_embedding rule_obj assgn
+  let asgn = AssignmentSet.choose_fo default matches in
+  assignment_to_embedding rule_obj asgn
 
-let rec enumerate_assgns all_elems vars = function
+let rec enumerate_asgns all_elems vars = function
     | AssignmentSet.Any ->
 	(* let all_elems = Structure.Elems.elements all_elems in *)
 	let elems = List.map (fun _ -> all_elems) vars in
@@ -207,19 +207,19 @@
 	let vars = list_remove v vars in
 	concat_map (fun (e,sub)->
 	  List.map (fun tl->(v,e)::tl)
-	    (enumerate_assgns all_elems vars sub)) els
+	    (enumerate_asgns all_elems vars sub)) els
     | AssignmentSet.MSO (_, els) ->
 	concat_map (fun (e,sub)->
-	  enumerate_assgns all_elems vars sub) els 
+	  enumerate_asgns all_elems vars sub) els 
     | AssignmentSet.Real _ -> failwith "real matches unsupported"
 
 (* Enumerate matchings returned by {!find_matchings} for the same
    structure and rewrite rule. *)
 let enumerate_matchings model rule matches =
   let all_elems = Structure.Elems.elements model.Structure.elements in
-  let assgns =
-    enumerate_assgns all_elems rule.lhs_elem_vars matches in
-  List.map (assignment_to_embedding rule) assgns
+  let asgns =
+    enumerate_asgns all_elems rule.lhs_elem_vars matches in
+  List.map (assignment_to_embedding rule) asgns
 
 (* Helpers for special relations. *)
 let orig_rel_of rel =
@@ -573,12 +573,12 @@
       let arg_tup = Array.of_list args in
       map_some (fun (brel, ar) ->
         let selector = Structure.free_for_rel brel ar in
-        let assgn =
+        let asgn =
           Solver.M.evaluate selector rphi in
         let btup = Array.init ar (fun i->i+1) in
         (* [selector] has only [btup] with its elements *)
         let selvars =
-          enumerate_assgns (Array.to_list btup) args assgn in
+          enumerate_asgns (Array.to_list btup) args asgn in
         (* inverse image of [tups] *)
         let btups =
           concat_map (fun tup ->
@@ -781,17 +781,17 @@
   let rhs_opt_rels, rhs_rels, _ =
     compile_opt_rels rhs_rels in
   if List.exists (fun (drel, _) -> List.mem_assoc drel rhs_rels)
-   defined_rels
+    defined_rels
   then failwith
     ("Non-optional defined relation(s) "^
         String.concat ", " (Aux.map_some (fun (drel,_) ->
           if List.mem_assoc drel rhs_rels then Some drel else None)
                               defined_rels)
-        ^" on RHS.");
+     ^" on RHS.");
   (* if the rule is optimized for "nonstructural" rewriting, elements
      are already renamed; raises Not_found when adding elements *)
   let mapf_rn = if rlmap = None then fun x->x else
-    Array.map (fun e-> List.assoc e rule_src.rule_s) in
+      Array.map (fun e-> List.assoc e rule_src.rule_s) in
   (* a tuple is positive when it (possibly) has to be added: it does
      not occur on the LHS *)
   let rhs_pos_tuples =
@@ -799,13 +799,13 @@
       rel, List.filter (fun tup ->
         try
           not (List.mem (mapf_rn tup)
-            (try List.assoc rel lhs_pos_expanded with Not_found -> []))
+                 (try List.assoc rel lhs_pos_expanded with Not_found -> []))
         with Not_found -> true          (* new element: has to be added *)
       ) tups)
       rhs_rels in
   let rhs_all_tups n =
     List.map Array.of_list (Aux.product
-      (Aux.fold_n (fun acc -> rhs_elems::acc) [] n)) in
+                              (Aux.fold_n (fun acc -> rhs_elems::acc) [] n)) in
   (* a tuple is negative when it has to be removed: it is in $\tau_e$
      and in the LHS, but it does not occur on the RHS even optionally *)
   let rhs_neg_tuples = 
@@ -813,16 +813,16 @@
       rel, List.filter (fun tup ->
         try
           (List.mem (mapf_rn tup)
-            (try List.assoc rel lhs_pos_expanded with Not_found -> [])
-          ||
-            List.mem (mapf_rn tup)
-            (try List.assoc rel lhs_opt_rels with Not_found -> []))
+             (try List.assoc rel lhs_pos_expanded with Not_found -> [])
+           ||
+             List.mem (mapf_rn tup)
+             (try List.assoc rel lhs_opt_rels with Not_found -> []))
           &&
             not (
               (List.mem tup
-                (try List.assoc rel rhs_rels with Not_found -> [])
-              || List.mem tup
-                (try List.assoc rel rhs_opt_rels with Not_found -> []))
+                 (try List.assoc rel rhs_rels with Not_found -> [])
+               || List.mem tup
+                 (try List.assoc rel rhs_opt_rels with Not_found -> []))
             )
         with Not_found -> false         (* adding element: can't be negative *)
       ) (rhs_all_tups (List.assoc rel signat)))
@@ -834,8 +834,19 @@
     rel, List.map (fun tup -> Array.map rhs_name_of tup) tups)
     rhs_neg_tuples in
   (* Optimizing the embedding formula. *)
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "compile_rule: embedding formula = %s\n%!"
+      (Formula.sprint emb)
+  );
+  (* }}} *)
   let lhs_form_pp =
     Solver.M.register_formula emb in
+(* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "compile_rule: done.\n%!";
+  );
+  (* }}} *)
   {
     lhs_elem_names = lhs_elem_names;
     lhs_elem_inv_names = lhs_elem_inv_names;
@@ -865,13 +876,17 @@
     List.map fst rels1 @ List.map fst rels2
     @ acc)[]  rules
 
-let translate_from_precond ~precond ~add ~del =
-  let diff a b = List.filter (fun e -> not (List.mem e b)) a in
-  let del = diff del add in
+(* Build a rule by translating the "add" list into the RHS structure
+   directly, and separating out from a precondition the LHS structure
+   over the [struc_vars] variables. All relations are
+   considered embedded. (Obviously, not all rules can be generated in
+   this way.) *)
+let translate_from_precond ~precond ~add ~embed ~struc_elems =
   let rhs_names = Aux.unique_sorted
-    (Aux.concat_map (fun (_,arg) -> Array.to_list arg) (add @ del)) in
+    (Aux.concat_map (fun (_,arg) -> Array.to_list arg) add) in
+  assert (Aux.list_diff rhs_names struc_elems = []);
   let rewritable args =
-    Aux.array_for_all (fun v -> List.mem (Formula.var_str v) rhs_names)
+    Aux.array_for_all (fun v -> List.mem (Formula.var_str v) struc_elems)
       args in
   let conjs = FormulaOps.flatten_ands precond in
   let literals, conjs = Aux.partition_map (function
@@ -881,40 +896,35 @@
       Left (Right (rel,args))
     | phi -> Right phi) conjs in
   let posi, nega = Aux.partition_choice literals in
+  (* FIXME: TODO: check and at least warn when [nega] is smaller than
+     the complement of [posi] over embedded rels *)
   let precond = Formula.And conjs in
   let fvars = FormulaOps.free_vars precond in
   let local_vars =
     List.filter (fun v->
-      not (List.mem (Formula.var_str v) rhs_names)) fvars in
+      not (List.mem (Formula.var_str v) struc_elems)) fvars in
   let precond =
     if local_vars = [] then precond
     else Formula.Ex (local_vars, precond) in
-  let emb_rels = Aux.unique_sorted
-    (List.map fst (add @ del) @ List.map fst nega) in
+  let emb_rels = Aux.list_inter embed
+    (Aux.unique_sorted
+       (List.map fst add @ List.map fst (posi @ nega))) in
   let posi_s =
     List.map (fun (rel, args) -> rel, Array.map Formula.var_str args)
       posi in
-  let nega_s =
-    List.map (fun (rel, args) -> rel, Array.map Formula.var_str args)
-      nega in
-  let posi_emb =
-    List.filter (fun (rel,_) -> List.mem rel emb_rels) posi_s in
-  let del = List.filter (fun d -> not (List.mem d nega_s)) del in
-  let rhs_struc, rhs_names =
-    List.fold_left (fun (rhs_struc, rhs_names) name ->
+  let rhs_struc, struc_elems =
+    List.fold_left (fun (rhs_struc, struc_elems) name ->
       let rhs_struc, elem =
         Structure.add_new_elem rhs_struc ~name () in
-      rhs_struc, (name, elem)::rhs_names)
-      (Structure.empty_structure (), []) rhs_names in
+      rhs_struc, (name, elem)::struc_elems)
+      (Structure.empty_structure (), []) struc_elems in
   let add_rels = List.fold_left (fun struc (rel, args) ->
     Structure.add_rel struc rel
-      (Array.map (fun n -> List.assoc n rhs_names) args)) in
+      (Array.map (fun n -> List.assoc n struc_elems) args)) in
   let lhs_struc = rhs_struc in
-  let rhs_struc = add_rels rhs_struc (add @ diff posi_emb del) in
+  let rhs_struc = add_rels rhs_struc add in
   let lhs_struc = add_rels lhs_struc posi_s in
-  let lhs_struc = add_rels lhs_struc
-    (List.map (fun (rel,args) -> "_opt_"^rel, args)
-       (diff del (posi_emb @ nega_s))) in
+  (* no relations are optional, righ? *)
   {
     lhs_struc = lhs_struc;
     rhs_struc = rhs_struc;

Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Arena/DiscreteRule.mli	2011-02-22 01:08:46 UTC (rev 1324)
@@ -41,6 +41,7 @@
   rlmap          : (string * string) list option; (* rule_s on variables (?) *)
 }
 
+val elemvar_of_elem : elem_inv_names -> int -> string
 
 (* We call fluents the relations that can be modified by a rule. *)
 val fluents : rule_obj -> string list
@@ -116,7 +117,7 @@
 
 val translate_from_precond :
   precond:Formula.formula -> add:(string * string array) list ->
-  del:(string * string array) list -> rule
+  embed:string list -> struc_elems:string list -> rule
 
 (** {2 Printing.} *)
 val matching_str : matching -> string

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Formula/Aux.ml	2011-02-22 01:08:46 UTC (rev 1324)
@@ -18,6 +18,24 @@
 let ints_of_list nvs =
   add_ints nvs Ints.empty
 
+module StrMap = Map.Make
+  (struct type t = string let compare = String.compare end)   
+let rec strmap_of_assoc =
+  function
+    | [] -> StrMap.empty
+    | (k,v)::tl -> StrMap.add k v (strmap_of_assoc tl)
+let strmap_filter p m =
+  StrMap.fold (fun k v acc -> if p k v then (k,v)::acc else acc) m []
+
+module IntMap = Map.Make
+  (struct type t = int let compare x y = x - y end)   
+let rec intmap_of_assoc =
+  function
+    | [] -> IntMap.empty
+    | (k,v)::tl -> IntMap.add k v (intmap_of_assoc tl)
+let intmap_filter p m =
+  IntMap.fold (fun k v acc -> if p k v then (k,v)::acc else acc) m []
+
 let is_digit c =
   (c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') || 
     (c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9') 
@@ -71,6 +89,10 @@
 
 let list_remove v l = List.filter (fun w->v<>w) l
 
+let list_diff a b = List.filter (fun e -> not (List.mem e b)) a
+
+let list_inter a b = List.filter (fun e -> List.mem e b) a
+
 let rec rev_assoc l x = match l with
     [] -> raise Not_found
   | (a,b)::l -> if b = x then a else rev_assoc l x
@@ -110,6 +132,16 @@
       else aux (pair :: acc) l in
   aux [] l
 
+let rec update_assoc k v0 f l =
+  let rec aux acc = function
+    | [] -> [k, f v0]
+    | (a, b as pair) :: l ->
+      if compare a k = 0 then List.rev_append acc ((k, f b)::l)
+      else aux (pair :: acc) l in
+  aux [] l
+
+let cons e l = e::l
+
 let unsome = function
   | Some v -> v
   | None -> raise (Invalid_argument "unsome")

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Formula/Aux.mli	2011-02-22 01:08:46 UTC (rev 1324)
@@ -11,6 +11,16 @@
 val add_ints : int list -> Ints.t -> Ints.t
 val ints_of_list : int list -> Ints.t
 
+module StrMap : Map.S with type key = string
+val strmap_of_assoc : (string * 'a) list -> 'a StrMap.t
+val strmap_filter :
+  (string -> 'a -> bool) -> 'a StrMap.t -> (string * 'a) list
+
+module IntMap : Map.S with type key = int
+val intmap_of_assoc : (int * 'a) list -> 'a IntMap.t
+val intmap_filter :
+  (int -> 'a -> bool) -> 'a IntMap.t -> (int * 'a) list
+
 val is_digit : char -> bool
 
 val fst3 : 'a * 'b * 'c -> 'a
@@ -44,6 +54,12 @@
     inequality. *)
 val list_remove : 'a -> 'a list -> 'a list
 
+(** Difference: [List.filter (fun e -> not (List.mem e b)) a]. *)
+val list_diff : 'a list -> 'a list -> 'a list
+
+(** Intersection: [list_inter a b = List.filter (fun e -> List.mem e b) a]. *)
+val list_inter : 'a list -> 'a list -> 'a list
+
 (** Return first key with the given value from the key-value pairs,
     using structural equality. *)
 val rev_assoc : ('a * 'b) list -> 'b -> 'a
@@ -56,16 +72,24 @@
 val assoc_all : 'a -> ('a * 'b) list -> 'b list
 
 (** Replace the value of a first occurrence of a key, or place it at
-    the end of the assoc list. *)
+    the end of the assoc list. Not tail-recursive. *)
 val replace_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list
 
 (** Find the value associated with the first occurrence of the key and
-    remove them from the list. Uses structural equality. *)
+    remove them from the list. Uses structural equality. Tail-recursive. *)
 val pop_assoc : 'a -> ('a * 'b) list -> 'b * ('a * 'b) list
 
-(** As {!Aux.pop_assoc}, but uses physical equality. *)
+(** As {!Aux.pop_assoc}, but uses physical equality. Tail-recursive. *)
 val pop_assq : 'a -> ('a * 'b) list -> 'b * ('a * 'b) list
 
+(** Update the value associated with the first occurrence of the key,
+    if no key is present update the given default "zero"
+    value. Tail-recursive. *)
+val update_assoc : 'a -> 'b -> ('b -> 'b) -> ('a * 'b) list -> ('a * 'b) list
+
+(** [cons e l = e::l]. *)
+val cons : 'a -> 'a list -> 'a list
+
 (** unConstructors. *)
 val unsome : 'a option -> 'a
 

Modified: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/Formula/AuxTest.ml	2011-02-22 01:08:46 UTC (rev 1324)
@@ -77,7 +77,7 @@
     );  
 
 
-  "replace_assoc, pop_assoc, pop_assq" >::
+  "replace_assoc, pop_assoc, pop_assq, update_assoc" >::
     (fun () ->
       assert_equal ~printer:(print_alist (fun x -> x))
         ["B","f";"C","B"; "G","replaced"; "G", "T"]
@@ -111,6 +111,10 @@
         Not_found
         (fun () -> Aux.pop_assq g
           ["B","f";"G", "T0"; "C","B"; "F","Ts"]);
+
+      assert_equal ~msg:"update_assoc: two-level trie"
+        [(7, [('b', ["ha"])])]
+        (Aux.update_assoc 7 [] (Aux.update_assoc 'b' [] (Aux.cons "ha")) [])
     );  
 
   "unsome, map_try" >::

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-02-19 17:22:41 UTC (rev 1323)
+++ trunk/Toss/GGP/GDL.ml	2011-02-22 01:08:46 UTC (rev 1324)
@@ -11,7 +11,8 @@
 
     (1) Aggregate playout: generate successive states as if all moves
     legal in the previous state were performed. Do not check the
-    termination predicate.
+    termination predicate. To avoid ungrounded player variables, add
+    "role" filter to "legal" rules.
 
     (1a) Reason for unsoundness: "legal" or "next" preconditions can
     depend negatively on state, preventing further moves in the
@@ -35,6 +36,13 @@
     (2) Arena graph: currently, only a simple cycle is allowed. The
     succession of players is determined from the aggregate playout.
 
+    In case of problems, it should be relatively easy to expand the
+    translation to use a single location per player, and for rules to
+    determine which player is active after the rule takes effect
+    (i.e. the target location.) Once Toss has a good system for
+    simultaneous moves, we can simplify by translating into a single
+    location game, obsoleting this "chapter".
+
     (2a) We need to recognize which player actually makes a move in a
     state. For this we need to locate the "noop" arguments to "legal"
     and "does" relations. A noop action in a location is the only
@@ -206,7 +214,7 @@
     (7a) We translate each branch of the "legal" relation definition
     as one or more rewrite rules. Currently, we base availability of
     rules in a location on the player in the location and noop actions
-    of other players in it, compared to the the "legal" definition
+    of other players in it, compared to the "legal" definition
     branch (currently, we do not allow simultaneous moves). If the
     branch of "legal" definition has a variable for a player, it is
     instantiated for each player in the game, and the variable
@@ -293,6 +301,13 @@
 
     (7g) Instantiate remaining unfixed variables. Implementation TODO.
 
+    (7g1) Duplicate non-frame rules with unfixed variables for each
+    instantiation of the unfixed variables warranted by the aggregate
+    playout. (Perhaps can be done "symbolically" to avoid explosion.)
+
+    (7g2) Then, add instantiations of frame rules for each case their
+    head term unifies with one from all the non-frame rules.
+
     (7h) Introduce a new element variable for each class of "next" and
     "true" terms equal modulo mask (i.e. there is a mask matching them
     and they differ only at-or-below metavariables). (Remember the
@@ -401,7 +416,9 @@
     The rewrite rule is generated by joining the derived conjunctions
     from "next" atoms as RHS, and from bodies as the
     precondition. Exactly the RHS variables are listed in the LHS
-    (other variables are existentially closed in the precondition).
+    (other variables are existentially closed in the
+    precondition). All the relations that appear in either LHS or RHS
+    are considered embedded.
 
     (7o) After the rules are translated, perform an aggregated playout
     of the Toss variant of the game. Remove the rules that were never
@@ -420,8 +437,51 @@
     branches from the definition). For each goal value we collect
     bodies to form a disjunction.
 
-()
+    (9) To translate an incoming action, we:
 
+    (9a) find the "lead legal" term to which the "does move" ground
+    term of the current player matches;
+
+    (9b) earlier, remember which Toss variables of a rule contain which
+    fixed variables at which positions in their masks;
+
+    (9c) find anchor predicates corresponding to instantiations of the
+    "lead legal" variables, anchoring positions found by (9b) "fixed
+    var" - "mask + mask var" correspondence;
+
+    (9d) build a conjunction of anchor predicates over variables that
+    contain the fixed variable which is "instantiated" by the anchor
+    of the corresponding position, as established by (9c);
+
+    (9e) conjoin the (9d) with the "matching" formula of a rule, and
+    evaluate the result for all rules (of the located "lead legal"
+    class); only a single rule should have a match, and only a single
+    assignment should be returned; this rule with this assignment is
+    the translated move.
+
+    (10) To translate an outgoing action, we:
+
+    (10a) associate the rule with its corresponding data: the "lead
+    legal" term, the fixed variables corresponding to rule elements,
+    ...
+
+    (10b) earlier, return/store the mapping from an element to the
+    mask and subsitution that define the element;
+
+    (10c) earlier, for each rule store a mapping from fixed variables
+    to rule variables and the mask variables that in the rule variable
+    are instantiated by the fixed variables;
+
+    (10d) to determine how to instantiate the fixed variables in the
+    "lead legal" term, find the (10b) substitutions of assigned
+    elements and (10c) mask variables for fixed variables; compose the
+    maps to get fixed variable to GDL ground term mapping, each
+    "route" should give the same term.
+
+    Implementation TODO: once the LHS-RHS structures are removed from
+    the backbone and formula registration is removed, some
+    simplifications can be done in (9) and (10).
+
 *)
 
 let debug_level = ref 0
@@ -467,6 +527,47 @@
   | Stop of string * term list
   (* game ends here: match id, actions on previous step *)
 
+type tossrule_data = {
+  lead_legal : term;
+  (* the "legal"/"does" term of the player that performs the move, we
+     call its parameters "fixed variables" as they are provided externally *)
+  precond : Formula.formula;
+  (* the LHS match condition (the LHS structure and the precondition) *)
+  rhs_add : (string * string array) list;
+  (* the elements of LHS/RHS structures, corresponding to the "next"
+     terms *)
+  struc_elems : string list;
+  fixvar_elemvars :
+    (string * (term * (string * string list) list) list) list;
+  (* "state" terms indexed by variables that they contain, together
+     with the mask-path of the variable *)
+  elemvars : term Aux.StrMap.t;
+(* "state" terms indexed by Toss variable names they generate *)
+}
+
+type gdl_translation = {
+  anchor_terms :
+  (term * (string * (term * string) list) list) list;
+  (* mask path (i.e. mask+var) and a ground term to anchor predicate *)
+  tossrule_data : tossrule_data Aux.StrMap.t;
+  (* rule name to rule translation data *)
+  t_elements : term Aux.IntMap.t;
+  (* element terms (with metavariables only) *)
+  playing_as : int;
+  (* "active" player *)
+  noop_actions : term option array;
+  (* NOOP actions of "active" player indexed by locations *)
+  fluents : string list;
+}
+
+let empty_gdl_translation =
+  {anchor_terms = [];
+   tossrule_data = Aux.StrMap.empty;
+   t_elements = Aux.IntMap.empty;
+   playing_as = 0;
+   noop_actions = [||];
+   fluents = []}
+
 let rec term_str = function
   | Const c -> c
   | Var v -> "?"^v
@@ -836,6 +937,7 @@
 
 (* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
    TODO: optimize by using constant-time append data structure. *)
+(* Variables still left after saturation have universal interpretation! *)
 let saturate base rules =
 
   let instantiate_one tot_base cur_base irules =
@@ -927,7 +1029,6 @@
     (List.map rules_of_defs (stratify [] (defs_of_rules rules)))
 
 
-let playing_as = ref (Const "uninitialized")
 let game_description = ref []
 let player_terms = ref [| |]
 
@@ -1115,17 +1216,39 @@
 
 (* Collect the aggregate playout, but also the actions available in
    the state. *)
+exception Playout_over
 let aggregate_ply players static current rules =
   let base =
     Aux.map_prepend static (fun term -> "true", [term]) current in
   let base = saturate (base @ static) rules in
+  (* {{{ log entry *)
+  if !debug_level > 4 then (
+    Printf.printf "GDL.aggregate_ply: updated base -- %s\n%!"
+      (String.concat " " (List.map fact_str base))
+  );
+  (* }}} *)
   let does = Aux.map_some (fun (rel, args) ->
     if rel = "legal" then Some ("does", args) else None) base in
   if                                    (* no move *)
     Aux.array_existsi (fun _ player ->
-      List.for_all (function _, (actor::_) -> player <> actor | _ -> true)
+      List.for_all (function
+        |_, (Var _::_) -> false
+        | _, (actor::_) -> player <> actor | _ -> true)
         does) players
-  then raise Not_found
+  then (
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      let players_nomove =
+        Aux.array_find_all (fun player ->
+          List.for_all (function _, (actor::_) -> player <> actor
+            | _ -> true)
+            does) players in          
+      Printf.printf
+        "GDL.aggregate_ply: playout over due to no move for %s\n%!"
+        (String.concat ", " (List.map term_str players_nomove))
+    );
+    (* }}} *)
+    raise Playout_over)
   else
     let step = saturate (does @ base) rules in
     let step = Aux.map_some (function ("next", [arg]) -> Some arg
@@ -1136,7 +1259,13 @@
             Aux.array_existsi (fun _ player -> arg=player) players -> true
         | term -> List.mem term current
       ) step
-    then raise Not_found
+    then (
+      (* {{{ log entry *)
+      if !debug_level > 0 then (
+        Printf.printf "GDL.aggregate_ply: playout over due to fixpoint\n%!";
+      );
+      (* }}} *)
+      raise Playout_over)
     else
       List.map snd does, step
 
@@ -1161,13 +1290,14 @@
     (fun ((rel,_),_,_) -> List.mem rel static_rels) rules in
   let static_base = saturate [] static_rules in
   let state_rules =
-    (* 1a *)
-    if !aggregate_drop_negative then
-      List.map (function
-        | ("legal", _ as head), body, _ -> head, body, []
-        | ("does", _ as head), body, _ -> head, body, []
-        | rule -> rule) dynamic_rules
-    else dynamic_rules in    
+    (* 1, 1a *)
+    List.map (function
+      | ("legal", [player; _] as head), body, neg_body ->
+        head, ("role", [player])::body,
+        if !aggregate_drop_negative then [] else neg_body
+      | ("does", _ (* as head *)), body, _ -> assert false
+        (* head, body, [] *)
+      | rule -> rule) dynamic_rules in
   let rec loop actions_accu state_accu step state =
     (* {{{ log entry *)
     if !debug_level > 0 then (
@@ -1177,17 +1307,17 @@
     (let try actions, next =
        aggregate_ply players static_base state state_rules in
     (* {{{ log entry *)
-    if !debug_level > 0 then (
-      Printf.printf "aggregate_playout: state %s\n%!"
-        (String.concat " " (List.map term_str next))
-    );
+     if !debug_level > 0 then (
+       Printf.printf "aggregate_playout: state %s\n%!"
+         (String.concat " " (List.map term_str next))
+     );
     (* }}} *)
-    if step < horizon then
-      loop (actions::actions_accu) (state::state_accu) (step+1) next
-    else 
-      List.rev (actions::actions_accu),
-      List.rev (next::state::state_accu)
-     with Not_found ->
+     if step < horizon then
+       loop (actions::actions_accu) (state::state_accu) (step+1) next
+     else 
+       List.rev (actions::actions_accu),
+       List.rev (next::state::state_accu)
+     with Playout_over ->
        List.rev actions_accu, List.rev (state::state_accu)) in
   (* FIXME: this is identity, right? remove *)
   let init_base = saturate static_base state_rules in
@@ -1205,6 +1335,12 @@
 
 
 let find_cycle cands =
+  (* {{{ log entry *)
+  if !debug_level > -1 then (
+    Printf.printf "GDL.find_cycle: %s\n%!" (String.concat ", " (
+      List.map (function Some c -> term_str c | None -> "None") cands))
+  );
+  (* }}} *)
   let rec loop cycle trav pref rem path =
     if cycle = [] then
       let ini = [List.hd path] in
@@ -1270,12 +1406,15 @@
     ) masks in
   let mask, sb, m_sb = match mask_cands with
     | [mask, (sb, m_sb)] -> mask, sb, m_sb
-    | _ -> assert false in
+    | _ ->
+      Printf.printf "GDL.term_to_blank: bad state term %s\n%!"
+        (term_str next_arg);
+      assert false in
   mask, sb, m_sb, blank_out (next_arg, mask)
 
 let toss_var masks term =
   let mask, _, _, blank = term_to_blank masks term in
-  mask, Formula.fo_var_of_string (term_to_name blank)
+  mask, Formula.fo_var_of_string (String.lowercase (term_to_name blank))
 
 let translate_branches struc masks static_rnames dyn_rels
     (brs : exp_def_branch list) =
@@ -1356,7 +1495,8 @@
     Aux.concat_map (fun term ->
       let mask, sb, m_sb, blanked = term_to_blank masks term in
       Aux.map_some (function
-        | v, Var t -> Some ((mask, v), (t, term))
+        | v, Var t ->
+          Some ((mask, v), (t, term))
         | _ -> None) sb
     ) state_terms in
   let path_subterms = Aux.collect path_subterms in
@@ -1460,21 +1600,19 @@
   (* 7k *)
   let brs =
     List.map (fun (static_conjs, (next_arg,body,neg_body)) ->
-      let rhs_pos_preds, rhs_possneg_preds =
-        if next_arg = Const "_IGNORE_RHS_" then [], []
+      let rhs_pos_preds =
+        if next_arg = Const "_IGNORE_RHS_" then []
         else      
           let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
           let rhs_elem =
-            (* Formula.fo_var_of_string *) (term_to_name blanked) in
-          Aux.partition_map (fun (v,t as v_sb) ->
-            if t = Const "_BLANK_" then
-              let neg_rels = List.assoc (mask, v) dyn_rels in
-              Aux.Right (List.map (fun rel->rel, [|rhs_elem|]) neg_rels)
+            (* Formula.fo_var_of_string *)
+            (String.lowercase (term_to_name blanked)) in
+          Aux.map_some (fun (v,t as v_sb) ->
+            if t = Const "_BLANK_" then None
             else
               let rname = term_to_name (subst_one v_sb mask) in
-              Aux.Left (rname, [|rhs_elem|])
+              Some (rname, [|rhs_elem|])
           ) m_sb in
-      let rhs_possneg_preds = List.flatten rhs_possneg_preds in
       let dyn_conjs =
         Aux.concat_map (fun (rel, args) ->
           if rel = "true" then
@@ -1483,22 +1621,13 @@
             let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
             let _, svar = toss_var masks true_arg in
 
-            let lhs_pos_preds, lhs_possneg_preds =
-              Aux.partition_map (fun (v,t as v_sb) ->
-                if t = Const "_BLANK_" then
-                      (*
-                        let neg_rels = List.assoc (mask, v) dyn_rels in
-                        Aux.Right (List.map (fun rel->
-                        Formula.Rel (rel, [|svar|])) neg_rels)
-                      *) assert false
-                else
-                  let rname = term_to_name (subst_one v_sb mask) in
-                  Aux.Left (Formula.Rel (rname, [|svar|]))
-              ) m_sb in
-            (*
-              let lhs_possneg_preds = List.flatten lhs_possneg_preds in
-            *)
-            lhs_pos_preds
+            Aux.map_some (fun (v,t as v_sb) ->
+              if t = Const "_BLANK_" then
+                (* None *) assert false
+              else
+                let rname = term_to_name (subst_one v_sb mask) in
+                Some (Formula.Rel (rname, [|svar|]))
+            ) m_sb
           else if List.mem rel static_rnames || rel = "_DOES_PLACEHOLDER_"
           then []
           else (
@@ -1548,7 +1677,7 @@
             | [disj] -> Some disj
             | _ -> Some (Formula.Or disjs)) neg_body in
       let all_conjs = static_conjs @ dyn_conjs @ neg_conjs in
-      (rhs_pos_preds, rhs_possneg_preds, static_conjs, all_conjs),
+      (rhs_pos_preds, static_conjs, all_conjs),
       (next_arg, body, neg_body)) brs in
   uni_toss_vars, conjs_4b, brs
 
@@ -1585,14 +1714,20 @@
   (* }}} *)
   res    
 
-let translate_game game_descr =
+let translate_game player_term game_descr =
   freshen_count := 0;
   let player_terms =
     Array.of_list
       (Aux.map_some (function Role p -> Some p | _ -> None) game_descr) in
   let players_n = Array.length player_terms in
   let find_player player =
-    Aux.array_argfind (fun p->p=player) player_terms in
+    try
+      Aux.array_argfind (fun p->p=player) player_terms
+    with Not_found -> failwith
+      (Printf.sprintf
+         "GDL.initialize_game: player %s not found among %s"
+         (term_str player) (String.concat ", " (
+           Array.to_list (Array.map term_str player_terms)))) in
   let rules = Aux.concat_map rules_of_entry game_descr in
   let static_rules, dynamic_rules, static_base, init_state,
     (agg_actions, agg_states) =
@@ -1802,15 +1937,15 @@
     (mask, if List.mem sb sbs then sbs else sb::sbs)::elements
   ) [] element_terms in
   let struc = Structure.empty_structure () in
-  let struc, elements =
-    List.fold_left (fun (struc, elements) (mask, sbs) ->
+  let struc, elements, t_elements =
+    List.fold_left (fun (struc, elements, t_elements) (mask, sbs) ->
       (* {{{ log entry *)
       if !debug_level > 2 then (
         Printf.printf "mask-elements:";
       );
       (* }}} *)
-      let struc, m_elements =
-        List.fold_left (fun (struc, m_elements) sb ->
+      let struc, m_elements, t_elements =
+        List.fold_left (fun (struc, m_elements, t_elements) sb ->
           let e_term = subst sb mask in
           (* {{{ log entry *)
           if !debug_level > 2 then (
@@ -1819,15 +1954,16 @@
           (* }}} *)
           let struc, elem =
             Structure.add_new_elem struc ~name:(term_to_name e_term) () in
-          struc, (sb, elem)::m_elements
-        ) (struc, []) sbs in
+          struc, (sb, elem)::m_elements,
+          Aux.IntMap.add elem e_term t_elements
+        ) (struc, [], t_elements) sbs in
       (* {{{ log entry *)
       if !debug_level > 2 then (
         Printf.printf "\n%!";
       );      
       (* }}} *)
-      struc, (mask, m_elements)::elements
-    ) (struc, []) elements in
+      struc, (mask, m_elements)::elements, t_elements
+    ) (struc, [], Aux.IntMap.empty) elements in
   (* 4 *)
   (* currently, position paths are approximated by variables
      (non-variable positions are ignored) *)
@@ -1849,10 +1985,12 @@
     List.fold_left (fun struc (brel, arity, path_tups) ->
       let brel_tups = List.assoc brel static_base in
       (* {{{ log entry *)
+
       if !debug_level > 0 then (
         Printf.printf "Translating static relation %s with %d tuples:\n%s\n%!"
           brel (List.length brel_tups) (tuples_str brel_tups);
       );
+
       (* }}} *)
       List.fold_left (fun struc ptup ->
         let rname = brel ^ "__" ^ String.concat "__"
@@ -1910,10 +2048,12 @@
       Structure.add_rel_name rname 2 struc in
     let elems = List.assoc mask elements in
     (* {{{ log entry *)
+
     if !debug_level > 0 then (
       Printf.printf "Adding static EQ relation %s over %d elements.\n%!"
         rname (List.length elems);
     );
+
     (* }}} *)
     let elem_tups =
       List.fold_left (fun tups (sb1, e1) ->
@@ -1946,19 +2086,25 @@
       Structure.add_rel_name rname 1 struc in
     let elems = List.assoc mask elements in
     (* {{{ log entry *)
+
     if !debug_level > 0 then (
       Printf.printf "Adding mask anchor predicate %s over %d elements.\n%!"
         rname (List.length elems);
     );
+
     (* }}} *)
     let elem_tups =
       List.map (fun (sb, e) -> [|e|]) elems in
     Structure.unsafe_add_rels struc rname elem_tups
   ) struc masks in
+  let anchor_terms = ref [] in
   let struc = List.fold_left (fun struc (mask, elems) ->
     List.fold_left (fun struc (sb, elem) ->
       List.fold_left (fun struc (v,t as v_sb) ->
         let rname = term_to_name (subst_one v_sb mask) in
+        anchor_terms := Aux.update_assoc mask []
+          (Aux.update_assoc v [] (Aux.update_assoc t "" (fun _ ->rname)))
+          !anchor_terms;
         Structure.add_rel struc rname [|elem|]) struc sb) struc elems
   ) struc elements in
   
@@ -2304,6 +2450,7 @@
         rules_brs
       ) joint_legal_branches
     ) loc_joint_legal in
+  (* 7g: (7g1) and (7g2) TODO *)
   (* {{{ log entry *)
   if !debug_level > 1 then (
     Array.iteri (fun loc rules_brs ->
@@ -2340,7 +2487,6 @@
         let uni_vars, conjs_4b, brs =
           translate_branches struc masks static_rnames dyn_rels
             (brs @ synth_brs) in
-
         (* 7l *)
         let brs = Array.of_list brs in  (* indexing branches *)
         let full_set = Aux.ints_of_list
@@ -2407,6 +2553,7 @@
           Aux.array_existsi (fun ply states ->
             if ply mod loc_n = loc then (
               (* {{{ log entry *)
+
               if !debug_level > 4 then (
                 let posi =
                   Aux.map_some (function
@@ -2416,6 +2563,7 @@
                   "Checking branch at states:\n%s\npositives:\n%s\n"
                   (terms_str states) (terms_str posi)
               );
+
               (* }}} *)
               let res =
                 List.for_all (function
@@ -2433,51 +2581,70 @@
         let cases = Aux.map_try (fun c_brs ->
           let c_brs = List.map (Array.get brs) c_brs in
           List.fold_left (fun
-            (rhs_pos_acc, rhs_neg_acc, static_conjs_acc, conjs_acc)
-            ((rhs_pos, rhs_neg, static_conjs, conjs),
-             (_,body,_)) ->
+            (var_elems, struc_elems, rhs_pos_acc,
+             static_conjs_acc, conjs_acc)
+            ((rhs_pos, static_conjs, conjs),
+             (next_arg,body,_)) ->
               if not (check_branch body)
               then raise Not_found;
-              rhs_pos @ rhs_pos_acc, rhs_neg @ rhs_neg_acc,
-                static_conjs @ static_conjs_acc, conjs @ conjs_acc)
-            ([],[],conjs_4b,conjs_4b) c_brs
+              let nsvar =
+                if next_arg = Const "_IGNORE_RHS_"
+                then []
+                else [Formula.var_str (snd (toss_var masks next_arg)),
+                      next_arg] in
+              let var_elems =
+                List.fold_left (fun acc -> function
+                  | "true", [true_arg] ->
+                    let _, svar = toss_var masks true_arg in
+                    (Formula.var_str svar, true_arg)::acc
+                  | _ -> acc)
+                  (nsvar @ var_elems) body in
+              var_elems, List.map fst nsvar @ struc_elems,
+              rhs_pos @ rhs_pos_acc,
+              static_conjs @ static_conjs_acc, conjs @ conjs_acc)
+            ([],[],[],conjs_4b,conjs_4b) c_brs
         ) cases in
         (* 7m *)
-        let cases = Aux.map_some (fun (rhs_pos,rhs_neg,static_phis,phis) ->
-          if rhs_pos = [] && rhs_neg = [] then None
-          else Some (
-            Aux.unique_sorted rhs_pos, Aux.unique_sorted rhs_neg,
-            static_phis, phis)) cases in
-        let cases = Aux.map_some (fun (rhs_pos,rhs_neg,static_phis,phis) ->
-          let phi = Formula.And static_phis in
-          let rphi = Solver.M.register_formula phi in
-          (* {{{ log entry *)
-          if !debug_level > 4 then (
-            (* do not print, because it generates too many
-               answers -- too little constraints per number of
-               variables when considering a single branch *)
-            (*
-              let assgn = Solver.M.evaluate struc rphi in
-              let avars = List.map Formula.var_str
-              (FormulaOps.free_vars phi) in
-              let atups =
-              AssignmentSet.tuples struc.Structure.elements
-              avars assgn in *)
-            Printf.printf "evaluating: %s\n%!"
-              (Formula.str phi)
-          (* (List.length atups) *)
-          );
-          (* }}} *)
-          let res = Solver.M.check_formula struc rphi in
-          (* {{{ log entry *)
-          if !debug_level > 4 && res then (
-            Printf.printf "holds\n%!"
-          );
-          (* }}} *)
-          if res then Some (rhs_pos, rhs_neg, phis)
-          else None) cases in
-        List.map (fun (rhs_pos, rhs_neg, conjs) ->
-          lead, (rhs_pos, rhs_neg, lift_universal uni_vars conjs)) cases
+        let cases = Aux.map_some (
+          fun (var_elems,struc_elems,rhs_pos,static_phis,phis) ->
+            if rhs_pos = [] then None
+            else Some (
+              Aux.unique_sorted var_elems,
+              Aux.unique_sorted struc_elems,
+              Aux.unique_sorted rhs_pos,
+              static_phis, phis)) cases in
+        let cases = Aux.map_some (
+          fun (var_elems,struc_elems,rhs_pos,static_phis,phis) ->
+            let phi = Formula.And static_phis in
+            let rphi = Solver.M.register_formula phi in
+            (* {{{ log entry *)
+            if !debug_level > 4 then (
+              (* do not print, because it generates too many
+                 answers -- too little constraints per number of
+                 variables when considering a single branch *)
+              (*
+                let assgn = Solver.M.evaluate struc rphi in
+                let avars = List.map Formula.var_str
+                (FormulaOps.free_vars phi) in
+                let atups =
+                AssignmentSet.tuples struc.Structure.elements
+                avars assgn in *)
+              Printf.printf "evaluating: %s\n%!"
+                (Formula.str phi)
+            (* (List.length atups) *)
+            );
+            (* }}} *)
+            let res = Solver.M.check_formula struc rphi in
+            (* {{{ log entry *)
+            if !debug_level > 4 && res then (
+              Printf.printf "holds\n%!"
+            );
+            (* }}} *)
+            if res then Some (var_elems, struc_elems, rhs_pos, phis)
+            else None) cases in
+        List.map (fun (var_elems, struc_elems, rhs_pos, conjs) ->
+          lead, (var_elems, struc_elems, rhs_pos,
+                 lift_universal uni_vars conjs)) cases
       ) rules_brs
     ) loc_next_classes in
   (* 7n *)
@@ -2487,7 +2654,7 @@
       | _ -> assert false) terminal_rules in
   let terminal_uni_vars, terminal_4b, terminal_brs =
     translate_branches struc masks static_rnames dyn_rels terminal_brs in
-  let terminal_disjs = List.map (fun ((_,_,_,conjs),_) ->
+  let terminal_disjs = List.map (fun ((_,_,conjs),_) ->
     let disj_vars = FormulaOps.free_vars (Formula.And conjs) in
     let disj_4b =
       List.filter (fun a -> List.exists (fun v->List.mem v disj_vars)
@@ -2497,8 +2664,8 @@
                   (disj_4b @ conjs))) terminal_brs in
   let terminal_phi = Formula.Or terminal_disjs in
 
-  let fluents = Aux.strings_of_list
-    (Aux.concat_map (fun (_,drels) -> drels) dyn_rels) in
+  (* let fluents = Aux.strings_of_list
+     (Aux.concat_map (fun (_,drels) -> drels) dyn_rels) in *)
   (* {{{ log entry *)
   if !debug_level > 1 then (
     Printf.printf "GDL.translate_game: terminal condition -- %s\n%!"
@@ -2538,13 +2705,14 @@
           | _ -> assert false in
       let goal_uni_vars, goal_4b, brs =
         translate_branches struc masks static_rnames dyn_rels brs in
-      let goal_disjs = List.map (fun ((_,_,_,conjs),_) ->
+      let goal_disjs = List.map (fun ((_,_,conjs),_) ->
         let disj_vars = FormulaOps.free_vars (Formula.And conjs) in
         let disj_4b =
           List.filter (fun a -> List.exists (fun v->List.mem v disj_vars)
             (FormulaOps.free_vars a)) goal_4b in
-        lift_universal goal_uni_vars
-          (disj_4b @ conjs)) brs in
+        let disj = lift_universal goal_uni_vars (disj_4b @ conjs) in
+        Formula.Ex (FormulaOps.free_vars disj, disj)
+      ) brs in
       let guard = Formula.Or goal_disjs in
       Formula.Plus (sum, Formula.Times (
         Formula.Const score, Formula.Char guard))
@@ -2563,47 +2731,97 @@
   (* }}} *)
 
   (* {{{ log entry *)
+
   if !debug_level > 1 then (
     Array.iteri (fun loc rules_brs ->
       Printf.printf "Rule translations for loc %d:\n%!" loc;
-      List.iter (fun (lead, (rhs_pos,rhs_neg,precond)) ->
+      List.iter (fun (lead, (_,_,rhs_pos,precond)) ->
         Printf.printf
-          "Rule-translation: player %s move %s precond:\n%s\naction:\nADD %s... DEL %s\n%!"
+          "Rule-translation: player %s move %s precond:\n%s\naction:\nADD %s\n%!"
           (term_str loc_players.(loc)) (term_str lead)
           (Formula.sprint precond)
           (String.concat "; " (List.map proto_rel_str rhs_pos))
-          (String.concat "; " (List.map proto_rel_str rhs_neg))
       ) rules_brs;
     ) loc_toss_rules;
   );
+
   (* }}} *)
   let signature = Structure.rel_signature struc in
   let payoffs = Aux.array_from_assoc
     (List.map (fun (player, payoff) -> find_player player, payoff)
        payoffs) in
   let payoffs_pp =
-    Array.map (fun pay -> Solver.M.register_real_expr pay) payoffs in
+    Array.map (fun pay ->
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf "Registering payoff %s...\n%!" (Formula.real_str pay)
+      );
+      (* }}} *)
+      Solver.M.register_real_expr pay) payoffs in
+  let tossrule_data = ref Aux.StrMap.empty in
+  let fluents = Aux.concat_map snd dyn_rels in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "fluents: %s\n%!" (String.concat ", " fluents)
+  );
+  (* }}} *)
   let rules_and_locations =
     let rnames = ref Aux.Strings.empty in
     Array.mapi (fun loc rules_brs ->
       let labelled_rules =
-        List.map (fun (lead, (rhs_pos,rhs_neg,precond)) ->
+        List.map (fun (lead, (var_elems,struc_elems,rhs_pos,precond)) ->
           let precond =
             Formula.And [precond; Formula.Not terminal_phi] in
           let rname = Aux.not_conflicting_name !rnames
             ((term_to_name lead) ^ "_" ^ string_of_int loc) in
           rnames := Aux.Strings.add rname !rnames;
+          let fixvar_elemvars =
+            List.fold_left (fun acc (evar,elem) ->
+              let mask, sb, m_sb, blank = term_to_blank masks elem in
+              List.fold_left (fun acc (path,t) ->
+                match t with
+                  | Var v ->
+                    Aux.update_assoc v []
+                      (Aux.update_assoc mask []
+                         (Aux.update_assoc path [] (Aux.cons evar))) acc
+                  | _ -> acc
+              ) acc sb
+            ) [] var_elems in
+          tossrule_data :=
+            Aux.StrMap.add rname {
+              lead_legal = lead; precond = precond;
+              fixvar_elemvars = fixvar_elemvars;
+              rhs_add = rhs_pos; struc_elems = struc_elems;
+              elemvars = Aux.strmap_of_assoc var_elems}
+            !tossrule_data;
           let next_loc = (loc + 1) mod loc_n in
           let label = {
             Arena.rule = rname;
             time_in = 0.1, 0.1; parameters_in = []
           }, next_loc in
+          (* {{{ log entry *)
+          if !debug_level > 2 then (
+            Printf.printf "Translating rule %s into LHS/RHS structures...\n%!"
+              rname
+          );
+          (* }}} *)
           let discrete =
             DiscreteRule.translate_from_precond ~precond
-              ~add:rhs_pos ~del:rhs_neg in
+              ~add:rhs_pos ~embed:fluents ~struc_elems in
+          (* {{{ log entry *)
+          if !debug_level > 2 then (
+            Printf.printf "Making rule %s of:\n%s\n%!" rname
+              (DiscreteRule.sprint_rule discrete)
+          );
+          (* }}} *)
           let rule =
             ContinuousRule.make_rule signature [] discrete
               [] [] ~pre:discrete.DiscreteRule.pre () in
+          (* {{{ log entry *)
+          if !debug_level > 2 then (
+            Printf.printf "Rule %s done.\n%!" rname
+          );
+          (* }}} *)
           label, (rname, rule)
         ) rules_brs in
       let labels, rules = List.split labelled_rules in
@@ -2635,18 +2853,169 @@
     cur_loc = 0;
     data = [];
   } in
+  let playing_as = find_player player_term in
+  let noop_actions =
+    Array.mapi (fun loc noops->
+      match noops.(playing_as) with
+        | Some ([lead_term], _, _) -> Some lead_term
+        | Some ([_; lead_term], _, _) -> Some lead_term
+        | _ -> None
+    ) loc_noop_legal in
   (* {{{ log entry *)
   if !debug_level > 1 then (
     Printf.printf "\n\nGDL.translate_game:\n%s\n%!"
       (Arena.sprint_state result)
   );
   (* }}} *)
-  result
+  {anchor_terms = !anchor_terms;
+   tossrule_data = !tossrule_data;
+   t_elements = t_elements;
+   playing_as = playing_as;
+   noop_actions = noop_actions;
+   fluents = fluents;
+  }, result
 
+(* 
+    (9a) find the "lead legal" term to which the "does move" ground
+    term of the current player matches;
 
-let player_name_terms = ref [|Const "uninit"|]
+    (9b) earlier, remember which Toss variables of a rule contain which
+    fixed variables at which positions in their masks;
 
+    (9c) find anchor predicates corresponding to instantiations of the
+    "lead legal" variables, anchoring positions found by (9b) "fixed
+    var" - "mask + mask var" correspondence;
 
+    (9d) build a conjunction of anchor predicates over variables that
+    contain the fixed variable which is "instantiated" by the anchor
+    of the corresponding position, as established by (9c);
+
+    (9e) conjoin the (9d) with the "matching" formula of a rule, and
+    evaluate the result for all rules (of the located "lead legal"
+    class); only a single rule should have a match, and only a single
+    assignment should be returned; this rule with this assignment is
+    the translated move.
+ *)
+let translate_incoming_move gdl state actions =
+  let loc = state.Arena.cur_loc in
+  let actions = Array.of_list actions in
+  let location = state.Arena.game.Arena.graph.(loc) in
+  let player_action = actions.(location.Arena.player) in
+  (* 9a *)
+  let tossrules =
+    Aux.strmap_filter (fun  _ rdata ->
+      try ignore (match_meta [] [] [player_action] [rdata.lead_legal]); true
+      with Not_found -> false
+    ) gdl.tossrule_data in
+  let tossrules = Aux.collect
+    (List.map (fun (rname, rdata) ->
+      rdata.lead_legal,
+      (rname, rdata.precond, rdata.rhs_add, rdata.struc_elems,
+       rdata.fixvar_elemvars)) tossrules) in
+  let lead, tossrules =
+    match tossrules with
+      | [lead, tossrules] -> lead, tossrules
+      | _ -> assert false in
+  (* 9c *)
+  let fixed_inst, _ =
+    match_meta [] [] [player_action] [lead] in
+  let candidates = Aux.map_some (
+    fun (rname, precond, add, struc_elems, fixvar_elemvars) ->
+      (* 9d *)
+      let anchors = Aux.concat_map (fun (v,t) ->
+        let elemvars = List.assoc v fixvar_elemvars in
+        Aux.concat_map (fun (mask, pevs) ->
+          Aux.concat_map (fun (path, evs) -> 
+            let pred = List.assoc t
+              (List.assoc path (List.assoc mask gdl.anchor_terms)) in
+            List.map (fun ev->
+              Formula.Rel (pred, [|Formula.fo_var_of_string
+                                     (String.lowercase ev)|])) evs)
+            pevs) elemvars
+      ) fixed_inst in
+      let precond = Formula.And (anchors @ [precond]) in
+      let rule =
+        DiscreteRule.translate_from_precond ~precond ~add
+          ~embed:gdl.fluents ~struc_elems in
+      let rule =
+        DiscreteRule.compile_rule (Structure.rel_signature state.Arena.struc)
+          [] rule in
+      let asgns =
+        DiscreteRule.find_matchings state.Arena.struc rule in
+      (* faster *)
+      (* let emb =
+         DiscreteRule.choose_match state.Arena.struc rule asgns in *)
+      (* but we should check whether there's no ambiguity... *)
+      match
+        DiscreteRule.enumerate_matchings state.Arena.struc rule asgns
+      with
+        | [] -> None
+        | [emb] -> Some (rname, emb)
+        | _ -> failwith
+          ("GDL.translate_incoming_move: match ambiguity for rule "^rname)
+  ) tossrules in
+  match candidates with
+    | [rname, emb] -> rname, emb
+    | _ -> failwith
+      ("GDL.translate_incoming_move: ambiguity among rules "^
+          String.concat ", " (List.map fst candidates))
+
+
+(* 
+    (10a) associate the rule with its corresponding data: the "lead
+    legal" term, the fixed variables corresponding to rule elements,
+    ...
+
+    (10b) earlier, return/store the mapping from an element to the
+    mask and subsitution that define the element;
+
+    (10c) earlier, for each rule store a mapping from fixed variables
+    to rule variables and the mask variables that in the rule variable
+    are instantiated by the fixed variables;
+
+    (10d) to determine how to instantiate the fixed variables in the
+    "lead legal" term, find the (10b) substitutions of assigned
+    elements and (10c) mask variables for fixed variables; compose the
+    maps to get fixed variable to GDL ground term mapping, each
+    "route" should give the same term.
+ *)
+let translate_outgoing_move gdl state rname emb =
+  (* let loc = state.Arena.cur_loc in *)
+  (* let location = state.Arena.game.Arena.graph.(loc) in *)
+  let tossrule = Aux.StrMap.find rname gdl.tossrule_data in
+  let rule = List.assoc rname state.Arena.game.Arena.rules in
+  (* 10d *)
+  let emb = List.map (fun (v, e) ->
+    let vterm =
+      DiscreteRule.elemvar_of_elem
+        rule.ContinuousRule.compiled.DiscreteRule.lhs_elem_inv_names v in
+    Aux.StrMap.find vterm tossrule.elemvars,
+    Aux.IntMap.find e gdl.t_elements) emb in
+  let sb =
+    try
+      List.fold_left (fun sb (v_term, e_term) ->
+        fst (match_meta sb [] [e_term] [v_term])) [] emb
+    with Not_found -> failwith
+      ("GDL.translate_outgoing_move: inconsistent match for rule "
+       ^rname) in
+  term_str (subst sb tossrule.lead_legal)
+
+let our_turn gdl state =
+  let loc = state.Arena.cur_loc in
+  gdl.playing_as = state.Arena.game.Arena.graph.(loc).Arena.player
+
+let noop_move ?(force=false) gdl state =
+  let loc = state.Arena.cur_loc in
+  match gdl.noop_actions.(loc) with
+    | Some t -> term_str t
+    | None when force ->
+      term_str (Aux.array_map_some (fun x->x) gdl.noop_actions).(0)
+    | None -> failwith
+      ("GDL.noop_move: no NOOP move for active player at location "
+       ^string_of_int loc)
+
+
+
 let manual_translation = ref true
 let manual_game = ref "tictactoe"
 let top_exec_path = ref "." (* path to top Toss directory *)
@@ -2657,54 +3026,59 @@
 let pawn_whopping_descr = ref None
 
 
-let initialize_game_tictactoe state player game_descr startcl =
-  state := state_of_file (!top_exec_path ^ "/examples/Tic-Tac-Toe.toss");
-  playing_as := player;
+let initialize_game_tictactoe player game_descr startcl =
+  let state =
+    state_of_file (!top_exec_path ^ "/examples/Tic-Tac-Toe.toss") in
   game_description := game_descr;
-  player_name_terms := [|Const "XPLAYER"; Const "OPLAYER"|];
-  let effort, horizon, heur_adv_ratio =
+  let pterms = [|Const "XPLAYER"; Const "OPLAYER"|] in
+  let noops = [|Some (Const "NOOP"); Some (Const "NOOP")|] in
+  let (* effort, horizon, heur_adv_ratio *) params =
     6, 100, 4.0 in
-  effort, horizon, heur_adv_ratio
+  pterms, noops, state, Some params
 
-let initialize_game_gomoku state player game_descr startcl =
-  state := state_of_file (!top_exec_path ^ "/examples/Gomoku.toss");
-  playing_as := player;
+let initialize_game_gomoku player game_descr startcl =
+  let state =
+    state_of_file (!top_exec_path ^ "/examples/Gomoku.toss") in
   game_description := game_descr;
-  player_name_terms := [|Const "X"; Const "O"|];
+  let pterms = [|Const "X"; Const "O"|] in
+  let noops = [|Some (Const "NOOP"); Some (Const "NOOP")|] in
   Heuristic.use_monotonic := true;
-  let effort, horizon, heur_adv_ratio =
+  let (* effort, horizon, heur_adv_ratio *) params =
     4, 100, 4.0 in
-  effort, horizon, heur_adv_ratio
+  pterms, noops, state, Some params
 
-let initialize_game_connect4 state player game_descr startcl =
-  state := state_of_file (!top_exec_path ^ "/examples/Connect4.toss");
-  playing_as := player;
+let initialize_game_connect4 player game_descr startcl =
+  let state =
+    state_of_file (!top_exec_path ^ "/examples/Connect4.toss") in
   game_description := game_descr;
-  player_name_terms := [|Const "WHITE"; Const "RED"|];
+  let pterms = [|Const "WHITE"; Const "RED"|] in
+  let noops = [|Some (Const "NOOP"); Some (Const "NOOP")|] in
   Heuristic.use_monotonic := false;
-  let effort, horizon, heur_adv_ratio =
+  let (* effort, horizon, heur_adv_ratio *) params =
     10, 100, 4.0 in
-  effort, horizon, heur_adv_ratio
+  pterms, noops, state, Some params
 
-let initialize_game_breakthrough state player game_descr startcl =
-  state := state_of_file (!top_exec_path ^ "/examples/Breakthrough.toss");
-  playing_as := player;
+let initialize_game_breakthrough player game_descr startcl =
+  let state =
+    state_of_file (!top_exec_path ^ "/examples/Breakthrough.toss") in
   game_description := game_descr;
-  player_name_terms := [|Const "WHITE"; Const "BLACK"|];
-  let effort, horizon, heur_adv_ratio =
+  let pterms = [|Const "WHITE"; Const "BLACK"|] in
+  let noops = [|Some (Const "NOOP"); Some (Const "NOOP")|] in
+  let (* effort, horizon, heur_adv_ratio *) params =
     6, 100, 4.0 in
-  effort, horizon, heur_adv_ratio
+  pterms, noops, state, Some params
 
-let initialize_game_pawn_whopping state player game_d...
 
[truncated message content]