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

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

Revision: 1618
          http://toss.svn.sourceforge.net/toss/?rev=1618&view=rev
Author:   lukstafi
Date:     2011-11-01 09:32:09 +0000 (Tue, 01 Nov 2011)
Log Message:
-----------
GDL translation: enhancing erasure clauses, initial commit. Not verified, tests not updated yet.

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

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/Arena/DiscreteRule.ml	2011-11-01 09:32:09 UTC (rev 1618)
@@ -1060,7 +1060,7 @@
    [nondistinct_pairs] connects elements that are potentially not
    distinct, thus weakening the "embedding" requirement into
    "homomorphism" requirement for matching a rule. *)
-let translate_from_precond ~precond ~add ~nondistinct ~emb_rels
+let translate_from_precond ~precond ~add ?(del=[]) ~nondistinct ~emb_rels
     ~signat ~struc_elems =
   let rhs_names = Aux.unique_sorted
     (Aux.concat_map (fun (_,arg) -> Array.to_list arg) add) in
@@ -1139,6 +1139,36 @@
         List.map (fun args -> "_opt_"^rel, args) tups
       with Not_found -> [])
       emb_rels in
+  let opt_rhs =
+    Aux.concat_map (fun rel ->
+      try
+        let arity = List.assoc rel signat in
+        let tups =
+          List.map
+            Array.of_list
+            (*Aux.array_map_of_list Formula.var_str*)
+            (Aux.product (
+              Aux.fold_n (fun acc -> struc_elems::acc) [] arity)) in
+        let modified =
+          Aux.assoc_all rel add @ Aux.assoc_all rel del in
+        (* {{{ log entry *)
+        if !debug_level > 4 then (
+          Printf.printf
+            "translate_from_precond: RHS _opt_%s -- modified %s -- \
+                 remaining %s\n%!" rel
+            (String.concat "; "
+               (List.map (fun args ->
+                 String.concat " " (Array.to_list args)) modified))
+            (String.concat "; "
+               (List.map (fun args ->
+                 String.concat " " (Array.to_list args))
+                  (Aux.list_diff tups modified)))
+        );
+        (* }}} *)
+        let tups = Aux.list_diff tups modified in
+        List.map (fun args -> "_opt_"^rel, args) tups
+      with Not_found -> [])
+      emb_rels in
   let rhs_struc, struc_elems =
     List.fold_left (fun (rhs_struc, struc_elems) name ->
       let rhs_struc, elem =
@@ -1150,6 +1180,7 @@
       (Array.map (fun n -> List.assoc n struc_elems) args)) in
   let lhs_struc = rhs_struc in
   let rhs_struc = add_rels rhs_struc add in
+  let rhs_struc = add_rels rhs_struc opt_rhs in
   let lhs_struc = add_rels lhs_struc posi_s in
   let lhs_struc = add_rels lhs_struc opt_s in
   let lhs_struc = add_rels lhs_struc

Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/Arena/DiscreteRule.mli	2011-11-01 09:32:09 UTC (rev 1618)
@@ -148,6 +148,7 @@
    "homomorphism" requirement for matching a rule. *)
 val translate_from_precond :
   precond:Formula.formula -> add:(string * string array) list ->
+   ?del:(string * string array) list ->
   nondistinct:string array list ->
   (* del:(string * string array) list -> *)
   emb_rels:string list -> signat:(string * int) list ->

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/GGP/GDL.ml	2011-11-01 09:32:09 UTC (rev 1618)
@@ -1526,6 +1526,13 @@
     | _ -> [] in
   Aux.concat_map aux body
 
+let pos_state_terms body =
+  let rec aux = function
+    | Pos (True t) -> [t]
+    | Disj ls -> Aux.concat_map aux ls
+    | _ -> [] in
+  Aux.concat_map aux body
+
 let rec term_arities =
   function
     | Func (rel, args) ->

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/GGP/GDL.mli	2011-11-01 09:32:09 UTC (rev 1618)
@@ -174,6 +174,7 @@
 val term_to_name : ?nested:bool -> term -> string
 
 val state_terms : literal list -> term list
+val pos_state_terms : literal list -> term list
 val term_arities : term -> (string * int) list
 
 val atom_str : atom -> string

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-11-01 09:32:09 UTC (rev 1618)
@@ -91,14 +91,6 @@
     literals). *)
 let filter_possibly_redundant = ref true
 
-(** When [require_all_w_does] is true, rule generation is optimized by
-    requiring all "next" clauses that match a given "legal/does" term
-    -- that have a "does" atom -- be present in a rule. Setting to
-    true violates correctness for games like "asteroids" where a
-    single "(turn clock)" legal term is used for different headings
-    which have different "next" clauses. *)
-let require_all_w_does = ref false
-
 (** When true, keep only rule candidates with maximal sets of clauses. *)
 let filter_maximal_rules = ref true
 
@@ -116,7 +108,8 @@
      (then ordered in the same way as players),
      we call its parameters "fixed variables" as they are provided
      externally *)
-  rhs_add : (string * string array) list;
+  rule_add : (string * string array) list;
+  rule_del : (string * string array) list;
   struc_elems : string list;
   (* the elements of LHS/RHS structures, corresponding to the "next"
      terms *)
