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

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

Revision: 1623
          http://toss.svn.sourceforge.net/toss/?rev=1623&view=rev
Author:   lukstafi
Date:     2011-11-07 21:57:12 +0000 (Mon, 07 Nov 2011)
Log Message:
-----------
GDL translation: inlining relations with <does> atoms; eliminating pattern matching (and ground arguments as special case); handling positive <does> literals in erasure clauses (coming from negative <does> literals in frame clauses); small bug fix in erasure clause filtering. Experimental parameter turning off root predicate generation (a prudent way would be to eliminate root predicates whenever possible in GameSimpl).

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/GameSimpl.ml
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateFormula.mli
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss
    trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
    trunk/Toss/GGP/tests/2player_normal_form_joint-raw.toss
    trunk/Toss/GGP/tests/2player_normal_form_joint-simpl.toss
    trunk/Toss/GGP/tests/asteroids-scrambled-raw.toss
    trunk/Toss/GGP/tests/asteroids-scrambled-simpl.toss
    trunk/Toss/GGP/tests/breakthrough-raw.toss
    trunk/Toss/GGP/tests/breakthrough-simpl.toss
    trunk/Toss/GGP/tests/connect4-raw.toss
    trunk/Toss/GGP/tests/connect4-simpl.toss
    trunk/Toss/GGP/tests/connect5-raw.toss
    trunk/Toss/GGP/tests/connect5-simpl.toss
    trunk/Toss/GGP/tests/pacman3p-raw.toss
    trunk/Toss/GGP/tests/pacman3p-simpl.toss
    trunk/Toss/GGP/tests/tictactoe-other-raw.toss
    trunk/Toss/GGP/tests/tictactoe-other-simpl.toss
    trunk/Toss/GGP/tests/tictactoe-raw.toss
    trunk/Toss/GGP/tests/tictactoe-simpl.toss
    trunk/Toss/www/reference/reference.tex

Added Paths:
-----------
    trunk/Toss/GGP/tests/pawn_whopping-raw.toss
    trunk/Toss/GGP/tests/pawn_whopping-simpl.toss

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/Formula/Aux.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -145,6 +145,8 @@
 
 let list_inter a b = List.filter (fun e -> List.mem e b) a
 
+let list_init f n = Array.to_list (Array.init n f)
+
 let sorted_inter xs ys =
   let rec aux acc = function
     | [], _ | _, [] -> acc
@@ -165,6 +167,16 @@
       else aux (y::acc) (xs, ys') in
   List.rev (aux [] (xs, ys))
 
+let sorted_multiset_union xs ys =
+  let rec aux acc = function
+    | [], xs | xs, [] -> List.rev_append xs acc
+    | ((x,i as xi)::xs' as xs), ((y,j as yj)::ys' as ys) ->
+      let c = Pervasives.compare x y in
+      if c = 0 then aux ((x,i+j)::acc) (xs', ys')
+      else if c < 0 then aux (xi::acc) (xs', ys)
+      else aux (yj::acc) (xs, ys') in
+  List.rev (aux [] (xs, ys))
+
 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
@@ -634,7 +646,13 @@
     snd (first_i 0 (fun i -> s^(string_of_int i))
       (fun v -> not (Strings.mem v names)))
 
-let not_conflicting_names s names n =
+let not_conflicting_names ?(truncate=false) s names n =
+  let s =
+    if truncate then
+      let i = ref (String.length s - 1) in
+      while !i > 0 && is_digit s.[!i] do decr i done;
+      String.sub s 0 (!i + 1)
+    else s in
   List.rev (snd (List.fold_left (fun (i,res) _ ->
     let i', v = 
       first_i i (fun i -> s^(string_of_int i))

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/Formula/Aux.mli	2011-11-07 21:57:12 UTC (rev 1623)
@@ -93,6 +93,9 @@
 (** Intersection: [list_inter a b = List.filter (fun e -> List.mem e b) a]. *)
 val list_inter : 'a list -> 'a list -> 'a list
 
+(** Create a list of given length initialized from the indices. *)
+val list_init : (int -> 'a) -> int -> 'a list
+
 (** Set intersection of lists of unique increasing elements (as returned
     by {!Aux.unique_sorted}). *)
 val sorted_inter : 'a list -> 'a list -> 'a list
@@ -101,6 +104,9 @@
     by {!Aux.unique_sorted}). *)
 val sorted_merge : 'a list -> 'a list -> 'a list
 
+val sorted_multiset_union :
+  ('a * int) list -> ('a * int) list -> ('a * int) list
+
 (** Return first key with the given value from the key-value pairs,
     using structural equality. *)
 val rev_assoc : ('a * 'b) list -> 'b -> 'a
@@ -308,6 +314,7 @@
 
 (** Returns [n] strings proloning [s] and not appearing in [names]. *)
 val not_conflicting_names :
+  ?truncate:bool ->
   string -> Strings.t -> 'a list -> string list
 
 (** Character classes. *)

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/GDL.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -96,6 +96,15 @@
 and terms_vars args =
   Array.fold_left Aux.Strings.union Aux.Strings.empty
     (Array.map term_vars args)
+
+let rec count_term_vars = function
+  | Const _ -> []
+  | Var v -> [v,1]
+  | Func (f, args) -> count_terms_vars args
+
+and count_terms_vars args =
+  Array.fold_left Aux.sorted_multiset_union []
+    (Array.map count_term_vars args)
   
 let rec atoms_of_body body =
   Aux.concat_map
@@ -141,17 +150,33 @@
     (List.map terms_vars
        (head_args::List.map snd (body @ neg_body)))
 
+let count_gdl_rule_vars ((_,head_args), body, neg_body) =
+  List.fold_left Aux.sorted_multiset_union []
+    (List.map count_terms_vars
+       (head_args::List.map snd (body @ neg_body)))
+
 let gdl_rules_vars brs =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map gdl_rule_vars brs)
 
+let count_gdl_rules_vars brs =
+  List.fold_left Aux.sorted_multiset_union []
+    (List.map count_gdl_rule_vars brs)
+
 let rels_vars (body : (string * term array) list) =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map (fun (_,args)->terms_vars args) body)
 
+let count_rels_vars (body : (string * term array) list) =
+  List.fold_left Aux.sorted_multiset_union []
+    (List.map (fun (_,args)->count_terms_vars args) body)
+
 let literals_vars body =
   rels_vars (List.map rel_of_atom (atoms_of_body body))
 
+let count_literals_vars body =
+  count_rels_vars (List.map rel_of_atom (atoms_of_body body))
+
 let gdl_defs_vars defs =
     rels_vars
       (Aux.concat_map (fun (hd,body,neg_body) ->
@@ -1026,85 +1051,168 @@
         | _ -> assert false) lits
   ) (flatten_disjs body)
 
-
-let find_ground_arg rel clauses =
+(* Find an argument which is not a variable in any branch of the [rel]
+   definition: i.e. find a wildcard-free pattern-matching argument. *)
+let find_pattern_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)
+            match args.(i) with Var _ -> false | _ -> true) all_args)
         args
 
-let elim_ground_arg_in_body rel arg grounding (head, body) =
+(* Modify all call-sites of a pattern-matching argument by expanding
+   them (introducing disjunction if possible, otherwise duplicating
+   clauses). [froots] are the root functors of the pattern paired
+   with their arity. *)
+let elim_pattern_arg_in_body rel arg froots (head, body) =
+  let var_count = Aux.sorted_multiset_union
+    (count_terms_vars (snd head)) (count_literals_vars body) in
 
-  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 expand_atom neg_disj args add_lits (sb, ((h_rel, h_args as h), body)) =
+    let args = Array.map (subst sb) args in
+    let single_br, sb_m_args =
+      match args.(arg) with
+        | Func (f, m_args) when List.mem_assoc f froots ->
+          true, [(f, Array.length m_args), [], m_args]
+        | Const f when List.mem_assoc f froots ->
+          true, [(f, 0), [], [| |]]
+        | Var v ->
+          not neg_disj &&
+            (try List.assoc v var_count with Not_found -> 0) < 2,
+          List.map (fun (func, arity as froot) ->
+            let nvars =
+              Aux.not_conflicting_names
+                ~truncate:true "pv" !used_vars
+                (Aux.list_init (fun x->x) arity) in
+            used_vars := Aux.add_strings nvars !used_vars;
+            let m_args = Aux.array_map_of_list (fun v -> Var v) nvars in
+            let t =
+              if arity = 0 then Const func else Func (func, m_args) in
+            froot, [v, t], m_args) froots
+        (* get rid of a clause that calls the relation with a term
+           not covered by pattern matching *)
+        | _ -> false, [] in
+    let make_br ((func, arity), v_sb, m_args) =
+      let exp_args = Array.init (Array.length args - 1 + arity)
+        (fun i ->
+          if i < arg then args.(i)
+          else if i >= arg + arity then args.(i+1-arity)
+          else m_args.(i-arg)) in
+      let r_gr = rel ^ "__" ^ func in
+      v_sb, Rel (r_gr, exp_args) in
+    let brs = List.map make_br sb_m_args in
+    if single_br then
+      let atoms = List.map snd brs in   (* sbs are empty or not relevant *)
+      (* [atoms] are already substituted, because [args] are *)
+      [sb, (h, add_lits atoms body)]
+    else List.map
+      (fun (v_sb, atom) ->
+        compose_sb v_sb sb,
+        ((h_rel, Array.map (subst v_sb) h_args),
+         add_lits [atom] (subst_literals v_sb body)))
+      brs in
 
-  let rec expand_literal emb_lit literal (sb, (head, body) as accu) =
+  let rec expand_literal is_disj emb_lits 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
+        expand_atom false args
+          (fun atoms body ->
+            match atoms with [atom] -> emb_lits [Pos atom] body
+              | _ -> emb_lits [Disj (List.map (fun a->Pos a) atoms)] 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)]
+        expand_atom is_disj args
+          (fun atoms body ->
+            emb_lits (List.map (fun a->Neg a) atoms) body)
+          accu
+      | Pos _ | Neg _ ->
+        [sb, (head, emb_lits [subst_literal sb literal] body)]
       | Disj disjs ->
