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

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

Revision: 1544
          http://toss.svn.sourceforge.net/toss/?rev=1544&view=rev
Author:   lukstafi
Date:     2011-08-26 14:33:35 +0000 (Fri, 26 Aug 2011)
Log Message:
-----------
GDL translation: (fix) expand frame clasues for generating erasure clauses; (optimization) filter unrequired (mostly erasure) rule clauses before splitting rule candidates; various bug fixes (e.g. sign of Distinct atoms); specification-level fix for handling <negative true> literals during formula translation; related, adding blanked out <true> atoms of RHS terms to rewrite rule conditions just prior to translation. GameSimpl: minor bug fix; removing unused defined relations.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateFormula.mli
    trunk/Toss/GGP/TranslateFormulaTest.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/GGP/tests/breakthrough-raw.toss
    trunk/Toss/GGP/tests/breakthrough-simpl.toss
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/Formula/Aux.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -458,6 +458,17 @@
   done;
   !r
 
+let list_find_all_max cmp l =
+  match l with
+    | [] -> []
+    | a::l -> List.fold_left
+      (fun all_max cand ->
+        let res = cmp cand (List.hd all_max) in
+        if res > 0 then [cand]
+        else if res = 0 then cand::all_max
+        else all_max)
+      [a] l
+
 let array_find_all_max cmp a =
   let n = Array.length a in
   if n=0 then []

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/Formula/Aux.mli	2011-08-26 14:33:35 UTC (rev 1544)
@@ -249,6 +249,8 @@
     arrays are of different lengths. *)
 val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
 
+(** Find all maximal elements in a list. *)
+val list_find_all_max : ('a -> 'a -> int) -> 'a list -> 'a list
 (** Find all maximal elements in an array. *)
 val array_find_all_max : ('a -> 'a -> int) -> 'a array -> 'a list
 (** Find indices of all maximal elements in an array. *)

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -1052,6 +1052,9 @@
 let as_conjuncts phi =
   let rec conjuncts = function
     | And fl -> Aux.concat_map conjuncts fl
+    | Not (And [f]) -> conjuncts (Not f)
+    | Not (Or fl) ->
+      Aux.concat_map conjuncts (List.map (fun f->Not f) fl)
     | All (vs, f) -> List.map (fun f -> All (vs, f)) (conjuncts f)
     | Ex (vs, phi) ->
       (match conjuncts phi with

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-08-26 14:33:35 UTC (rev 1544)
@@ -43,7 +43,7 @@
   map_Sum : fo_var list -> formula -> real_expr -> real_expr
 }
 
-(** Identity map to be refined using the [with] clause. *)
+(** Identity map to be refined using the [with] syntax. *)
 val identity_map : formula_and_expr_map
 
 (** Map through the structure adjusting subformulas/subexpressions. *)

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/GDL.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -95,6 +95,8 @@
   | True arg -> "true", [|arg|]
   | Does (arg1, arg2) -> "does", [|arg1; arg2|]
 
+(** Remember that [rel_of_atom] inverts polarity of "distinct" --
+    invert back after using [atom_of_rel] if needed. *)
 let atom_of_rel = function
   | "distinct", args -> Distinct args
      (* not a proper relation -- avoid *)
@@ -106,7 +108,7 @@
 let rec bodies_of_literal = function
   | Pos (Distinct args) ->
     [Aux.Right ("distinct", args)] (* not negated actually! *)
-  | Neg (Distinct _) -> assert false
+  | Neg (Distinct args) -> [Aux.Left ("distinct",args)]
   | Pos atom -> [Aux.Left (rel_of_atom atom)]
   | Neg atom -> [Aux.Right (rel_of_atom atom)]
   | Disj disjs ->
@@ -201,8 +203,36 @@
                 not (List.mem_assoc rel1 rules))
               body) branches) stratum in
         stratify (stratum::strata) (more_rules @ rules)
-      
 
+(* Topological-like sort w.r.t. the call-graph. *)
+let topsort_callgraph clauses for_rels =
+  let defs = defs_of_rules (Aux.concat_map rules_of_clause clauses) in
+  (* building incidence list *)
+  let defs = List.map
+    (fun (rel, brs) ->
+      rel,
+      Aux.concat_map (fun (_,body,neg_body) ->
+        List.map fst body @ List.map fst neg_body) brs)
+    defs in
+  let defs = List.map
+    (fun (rel, drels) ->
+      rel, Aux.strings_of_list (Aux.list_inter drels for_rels)) defs in
+  let rec aux strata defs =
+    if defs = [] then List.flatten (List.rev strata)
+    else
+      (* like in topological sort, but don't restrict to empty call set *)
+      let stratum = Aux.list_find_all_max
+        (fun (_,a) (_,b) ->
+          Aux.Strings.cardinal b - Aux.Strings.cardinal a) defs in
+      let stratum = List.map fst stratum in
+      let visited = Aux.strings_of_list stratum in
+      let defs = List.filter
+        (fun (r,_) -> not (Aux.Strings.mem r visited)) defs in
+      let defs = List.map
+        (fun (r,calls) -> r, Aux.Strings.diff calls visited) defs in
+      aux (stratum::strata) defs in
+  aux [] (List.filter (fun (r,_) -> List.mem r for_rels) defs)
+
 let rec subst_one (x, term as sb) = function
   | Var y when x=y -> term
   | (Const _ | Var _ as t) -> t
@@ -236,7 +266,7 @@
     | _ -> raise Not_found
 
 
-(** A "blank" term. *)
+(** A "blank", or "wild-card", term. *)
 let blank = Const "_BLANK_"
 
 (* Match terms on the left to ground terms on the right, ignoring
@@ -714,6 +744,7 @@
   used_vars := Aux.StrMap.fold (fun _ cls acc ->
     Aux.Strings.union (clauses_vars cls) acc) p Aux.Strings.empty;
   used_vars := Aux.Strings.union !used_vars (clause_vars (("",[||]),g));
+  let g = preprocess_cl_body g in
   let sc_init fc sb = fun m -> fc () (sb::m) in
   let fc_init () = fun m -> m in
   let extract res = res [] in
@@ -731,6 +762,7 @@
   used_vars := Aux.StrMap.fold (fun _ cls acc ->
     Aux.Strings.union (clauses_vars cls) acc) p Aux.Strings.empty;
   used_vars := Aux.Strings.union !used_vars (clause_vars (("",[||]),g));
+  let g = preprocess_cl_body g in
   let sc_init fc _ = true in
   let fc_init () = false in
   run_goal g p sc_init fc_init []
@@ -740,10 +772,10 @@
 (* ************************************************************ *)
 (** {3 Transformations of GDL clauses: inlining, negation.} *)
 
-(** Expand branches of a definition inlining the provided definitions,
-    only expand positive literals. Iterate expansion to support
-    nesting of definitions. *)
-let expand_positive_lits defs brs =
+(** Expand branches of a definition inlining the provided
+    definitions. Iterate expansion to support nesting of
+    definitions. *)
+let expand_definitions defs brs =
   let used_vars = ref (gdl_defs_vars (("",brs)::defs)) in
   let freshen_brs brs =
     let br_vars = gdl_defs_vars ["",brs] in
@@ -755,7 +787,7 @@
       (Aux.Strings.elements br_vars) in
     let sb = List.map (fun (v,t) -> v, Var t) sb in
     List.map (subst_br sb) brs in
-  let expand_atom (rel, args as atom)
+  let expand_pos_atom (rel, args as atom)
       (sb, (head, r_body, r_neg_body)) =
     (let try def_brs = freshen_brs (List.assoc rel defs) in
      let args = Array.map (subst sb) args in
@@ -766,10 +798,39 @@
        sb, subst_br sb r_br
      ) def_brs
      with Not_found ->
-         [sb, (head, atom::r_body, r_neg_body)]) in
+       [sb, (head, (subst_rel sb atom)::r_body, r_neg_body)]) in
+  let pack_lits body neg_body =
+    List.map (fun a->Aux.Left a) body @
+      List.map (fun a->Aux.Right a) neg_body in
+  let expand_neg_atom (rel, args as atom)
+      (sb, (head, r_body, r_neg_body)) =
+    (let try def_brs = freshen_brs (List.assoc rel defs) in
+     let args = Array.map (subst sb) args in
+     let def_brs = Aux.map_try
+       (fun (params,body,neg_body) ->
+         let sb = unify_args ~sb params args in
+         let body = List.map (subst_rel sb) body
+         and neg_body = List.map (subst_rel sb) neg_body in
+         (* do not propagate the substitution further *)
+         pack_lits body neg_body)
+       def_brs in
+     if def_brs = [] then
+       [sb, (head, r_body, r_neg_body)]
+     else
+       (* DNF of the negation of [def_brs] disjunction --
+          [Left]/[Right] switch meaning *)
+       let dnf_of_neg = Aux.product def_brs in
+       List.map (fun dnf_br ->
+         let d_neg_body, d_body = Aux.partition_choice dnf_br in
+         sb, (head, d_body @ r_body, d_neg_body @ r_neg_body)
+       ) dnf_of_neg
+     with Not_found ->
+       [sb, (head, r_body, (subst_rel sb atom)::r_neg_body)]) in
+
   let expand_br (head, body, neg_body) =