@@ -1200,8 +1193,13 @@
   init_state, struc, ground_state_terms, elem_term_map,
   term_arities, argpaths
 
+(* The [Erasure_cl_OK] clauses do not have unfixed variables. The
+   [Erasure_cl_inst] stores the unfixed-variable-dependent part
+   separately, already instantiated. *)
+type cl_type =
+  | Legal_cl | Next_cl | Erasure_cl_OK
+  | Erasure_cl_inst of (term * literal list) list
 
-
 (* substitute a "next" clause with frame info *)
 let subst_fnextcl sb (head, frame, body) =
   subst sb head, frame, subst_literals sb body
@@ -1304,14 +1302,9 @@
        the rewrite rule. *)
     List.map (fun (sb, _, n_cls) ->
       let n_cls = List.map (fun (head,frame,body) ->
-        if List.exists
-          (function Pos (Does _) -> true | _ -> false) body
-        then
-          head, (frame, !require_all_w_does),
+          head, frame,
           List.filter
-            (function Pos (Does _) -> false | _ -> true) body
-        else
-          head, (frame, false), body) n_cls in
+            (function Pos (Does _) -> false | _ -> true) body) n_cls in
       sb, legal_tup, n_cls) cl_tups in
   Aux.concat_map move_clauses legal_tuples
 
@@ -1325,9 +1318,11 @@
       (String.concat ", " (Aux.Strings.elements fixed_vars))
   );
   (* }}} *)
-  let frame_cls =
-    Aux.map_some (fun (s, (frame, _), body) ->
-      if frame then Some (s, body) else None) next_cls in
+  let frame_cls, move_cl_bodies =
+    Aux.partition_map (fun (s, frame, body) ->
+      if frame then Aux.Left (s, body) else Aux.Right body) next_cls in
+  let move_cl_pos_terms =
+    Aux.concat_map pos_state_terms move_cl_bodies in
   (* two passes to ensure coverage and maximality *)
   (* Treating fixed-vars as consts, by substituting them with
      Const, and later substituting-back Var *)
@@ -1392,40 +1387,50 @@
       let nbodies = negate_bodies bodies in
       List.map
         (fun (nsb, b) ->
-          simult_subst f_paths blank (subst nsb s),
-          Aux.unique_sorted b)
+          let s = subst nsb s in
+          s, Aux.unique_sorted (Pos (True s) :: b))
         nbodies
     ) frames in
-  (* Remove erasure clauses that still have free variables, because
-     after negation they have universal interpretation. *)
-  let erasure_cls = List.filter
-    (fun (s, body) ->
-      let cl_vars = clause_vars (("erasure",[|s|]), body) in
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        Printf.printf "ERASURE: %s with vars %s\nbody: %s\n%!"
-          (term_str s)
-          (String.concat ", " (Aux.Strings.elements cl_vars))
-          (String.concat " " (List.map literal_str body))
-      );
-      (* }}} *)
-      Aux.Strings.is_empty cl_vars)
-    (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
-  let erasure_cls = List.map
-    (subst_consts_clause fixed_to_var)
-    (List.map (fun (s,body)->("erasure next",[|s|]),body) erasure_cls) in
-  (* Erasure clauses are considered as not having "does" atoms,
-     although of course the frame clauses did have "does" atoms. *)
-  let erasure_cls =
-    List.map (fun ((_,h),body) -> h.(0),false,body) erasure_cls in
+  (* Erasure clauses with unfixed variables need to be instantiated
+     against the body of remaining move clauses -- but after selecting
+     them for rule candidates. *)
+  let erasure_cls = Aux.map_some
+    (fun (s, body) ->
+      let local_ex_vars = term_vars s in
+      let local_uni_vars = Aux.Strings.diff
+        (literals_vars body) local_ex_vars in
+      if Aux.Strings.is_empty local_uni_vars then
+        let body, local_body = List.partition
+          (fun lit -> Aux.Strings.is_empty (literals_vars [lit]))
+          body in
+        let kind =
+          if Aux.Strings.is_empty local_ex_vars then Erasure_cl_OK
+          else
+            let sbs = Aux.map_try
+              (fun t -> unify [] [s] [t]) move_cl_pos_terms in
+            let local = List.map
+              (fun sb -> subst_consts fixed_to_var (subst sb s),
+                subst_consts_literals fixed_to_var
+                  (subst_literals sb local_body)) sbs in
+            Erasure_cl_inst local in
+        if kind = Erasure_cl_inst [] then None
+        else
+          Some (
+            subst_consts fixed_to_var s, kind,
+            subst_consts_literals fixed_to_var body)
+      else None)
+    (Aux.unique_sorted erasure_cls) in
+
   (* {{{ log entry *)
   if !debug_level > 2 then (
     Printf.printf "add_erasure_clauses: all erasure clauses --\n%!";
-    let print_erasure (s, _, body) =
-      Printf.printf "ERASURE: %s <== %s\n%!" (term_str s)
+    let print_erasure (s, kind, body) =
+      Printf.printf "ERASURE: %s %s <== %s\n%!"
+        (if kind = Erasure_cl_OK then " OK " else "inst") (term_str s)
         (String.concat " " (List.map literal_str body)) in
     List.iter print_erasure erasure_cls; flush stdout;
   );
@@ -1443,8 +1448,10 @@
   );
   (* }}} *)
   let next_cls =