-        let emb_lit lit body =
-          match body with
-            | Disj disjs::body -> Disj (lit::disjs)::body
+        let emb_lits lits body =
+          match body, lits with
+            | Disj disjs::body, [Disj lits] ->
+              Disj (lits @ disjs)::body
+            | Disj disjs::body, _ ->
+              Disj (lits @ 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
+        Aux.concat_foldr (expand_literal true emb_lits) 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
+    Aux.concat_foldr (expand_literal false (fun ls body-> ls @ body))
+      body init in
   List.map (fun (sb, cl) -> subst_clause sb cl) result
 
-let elim_ground_arg new_rels rel arg clauses =
+let elim_pattern_arg new_rels 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 froots = Aux.unique_sorted
+    (List.map (fun ((_,args),_) ->
+      match args.(arg) with
+        | Const c -> c, 0
+        | Func (f, m_args) -> f, Array.length m_args
+        | Var _ -> assert false) 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
+      let func, m_args, arity =
+      match args.(arg) with
+        | Const c -> c, [| |], 0
+        | Func (f, m_args) -> f, m_args, Array.length m_args
+        | Var _ -> assert false in
+      let exp_args = Array.init (Array.length args - 1 + arity)
+        (fun i ->
+          if i < arg then args.(i)
+          else if i >= arg + arity then args.(i+1-arity)
+          else m_args.(i-arg)) in
+      let rname = rel ^ "__" ^ func in
       new_rels := rname:: !new_rels;
-      (rname, short_args), body)
+      (rname, exp_args), body)
     rel_brs in
-  Aux.concat_map (elim_ground_arg_in_body rel arg grounding)
+  Aux.concat_map (elim_pattern_arg_in_body rel arg froots)
     (renamed_brs @ clauses)
 
-let elim_ground_args rels clauses =
+(* Find a relation with a non-wildcard pattern matching argument,
+   eliminate the pattern matching and modify the relation's call sites
+   accordingly. Repeat until no non-wildcard pattern matching
+   remains. *)
+let elim_pattern_args rels clauses =
   let new_rels = ref [] and all_rels = ref [] in
   let rec aux new_rels all_rels clauses = function
     | [] -> clauses
     | rel::rels ->