-    let init = [[], (head, [], neg_body)] in
-    Aux.concat_foldr expand_atom body init in
+    let init = [[], (head, [], [])] in
+    Aux.concat_foldr expand_neg_atom neg_body
+      (Aux.concat_foldr expand_pos_atom body init) in
   let rec fix n_brs brs i =
     let brs = Aux.concat_map expand_br brs in
     let new_n_brs = List.length brs in
@@ -787,15 +848,18 @@
   let placeholder = "", [] in
   let clauses = List.map (fun body -> placeholder, body) conjs in
   let clauses = Aux.concat_map rules_of_clause clauses 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 clauses = List.map (fun (_,body,neg_body) ->
-    List.map (fun a -> Pos (atom_of_rel a)) body @
-      List.map (fun a -> Neg (atom_of_rel a)) neg_body) clauses in
+    List.map (fun a -> pos (atom_of_rel a)) body @
+      List.map (fun a -> neg (atom_of_rel a)) neg_body) clauses in
   let negated = Aux.product clauses in
   (* can raise [Not_found] in case of unsatisfiable "not distinct" *)
   let nclause body =
     let uniterms, lits =
       Aux.partition_map (function
-        | Neg (Distinct terms) -> Aux.Left (Array.to_list terms)
+        (* we negate! so not (Pos Distinct) here *)
+        | Pos (Distinct terms) -> Aux.Left (Array.to_list terms)
         | Neg atom -> Aux.Right (Pos atom)
         | Pos atom -> Aux.Right (Neg atom)
         | Disj _ -> assert false) body in
@@ -1543,3 +1607,36 @@
   List.fold_left (fun clauses (p, ts) ->
     expand_path_vars_by prepare_lits p ts clauses
   ) clauses ps_sterms
+
+
+let blank_outside_subterm arities path subterm =
+  List.fold_right
+    (fun (rel, pos) acc ->
+      let subterms = Array.make (List.assoc rel arities) blank in
+      subterms.(pos) <- acc;
+      Func (rel, subterms))
+    path subterm
+
+(** Find a path in a term and substitute, raise [Not_found] if path
+    not present. Push past blank subterms. [subst_at_path a p s blank]
+    is the same as [blank_outside_subterm a p s]. *)
+let subst_past_blank arities p s t =
+  let rec aux = function
+    | [], _ -> s
+    | (rel1, pos)::p, Func (rel2, args) when rel1 = rel2 ->
+      let args = Array.copy args in
+      args.(pos) <- aux (p, args.(pos));
+      Func (rel1, args)
+    | (rel, pos)::p, t when t = blank ->
+      let subterms = Array.make (List.assoc rel arities) blank in
+      subterms.(pos) <- aux (p, blank);
+      Func (rel, subterms)
+    | _ -> raise Not_found in
+  aux (p, t)
+
+let blank_outside_subterms arities path_subts =
+  try
+    List.fold_left (fun acc (p, s) -> subst_past_blank arities p s acc)
+      blank path_subts
+  with Not_found ->
+    invalid_arg "blank_outside_subterms: conflicting paths"

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/GDL.mli	2011-08-26 14:33:35 UTC (rev 1544)
@@ -112,11 +112,15 @@
 
 (** {3 Transformations of GDL clauses: inlining, negation.} *)
 
-(** Expand branches of a definition inlining the provided definitions,
-    only expand positive literals. Iterate expansion to support
-    nesting of definitions. *)
-val expand_positive_lits : gdl_defs -> def_branch list -> def_branch list
+(** Expand branches of a definition inlining the provided
+    definitions. Iterate expansion to support nesting of
+    definitions. *)
+val expand_definitions : gdl_defs -> def_branch list -> def_branch list
 
+(** Remember that [rel_of_atom] inverts polarity of "distinct" --
+    invert back after using [atom_of_rel] if needed. *)
+val atom_of_rel : rel_atom -> atom
+
 (** Form clause bodies whose disjunction is equivalent to the
     negation of disjunction of given clause bodies. Keep the
     substitution so that the heads of corresponding clauses can be
@@ -154,6 +158,8 @@
 val literal_str : literal -> string
 val clause_str : clause -> string
 
+val topsort_callgraph : clause list -> string list -> string list
+
 (** {3 GDL whole-game operations.}
 
     Aggregate and random playout, player-denoting variable elimination. *)
@@ -235,10 +241,17 @@
 
 val path_str : path -> string
 
-(* [ground_vars_at_paths prepare_lits ps_sterms clauses] expands
-   variables that have occurrences at paths in [ps_sterms] in some
-   state term of a clause (from which pre-processed literals are
-   extracted by [prepare_lits]), by terms provided in [ps_sterms]. *)
+(** [ground_vars_at_paths prepare_lits ps_sterms clauses] expands
+    variables that have occurrences at paths in [ps_sterms] in some
+    state term of a clause (from which pre-processed literals are
+    extracted by [prepare_lits]), by terms provided in [ps_sterms]. *)
 val ground_vars_at_paths :
   (clause -> literal list) ->
   (path * term list) list -> clause list -> clause list
+
+
+val blank_outside_subterm :
+  (string * int) list -> path -> term -> term
+
+val blank_outside_subterms :
+  (string * int) list -> (path * term) list -> term

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -99,10 +99,13 @@
     used; if [keep_nonempty_predicates] is true, do not remove
     predicates.
 
+    Remove unused defined relations. Note that recursion loops are not
+    handled (i.e. mutually recursive relations are not removed).
+
     FIXME: why some unused (non-empty) predicates end up being empty?
 
     TODO: require an explicit set of relations to keep instead of
-    [keep_nonempty_predicates].
+    [keep_nonempty_predicates]. ???
 
     (5) TODO: Glue redundant rules (equal and having the same roles in
     the game graph).
@@ -479,13 +482,14 @@
     Structure.add_rels struc grel tuples in
 
   (* preparing (3a-d) *)
-  let add_rel rel acc =
+  let add_rel excl rel acc =
     match rel with
-      | Rel (rel,_) -> Aux.Strings.add rel acc
+      | Rel (rel,_) when rel <> excl -> Aux.Strings.add rel acc
       | _ -> acc in
+  let add_rels excl = FormulaOps.fold_over_atoms (add_rel excl) in
   let used_rels =
     Arena.fold_over_formulas ~include_defined_rels:false
-      (FormulaOps.fold_over_atoms add_rel)
+      (add_rels "")
       game Aux.Strings.empty in
   let used_rels = ref used_rels in
   let struc = ref state.Arena.struc in
@@ -829,22 +833,39 @@
   (* 4 *)
   (* since relations relevant for LHS structures occur in the
      "embedding formula", we can freely remove from all structures
-     static relations that do not occur in any formula *)
+     the relations that do not occur in any formula *)
   let used_rels =
     Arena.fold_over_formulas ~include_defined_rels:false