-    Aux.map_some (fun (s, (frame, required), body) ->
-      if not frame then Some (s, required, body) else None) next_cls in
+    Aux.map_some (fun (s, frame, body) ->
+      if not frame then
+        Some (s, Next_cl, body)
+      else None) next_cls in
   legal_tup, next_cls @ erasure_cls
 
 
@@ -1602,6 +1609,34 @@
 let remove_local_vars gvars lits =
   List.filter (fun l -> Aux.Strings.subset (literals_vars [l]) gvars) lits
 
+let split_rule_cand rule_cls =
+  let regular_cls, erasure_cls = Aux.partition_map
+    (function
+      | h, Erasure_cl_OK, body -> Aux.Right (Aux.Left (h, body))
+      | h, Erasure_cl_inst local, body -> Aux.Right (Aux.Right (local, body))
+      | h, _, body -> Aux.Left (h, body))
+    rule_cls in
+  let pos_rhs, conds = List.split regular_cls in
+  let erasure_OK, erasure_local = Aux.partition_choice erasure_cls in
+  let neg_rhs, more_conds = List.split erasure_OK in
+  let cond = List.concat (more_conds @ conds) in
+  let cond_sterms = pos_state_terms cond in
+  let erasure_loc_cls = Aux.concat_map
+    (fun (local, body) ->
+      Aux.map_some
+        (fun (h, loc_body) ->
+          if List.mem h cond_sterms then Some (h, loc_body @ body)
+          else None)
+        local)
+    erasure_local in
+  let more_neg_rhs, more_conds = List.split erasure_loc_cls in
+  let cond = List.concat (more_conds @ conds) in
+  let pos_rhs =
+    Aux.list_remove ignore_rhs (Aux.unique_sorted pos_rhs) in
+  pos_rhs,
+  Aux.unique_sorted (more_neg_rhs @ neg_rhs),
+  Aux.unique_sorted cond
+
 (* Assign rule clauses to rule cases, i.e. candidates for Toss
    rules. Collect the conditions and RHS state terms together. Frame
    clauses are already processed into erasure clauses. Rule clauses
@@ -1646,8 +1681,10 @@
   let counter_cls, rule_cls =
     split_counter_rule_cls counters num_functors rule_cls in
   let required_cls = Aux.map_some
-    (fun (h, required, body) ->
-      if required then Some (h, body) else None) rule_cls in
+    (fun (h, kind, body) ->
+      if kind = Legal_cl then Some (h, body)
+      else None)
+    rule_cls in
   let required_body = Aux.concat_map snd required_cls in
   (* {{{ log entry *)
   if !debug_level > 3 then (
@@ -1655,9 +1692,8 @@
       (literals_str required_body)
   );
   (* }}} *)
-  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 (_, kind, _) -> kind <> Legal_cl) rule_cls in  
   let forbidden_lits = Aux.unique_sorted
     (Aux.concat_map
        (fun (_, body) -> Aux.map_some (function
@@ -1666,73 +1702,83 @@
          | Neg a -> Some (Pos a)
          | _ -> None) body) required_cls) in
   let unrequired_cls = List.filter