-      (let try arg = find_ground_arg rel clauses in
-       let clauses = elim_ground_arg new_rels rel arg clauses in
+      (* {{{ log entry *)
+      if !debug_level > 3 then (
+        Printf.printf "elim_pattern_args: trying %s\n%!" rel
+      );
+      (* }}} *)
+      (let try arg = find_pattern_arg rel clauses in
+       (* {{{ log entry *)
+       if !debug_level > 2 then (
+         Printf.printf "elim_pattern_args: found arg=%d\n%!" arg
+       );
+       (* }}} *)
+       let clauses = elim_pattern_arg new_rels rel arg clauses in
+       (* {{{ log entry *)
+       if !debug_level > 3 then (
+         Printf.printf
+           "elim_pattern_args: rel=%s arg=%d transformed:\n%s\n\n%!"
+           rel arg (clauses_str clauses)
+       );
+       (* }}} *)
        aux new_rels all_rels clauses rels
        with Not_found ->
          all_rels := rel:: !all_rels;
          aux new_rels all_rels clauses rels) in
   let rec fix clauses =
     all_rels := !new_rels @ !all_rels;
+    let more_rels = !new_rels in
     new_rels := [];
-    let clauses = aux new_rels all_rels clauses rels in
+    let clauses = aux new_rels all_rels clauses (rels @ more_rels) in
     if !new_rels <> []
     then fix clauses
     else
@@ -1115,6 +1223,7 @@
       all_rels, clauses in
   fix clauses
 
+
 let elim_ground_distinct clauses =
   let rec filter_disj = function
     | Pos (Distinct ts) when Aux.Strings.is_empty (terms_vars ts) ->

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/GDL.mli	2011-11-07 21:57:12 UTC (rev 1623)
@@ -153,10 +153,11 @@
 
 val func_graph : string -> term list -> term array list
 
-(** Eliminate arguments of relations that are constant in each
-    defining clause. Return the new clauses, and also the new
+(** Eliminate arguments of relations that are defined by non-wildcard
+    pattern matching (i.e. do not have a variable in any of the
+    defining clauses). Return the new clauses, and also the new
     relation set. *)
-val elim_ground_args :
+val elim_pattern_args :
   string list -> clause list -> string list * clause list
 
 val elim_ground_distinct : clause list -> clause list

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/GDLTest.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -290,7 +290,7 @@
         (GDL.def_str ("legal", legal_def));
     );
 
-  "eliminate ground args simple" >::
+  "eliminate ground args" >::
     (fun () ->
       let descr = parse_game_descr
         "
@@ -338,7 +338,7 @@
     (true (cell ?x ?e o)))
 " in
       let defined_rels, result =
-        elim_ground_args ["conn5"; "col"; "row"] descr in
+        elim_pattern_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)
@@ -391,6 +391,86 @@
     (true (cell ?x ?e o)))"
         res_s
     );
+
+
+  "eliminate pattern matching" >::
+    (fun () ->
+      let descr = parse_game_descr
+        "
+(<= (can_move x (move ?x ?y1 ?x ?y2))
+    (true (cell ?x ?y1 x))
+    (succ ?y1 ?y2)
+    (not (occupied ?x ?y2)))
+(<= (can_move o (move ?x ?y1 ?x ?y2))
+    (true (cell ?x ?y1 o))
+    (succ ?y2 ?y1)
+    (not (occupied ?x ?y2)))
+; First move can be a double.
+(<= (can_move x (move ?x 2 ?x 4))
+    (true (cell ?x 2 x))
+    (not (occupied ?x 3))
+    (not (occupied ?x 4)))
+(<= (can_move o (move ?x 7 ?x 5))
+    (true (cell ?x 7 o))
+    (not (occupied ?x 6))
+    (not (occupied ?x 5)))
+; Capture diagonally
+(<= (can_move x (capture ?x1 ?y1 ?x2 ?y2))
+    (true (cell ?x1 ?y1 x))
+    (true (cell ?x2 ?y2 o))
+    (succ ?y1 ?y2)
+    (or (succ ?x1 ?x2)
+        (succ ?x2 ?x1)))
+(<= (can_move o (capture ?x1 ?y1 ?x2 ?y2))
+    (true (cell ?x1 ?y1 o))
+    (true (cell ?x2 ?y2 x))
+    (succ ?y2 ?y1)
+    (or (succ ?x1 ?x2)
+        (succ ?x2 ?x1)))
+(<= (can_move_somewhere ?p)
+    (can_move ?p ?m))
+" in
+      let defined_rels, result =
+        elim_pattern_args ["can_move"; "can_move_somewhere"] descr in
+      let res_s =
+        (String.concat "\n" (List.map GDL.clause_str result)) in
+      assert_equal ~printer:(fun x->x)
+        "can_move__o__capture, can_move__o__move, can_move__x__capture, can_move__x__move, can_move_somewhere__o, can_move_somewhere__x"
+        (String.concat ", " defined_rels);
+      assert_equal ~printer:(fun x->x)
+        "(<= (can_move__x__move ?x ?y1 ?x ?y2)
+    (true (cell ?x ?y1 x))
+    (succ ?y1 ?y2)
+    (not (occupied ?x ?y2)))
+(<= (can_move__x__move ?x 2 ?x 4)
+    (true (cell ?x 2 x))
+    (not (occupied ?x 3))
+    (not (occupied ?x 4)))
+(<= (can_move__x__capture ?x1 ?y1 ?x2 ?y2)
+    (true (cell ?x1 ?y1 x))
+    (true (cell ?x2 ?y2 o))
+    (succ ?y1 ?y2)
+    (or (succ ?x1 ?x2) (succ ?x2 ?x1)))
+(<= (can_move__o__move ?x ?y1 ?x ?y2)
+    (true (cell ?x ?y1 o))
+    (succ ?y2 ?y1)
+    (not (occupied ?x ?y2)))
+(<= (can_move__o__move ?x 7 ?x 5)
+    (true (cell ?x 7 o))
+    (not (occupied ?x 6))
+    (not (occupied ?x 5)))
+(<= (can_move__o__capture ?x1 ?y1 ?x2 ?y2)
+    (true (cell ?x1 ?y1 o))
+    (true (cell ?x2 ?y2 x))
+    (succ ?y2 ?y1)
+    (or (succ ?x1 ?x2) (succ ?x2 ?x1)))
+(<= (can_move_somewhere__o )
+    (or (can_move__o__capture ?pv0 ?pv1 ?pv2 ?pv3) (can_move__o__move ?pv4 ?pv5 ?pv6 ?pv7)))
+(<= (can_move_somewhere__x )
+    (or (can_move__x__capture ?pv8 ?pv9 ?pv10 ?pv11) (can_move__x__move ?pv12 ?pv13 ?pv14 ?pv15)))"
+        res_s;
+    );
+
 ]
 
 let bigtests = "GDLBig" >::: [
@@ -423,9 +503,12 @@
 ]
 
 let a () =
-  GDL.debug_level := 5
+  GDL.debug_level := 5;
+  (try
+     ()
+   with e -> print_endline (Printexc.to_string e);
+     flush stdout; flush stderr;  raise e);
+  (* failwith "tested"; *)
+  ()
 
-let a () =
-  ()    
-
 let exec = Aux.run_test_if_target "GDLTest" tests

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -120,6 +120,9 @@
     TODO-FIXME: extend operations (specifically 2) to handle formulas
     nested in real expressions; with special treatment for update
     expressions in rules (using the compiled precondition as context).