-      (FormulaOps.fold_over_atoms add_rel)
+      (FormulaOps.fold_over_atoms (add_rels ""))
       game Aux.Strings.empty in
+  let used_in_def =
+    List.fold_right (fun (drel, (_, def)) -> add_rels drel def)
+      game.Arena.defined_rels Aux.Strings.empty in
+  let used_in_def, defined_rels =
+    let rec aux (used_in_def, defined_rels) =
+      let defined_rels = List.filter
+        (fun (r, _) -> Aux.Strings.mem r used_rels ||
+          Aux.Strings.mem r used_in_def)
+        defined_rels in
+      let now_used_in_def =
+        List.fold_right (fun (drel, (_, def)) -> add_rels drel def)
+          defined_rels Aux.Strings.empty in
+      if Aux.Strings.subset used_in_def now_used_in_def
+      then now_used_in_def, defined_rels
+      else aux (now_used_in_def, defined_rels) in
+    aux (used_in_def, game.Arena.defined_rels) in
+  let used_rels = Aux.Strings.union used_in_def used_rels in
+  let game = {game with Arena.defined_rels = defined_rels} in
   let clear_rel rel =
     let rel =
       if DiscreteRule.special_rel_of rel = None then rel
       else DiscreteRule.orig_rel_of rel in
     let res =
       (not keep_nonempty_predicates ||
-         List.assoc rel signat > 1 ||
+         (try List.assoc rel signat > 1 with Not_found -> false) ||
          Structure.rel_size !struc rel = 0
       ) &&
         not (Aux.Strings.mem rel fluents) &&
-        not (List.mem_assoc rel game.Arena.defined_rels) &&
         not (Aux.Strings.mem rel used_rels) in
     (* {{{ log entry *)
     if !debug_level > 2 && res then (

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -56,9 +56,7 @@
       ) state_terms in
     other, pos_terms, neg_terms) disj
     
-(* Whether $i$th argument is a $\mathrm{DefSide}$ or a
-   $\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
-type defrel_arg_mode = (bool * path) array
+type defrel_argpaths = (GDL.path * int) list list
     
 type transl_data = {
   f_paths : path_set;                   (* fluent paths *)
@@ -66,7 +64,7 @@
   all_paths : path_set;                 (* sum of f_paths and m_paths *)
   mask_reps : term list;                (* mask terms *)
   defined_rels : string list;
-  defrel_arg_mode : (string * defrel_arg_mode) list ref;
+  mutable defrel_argpaths : (string * defrel_argpaths) list;
   (* late binding to store $ArgMode# data *)
   term_arities : (string * int) list;
   rel_default_path : (string * path option array) list;
@@ -78,7 +76,7 @@
   all_paths = empty_path_set;
   mask_reps = [];
   defined_rels = [];
-  defrel_arg_mode = ref [];
+  defrel_argpaths = [];
   term_arities = [];
   rel_default_path = [];
 }
@@ -89,25 +87,34 @@
 let var_of_term data t =
   Formula.fo_var_of_string (term_to_name (blank_out data t))
 
-let blank_outside_subterm data path subterm =
-  let arities = data.term_arities in
-  List.fold_right
-    (fun (rel, pos) acc ->
-      let subterms = Array.make (List.assoc rel arities) blank in
-      subterms.(pos) <- acc;
-      Func (rel, subterms))
-    path subterm
-
 let var_of_subterm data path subt =
   Formula.fo_var_of_string
-    (term_to_name (blank_outside_subterm data path subt))
+    (term_to_name (blank_outside_subterm data.term_arities path subt))
 
-(* placeholder *)
-let translate_defrel =
-  ref (fun data sterms_all sterms_in s_subterms sign rel args ->
-    assert false)
+let var_of_subterms data path_subts =
+  Formula.fo_var_of_string
+    (term_to_name (blank_outside_subterms data.term_arities path_subts))
 
-let transl_rels data rels_phi sterms_all sterms_in =
+  
+let find_defrel_arg sterms args apset =
+  List.find
+    (fun s -> List.for_all (fun (p,i) -> at_path s p = args.(i)) apset)
+    sterms
+
+let translate_defrel data sterms sign rel args =
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "translate_defrel: phi=%s, sign=%b\n"
+      (rel_atom_str (rel, args)) sign
+  );
+  (* }}} *)
+  let partition = List.assoc rel data.defrel_argpaths in
+  let s_l = List.map (find_defrel_arg sterms args) partition in
+  let vtup = Array.of_list (List.map (var_of_term data) s_l) in
+  let defrel_phi = Formula.Rel (rel, vtup) in
+  if sign then defrel_phi else Formula.Not defrel_phi
+
+let transl_rels data rels_phi sterms_all vterms_in =
   (* within-mask subterms to locate paths on which to generate relations *)
   let s_subterms = Aux.concat_map
     (fun sterm ->
@@ -132,7 +139,8 @@
      let stuples = Aux.product stuples in
      let stuples = List.filter
        (fun stup ->
-         List.exists (fun (sterm,_) -> List.mem sterm sterms_in) stup)
+         List.exists (fun (sterm,_) ->
+           List.mem (var_of_term data sterm) vterms_in) stup)
        stuples in
      let atoms = Aux.map_some
        (fun stup ->
@@ -151,8 +159,7 @@
   let transl_posdefrel sign rel args =
     if List.mem rel data.defined_rels
     then
-      [!translate_defrel data sterms_all sterms_in
-          s_subterms sign rel args]
+      [translate_defrel data sterms_all sign rel args]
     else transl_rel sign rel args in
   let rec aux = function
     | Pos (Rel (rel, args)) -> transl_posdefrel true rel args
@@ -263,7 +270,7 @@
       neg_ext @
         [
           (* positive because they form a "premise" *)
-          transl_rels data rels_eqs all_terms neg_terms;
+          transl_rels data rels_eqs all_terms neg_vars;
           (* the universal "conclusion" *)
           negated_neg_state_transl]) in
   let universal_part =