-    (fun (_, body) ->
+    (fun (_, _, body) ->
       not (List.exists (fun flit -> List.mem flit body)
              forbidden_lits))
     unrequired_cls in
-  let unrequired_cls = List.filter
-    (fun (_, unreq_body) ->
-      let static_goal = optimize_goal ~testground
-        (keep_rels static_rels (required_body @ unreq_body)) in
+  let filter_goal goal =
+    let static_goal = optimize_goal ~testground
+      (keep_rels static_rels goal) in
       (* {{{ log entry *)
-      if !debug_level > 3 then (
-        Printf.printf
-          "\nrule_cases: checking unrequired %s\nstatic_goal=%s\n%!"
-          (String.concat " "(List.map literal_str unreq_body))
-          (String.concat " "(List.map literal_str static_goal));
-      );
+    if !debug_level > 3 then (
+      Printf.printf
+        "\nrule_cases: checking static_goal=%s\goal=%s\n%!"
+        (String.concat " "(List.map literal_str static_goal))
+        (String.concat " "(List.map literal_str goal));
+    );
       (* }}} *)
-      let res =
-        run_prolog_check_goal static_goal program &&
-          let goal = optimize_goal ~testground
-            (required_body @ unreq_body) in
+    let res =
+      run_prolog_check_goal static_goal program &&
+        let goal = optimize_goal ~testground goal in
           (* {{{ log entry *)
-          if !debug_level > 3 then (
-            Printf.printf
-              "goal=%s\n%!" (String.concat " "(List.map literal_str goal))
-          );
+        if !debug_level > 3 then (
+          Printf.printf
+            "goal=%s\n%!" (String.concat " "(List.map literal_str goal))
+        );
           (* }}} *)
-          List.exists
-            (fun state ->
+        List.exists
+          (fun state ->
               (* {{{ log entry *)
-              if !debug_level > 3 then Printf.printf ".%!";
+            if !debug_level > 3 then Printf.printf ".%!";
               (* }}} *)
-              run_prolog_check_goal goal
-                (replace_rel_in_program "true" (state_cls state) program))
-            playout_states in
+            run_prolog_check_goal goal
+              (replace_rel_in_program "true" (state_cls state) program))
+          playout_states in
       (* {{{ log entry *)
-      if !debug_level > 3 then Printf.printf " %B\n%!" res;
+    if !debug_level > 3 then Printf.printf " %B\n%!" res;
       (* }}} *)
-      res
-    )
+    res in
+  let unrequired_cls = Aux.map_some
+    (function
+      | h, Erasure_cl_inst local, cl_body ->
+        let local = List.filter
+          (fun (head, loc_body) ->
+            filter_goal
+              (Pos (True head)::required_body @ loc_body @ cl_body))
+          local in
+        if local = [] then None
+        else Some (h, Erasure_cl_inst local, cl_body)
+      | _, _, cl_body as cl ->
+        if filter_goal (required_body @ cl_body)
+        then Some cl else None)
     unrequired_cls in
   let req_atoms = List.map
     (function Pos a -> a | Neg a -> a | _ -> assert false)
     forbidden_lits in
   let unreq_atoms = Aux.unique_sorted
     (Aux.concat_map
-       (fun (_, body) -> Aux.map_some (function
+       (fun (_, _, body) -> Aux.map_some (function
          | 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 *)
-    let rule_cls = required_cls @ unrequired_cls in
-    let case_rhs, case_conds = List.split rule_cls in
-    let case_rhs = Aux.list_remove ignore_rhs case_rhs in
+    let rule_cls = Aux.map_prepend unrequired_cls
+      (fun (h,b) -> h, Legal_cl, b) required_cls in
+    let case_pos_rhs, case_neg_rhs, case_cond =
+      split_rule_cand rule_cls in
     (* {{{ log entry *)
     if !debug_level > 2 then (
       Printf.printf "rule_cases: single partition\n%!";
     );
     (* }}} *)
     [Aux.Ints.singleton 0,
-     (Aux.unique_sorted case_rhs, counter_cls,
-      Aux.unique_sorted (List.concat case_conds))]
+     (case_pos_rhs, case_neg_rhs, counter_cls, case_cond)]
   else
     let patterns =
       let unrequired_cls = Array.of_list unrequired_cls in
       List.map (fun a ->
-        Array.mapi (fun i (_, body) ->
+        Array.mapi (fun i (_, _, body) ->
           if List.mem (Neg a) body then -1
           else if List.mem (Pos a) body then 1
           else 0
@@ -1751,11 +1797,15 @@
           (Aux.array_fprint (fun ch -> Printf.fprintf ch "%+d")) pattern
           (String.concat " " (List.map atom_str atoms)) in
       List.iter print_pat patterns;
-      let print_cl i (h, body) =
-        Printf.printf "%d: %s <== %s\n%!" i (term_str h)
+      let print_cl i (h, kind, body) =
+        Printf.printf "%d: (%s) %s <== %s\n%!" i
+          (match kind with Erasure_cl_OK | Erasure_cl_inst _ -> "eras"
+            | _ -> "move")
+          (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);
+      Array.iteri print_cl (Aux.array_map_of_list
+                              (fun (h,b)->h,Legal_cl,b) required_cls);
       Printf.printf "rule_cases: split on cls --\n%!";
       Array.iteri print_cl (Array.of_list unrequired_cls)
     );
@@ -1766,7 +1816,7 @@
       let separation_cond =
         List.map (fun (a,b) -> if b then Pos a else Neg a) choice in
       let case =
-        Aux.array_mapi_some (fun i (_, body as cl) ->
+        Aux.array_mapi_some (fun i (_, _, body as cl) ->
           if
             List.for_all (fun (a,b) ->
               if b then                     (* atom not excluded *)
@@ -1781,14 +1831,12 @@
       Aux.ints_of_list ids, separation_cond, cls in
     let cases = List.map rule_case choices in
     let process_case (ids, separation_cond, case_cls) =
-      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 (Aux.unique_sorted case_rhs) in
-      let case_conds =
-        Aux.unique_sorted (List.concat case_conds) in
+      let case_cls = Aux.map_prepend case_cls
+        (fun (h,b) -> h, Legal_cl, b) required_cls in
+      let case_pos_rhs, case_neg_rhs, case_cond =
+        split_rule_cand case_cls in
       let separation_cond =
-        remove_local_vars (literals_vars case_conds) separation_cond in
+        remove_local_vars (literals_vars case_cond) separation_cond in
       (* {{{ log entry *)
       if !debug_level > 3 then (
         let cond_upd_str (cond, update) =
@@ -1798,15 +1846,16 @@
           counter^": "^String.concat ", "
             (List.map cond_upd_str cond_updates) in
         Printf.printf
-          "\nRCAND:\nsep_cond: %s\nRHS: %s\nCOUNTER_CLs: %s\ncase_conds: %s\n\n%!"
+          "\nRCAND:\nsep_cond: %s\nPOS-RHS: %s\nNEG-RHS: %s\nCOUNTER_CLs: %s\ncase_cond: %s\n\n%!"
           (String.concat " " (List.map literal_str separation_cond))
-          (String.concat " " (List.map term_str case_rhs))
+          (String.concat " " (List.map term_str case_pos_rhs))
+          (String.concat " " (List.map term_str case_neg_rhs))
           (String.concat "; " (List.map counters_str counter_cls))
-          (String.concat " " (List.map literal_str case_conds))
+          (String.concat " " (List.map literal_str case_cond))
       );
       (* }}} *)
       let case_cond =
-        Aux.unique_sorted (separation_cond @ case_conds) in
+        Aux.unique_sorted (separation_cond @ case_cond) in
       let counter_cls = List.map
         (fun (f, brs) ->
           let brs = List.map
@@ -1816,7 +1865,7 @@
             brs in
           f, brs)
         counter_cls in      
-      ids, (case_rhs, counter_cls, case_cond) in
+      ids, (case_pos_rhs, case_neg_rhs, counter_cls, case_cond) in
     let res = List.map process_case cases in
     (* {{{ log entry *)
     if !debug_level > 2 then (
@@ -1827,9 +1876,11 @@
         counter^": "^String.concat ", "
           (List.map cond_upd_str cond_updates) in
       Printf.printf "rule_cases: next clauses partitioned into rules\n%!";
-      let print_case  i (ids, (case_rhs, counter_cls, case_cond)) =
-        Printf.printf "\nRCAND: #%d\nRHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
-          (String.concat " " (List.map term_str case_rhs))
+      let print_case  i
+          (ids, (case_pos_rhs, case_neg_rhs, counter_cls, case_cond)) =
+        Printf.printf "\nRCAND: #%d\nPOS-RHS: %s\nNEG-RHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
+          (String.concat " " (List.map term_str case_pos_rhs))
+          (String.concat " " (List.map term_str case_neg_rhs))
           (String.concat "; " (List.map counters_str counter_cls))
           (String.concat " " (List.map literal_str case_cond)) in
       Array.iteri print_case (Array.of_list res)
@@ -1838,6 +1889,7 @@
     res
 
 
+
 let process_rule_cands used_vars f_paths next_cls mode
     players_wo_env legal_tuples =
   let move_tups =
@@ -1850,9 +1902,9 @@
   if !debug_level > 2 then (
     Printf.printf
       "process_rule_cands: move tuples before adding erasure cls--\n%!";
-    let nclause_str (rhs, (is_frame, required), body) =
+    let nclause_str (rhs, is_frame, body) =
       Printf.printf
-        "%s <=fr:%B;req:%B= %s\n%!"(term_str rhs) is_frame required
+        "%s <=fr:%B= %s\n%!"(term_str rhs) is_frame
         (String.concat " "(List.map literal_str body)) in
     let print_tup i (legal_tup, n_cls) =
       Printf.printf "CAND: #%d\nlegal_tup: %s\n%!" i
@@ -1881,30 +1933,30 @@
     (fun v -> v, Const v) fixed_vars in
   let legal_lits = subst_literals var_to_fixed legal_lits in
   let next_cls = List.map               (* fix [legal_tup] vars in "next" *)
-    (fun (head, req, body) ->
-      subst_consts var_to_fixed head, req,
+    (fun (head, kind, body) ->
+      subst_consts var_to_fixed head, kind,
       subst_consts_literals var_to_fixed body)
     next_cls in
   (* Filter-out redundant conditions. Note that unfixed variables in
      "next" clauses are local to clauses. *)
   let next_cls = List.map
-    (fun (head, req, body) ->
+    (fun (head, kind, body) ->
       let sb, body = filter_redundant legal_lits body in
-      subst sb head, req, subst_literals sb body)
+      subst sb head, kind, subst_literals sb body)
     next_cls in
   let fixed_to_var = List.map
     (fun v -> v, Var v) fixed_vars in
   let next_cls = List.map
-    (fun (head, req, body) ->
-      subst_consts fixed_to_var head, req,
+    (fun (head, kind, body) ->
+      subst_consts fixed_to_var head, kind,
       subst_consts_literals fixed_to_var body)
     next_cls in
   
-  let legal_cls = List.map (* required clauses *)
-    (fun body -> ignore_rhs, true, body) legal_conds in
+  let legal_cls = List.map
+    (fun body -> ignore_rhs, Legal_cl, body) legal_conds in
   List.map
-    (fun (ids, (case_rhs, updates, case_cond)) ->
-      ids, (legal_tup, case_rhs, updates, case_cond))
+    (fun (ids, (pos_rhs, neg_rhs, updates, case_cond)) ->
+      ids, (legal_tup, pos_rhs, neg_rhs, updates, case_cond))
     (rule_cases counters num_functors static_rels testground program
        playout_states (legal_cls @ next_cls))
 
@@ -2083,9 +2135,10 @@
     let counters_str (counter, cond_updates) =
       counter^": "^String.concat ", "
         (List.map cond_upd_str cond_updates) in
-    let print_rcand i (_, (_, case_rhs, counter_cls, case_cond)) =
-      Printf.printf "\nRCAND: #%d\nRHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
-        (String.concat " " (List.map term_str case_rhs))
+    let print_rcand i (_, (_, pos_rhs, neg_rhs, counter_cls, case_cond)) =
+      Printf.printf "\nRCAND: #%d\nPOS-RHS: %s\nNEG-RHS: %s\nCOUNTER_CLs: %s\nLHS: %s\n%!" i
+        (String.concat " " (List.map term_str pos_rhs))
+        (String.concat " " (List.map term_str neg_rhs))
         (String.concat "; " (List.map counters_str counter_cls))
         (String.concat " " (List.map literal_str case_cond)) in
     let print_rcands (player, rcands) =
@@ -2106,21 +2159,21 @@
     playout_states rule_cands =
   let check_cands cands =
     let cands =
-      List.filter (fun (_, (_, _, _, case_conds)) ->
+      List.filter (fun (_, (_, _, _, _, case_cond)) ->
         (* {{{ log entry *)
         if !debug_level > 1 then (
           Printf.printf "check_cands: cond %s%!"
-            (String.concat " "(List.map literal_str case_conds))
+            (String.concat " "(List.map literal_str case_cond))
         );
         (* }}} *)      
         let res =
-          run_prolog_check_goal (keep_rels static_rels case_conds) program
+          run_prolog_check_goal (keep_rels static_rels case_cond) program
           && List.exists
             (fun state ->
               (* {{{ log entry *)
               if !debug_level > 1 then Printf.printf ".%!";
               (* }}} *)
-              run_prolog_check_goal case_conds
+              run_prolog_check_goal case_cond
                 (replace_rel_in_program "true" (state_cls state) program))
             playout_states in
         (* {{{ log entry *)
@@ -2134,10 +2187,11 @@
       (Aux.maximal_unique
          (fun (s1, _) (s2, _) -> Aux.Ints.subset s1 s2)
          cands) in
-  let add_rhs_as_lhs (legal_tup, case_rhs, updates, case_cond) =
+  let add_rhs_as_lhs (legal_tup, pos_rhs, neg_rhs, updates, case_cond) =
     let case_blanks = List.map
-      (fun s -> Pos (True (simult_subst f_paths blank s))) case_rhs in
-    legal_tup, case_rhs, updates,
+      (fun s -> Pos (True (simult_subst f_paths blank s)))
+      (pos_rhs @ neg_rhs) in
+    legal_tup, pos_rhs, neg_rhs, updates,
     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
@@ -2300,7 +2354,7 @@
 let build_toss_rule num_functions transl_data rule_names
     framed_fluents f_paths struc fluents
     synch_elems synch_precond synch_postcond
-    (legal_tuple, case_rhs, counter_cls, case_cond) =
+    (legal_tuple, pos_rhs, neg_rhs, counter_cls, case_cond) =
   let rname =
     if legal_tuple = [] then term_to_name env_player
     else String.concat "_" (List.map term_to_name legal_tuple) in
@@ -2327,7 +2381,7 @@
       (Formula.str (Formula.And synch_precond)) (Formula.str case_precond)
   );
   (* }}} *)
-  let rhs_add = Aux.concat_map
+  let extract_tups = Aux.concat_map
     (fun sterm ->
       let s_subterms =
         map_paths (fun path subt -> subt, path)
@@ -2338,15 +2392,15 @@
       let vartup = [|term_to_name (blank_out transl_data sterm)|] in
       List.map (fun (subt, path) ->
         pred_on_path_subterm path subt, vartup)
-        s_subterms)
-    case_rhs in
-  let rhs_add = synch_postcond @ rhs_add in
-  (* let rhs_add = if counter_cls = [] then rhs_add else  *)
+        s_subterms) in
+  let add = synch_postcond @ extract_tups pos_rhs in
+  (* let add = if counter_cls = [] then add else  *)
+  let del = extract_tups neg_rhs in
   let signat = Structure.rel_signature struc in
   (* we find which rule results should have their old values erased,
      in cases not covered by erasure clauses *)
   let used_fluents = Aux.concat_map
-    (map_paths (fun p subt -> p, subt) f_paths) case_rhs in
+    (map_paths (fun p subt -> p, subt) f_paths) pos_rhs in
   let unframed_fluents = List.filter
     (fun (p, subt) ->
       let f_subts = Aux.assoc_all p framed_fluents in
@@ -2358,7 +2412,7 @@
     (fun st -> List.exists
       (fun (p,subt) -> try at_path st p = subt with Not_found -> false)
       unframed_fluents)
-    (Aux.list_diff (state_terms case_cond) case_rhs) in
+    (Aux.list_diff (state_terms case_cond) pos_rhs) in
   (* {{{ log entry *)
   if !debug_level > 3 then (
     Printf.printf "build_toss_rule: unframed_fluents=%s; unframed_elems=%s\n%!"
@@ -2367,8 +2421,10 @@
       (String.concat ", " (List.map term_str unframed_elems))
   );
   (* }}} *)
+  let all_rhs = pos_rhs @ neg_rhs in
   let struc_elems = List.map
-    (fun sterm -> term_to_name (blank_out transl_data sterm)) case_rhs in
+    (fun sterm -> term_to_name (blank_out transl_data sterm))
+    all_rhs in
   let unframed_elems = List.map
     (fun sterm -> term_to_name (blank_out transl_data sterm))
     unframed_elems in
@@ -2379,7 +2435,7 @@
       (Aux.product [unframed_elems; struc_elems])
     @ List.map (fun (x,y) -> [|x; y|]) (Aux.pairs unframed_elems) in
   let rulevar_terms = Aux.strmap_of_assoc
-    (List.combine struc_elems case_rhs) in
+    (List.combine struc_elems all_rhs) in
   let struc_elems = Aux.unique_sorted
     (synch_elems @ unframed_elems @ struc_elems) in
   let struc_elems =
@@ -2392,15 +2448,16 @@
     let add_str (rel, args) =
       rel^"("^String.concat ", " (Array.to_list args)^")" in
     Printf.printf
-      "build_toss_rule: rhs_add=%s; struc_elems=%s; total precond=\n%s\n\n%!"
-      (String.concat ", "(List.map add_str rhs_add))
+      "build_toss_rule: rule_add=%s; struc_elems=%s; total precond=\n%s\n\n%!"
+      (String.concat ", "(List.map add_str add))
       (String.concat ", " struc_elems)
       (Formula.str precond)
   );
   (* }}} *)
   let discrete =
     DiscreteRule.translate_from_precond ~precond
-      ~add:rhs_add ~nondistinct ~emb_rels:fluents ~signat ~struc_elems in
+      ~add ~del ~nondistinct ~emb_rels:fluents
+      ~signat ~struc_elems in
   let ctx_terms = state_terms case_cond in
   (* {{{ log entry *)
   if !debug_level > 3 && counter_cls <> [] then (
@@ -2426,11 +2483,12 @@
       (fun path -> function Var v -> v, (sterm, path)
         | _ -> assert false)
       (term_paths (function Var _ -> true | _ -> false) sterm) sterm)
-    case_rhs in
+    all_rhs in
   let fixvar_terms = Aux.collect fixvar_terms in
   let tossrule_data = {
     legal_tuple = Array.of_list legal_tuple;
-    rhs_add = rhs_add;
+    rule_add = add;
+    rule_del = del;
     struc_elems = struc_elems;
     fixvar_terms = fixvar_terms;
     rulevar_terms = rulevar_terms;
@@ -2449,7 +2507,7 @@
       (* a rule belongs to a player if other players' legal terms
          in the legal tuple are their noop terms for current location *)
       let loc_rules = Aux.map_some
-        (fun (legal_tup, _, _, _ as rcand) ->
+        (fun (legal_tup, _, _, _, _ as rcand) ->
           let legal_tup = Array.of_list legal_tup in
           if Aux.array_for_alli
             (fun pl noop -> pl = player_num ||
@@ -2673,13 +2731,13 @@
   let proc_counter_upds i (counter, updates) =
     let updates = List.map (proc_update i) updates in
     counter, updates in
-  let proc_cand (legal_tup, rhs_tup, updates, cond) =
+  let proc_cand (legal_tup, pos_tup, neg_tup, updates, cond) =
     let i = !rule_cl_i in
     incr rule_cl_i; rule_upd_j := 0;
     let updates = List.map (proc_counter_upds i) updates in
     more_cls := (("rule clause", [|Const (string_of_int i)|]), cond)::
       !more_cls;
-    legal_tup, rhs_tup, updates, i in
+    legal_tup, pos_tup, neg_tup, updates, i in
   let rule_cands =
     match rule_cands with
       | Aux.Left cands -> Aux.Left (List.map proc_cand cands)
@@ -2706,8 +2764,8 @@
   let proc_counter_upds i (counter, updates) =
     let updates = List.map (proc_update i) updates in
     counter, updates in
-  let proc_cand (legal_tup, rhs_tup, updates, i) =
-    legal_tup, rhs_tup, List.map (proc_counter_upds i) updates,
+  let proc_cand (legal_tup, pos_tup, neg_tup, updates, i) =
+    legal_tup, pos_tup, neg_tup, List.map (proc_counter_upds i) updates,
     List.assoc i rule_cls in
   let rule_cands =
     match rule_cands with
@@ -3025,8 +3083,8 @@
   (* optimize candidates for fast pruning *)
   let rule_cands =
     let process cands = List.map
-      (fun (ids, (legal_tup, rhs_tup, updates, cond)) ->
-        ids, (legal_tup, rhs_tup, updates,
+      (fun (ids, (legal_tup, pos_rhs_tup, neg_rhs_tup, updates, cond)) ->
+        ids, (legal_tup, pos_rhs_tup, neg_rhs_tup, updates,
               optimize_goal ~testground cond))
       cands in
     match rule_cands with

Modified: trunk/Toss/GGP/TranslateGame.mli
===================================================================
--- trunk/Toss/GGP/TranslateGame.mli	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/GGP/TranslateGame.mli	2011-11-01 09:32:09 UTC (rev 1618)
@@ -34,7 +34,8 @@
      (then ordered in the same way as players),
      we call its parameters "fixed variables" as they are provided
      externally *)
-  rhs_add : (string * string array) list;
+  rule_add : (string * string array) list;
+  rule_del : (string * string array) list;
   struc_elems : string list;
   (* the elements of LHS/RHS structures, corresponding to the "next"
      terms *)

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-10-25 21:40:52 UTC (rev 1617)
+++ trunk/Toss/www/reference/reference.tex	2011-11-01 09:32:09 UTC (rev 1618)
@@ -1971,23 +1971,35 @@
 such that 
 \[ \neg( \rho(b_1) \lor \dots \lor \rho(b_{|J|})) \ \equiv \ (e_1 \lor
 e_2 \ldots \lor e_l). \] As the head of each erasure clause we use
-$\rho(s_1) = \dots = \rho(s_{|J|})$, with the one technical change
-that we ignore the fluent paths in this term.  We replace these fluent
-paths with \texttt{BLANK} and thus allow them to be deleted in case
-they are not preserved by other \texttt{next} clauses of the rule. Let
-us denote by $h$ the term $\rho(s_1)$ after the above
-replacement. Finally, we eliminate the clauses that contain variables
-other than the ``fixed variables'' of the \texttt{legal} clauses,
-since after negation they will have universal interpretation (and
-therefore such clause bodies are unlikely to hold). The resulting
-erasure clauses are $\calE_{\ol{\calC}, \ol{\calN}}(J) = \{
-\mathtt{(<=\ h\ e_i)} \  | \  FVar(\mathtt{(<=\ h\ e_i)}) \setminus
-FVar(\ol{\calC}) = \emptyset, i = 1,\dots,l \}$, and we write
-$\calE_{\ol{\calC}, \ol{\calN}}$ for the union of all
-$\calE_{\ol{\calC}, \ol{\calN}}(J)$, \ie for the set of all
-$\ol{\calC}, \ol{\calN}$ erasure clauses.
+$\rho(s_1) = \dots = \rho(s_{|J|})$.
 
+Erasure clauses that contain variables other than the ``fixed
+variables'' of the \texttt{legal} clauses are problematic. If such
+``unfixed'' variables appear in the head, the erasure clause should
+apply to all instantiating variables in a single application of the
+rewrite rule, which is too difficult to achieve using Toss
+semantics. Rather, we match $\rho(s_1)$ against positive atoms in the
+bodies of the move clauses and add an instantiated clause for each
+match. If such ``unfixed'' variables occur only in the body, they
+should be quantified universally. We just ignore erasure clauses
+containing unfixed variables that occur only in the body.
 
+The resulting erasure clauses are
+
+\begin{align*}
+\calE_{\ol{\calC}, \ol{\calN}}(J) =
+\{ (\mathtt{<=}\ \sigma (\rho (s_1))\ \sigma (e_i)) \ | & \ \sigma
+\textit{ unifies } \rho(s_1) \textit{ with a pos. atom of }
+\ \ol{\calN} \\ & \lor (\sigma = id \land FVar(\mathtt{(<=\ h\ e_i)}) \setminus
+FVar(\ol{\calC}) = \emptyset), \\ & i = 1, \dots , l \}
+\end{align*}
+
+and we write $\calE_{\ol{\calC},
+  \ol{\calN}}$ for the union of all $\calE_{\ol{\calC},
+  \ol{\calN}}(J)$, \ie for the set of all $\ol{\calC}, \ol{\calN}$
+erasure clauses.
+
+
 \begin{example}
 In our example, $\calN_3$ and its counterpart for the other player
 are the only frame clauses in $G$. After negation, $\sigma(\calN_3)$
@@ -2076,20 +2088,16 @@
 described in Section~\ref{subsec-translate}.
 
 In the second step, we build a Toss rewrite rule itself. From the
-heads of rule clauses of a rule candidate, we build the
-$\frakR$-structure: each \texttt{next} term, with its fluent paths
-replaced by \texttt{BLANK} (\ie for $(\mathtt{next} \ e)$, the term
-$\mathtt{BL}(s)$), is an $\frakR$ element, and the fluent predicates
-holding for the \texttt{next} state terms are the relations of
-$\frakR$; we add atoms $(\mathtt{true} \ \mathtt{BL}(s))$ to the
-matching condition, not to lose any facts constraining the rule
-structure elements (but only after the rule candidates are checked for
-satisfiability). The $\frakL$-structure and precondition of the Toss
-rule is built from the matching condition, based on elements of
-$\frakR$. Quantification over variables corresponding to $\frakR$
-elements (which are the same as $\frakL$ elements) is dropped, and
-atoms involving only these variables and not occurring inside
-disjunctions are extracted to be relations tuples in $\frakL$.
+heads of the move clauses of a rule candidate, we build the
+\texttt{ADD} part of the rule effect; from heads of the erasure
+clauses we build the \texttt{DELETE} part. We add ``blanked-out''
+heads of the clauses (atoms $(\mathtt{true} \ \mathtt{BL}(s))$ for
+clause heads $(\mathtt{next}\ s)$) to the matching condition, not to
+lose any facts constraining the rule structure elements (but only
+after the rule candidates are checked for satisfiability). The
+precondition of the Toss rule is built from the matching
+condition. Quantification in the precondition over variables occurring
+in the \texttt{ADD} and \texttt{DELETE} parts is dropped.
 
 \paragraph{Translating Counter Clauses}
 

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