+
+    TODO: Selectively distribute atomic conjuncts over disjunction when it
+    leads to new glueings (point (3)).
 *)
 
 open Formula

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -5,6 +5,12 @@
 
 let debug_level = ref 0
 
+(* Whether to add root predicates. Note that not adding root
+   predicates [no_root_predicates := true] will violate correctness
+   of some translations. *)
+let no_root_predicates = ref true
+
+
 type transl_data = {
   f_paths : path_set;                   (* fluent paths *)
   c_paths : path_set;                   (* coordinate paths *)
@@ -284,11 +290,14 @@
     let coord_and_fluent_preds =
       List.map (fun (subt, path) ->
         Formula.Rel (pred_on_path_subterm path subt, vartup)) s_subterms in
-    let root_preds = Aux.map_some
-      (fun root ->
-        if root = simult_subst data.all_paths blank sterm
-        then Some (Formula.Rel (term_to_name root, vartup))
-        else None) data.root_reps in
+    let root_preds =
+      if !no_root_predicates then []
+      else
+        Aux.map_some
+          (fun root ->
+            if root = simult_subst data.all_paths blank sterm
+            then Some (Formula.Rel (term_to_name root, vartup))
+            else None) data.root_reps in
     coord_and_fluent_preds @ root_preds in
   let rec aux = function
     | Pos (True sterm) -> transl_sterm sterm

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-11-07 21:57:12 UTC (rev 1623)
@@ -1,5 +1,10 @@
 val debug_level : int ref
 
+(** Whether to add root predicates. Note that not adding root
+    predicates [no_root_predicates := true] will violate correctness of
+    some translations. *)
+val no_root_predicates : bool ref
+
 type transl_data = {
   f_paths : GDL.path_set;             (** fluent paths *)
   c_paths : GDL.path_set;             (** coordinate paths *)

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -57,10 +57,6 @@
     less fluent paths.) *)
 let propose_leaf_f_paths = ref true
 
-(** Whether to eliminate an argument of a relation when it is ground
-    in all clauses defining the relation. *)
-let perform_ground_arg_elim = ref true
-
 (** two heuristics for selecting defined relations: select relations
     with arity smaller than three; or, select relations that have ground
     defining clauses (i.e. defining clauses with empty bodies). *)
@@ -975,6 +971,37 @@
     ("EQ_", Aux.Left (Array.make 2 c_pathl)) :: argpaths, clauses
 
 
+(* Expand the given relations in the given clauses: split the clauses
+   into those defining the relations, those using them and remaining
+   ones, expand the relations, and return the expanded clauses
+   together with the remaining clauses (discard the defining clauses). *)
+let expand_defs_in_clauses expand_rels clauses =
+  let defs = defs_of_rules (Aux.concat_map rules_of_clause clauses) in
+  let exp_defs = List.filter
+    (fun (rel,_) -> List.mem rel expand_rels) defs in
+  let cl_defs = List.filter
+    (fun (rel,brs) -> not (List.mem rel expand_rels) &&
+      List.exists (fun (_, pos, neg) ->
+        List.exists (fun (rel,_) ->
+          List.mem_assoc rel (pos @ neg)) exp_defs) brs) defs in
+  let operated =
+    Aux.map_prepend (List.map fst cl_defs) fst exp_defs in
+  let remaining = List.filter
+    (fun ((rel, _), _) -> not (List.mem rel operated)) clauses in
+  let expanded = List.map
+    (fun (rel,brs) -> rel, expand_definitions exp_defs brs)
+    cl_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
+  let br_to_clause rel (args, body, neg_body) =
+    (rel, args),
+    List.map (fun a->pos (atom_of_rel a)) body @
+      List.map (fun a->neg (atom_of_rel a)) neg_body in
+  let def_to_clauses (rel, brs) = List.map (br_to_clause rel) brs in
+  let exp_clauses = Aux.concat_map def_to_clauses expanded in
+  exp_clauses @ remaining
+
+
 let process_frame_clauses clauses frame_clauses =
   (* we need to expand frame clauses so that later local variables will get
      eliminated from erasure clauses *)
@@ -999,12 +1026,12 @@
     expand_definitions ["does", legal_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
-  let def_to_clause (args, body, neg_body) =
+  let br_to_clause (args, body, neg_body) =
     ("next", args),
     List.map (fun a->pos (atom_of_rel a)) body @
       List.map (fun a->neg (atom_of_rel a)) neg_body in
-  let frame_clauses = List.map def_to_clause exp_frame_defs in
-  let lexp_frame_clauses = List.map def_to_clause lexp_frame_defs in
+  let frame_clauses = List.map br_to_clause exp_frame_defs in
+  let lexp_frame_clauses = List.map br_to_clause lexp_frame_defs in
   lexp_frame_clauses, frame_clauses
 
 
@@ -1318,9 +1345,11 @@
       sb, legal_tup, n_cls) cl_tups in
   Aux.concat_map move_clauses legal_tuples
 
-
-let add_erasure_clauses f_paths (legal_tup, next_cls) =
-  let fixed_vars = terms_vars (Aux.array_map_of_list fst legal_tup) in
+(* We need to know players to pick the relevant legal term from
+   [legal_tup] when filtering-out "does" atoms. *)
+let add_erasure_clauses f_paths players_wo_env (legal_tup, next_cls) =
+  let legal_t_tup = Aux.array_map_of_list fst legal_tup in
+  let fixed_vars = terms_vars legal_t_tup in
   check_timeout "TranslateGame: add_erasure_clauses: start";
   let legal_cl_bodies = List.map snd legal_tup in
   let frame_cls, move_cl_bodies =
@@ -1409,6 +1438,25 @@
         nbodies
     ) frames in
 
+  (* Filter-out clauses which contain a non-matching positive "does"
+     atom, while removing the matching "does" atoms. *)
+  let erasure_cls = Aux.map_try
+    (fun (s, body) ->
+      let does_atoms, body = List.partition
+        (function Pos (Does _) -> true | _ -> false)
+        body in
+      let sb = List.fold_left (fun sb ->
+        function
+          | Pos (Does (player, t)) ->
+            let pnum = Aux.array_argfind
+              (fun p->p=player) players_wo_env in
+            unify sb [t] [legal_t_tup.(pnum)]
+          | _ -> assert false)
+        [] does_atoms in
+      if sb = [] then s, body
+      else subst sb s, subst_literals sb body)
+    (Aux.unique_sorted erasure_cls) in
+
   (* Recover fixed variables. *)
   let fixed_to_var = List.map
     (fun v -> v, Var v) (Aux.Strings.elements fixed_vars) in