@@ -275,7 +282,7 @@
   let base_part =
     Formula.And (
       pos_ext @
-      [ transl_rels data rels_eqs pos_terms pos_terms;
+      [ transl_rels data rels_eqs pos_terms pos_vars;
         transl_state data pos_state_phi] @
         universal_part) in
   if pos_vars = [] then base_part
@@ -294,187 +301,173 @@
 (* **************************************** *)
 (* {3 Build and use defined relations.} *)
 
-let select_defrel_argpaths data all_branches =
-  (* TODO: code-review this and [build_defrel] functions *)
-  let select_for_defrel rel =
-    (* searching for ArgMode = DefSide,S,p *)
-    let branches = Aux.assoc_all rel all_branches in
-    (* {{{ log entry *)
-    if !debug_level > 2 then (
-      Printf.printf "select_defrel_argpaths: rel=%s, no of brs=%d\n%!"
-        rel (List.length branches)
-    );
-    (* }}} *)
-    (* first find the common paths, we will find the state terms later *)
-    let branch_paths =
-      List.map (fun (args, (_, sterms_pos, sterms_neg)) ->
-        let sterms = state_terms (sterms_pos @ sterms_neg) in
-        Array.map (fun arg ->
-          Aux.concat_map (fun sterm ->
-            Aux.map_some (fun x->x)
-              (map_paths (fun p subt ->
-                if subt = arg then Some p else None) data.m_paths sterm)
-          ) sterms) args
-      ) branches in
-    let p_defside = List.fold_left
-      (Aux.array_map2 Aux.list_inter)
-      (List.hd branch_paths) (List.tl branch_paths) in
-    let p_defside = Array.map
-      (function path::_ -> Some path | [] -> None) p_defside in
-    (* now find the mapping $\calS_i$ for the DefSide result *)
-    let branch_sterms (args, (_, sterms_pos, sterms_neg)) =
-      let sterms = state_terms (sterms_pos @ sterms_neg) in
-      Aux.array_map2
-        (fun arg -> function None -> None
-          | Some path ->
-            Some (List.find (fun sterm ->
-              List.mem (Some path)
-                (map_paths (fun p subt ->
-                  if subt = arg then Some p else None) data.m_paths sterm)
-            ) sterms))
-        args p_defside in
-    let s_defside = List.map branch_sterms branches in
-    (* now computing the ArgMode(R,i) = CallSide,p variant *)
-    let call_branches = Aux.concat_map
-      (fun (_,(_, (phi, _, _ as body))) ->
-        let calls = Aux.assoc_all rel (rel_atoms phi) in
-        List.map (fun args -> args, body) calls
-      ) all_branches in
-    let callside_for_arg i =
-      let call_paths = Aux.concat_map
-        (fun (args, (_, sterms_pos, sterms_neg)) ->
-          let sterms = state_terms (sterms_pos @ sterms_neg)
-          and arg = args.(i) in
-          let paths = Aux.concat_map (fun sterm ->
-            Aux.map_some (fun x->x)
-              (map_paths (fun p subt ->
-                if subt = arg then Some p else None) data.m_paths sterm)
-          ) sterms in
-          List.map (fun p -> p, ()) paths
-        ) call_branches in
-      let call_paths = List.map
-        (fun (p, ns) -> List.length ns, p)
-        (Aux.collect call_paths) in
-      (* decreasing order *)
-      match List.sort (fun (x,_) (y,_) -> y-x) call_paths with
-        | [] -> None
-        | (_,p)::_ -> Some p in
-    let p_callside = Array.mapi
-      (fun i ->
-        function Some _ -> None | None -> callside_for_arg i)
-      p_defside in
-    let arg_paths = Array.mapi
-      (fun i defside ->
-        let callside = p_callside.(i) in
-        match defside, callside with
-          | Some p, _ | None, Some p -> p
-          | None, None ->
-            (* the ArgMode(R,i) = NoSide,p variant is precomputed *)
-            try
-              match (List.assoc rel data.rel_default_path).(i) with
-                | Some p -> p
-                | None -> raise Not_found
-            with Not_found ->
-              failwith
-                (Printf.sprintf
-                   "TranslateFormula.build_defrels: could not \
-  determine path for relation %s argument %d" rel i)
-      ) p_defside in
-    let defrel_arg_mode = Aux.array_map2
-      (fun defside path -> defside <> None, path)
-      p_defside arg_paths  in
-    data.defrel_arg_mode :=
-      (rel, defrel_arg_mode) :: !(data.defrel_arg_mode);
-    rel, (p_defside, s_defside, arg_paths) in
-  List.map select_for_defrel data.defined_rels
-
-
-let build_defrels data clauses =
-  let all_branches = Aux.concat_map
-    (fun ((rel,args),body) ->
-      List.map (fun phi -> rel, (args, phi)) (separate_disj [body]))
+let select_defrel_argpaths drel data clauses =
+  let atoms_sterms = List.map
+    (fun ((rel,args), body) ->
+      let r_atoms = if rel = drel then [args] else [] in
+      let r_atoms = r_atoms @ Aux.map_some
+        (function Rel (rel, args) when rel = drel -> Some args
+          | _ -> None)
+        (atoms_of_body body) in
+      r_atoms, state_terms body
+      (* we take all state terms to have more compact partition *)
+      (*Aux.map_some
+        (function Pos (True s) -> Some s | _ -> None) body*))
     clauses in
-  let sel_argpaths = select_defrel_argpaths data all_branches in
-  let build_defrel rel =
-    (* now building the translation *)
-    let (p_defside, s_defside, arg_paths) =
-      List.assoc rel sel_argpaths in
-    let defvars =
-      Array.mapi (fun i _ -> "v"^string_of_int i) arg_paths in
-    let defbody (args,(rels_phi,pos_state,neg_state)) s_defside =        
-      let arg_eqs = Array.mapi          (* $E_{j,l}$ *)
-        (fun i v ->
-          let v = Formula.fo_var_of_string v in
-          let in_I = p_defside.(i) <> None in
-          if in_I
-          then
-            let s_i = match s_defside.(i) with
-              | Some s -> var_of_term data s
-              | None -> assert false in
-            Formula.Eq (v, s_i)
-          else Formula.Eq (v, var_of_subterm data arg_paths.(i) args.(i)))
-        defvars in
-      let arg_eqs = Array.to_list arg_eqs in
-      let callside_sterms =             (* $S_{j,l}$ *)
-        Aux.array_mapi_some
-          (fun i path ->
-            if p_defside.(i) <> None then None (* only for not in I *)
-            else Some (blank_outside_subterm data path args.(i)))
-          arg_paths in
-      (* packing sterms back as a formula *)
-      let callside_sterms = Array.to_list
-        (Array.map (fun sterm -> Pos (True sterm)) callside_sterms) in
-      transl_disjunct data rels_phi
-        (callside_sterms @ pos_state) neg_state arg_eqs in
-    let branches = Aux.assoc_all rel all_branches in
-    let def_disjuncts = List.map2 defbody branches s_defside in
-    rel, (Array.to_list defvars, Formula.Or def_disjuncts) in
-  List.map build_defrel data.defined_rels
+  let check_path args p s_p =
+    let inds = Aux.array_argfind_all (fun r -> r=s_p) args in
+    List.map (fun i->p,i) inds in
+  let sterm_path_sets args s =
+    let ptups = Aux.product
+      (map_paths (check_path args) data.m_paths s) in
+    (* distinct [p] in a tuple is already ensured *)
+    List.filter (fun tup ->
+      not (Aux.not_unique (List.map snd tup))) ptups in
+  let argpath_sets = Aux.concat_map
+    (fun (atoms, sterms) -> Aux.concat_map
+      (fun args -> Aux.concat_map (sterm_path_sets args) sterms)
+      atoms)
+    atoms_sterms in
+  let argpath_sets =
+    Aux.map_reduce (fun pset -> pset, 1) (+) 0 argpath_sets in
+  let argpath_sets = List.sort Pervasives.compare
+    (List.map                           (* lexicographic comparison *)
+       (fun (pset,count) -> List.length pset, count, pset)
+       argpath_sets) in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf
+      "select_defrel_argpaths: drel=%s; argpath_sets=\n%!" drel;
+    List.iter (fun (len, count, pset) ->
+      Printf.printf "len=%d; count=%d; pset=%s\n%!" len count
+        (String.concat ", "
+           (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+      argpath_sets
+  );
+  (* }}} *)
+  let argpath_sets = List.map Aux.trd3 (List.rev argpath_sets) in
+  (* now greedily -- by traversing the ordering -- select covering *)
+  let apsets_cover = List.fold_left
+    (fun cover apset ->
+      if List.exists
+        (fun (_,i) -> not (List.exists (fun cov_apset ->
+          List.exists (fun (_,j)->i=j) cov_apset) cover)) apset
+      then apset::cover else cover)
+    [] argpath_sets in
+  (* eliminating multiple points -- starting with best apsets so
+     they're unchanged *)
+  let partition = List.fold_left
+    (fun partition apset ->
+      let apset = List.filter (fun (_,i) ->
+        not (List.exists (fun cov_apset ->
+          List.exists (fun (_,j)->i=j) cov_apset) partition)) apset in
+      if apset = [] then partition else apset::partition)
+    [] apsets_cover in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf
+      "select_defrel_argpaths: drel=%s; partition=\n%!" drel;
+    List.iter (fun pset ->
+      Printf.printf "pset=%s\n%!"
+        (String.concat ", "
+           (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+      partition
+  );
+  (* }}} *)
+  (* filling-in missing paths from precomputed defaults *)
+  let arity = Array.length
+    (List.hd (fst (List.find (fun (atoms,_) -> atoms<>[])
+                     atoms_sterms))) in
+  let argpaths = Array.init arity
+    (fun i ->
+      try List.find (List.exists (fun (_,j)->i=j)) partition
+      with Not_found ->
+        try
+          match (List.assoc drel data.rel_default_path).(i) with
+            | Some p -> [p, i]
+            | None -> raise Not_found
+        with Not_found ->
+          failwith
+            (Printf.sprintf
+               "TranslateFormula.build_defrels: could not \
+  determine path for relation %s argument %d" drel i)
+    ) in
+  let res = Aux.unique (=) (Array.to_list argpaths) in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf
+      "select_defrel_argpaths: drel=%s; result=\n%!" drel;
+    List.iter (fun pset ->
+      Printf.printf "pset=%s\n%!"
+        (String.concat ", "
+           (List.map (fun (p,i)->path_str p^": "^string_of_int i) pset)))
+      res
+  );
+  (* }}} *)
+  res
 
 
-let transl_defrel data sterms_all sterms_in s_subterms sign rel args =
+let defrel_transform drel partition data ((h_rel,h_args as h),body as cl) =
+  (* adding "true" atoms to clauses for missing argpath state terms *)
+  let r_atoms = if h_rel = drel then [h_args] else [] in
+  let r_atoms = r_atoms @ Aux.map_some
+    (function Rel (rel, args) when rel = drel -> Some args
+      | _ -> None)
+    (atoms_of_body body) in
+  let sterms = Aux.map_some
+    (function Pos (True s) -> Some s | _ -> None) body in
+  let sterm_arg_for_atom args apset =
+    try ignore (find_defrel_arg sterms args apset); None
+    with Not_found ->
+      let path_subts = List.map (fun (p,i)->p, args.(i)) apset in
+      Some (blank_outside_subterms data.term_arities path_subts) in
+  let add_sterms = Aux.concat_map
+    (fun args -> Aux.map_some (sterm_arg_for_atom args) partition)
+    r_atoms in
   (* {{{ log entry *)
-  if !debug_level > 2 then (
-    Printf.printf "transl_defrel: phi=%s, sign=%b\n"
-      (rel_atom_str (rel, args)) sign
+  if !debug_level > 2 && add_sterms <> [] then (
+    Printf.printf
+      "defrel_transform: add_sterms=%s; clause=\n%s\n\n%!"
+      (String.concat ", " (List.map term_str add_sterms))
+      (clause_str cl)
   );
   (* }}} *)
-  let arg_mode = List.assoc rel !(data.defrel_arg_mode) in
-  (* the $s \tpos_{p_{R,i}} = t_i$ state terms *)
-  let arg_sterms = Array.mapi
-    (fun i (defside, path) -> if defside then None else
-        try Some (
-          List.find (fun s -> at_path s path = args.(i)) sterms_all)
-        with Not_found -> None)
-    arg_mode in
-  let var_args = Array.mapi
-    (fun i (_, path) ->
-      match arg_sterms.(i) with
-        | None -> var_of_subterm data path args.(i) (* in J *)
-        | Some sterm -> var_of_term data sterm)
-    arg_mode in
-  let defrel_phi = Formula.Rel (rel, var_args) in
-  let defrel_phi =
-    if sign then defrel_phi else Formula.Not defrel_phi in
-  let ex_vars = Array.to_list
-    (Aux.array_mapi_some (fun i (_,path) ->
-      if arg_sterms.(i) = None
-      then Some (var_of_subterm data path args.(i))
-      else None) arg_mode) in
-  let in_J_eq_transl i (_,path) =
-    if arg_sterms.(i) = None
-    then
-      let eq_phi = [Pos (Rel ("EQ_", [|args.(i); args.(i)|]))] in
-      let v = blank_outside_subterm data path args.(i) in
-      Some (transl_rels data eq_phi (v::sterms_all) [v])
-    else None in
-  let eqs_phi = Array.to_list
-    (Aux.array_mapi_some in_J_eq_transl arg_mode) in
-  let base =
-    if eqs_phi = [] then defrel_phi
-    else Formula.And (defrel_phi::eqs_phi) in
-  if ex_vars = [] then base
-  else Formula.Ex ((ex_vars :> Formula.var list), base)
+  h, Aux.map_rev_prepend body (fun s -> Pos (True s)) add_sterms
 
-let _ = translate_defrel := transl_defrel
 
+let build_defrels data clauses =
+  let defined_rels_ord =
+    topsort_callgraph clauses data.defined_rels in
+  let process_drel clauses drel =
+    let partition =    
+      select_defrel_argpaths drel data clauses in
+    data.defrel_argpaths <- (drel, partition)::data.defrel_argpaths;
+    List.map (defrel_transform drel partition data) clauses in
+  (* first arguments processed first -- fold_left *)
+  let clauses = List.fold_left process_drel clauses defined_rels_ord in
+  let build_defrel drel =
+    (* now building the translation *)
+    let partition = List.assoc drel data.defrel_argpaths in
+    let r_clauses = Aux.map_some
+      (fun ((rel,args),body) ->
+        if rel=drel then Some (args,body) else None) clauses in
+    let d_arity = List.length partition in
+    let defvars =
+      Array.init d_arity (fun i -> "v"^string_of_int i) in
+    let tr_def_r (args, body) =
+      let sterms = Aux.map_some
+        (function Pos (True s) -> Some s | _ -> None) body in
+      let s_l = List.map (find_defrel_arg sterms args) partition in
+      let v_l = List.map (var_of_term data) s_l in
+      let eqs = List.map2
+        (fun v sv -> Formula.Eq (`FO v, sv))
+        (Array.to_list defvars) v_l in
+      let def_phi = FormulaOps.del_vars_quant (v_l :> Formula.var list)
+        (translate data [body]) in
+      if v_l = [] then Formula.And (eqs @ [def_phi])
+      else Formula.Ex ((v_l :> Formula.var list),
+                       Formula.And (eqs @ [def_phi])) in
+    drel, (Array.to_list defvars,
+           Formula.Or (List.map tr_def_r r_clauses)) in
+  clauses, List.map build_defrel defined_rels_ord  
+

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-08-26 14:33:35 UTC (rev 1544)
@@ -1,8 +1,6 @@
 val debug_level : int ref
 
-(* Whether $i$th argument is a $\mathrm{DefSide}$ or a
-   $\mathrm{CallSide}$, and the $p_{R,i}$ path for a relation $R$. *)
-type defrel_arg_mode = (bool * GDL.path) array
+type defrel_argpaths = (GDL.path * int) list list
 
 type transl_data = {
   f_paths : GDL.path_set;             (** fluent paths *)
@@ -10,8 +8,8 @@
   all_paths : GDL.path_set;          (** sum of f_paths and m_paths *)
   mask_reps : GDL.term list;         (** mask terms *)
   defined_rels : string list;
-  defrel_arg_mode : (string * defrel_arg_mode) list ref;
-  (** late binding to store $ArgMode$ data *)
+  mutable defrel_argpaths : (string * defrel_argpaths) list;
+  (** late binding to store argument paths data *)
   term_arities : (string * int) list;
   rel_default_path : (string * GDL.path option array) list;
 }
@@ -31,4 +29,4 @@
 
 val build_defrels :
   transl_data -> GDL.clause list ->
-  (string * (string list * Formula.formula)) list
+  GDL.clause list * (string * (string list * Formula.formula)) list

Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -66,7 +66,7 @@
     all_paths = all_paths;
     mask_reps = mask_reps;
     defined_rels = defined_rels;
-    defrel_arg_mode = ref [];
+    defrel_argpaths = [];
     term_arities = term_arities;
     rel_default_path = rel_default_path;
   }
@@ -153,15 +153,16 @@
         GDL.ground_vars_at_paths prepare_lits ground_at_f_paths clauses in
       let defined_rels, clauses =
         GDL.elim_ground_args transl_data.defined_rels clauses in
+      let transl_data = {transl_data with defined_rels = defined_rels} in
+      let clauses, defined_rels =
+        TranslateFormula.build_defrels transl_data clauses in
       (* {{{ log entry *)
       if !TranslateFormula.debug_level > 2 then (
-        Printf.printf "defined relations connect5: clauses =\n%s\n%!"
+        Printf.printf
+          "defined relations connect5: transformed clauses =\n%s\n%!"
           (String.concat "\n" (List.map GDL.clause_str clauses))
       );
       (* }}} *)
-      let transl_data = {transl_data with defined_rels = defined_rels} in
-      let defined_rels =
-        TranslateFormula.build_defrels transl_data clauses in
       let result drel =
         let args, body = List.assoc drel defined_rels in
         drel^"("^String.concat ", " args^
@@ -169,38 +170,7 @@
 
       assert_equal ~msg:"adjacent_cell defined relation translation"
         ~printer:(fun x->x)
-        "adjacent_cell(v0, v1, v2, v3) = ex cell_x__BLANK___BLANK_, cell_y__BLANK___BLANK_, cell_x1__BLANK___BLANK_,
- cell_y1__BLANK___BLANK_
- (cell__BLANK___BLANK___BLANK_(cell_x__BLANK___BLANK_) and
-  cell__BLANK___BLANK___BLANK_(cell_y__BLANK___BLANK_) and
-  cell__BLANK___BLANK___BLANK_(cell_x1__BLANK___BLANK_) and
-  cell__BLANK___BLANK___BLANK_(cell_y1__BLANK___BLANK_) and
-  adjacent__cell_0__cell_0(cell_x__BLANK___BLANK_,
-  cell_x1__BLANK___BLANK_) and
-  adjacent__cell_0__cell_0(cell_y__BLANK___BLANK_,
-  cell_y1__BLANK___BLANK_) and v0 = cell_x__BLANK___BLANK_ and
-  v1 = cell_y__BLANK___BLANK_ and v2 = cell_x1__BLANK___BLANK_ and
-  v3 = cell_y1__BLANK___BLANK_) or
- ex cell_x__BLANK___BLANK_, cell_y__BLANK___BLANK_, cell_x1__BLANK___BLANK_,
-  cell_y__BLANK___BLANK_
-  (cell__BLANK___BLANK___BLANK_(cell_x__BLANK___BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_x1__BLANK___BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_y__BLANK___BLANK_) and
-   adjacent__cell_0__cell_0(cell_x__BLANK___BLANK_,
-   cell_x1__BLANK___BLANK_) and
-   coordinate__cell_0(cell_y__BLANK___BLANK_) and
-   v0 = cell_x__BLANK___BLANK_ and v1 = cell_y__BLANK___BLANK_ and
-   v2 = cell_x1__BLANK___BLANK_ and v3 = cell_y__BLANK___BLANK_) or
- ex cell_x__BLANK___BLANK_, cell_y__BLANK___BLANK_, cell_x__BLANK___BLANK_,
-  cell_y1__BLANK___BLANK_
-  (cell__BLANK___BLANK___BLANK_(cell_y__BLANK___BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_x__BLANK___BLANK_) and
-   cell__BLANK___BLANK___BLANK_(cell_y1__BLANK___BLANK_) and
-   adjacent__cell_0__cell_0(cell_y__BLANK___BLANK_,
-   cell_y1__BLANK___BLANK_) and
-   coordinate__cell_0(cell_x__BLANK___BLANK_) and
-   v0 = cell_x__BLANK___BLANK_ and v1 = cell_y__BLANK___BLANK_ and
-   v2 = cell_x__BLANK___BLANK_ and v3 = cell_y1__BLANK___BLANK_)"
+        "adjacent_cell(v0, v1) ="
         (result "adjacent_cell");
       assert_equal ~msg:"conn5__o defined relation translation"
         ~printer:(fun x->x)

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -185,7 +185,7 @@
       (* it should actually be a single element association *)
       let brs_c =
         List.assoc "next" (defs_of_rules (rules_of_clause c)) in
-      c, expand_positive_lits inline_defs brs_c) next_clauses in
+      c, expand_definitions inline_defs brs_c) next_clauses in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     let next_exp = Aux.concat_map snd next_e in
@@ -302,7 +302,6 @@
       (String.concat ", " (List.map term_str element_reps))
   );
   (* }}} *)
-
   let m_paths = List.map
     (term_paths ~prefix_only:true (Aux.neg contains_blank)) element_reps in
   let m_paths =
@@ -340,6 +339,20 @@
     static_rels in
   let struc_rels = "EQ_"::struc_rels in
   let defined_rels = defined_rels @ nonstatic_rels in
+  let defs = List.filter
+    (fun ((rel,_),_) -> List.mem rel defined_rels) clauses in
+  let defs = defs_of_rules (Aux.concat_map rules_of_clause defs) in
+  let frame_defs = List.assoc "next"
+    (defs_of_rules (Aux.concat_map rules_of_clause frame_clauses)) in
+  let frame_defs = expand_definitions defs frame_defs in
+  let pos = function Distinct _ as a -> Neg a | a -> Pos a in
+  let neg = function Distinct _ as a -> Pos a | a -> Neg a in
+  let frame_clauses = List.map
+    (fun (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)
+    frame_defs in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf
@@ -421,6 +434,7 @@
     List.filter (fun ((rel,_),_) -> rel <> "next") clauses in
   let frame_clauses = List.map
     (fun ((_,args),body) -> ("frame next", args), body) frame_clauses in
+
   players, rules,
   frame_clauses @ move_clauses @ clauses,
   f_paths, m_paths, mask_reps, defined_rels,
@@ -672,13 +686,25 @@
     List.map (fun ((_,h),body) -> h.(0),false,body) erasure_cls in
   (* {{{ log entry *)
   if !debug_level > 2 then (
-    Printf.printf "add_erasure_clauses: erasure clauses --\n%!";
+    Printf.printf "add_erasure_clauses: all erasure clauses --\n%!";
     let print_erasure (s, _, body) =
       Printf.printf "ERASURE: %s <== %s\n%!" (term_str s)
         (String.concat " " (List.map literal_str body)) in
     List.iter print_erasure erasure_cls; flush stdout;
   );
   (* }}} *)
+  let erasure_cls = Aux.maximal
+    (fun (h1,_,b1) (h2,_,b2) -> h1=h2 && Aux.list_diff b2 b1 = [])
+    erasure_cls in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "add_erasure_clauses: minimal erasure clauses --\n%!";
+    let print_erasure (s, _, body) =
+      Printf.printf "ERASURE: %s <== %s\n%!" (term_str s)
+        (String.concat " " (List.map literal_str body)) in
+    List.iter print_erasure erasure_cls; flush stdout;
+  );
+  (* }}} *)
   let next_cls =
     Aux.map_some (fun (s, (frame, required), body) ->
       if not frame then Some (s, required, body) else None) next_cls in
@@ -715,19 +741,32 @@
    excluded. If this poses problems we might need to expand
    disjunctions containing potentially case-split atoms.
 
+   TODO: (important) filter-out case-split atoms based on conjoining
+   them with deterministic literals of required clauses (and checking
+   on the suite of random playout states).
 *)
-let rule_cases rule_cls =
+let rule_cases program playout_states rule_cls =
   let required_cls = Aux.map_some
     (fun (h, required, body) ->
       if required then Some (h, body) else None) rule_cls in
+  let required_body = Aux.concat_map snd required_cls in
   let unrequired_cls = Aux.map_some
     (fun (h, required, body) ->
       if not required then Some (h, body) else None) rule_cls in  
+  let unrequired_cls = List.filter
+    (fun (_, unreq_body) ->
+      List.exists
+        (fun state ->
+          run_prolog_check_goal (required_body @ unreq_body)
+            (replace_rel_in_program "true" (state_cls state) program))
+        playout_states)
+    unrequired_cls in
   let forbidden_lits = Aux.unique_sorted
     (Aux.concat_map
        (fun (_, body) -> Aux.map_some (function
-         | Pos (Rel _ as a) | Pos (True _ as a) -> Some (Neg a)
-         | Neg (Rel _ as a) | Neg (True _ as a) -> Some (Pos a)
+         | Pos (Does _) | Neg (Does _) -> None
+         | Pos a -> Some (Neg a)
+         | Neg a -> Some (Pos a)
          | _ -> None) body) required_cls) in
   let unrequired_cls = List.filter
     (fun (_, body) ->
@@ -740,8 +779,8 @@
   let unreq_atoms = Aux.unique_sorted
     (Aux.concat_map
        (fun (_, body) -> Aux.map_some (function
-         | Pos (Rel _ as a) | Pos (True _ as a)
-         | Neg (Rel _ as a) | Neg (True _ as a) -> Some a
+         | Pos (Does _) | Neg (Does _) -> None
+         | Pos a | Neg a -> Some a
          | _ -> None) body) unrequired_cls) in
   let split_atoms = Aux.list_diff unreq_atoms req_atoms in
   if split_atoms = [] then                    (* single partition *)
@@ -777,7 +816,14 @@
         Printf.printf "%a: %s\n%!"
           (Aux.array_fprint (fun ch -> Printf.fprintf ch "%+d")) pattern
           (String.concat " " (List.map atom_str atoms)) in
-      List.iter print_pat patterns
+      List.iter print_pat patterns;
+      let print_cl i (h, body) =
+        Printf.printf "%d: %s <== %s\n%!" i (term_str h)
+          (String.concat " " (List.map literal_str body)) in
+      Printf.printf "rule_cases: required cls --\n%!";
+      Array.iteri print_cl (Array.of_list required_cls);
+      Printf.printf "rule_cases: split on cls --\n%!";
+      Array.iteri print_cl (Array.of_list unrequired_cls)
     );
     (* }}} *)
     let choices = Aux.power split_atoms [false; true] in
@@ -795,11 +841,22 @@
         ) unrequired_cls in
       let case_cls = case_cls @ required_cls in
       let case_rhs, case_conds = List.split case_cls in
-      let case_rhs = Aux.list_remove ignore_rhs case_rhs in
-      Aux.unique_sorted case_rhs,
-      Aux.unique_sorted (separation_cond @ List.concat case_conds) in
+      let case_rhs =
+        Aux.list_remove ignore_rhs (Aux.unique_sorted case_rhs) in
+      let case_conds =
+        Aux.unique_sorted (List.concat case_conds) in
+      (* {{{ log entry *)
+      if !debug_level > 3 then (
+        Printf.printf "\nRCAND:\nsep_cond: %s\nRHS: %s\ncase_conds: %s\n\n%!"
+          (String.concat " " (List.map literal_str separation_cond))
+          (String.concat " " (List.map term_str case_rhs))
+          (String.concat " " (List.map literal_str case_conds))
+      );
+      (* }}} *)
+      case_rhs,
+        Aux.unique_sorted (separation_cond @ case_conds) in
     let res = List.map rule_case choices in
-  (* {{{ log entry *)
+    (* {{{ log entry *)
     if !debug_level > 2 then (
       Printf.printf "rule_cases: next clauses partitioned into rules\n%!";
       let print_case  i (case_rhs, case_cond) =
@@ -808,7 +865,7 @@
           (String.concat " " (List.map literal_str case_cond)) in
       Array.iteri print_case (Array.of_list res)
     );
-  (* }}} *)
+    (* }}} *)
     res
 
 
@@ -838,16 +895,17 @@
   List.map (add_erasure_clauses f_paths) move_tups
 
 
-let add_legal_cond (legal_tup, next_cls) =
+let add_legal_cond program playout_states (legal_tup, next_cls) =
   let legal_tup, legal_conds = List.split legal_tup in
   let legal_cls = List.map (* required clauses *)
     (fun body -> ignore_rhs, true, body) legal_conds in
   List.map
     (fun (case_rhs, case_cond) -> legal_tup, case_rhs, case_cond)
-    (rule_cases (legal_cls @ next_cls))
+    (rule_cases program playout_states (legal_cls @ next_cls))
 
 
-let turnbased_rule_cases loc_noops used_vars f_paths next_cls
+let turnbased_rule_cases loc_noops used_vars f_paths
+    program playout_states next_cls
     players legal_by_player =
   let legal_tuples = Aux.product legal_by_player in
   (* remove tuples with multiple players making moves
@@ -874,14 +932,16 @@
   let move_tups =
     process_rule_cands
       used_vars f_paths next_cls `General players legal_tuples in
-  let rules = Aux.concat_map add_legal_cond move_tups in
+  let rules = Aux.concat_map
+    (add_legal_cond program playout_states) move_tups in
   (* we do not look for the players -- for turn-based case, it's done
      while building game graph *)
   Aux.Left rules
 
 
 (* If "Concurrent Moves" case, divide rule clauses among players. *)
-let concurrent_rule_cases used_vars f_paths  next_cls players legal_by_player =
+let concurrent_rule_cases used_vars f_paths program playout_states
+    next_cls players legal_by_player =
   let env_pl_tups =
     env_player,
     process_rule_cands used_vars f_paths next_cls `Environment [] [[]] in
@@ -896,11 +956,12 @@
     ) players legal_by_player in
   let player_rules = List.map
     (fun (player, move_tups) ->
-      player, Aux.concat_map add_legal_cond move_tups)
+      player, Aux.concat_map (add_legal_cond program playout_states) move_tups)
     (player_rules @ [env_pl_tups]) in
   Aux.Right player_rules
 
-let general_int_rule_cases used_vars f_paths next_cls players legal_by_player =
+let general_int_rule_cases used_vars f_paths program playout_states
+    next_cls players legal_by_player =
   failwith "General Interaction Games not implemented yet"
 
 
@@ -914,7 +975,8 @@
    are built. The rules are partitioned among players. The last
    player is the environment, [env_player] (this way, the numbering of
    players can be the same as in turn-based case). *)
-let create_rule_cands is_turn_based used_vars f_paths next_cls clauses =
+let create_rule_cands is_turn_based used_vars f_paths
+    program playout_states next_cls clauses =
   let players = (* Array.of_list *)
     Aux.map_some (function
       | ("role", [|player|]), _ -> Some player
@@ -945,14 +1007,17 @@
     ) players in
   let result =
     if is_concurrent then
-      concurrent_rule_cases used_vars f_paths next_cls players legal_by_player
+      concurrent_rule_cases used_vars f_paths program playout_states
+        next_cls players legal_by_player
     else
       match is_turn_based with
         | Some (_, loc_noops) ->
-          turnbased_rule_cases loc_noops used_vars f_paths next_cls
+          turnbased_rule_cases loc_noops used_vars f_paths
+            program playout_states next_cls
             players legal_by_player
         | None ->
-          general_int_rule_cases used_vars f_paths next_cls
+          general_int_rule_cases used_vars f_paths
+            program playout_states next_cls
             players legal_by_player
   in
   (* {{{ log entry *)
@@ -975,34 +1040,17 @@
 
 (* We use a bunch of possible game states, generated by random
    playouts, to approximate which rule candidates are satisfiable in
-   some reachable state. *)
-let filter_rule_cands players program rule_cands =
-  (* {{{ log entry *)
-  if !debug_level > 1 then (
-    Printf.printf "filter_rule_cands: generating states...\n%!";
-    (* GDL.debug_level := 4; *)
-  );
-  (* }}} *)
-  let states = Aux.fold_n
-    (fun acc ->
-      let _, states =
-        playout_prolog ~aggregate:false players !playout_horizon
-          program in
-      states @ acc) [] !playouts_for_rule_filtering in
-  (* {{{ log entry *)
-  if !debug_level > 1 then (
-    (* GDL.debug_level := 0; *)
-    Printf.printf "filter_rule_cands: generated %d states.\n%!"
-      (List.length states)
-  );
-  (* }}} *)
+   some reachable state. After filtering, we add blanked-out RHS
+   terms as "true" atoms (so they are properly constrained and treated
+   existentially). *)
+let filter_rule_cands players f_paths program playout_states rule_cands =
   let check_cands cands =
     List.filter (fun (_, _, case_conds) ->
       let res = List.exists
         (fun state ->
           run_prolog_check_goal case_conds
             (replace_rel_in_program "true" (state_cls state) program))
-        states in
+        playout_states in
       (* {{{ log entry *)
       if !debug_level > 1 then (
         Printf.printf "check_cands: cond %s -- %b\n%!"
@@ -1011,10 +1059,15 @@
       (* }}} *)      
       res
     ) cands in
+  let add_rhs_as_lhs (legal_tup, case_rhs, case_cond) =
+    let case_blanks = List.map
+      (fun s -> Pos (True (simult_subst f_paths blank s))) case_rhs in
+    legal_tup, case_rhs, Aux.unique_sorted (case_blanks @ case_cond) in
+  let process cands = List.map add_rhs_as_lhs (check_cands cands) in
   match rule_cands with
-    | Aux.Left cands -> Aux.Left (check_cands cands)
+    | Aux.Left cands -> Aux.Left (process cands)
     | Aux.Right cands ->
-      Aux.Right (List.map (fun (p,cands) -> p, check_cands cands) cands)
+      Aux.Right (List.map (fun (p,cands) -> p, process cands) cands)
 
 
 exception Not_turn_based
@@ -1422,7 +1475,64 @@
           intersects
   ) defined_rels
 
+(* Representing rule candidates as (rule) clauses. *)
+let encode_rule_cands_in_clauses rule_cands clauses =
+  let rule_cl_i = ref 0 in
+  let more_cls = ref [] in
+  let proc_cand (legal_tup, rhs_tup, cond) =
+    let i = !rule_cl_i in
+    incr rule_cl_i;
+    more_cls := (("rule clause", [|Const (string_of_int i)|]), cond)::
+      !more_cls;
+    legal_tup, rhs_tup, i in
+  let rule_cands =
+    match rule_cands with
+      | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
+      | Aux.Right cands -> Aux.Right
+        (List.map (fun (p,cands) -> p, List.map proc_cand cands)
+           cands) in
+  rule_cands, !more_cls @ clauses
 
+
+let decode_rule_cands_of_clauses rule_cands clauses =
+  let rule_cls, clauses = Aux.partition_map
+    (function
+      | ("rule clause", [|Const i|]), cond ->
+        Aux.Left (int_of_string i, cond)
+      | cl -> Aux.Right cl)
+    clauses in
+  let proc_cand (legal_tup, rhs_tup, cond_i) =
+    legal_tup, rhs_tup, List.assoc cond_i rule_cls in
+  let rule_cands =
+    match rule_cands with
+      | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
+      | Aux.Right cands -> Aux.Right
+        (List.map (fun (p,cands) -> p, List.map proc_cand cands)
+           cands) in
+  rule_cands, clauses
+
+let generate_playout_states program players =
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: generating states...\n%!";
+    (* GDL.debug_level := 4; *)
+  );
+  (* }}} *)
+  let states = Aux.fold_n
+    (fun acc ->
+      let _, states =
+        playout_prolog ~aggregate:false players !playout_horizon
+          program in
+      states @ acc) [] !playouts_for_rule_filtering in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    (* GDL.debug_level := 0; *)
+    Printf.printf "translate_game: generated %d states.\n%!"
+      (List.length states)
+  );
+  (* }}} *)
+  states
+
 (* [playing_as] is only used for building move translation data, the
    translation is independent of the selected player. *)
 let translate_game ~playing_as clauses =
@@ -1462,13 +1572,16 @@
     (List.map (fun ((rel,args),body as cl)->
       if rel = "frame next" then ("next", args), body
       else cl) clauses) in
+  let playout_states = generate_playout_states program players in
   let turn_data =
     try Some (check_turn_based players program)
     with Not_turn_based -> None in
   let rule_cands, is_concurrent =
-    create_rule_cands turn_data used_vars f_paths next_cls clauses in
+    create_rule_cands turn_data used_vars f_paths
+      program playout_states next_cls clauses in
   let rule_cands =
-    filter_rule_cands players program rule_cands in
+    filter_rule_cands players f_paths program playout_states rule_cands in
+
   let term_arities = Aux.unique_sorted
     (Aux.concat_map term_arities ground_state_terms) in
   let defined_rel_arities = List.map
@@ -1482,13 +1595,24 @@
     all_paths = paths_union f_paths m_paths;
     mask_reps = mask_reps;
     defined_rels = defined_rels;
-    defrel_arg_mode = ref [];           (* built in TranslateFormula *)
+    defrel_argpaths = [];           (* built in TranslateFormula *)
     term_arities = term_arities;
     rel_default_path =
       transl_arg_type_no_side defined_rel_arities init_state program
         (ground_at m_paths);
   } in
-  let defined_rels = TranslateFormula.build_defrels transl_data clauses in
+  (* Building defined rels needs to happen between creating rule
+     candidates and rule translation, so that transformed clauses don't
+     affect the GDL-side of construction, but are ready for
+     precondition formula translation. *)
+  (* Transform the rule conditions as well so they can be translated. *)
+  let rule_cands, clauses =
+    encode_rule_cands_in_clauses rule_cands clauses in
+  let clauses, defined_rels =
+    TranslateFormula.build_defrels transl_data clauses in
+  let rule_cands, clauses =
+    decode_rule_cands_of_clauses rule_cands clauses in
+
   let player_names = Array.to_list
     (Array.mapi (fun i p -> term_to_name p, i) players) in
   (* possibly update the structure with a control element and predicate *)

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2011-08-21 10:27:37 UTC (rev 1543)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2011-08-26 14:33:35 UTC (rev 1544)
@@ -177,17 +177,17 @@
     (fun () ->
       game_test_case ~game_name:"breakthrough" ~player:"white"
         ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"move_x239_y257_x238_y256_0"
+        ~loc0_rule_name:"move_x2_y3_x3_y4_noop"
         ~loc0_emb:[
-          "cellholds_x239_y257__blank_", "cellholds_2_2_MV1";
-          "cellholds_x238_y256__blank_", "cellholds_1_3_MV1";
-          "control__blank_", "control_MV1"]
+          "cellholds_x2_y3__BLANK_", "cellholds_2_2__BLANK_";
+          "cellholds_x3_y4__BLANK_", "cellholds_1_3__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
         ~loc0_move:"(move 2 2 1 3)" ~loc0_noop:"noop" ~loc1:1
-        ~loc1_rule_name:"move_x467_y497_x466_y496_1"
+        ~loc1_rule_name:"noop_move_x7_y9_x8_y10"
         ~loc1_emb:[
-          "cellholds_x467_y497__blank_", "cellholds_7_7_MV1";
-          "cellholds_x466_y496__blank_", "cellholds_6_6_MV1";
-          "control__blank_", "control_MV1"]
+          "cellholds_x7_y9__blank_", "cellholds_7_7__BLANK_";
+          "cellholds_x8_y10__blank_", "cellholds_6_6__BLANK_";
+          "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(move 7 7 6 6)"
     );
   
@@ -226,17 +226,17 @@
 let a () =
       game_test_case ~game_name:"breakthrough" ~player:"white"
         ~own_plnum:0 ~opponent_plnum:1
-        ~loc0_rule_name:"move_x239_y257_x238_y256_0"
+        ~loc0_rule_name:"move_x2_y3_x3_y4_noop"
         ~loc0_emb:[
-          "cellholds_x239_y257__blank_", "cellholds_2_2_MV1";
-          "cellholds_x238_y256__blank_", "cellholds_1_3_MV1";
-          "control__blank_", "control_MV1"]
+          "cellholds_x2_y3__BLANK_", "cellholds_2_2__BLANK_";
+          "cellholds_x3_y4__BLANK_", "cellholds_1_3__BLANK_";
+    ...
 
[truncated message content]