@@ -1417,7 +1465,7 @@
      them for rule candidates. *)
   let erasure_cls = Aux.map_some
     (fun (s, body) ->
-      let local_ex_vars = term_vars s in
+      let local_ex_vars = Aux.Strings.diff (term_vars s) fixed_vars in
       let local_uni_vars = Aux.Strings.diff
         (literals_vars body) local_ex_vars in
       (* {{{ log entry *)
@@ -1455,7 +1503,7 @@
             subst_consts fixed_to_var s, kind,
             subst_consts_literals fixed_to_var body)
       else None)
-    (Aux.unique_sorted erasure_cls) in
+    erasure_cls in
 
   (* {{{ log entry *)
   if !debug_level > 2 then (
@@ -1966,7 +2014,7 @@
     Array.iteri print_tup (Array.of_list move_tups)
   );
   (* }}} *)
-  List.map (add_erasure_clauses f_paths) move_tups
+  List.map (add_erasure_clauses f_paths players_wo_env) move_tups
 
 
 (* Filter the "next" clauses removing conditions common with legal
@@ -2504,6 +2552,7 @@
   let add = Aux.unique_sorted (synch_postcond @ extract_tups pos_rhs) in
   (* let add = if counter_cls = [] then add else  *)
   let del = Aux.unique_sorted (unframed_tups @ extract_tups neg_rhs) in
+  let del = Aux.sorted_diff del add in
   let all_rhs = pos_rhs @ neg_rhs in
   let struc_elems = List.map
     (fun sterm -> term_to_name (blank_out transl_data sterm))
@@ -3091,6 +3140,17 @@
   let counters = List.map fst counter_inits in
   let goal_cls_w_counters, clauses =
     encode_goals_w_counters num_functors counters goal_cls_w_counters clauses in
+  let rec has_does = function
+    | Pos (Does _) | Neg (Does _) -> true
+    | Disj disj -> List.exists has_does disj
+    | _ -> false in
+  let rels_w_does_atoms =
+    (Aux.unique_sorted -| List.map (fst -| fst) -|
+        List.filter (List.exists has_does -| snd))
+      clauses in
+  let clauses = expand_defs_in_clauses
+    (Aux.list_diff rels_w_does_atoms ["next"; "frame next"; "legal"])
+    clauses in
   check_timeout "TranslateGame: basic clauses";
   let ground_at paths = List.map
     (fun p ->
@@ -3115,16 +3175,12 @@
     (fun rel -> List.exists (fun ((r,_),b) -> r=rel && b=[]) clauses)
     static_rels in
   let elim_static_rels, clauses =
-    if !perform_ground_arg_elim
-    then elim_ground_args elim_static_rels clauses
-    else elim_static_rels, clauses in
+    elim_pattern_args elim_static_rels clauses in
   let static_rels = elim_static_rels @ nonelim_static_rels in
   let nonstatic_rels =
-    Aux.list_diff nonstatic_rels ["goal"; "legal"; "next"] in
+    Aux.list_diff nonstatic_rels ["goal"; "legal"; "next"; "frame next"] in
   let nonstatic_rels, clauses =
-    if !perform_ground_arg_elim
-    then elim_ground_args nonstatic_rels clauses
-    else nonstatic_rels, clauses in
+    elim_pattern_args nonstatic_rels clauses in
   (* eliminate once again since more variables have been instantiated *)
   let clauses = elim_ground_distinct clauses in
   let nonstatic_rels = "goal"::(* "legal":: *)nonstatic_rels in

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-11-07 21:57:12 UTC (rev 1623)
@@ -344,6 +344,24 @@
         ~loc1_move:"thrust" ();
     );
 
+  "pawn_whopping" >::
+    (fun () ->
+      game_test_case ~game_name:"pawn_whopping" ~player:"x"
+        ~own_plnum:0 ~opponent_plnum:1
+        ~loc0_rule_name:"move_pv28_pv29_pv30_pv31_noop"
+        ~loc0_emb:[
+          "cell_pv28_pv29__BLANK_", "cell_2_2__BLANK_";
+          "cell_pv30_pv31__BLANK_", "cell_2_4__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
+        ~loc0_move:"(move 2 2 2 4)" ~loc0_noop:"noop" ~loc1:1
+        ~loc1_rule_name:"noop_move_pv12_pv13_pv14_pv15"
+        ~loc1_emb:[
+          "cell_pv12_pv13__BLANK_", "cell_7_7__BLANK_";
+          "cell_pv14_pv15__BLANK_", "cell_7_6__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
+        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 7 6)" ()
+    );
+  
 ]
 
 let set_debug_level i =
@@ -356,32 +374,22 @@
 
 
 let a () =
-  (* set_debug_level 4; *)
+  set_debug_level 4;
   (try
-     game_test_case ~game_name:"asteroids-scrambled" ~player:"ship"
-       ~own_plnum:0 ~opponent_plnum:0
-       ~loc0_rule_name:"turn_clock2"
-       ~loc0_emb:[
-         "value___BLANK__old0", "value___BLANK__i10";
-         "value___BLANK__old", "value___BLANK__i10";
-         "value___BLANK__new0", "value___BLANK__i13";
-         "value___BLANK__new", "value___BLANK__i12";
-         "value___BLANK__east", "value___BLANK__east";
-         "value___BLANK__north", "value___BLANK__north";
-         "gdl__counter", "gdl__counter";
-       ]
-       ~loc0_move:"(turn clock)"
-       ~loc1:0 ~loc1_rule_name:"thrust0"
-       ~loc1_emb:[
-         "gdl__counter", "gdl__counter";
-         "value___BLANK__new", "value___BLANK__i14";
-         "value___BLANK__new0", "value___BLANK__i16";
-         "value___BLANK__old", "value___BLANK__i12";
-         "value___BLANK__old0", "value___BLANK__i13";
-         "value___BLANK__s11", "value___BLANK__i2";
-         "value___BLANK__s12", "value___BLANK__i3";
-         "value___BLANK__s15", "value___BLANK__i2"]
-       ~loc1_move:"thrust" ();
+      game_test_case ~game_name:"pawn_whopping" ~player:"x"
+        ~own_plnum:0 ~opponent_plnum:1
+        ~loc0_rule_name:"move_pv28_pv29_pv30_pv31_noop"
+        ~loc0_emb:[
+          "cell_pv28_pv29__BLANK_", "cell_2_2__BLANK_";
+          "cell_pv30_pv31__BLANK_", "cell_2_4__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
+        ~loc0_move:"(move 2 2 2 4)" ~loc0_noop:"noop" ~loc1:1
+        ~loc1_rule_name:"noop_move_pv12_pv13_pv14_pv15"
+        ~loc1_emb:[
+          "cell_pv12_pv13__BLANK_", "cell_7_7__BLANK_";
+          "cell_pv14_pv15__BLANK_", "cell_7_6__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
+        ~loc1_noop:"noop" ~loc1_move:"(move 7 7 7 6)" ();
    with e -> print_endline (Printexc.to_string e);
      flush stdout; flush stderr;  raise e);
   (* failwith "tested"; *)
@@ -421,16 +429,16 @@
   TranslateGame.generate_test_case := None
 
 let a () =
-  (* regenerate ~debug:false ~game_name:"tictactoe" ~player:"xplayer"; *)
-  (* regenerate ~debug:false ~game_name:"tictactoe-other" ~player:"xPLAYER"; *)
-  (* regenerate ~debug:false ~game_name:"connect5" ~player:"x"; *)
-  (* regenerate ~debug:false ~game_name:"breakthrough" ~player:"white"; *)
-  (* regenerate ~debug:false ~game_name:"pawn_whopping" ~player:"x"; *)
-  (* regenerate ~debug:false ~game_name:"connect4" ~player:"white"; *)
-  (* regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row"; *)
-  (* regenerate ~debug:false ~game_name:"2player_normal_form_joint" ~player:"row"; *)
-  (* regenerate ~debug:false ~game_name:"pacman3p" ~player:"pacman"; *)
-  (* regenerate ~debug:false ~game_name:"asteroids-scrambled" ~player:"ship"; *)
+  regenerate ~debug:false ~game_name:"tictactoe" ~player:"xplayer";
+  regenerate ~debug:false ~game_name:"tictactoe-other" ~player:"xPLAYER";
+  regenerate ~debug:false ~game_name:"connect5" ~player:"x";
+  regenerate ~debug:false ~game_name:"breakthrough" ~player:"white";
+  regenerate ~debug:false ~game_name:"pawn_whopping" ~player:"x";
+  regenerate ~debug:false ~game_name:"connect4" ~player:"white";
+  regenerate ~debug:false ~game_name:"2player_normal_form_2010" ~player:"row";
+  regenerate ~debug:false ~game_name:"2player_normal_form_joint" ~player:"row";
+  regenerate ~debug:false ~game_name:"pacman3p" ~player:"pacman";
+  regenerate ~debug:false ~game_name:"asteroids-scrambled" ~player:"ship";
   (* failwith "generated"; *)
   ()
 

Modified: trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/tests/2player_normal_form_2010-raw.toss	2011-11-07 21:57:12 UTC (rev 1623)
@@ -1,20 +1,13 @@
 REL terminal() =
- ex did__BLANK__m11
-  (true and
-   did_0column(did__BLANK__m11) and did__BLANK___BLANK_(did__BLANK__m11)) or
-  ex did__BLANK__m11
-   (true and
-    did_0row(did__BLANK__m11) and did__BLANK___BLANK_(did__BLANK__m11))
+ ex did__BLANK__m11 (true and did_0column(did__BLANK__m11)) or
+  ex did__BLANK__m11 (true and did_0row(did__BLANK__m11))
 PLAYERS environment, row, column
 RULE m:
  MATCH
   not terminal() and not row__SYNC(synch_control_) and
    synch_control_(synch_control_) and
    ex val__r0, val__r, did__BLANK__m0
-    (reward(did__BLANK__m, did__BLANK__m0, val__r, val__r0) and
-     val___BLANK_(val__r0) and val___BLANK_(val__r) and
-      did__BLANK___BLANK_(did__BLANK__m0) and
-      did__BLANK___BLANK_(did__BLANK__m))
+    (reward(did__BLANK__m, did__BLANK__m0, val__r, val__r0) and true)
   ADD
    RELS did_0row(did__BLANK__m), row__SYNC(synch_control_),
     synch_control_(synch_control_)
@@ -23,10 +16,7 @@
   not terminal() and not column__SYNC(synch_control_) and
    synch_control_(synch_control_) and
    ex val__r2, val__r1, did__BLANK__m1
-    (reward(did__BLANK__m1, did__BLANK__m2, val__r1, val__r2) and
-     val___BLANK_(val__r2) and val___BLANK_(val__r1) and
-      did__BLANK___BLANK_(did__BLANK__m1) and
-      did__BLANK___BLANK_(did__BLANK__m2))
+    (reward(did__BLANK__m1, did__BLANK__m2, val__r1, val__r2) and true)
   ADD
    RELS column__SYNC(synch_control_), did_0column(did__BLANK__m2),
     synch_control_(synch_control_)
@@ -43,80 +33,64 @@
     :(
      ex val__r6, val__10, did__BLANK__m7, did__BLANK__m8
       (reward(did__BLANK__m7, did__BLANK__m8, val__10, val__r6) and
-       val___BLANK_(val__r6) and val__010(val__10) and
-        val___BLANK_(val__10) and did_0row(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m7) and
-        did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+       val__010(val__10) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
      )
     +
     100. *
      :(
       ex val__r6, val__100, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__100, val__r6) and
-        val___BLANK_(val__r6) and val__0100(val__100) and
-         val___BLANK_(val__100) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__0100(val__100) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     20. *
      :(
       ex val__r6, val__20, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__20, val__r6) and
-        val___BLANK_(val__r6) and val__020(val__20) and
-         val___BLANK_(val__20) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__020(val__20) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     30. *
      :(
       ex val__r6, val__30, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__30, val__r6) and
-        val___BLANK_(val__r6) and val__030(val__30) and
-         val___BLANK_(val__30) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__030(val__30) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     40. *
      :(
       ex val__r6, val__40, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__40, val__r6) and
-        val___BLANK_(val__r6) and val__040(val__40) and
-         val___BLANK_(val__40) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__040(val__40) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     50. *
      :(
       ex val__r6, val__50, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__50, val__r6) and
-        val___BLANK_(val__r6) and val__050(val__50) and
-         val___BLANK_(val__50) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__050(val__50) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     80. *
      :(
       ex val__r6, val__80, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__80, val__r6) and
-        val___BLANK_(val__r6) and val__080(val__80) and
-         val___BLANK_(val__80) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__080(val__80) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     90. *
      :(
       ex val__r6, val__90, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__90, val__r6) and
-        val___BLANK_(val__r6) and val__090(val__90) and
-         val___BLANK_(val__90) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__090(val__90) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
   MOVES [m -> 0] }
   PLAYER column {
@@ -125,87 +99,64 @@
     :(
      ex val__10, val__r7, did__BLANK__m9, did__BLANK__m10
       (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__10) and
-       val__010(val__10) and val___BLANK_(val__10) and
-        val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-        did__BLANK___BLANK_(did__BLANK__m9) and
-        did_0column(did__BLANK__m10) and did__BLANK___BLANK_(did__BLANK__m10))
+       val__010(val__10) and did_0row(did__BLANK__m9) and
+        did_0column(did__BLANK__m10))
      )
     +
     100. *
      :(
       ex val__100, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__100) and
-        val__0100(val__100) and val___BLANK_(val__100) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__0100(val__100) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     20. *
      :(
       ex val__20, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__20) and
-        val__020(val__20) and val___BLANK_(val__20) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__020(val__20) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     30. *
      :(
       ex val__30, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__30) and
-        val__030(val__30) and val___BLANK_(val__30) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__030(val__30) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     40. *
      :(
       ex val__40, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__40) and
-        val__040(val__40) and val___BLANK_(val__40) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__040(val__40) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     50. *
      :(
       ex val__50, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__50) and
-        val__050(val__50) and val___BLANK_(val__50) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__050(val__50) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     80. *
      :(
       ex val__80, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__80) and
-        val__080(val__80) and val___BLANK_(val__80) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__080(val__80) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
     +
     90. *
      :(
       ex val__90, val__r7, did__BLANK__m9, did__BLANK__m10
        (reward(did__BLANK__m9, did__BLANK__m10, val__r7, val__90) and
-        val__090(val__90) and val___BLANK_(val__90) and
-         val___BLANK_(val__r7) and did_0row(did__BLANK__m9) and
-         did__BLANK___BLANK_(did__BLANK__m9) and
-         did_0column(did__BLANK__m10) and
-         did__BLANK___BLANK_(did__BLANK__m10))
+        val__090(val__90) and did_0row(did__BLANK__m9) and
+         did_0column(did__BLANK__m10))
       )
   MOVES [m2 -> 0] }
 }

Modified: trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/tests/2player_normal_form_2010-simpl.toss	2011-11-07 21:57:12 UTC (rev 1623)
@@ -1,18 +1,13 @@
 REL terminal() =
- ex did__BLANK__m11
-  (did__BLANK___BLANK_(did__BLANK__m11) and did_0column(did__BLANK__m11)) or
-  ex did__BLANK__m11
-   (did__BLANK___BLANK_(did__BLANK__m11) and did_0row(did__BLANK__m11))
+ ex did__BLANK__m11 did_0column(did__BLANK__m11) or
+  ex did__BLANK__m11 did_0row(did__BLANK__m11)
 PLAYERS environment, row, column
 RULE m:
  MATCH
   synch_control_(synch_control_) and not terminal() and
    not row__SYNC(synch_control_) and
-   ex val__r0, val__r, did__BLANK__m0
-    (did__BLANK___BLANK_(did__BLANK__m) and
-     did__BLANK___BLANK_(did__BLANK__m0) and val___BLANK_(val__r) and
-     val___BLANK_(val__r0) and reward(did__BLANK__m, did__BLANK__m0, val__r,
-     val__r0))
+   ex val__r0, val__r, did__BLANK__m0 reward(did__BLANK__m, did__BLANK__m0,
+    val__r, val__r0)
   ADD
    RELS did_0row(did__BLANK__m), row__SYNC(synch_control_),
     synch_control_(synch_control_)
@@ -20,11 +15,8 @@
  MATCH
   synch_control_(synch_control_) and not terminal() and
    not column__SYNC(synch_control_) and
-   ex val__r2, val__r1, did__BLANK__m1
-    (did__BLANK___BLANK_(did__BLANK__m1) and
-     did__BLANK___BLANK_(did__BLANK__m2) and val___BLANK_(val__r1) and
-     val___BLANK_(val__r2) and reward(did__BLANK__m1, did__BLANK__m2,
-     val__r1, val__r2))
+   ex val__r2, val__r1, did__BLANK__m1 reward(did__BLANK__m1, did__BLANK__m2,
+    val__r1, val__r2)
   ADD
    RELS column__SYNC(synch_control_), did_0column(did__BLANK__m2),
     synch_control_(synch_control_)
@@ -40,19 +32,14 @@
    10. *
     :(
      ex val__r6, val__10, did__BLANK__m7, did__BLANK__m8
-      (did__BLANK___BLANK_(did__BLANK__m7) and
-       did__BLANK___BLANK_(did__BLANK__m8) and val__010(val__10) and
-       val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-       val__10, val__r6) and did_0row(did__BLANK__m7) and
-       did_0column(did__BLANK__m8))
+      (val__010(val__10) and reward(did__BLANK__m7, did__BLANK__m8, val__10,
+       val__r6) and did_0row(did__BLANK__m7) and did_0column(did__BLANK__m8))
      )
     +
     100. *
      :(
       ex val__r6, val__100, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__0100(val__100) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
+       (val__0100(val__100) and reward(did__BLANK__m7, did__BLANK__m8,
         val__100, val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
@@ -60,60 +47,48 @@
     20. *
      :(
       ex val__r6, val__20, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__020(val__20) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__20, val__r6) and did_0row(did__BLANK__m7) and
+       (val__020(val__20) and reward(did__BLANK__m7, did__BLANK__m8, val__20,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
     +
     30. *
      :(
       ex val__r6, val__30, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__030(val__30) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__30, val__r6) and did_0row(did__BLANK__m7) and
+       (val__030(val__30) and reward(did__BLANK__m7, did__BLANK__m8, val__30,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
     +
     40. *
      :(
       ex val__r6, val__40, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__040(val__40) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__40, val__r6) and did_0row(did__BLANK__m7) and
+       (val__040(val__40) and reward(did__BLANK__m7, did__BLANK__m8, val__40,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
     +
     50. *
      :(
       ex val__r6, val__50, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__050(val__50) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__50, val__r6) and did_0row(did__BLANK__m7) and
+       (val__050(val__50) and reward(did__BLANK__m7, did__BLANK__m8, val__50,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
     +
     80. *
      :(
       ex val__r6, val__80, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__080(val__80) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__80, val__r6) and did_0row(did__BLANK__m7) and
+       (val__080(val__80) and reward(did__BLANK__m7, did__BLANK__m8, val__80,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
     +
     90. *
      :(
       ex val__r6, val__90, did__BLANK__m7, did__BLANK__m8
-       (did__BLANK___BLANK_(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m8) and val__090(val__90) and
-        val___BLANK_(val__r6) and reward(did__BLANK__m7, did__BLANK__m8,
-        val__90, val__r6) and did_0row(did__BLANK__m7) and
+       (val__090(val__90) and reward(did__BLANK__m7, did__BLANK__m8, val__90,
+        val__r6) and did_0row(did__BLANK__m7) and
         did_0column(did__BLANK__m8))
       )
   MOVES [m -> 0] }
@@ -122,19 +97,15 @@
    10. *
     :(
      ex val__10, val__r7, did__BLANK__m9, did__BLANK__m10
-      (did__BLANK___BLANK_(did__BLANK__m10) and
-       did__BLANK___BLANK_(did__BLANK__m9) and val__010(val__10) and
-       val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
-       val__r7, val__10) and did_0column(did__BLANK__m10) and
+      (val__010(val__10) and reward(did__BLANK__m9, did__BLANK__m10, val__r7,
+       val__10) and did_0column(did__BLANK__m10) and
        did_0row(did__BLANK__m9))
      )
     +
     100. *
      :(
       ex val__100, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__0100(val__100) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__0100(val__100) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__100) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -142,9 +113,7 @@
     20. *
      :(
       ex val__20, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__020(val__20) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__020(val__20) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__20) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -152,9 +121,7 @@
     30. *
      :(
       ex val__30, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__030(val__30) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__030(val__30) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__30) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -162,9 +129,7 @@
     40. *
      :(
       ex val__40, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__040(val__40) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__040(val__40) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__40) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -172,9 +137,7 @@
     50. *
      :(
       ex val__50, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__050(val__50) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__050(val__50) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__50) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -182,9 +145,7 @@
     80. *
      :(
       ex val__80, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__080(val__80) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__080(val__80) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__80) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )
@@ -192,9 +153,7 @@
     90. *
      :(
       ex val__90, val__r7, did__BLANK__m9, did__BLANK__m10
-       (did__BLANK___BLANK_(did__BLANK__m10) and
-        did__BLANK___BLANK_(did__BLANK__m9) and val__090(val__90) and
-        val___BLANK_(val__r7) and reward(did__BLANK__m9, did__BLANK__m10,
+       (val__090(val__90) and reward(did__BLANK__m9, did__BLANK__m10,
         val__r7, val__90) and did_0column(did__BLANK__m10) and
         did_0row(did__BLANK__m9))
       )

Modified: trunk/Toss/GGP/tests/2player_normal_form_joint-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/2player_normal_form_joint-raw.toss	2011-11-06 22:11:48 UTC (rev 1622)
+++ trunk/Toss/GGP/tests/2player_normal_form_joint-raw.toss	2011-11-07 21:57:12 UTC (rev 1623)
@@ -1,18 +1,13 @@
 REL terminal() =
  ex did__BLANK__m11, did__BLANK__m12
-  (true and
-   did_0row(did__BLANK__m11) and did__BLANK___BLANK_(did__BLANK__m11) and
-    did_0column(did__BLANK__m12) and did__BLANK___BLANK_(did__BLANK__m12))
+  (true and did_0row(did__BLANK__m11) and did_0column(did__BLANK__m12))
 PLAYERS environment, row, column
 RULE m:
  MATCH
   not terminal() and not row__SYNC(synch_control_) and
    synch_control_(synch_control_) and
    ex val__r0, val__r, did__BLANK__m0
-    (reward(did__BLANK__m, did__BLANK__m0, val__r, val__r0) and
-     val___BLANK_(val__r0) and val___BLANK_(val__r) and
-      did__BLANK___BLANK_(did__BLANK__m0) and
-      did__BLANK___BLANK_(did__BLANK__m))
+    (reward(did__BLANK__m, did__BLANK__m0, val__r, val__r0) and true)
   ADD
    RELS did_0row(did__BLANK__m), row__SYNC(synch_control_),
     synch_control_(synch_control_)
@@ -21,10 +16,7 @@
   not terminal() and not column__SYNC(synch_control_) and
    synch_control_(synch_control_) and
    ex val__r2, val__r1, did__BLANK__m1
-    (reward(did__BLANK__m1, did__BLANK__m2, val__r1, val__r2) and
-     val___BLANK_(val__r2) and val___BLANK_(val__r1) and
-      did__BLANK___BLANK_(did__BLANK__m1) and
-      did__BLANK___BLANK_(did__BLANK__m2))
+    (reward(did__BLANK__m1, did__BLANK__m2, val__r1, val__r2) and true)
   ADD
    RELS column__SYNC(synch_control_), did_0column(did__BLANK__m2),
     synch_control_(synch_control_)
@@ -41,80 +33,64 @@
     :(
      ex val__r6, val__10, did__BLANK__m7, did__BLANK__m8
       (reward(did__BLANK__m7, did__BLANK__m8, val__10, val__r6) and
-       val___BLANK_(val__r6) and val__010(val__10) and
-        val___BLANK_(val__10) and did_0row(did__BLANK__m7) and
-        did__BLANK___BLANK_(did__BLANK__m7) and
-        did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+       val__010(val__10) and did_0row(did__BLANK__m7) and
+        did_0column(did__BLANK__m8))
      )
     +
     100. *
      :(
       ex val__r6, val__100, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__100, val__r6) and
-        val___BLANK_(val__r6) and val__0100(val__100) and
-         val___BLANK_(val__100) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__0100(val__100) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     20. *
      :(
       ex val__r6, val__20, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__20, val__r6) and
-        val___BLANK_(val__r6) and val__020(val__20) and
-         val___BLANK_(val__20) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__020(val__20) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     30. *
      :(
       ex val__r6, val__30, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__30, val__r6) and
-        val___BLANK_(val__r6) and val__030(val__30) and
-         val___BLANK_(val__30) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__030(val__30) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     40. *
      :(
       ex val__r6, val__40, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__40, val__r6) and
-        val___BLANK_(val__r6) and val__040(val__40) and
-         val___BLANK_(val__40) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__040(val__40) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     50. *
      :(
       ex val__r6, val__50, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__50, val__r6) and
-        val___BLANK_(val__r6) and val__050(val__50) and
-         val___BLANK_(val__50) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__050(val__50) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     80. *
      :(
       ex val__r6, val__80, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLANK__m7, did__BLANK__m8, val__80, val__r6) and
-        val___BLANK_(val__r6) and val__080(val__80) and
-         val___BLANK_(val__80) and did_0row(did__BLANK__m7) and
-         did__BLANK___BLANK_(did__BLANK__m7) and
-         did_0column(did__BLANK__m8) and did__BLANK___BLANK_(did__BLANK__m8))
+        val__080(val__80) and did_0row(did__BLANK__m7) and
+         did_0column(did__BLANK__m8))
       )
     +
     90. *
      :(
       ex val__r6, val__90, did__BLANK__m7, did__BLANK__m8
        (reward(did__BLAN...
 
[truncated message content]