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

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

Revision: 1342
          http://toss.svn.sourceforge.net/toss/?rev=1342&view=rev
Author:   lukstafi
Date:     2011-03-03 21:40:00 +0000 (Thu, 03 Mar 2011)

Log Message:
-----------
GDL translation: progress on negation handling. Aux: tiny helper for below-diagonal pairs of elements. Various test fixes.

Modified Paths:
--------------
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/Arena/DiscreteRuleTest.ml
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/Play/GameTest.ml
    trunk/Toss/Server/Server.ml
    trunk/Toss/Server/ServerGDLTest.in2
    trunk/Toss/Server/ServerGDLTest.out2
    trunk/Toss/Server/ServerTest.ml

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Arena/DiscreteRule.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -754,15 +754,17 @@
   let varify_lhs tup =
     Array.map (fun e -> `FO (lhs_name_of e)) tup in
   (* summing up: the LHS structure embedding plus the precondition *)
-  let emb = And [
-    And (Aux.concat_map (fun (rel, tups) ->
-      List.map (fun tup -> Rel (rel, varify_lhs tup)) tups) lhs_pos_tups);
-    And (Aux.concat_map (fun (rel, tups) ->
-      List.map (fun tup -> Not (Rel (rel, varify_lhs tup))) tups) lhs_neg_tups);
-    And (List.map (function [x;y] -> Not (Eq (`FO x, `FO y))
-      | _ -> assert false) lhs_alldif_tups);
-    precond
-  ] in
+  let emb = And (
+    Aux.concat_map (fun (rel, tups) ->
+      List.map (fun tup -> Rel (rel, varify_lhs tup)) tups)
+      lhs_pos_tups @
+    Aux.concat_map (fun (rel, tups) ->
+      List.map (fun tup -> Not (Rel (rel, varify_lhs tup))) tups)
+      lhs_neg_tups @
+    List.map (function [x;y] -> Not (Eq (`FO x, `FO y))
+      | _ -> assert false) lhs_alldif_tups @
+      FormulaOps.flatten_ands precond
+  ) in
 
   (* Substitute defined relations, expanding their special variants. *)
   let transform_new_rel = function

Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -665,7 +665,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_one_of ~msg:"del defrel"
-        ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))";"((_del_P(b) and O(b) and (not P(b)) and (not Q(b))) or (_del_Q(b) and O(b) and (not P(b)) and (not Q(b))))-> (P(b) and (not O(b)))"]
+        ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))";"((_del_P(b) and O(b) and (not P(b)) and (not Q(b))) or (_del_Q(b) and O(b) and (not P(b)) and (not Q(b))))-> (P(b) and (not O(b)))";"((_del_P(b) or _del_Q(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))"]
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | _opt_D (e); _diffthan_P(e) | ]" in

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Formula/Aux.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -178,6 +178,12 @@
     concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
     l [[]]
 
+let rec pairs l =
+  match l with
+    | [] -> []
+    | hd::tl ->
+      List.rev_append (List.map (fun e-> hd, e) tl) (pairs tl)
+
 let all_tuples_for args elems =
   List.fold_left (fun tups _ ->
     concat_map (fun e -> (List.map (fun tup -> e::tup) tups))

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Formula/Aux.mli	2011-03-03 21:40:00 UTC (rev 1342)
@@ -113,6 +113,10 @@
 (** Cartesian product of lists. Not tail recursive. *)
 val product : 'a list list -> 'a list list
 
+(** A list of all pairs of elements that preserve the order of
+    elements from the list. *)
+val pairs : 'a list -> ('a * 'a) list
+
 (** An [n]th cartesian power of the second list, where [n] is the
     length of the first list. Tail recursive. *)
 val all_tuples_for : 'a list -> 'b list -> 'b list list

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/GGP/GDL.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -189,11 +189,39 @@
     [not (r, args) <=> not exist vars1 (args = params1 /\ body1) /\ ...
     /\ not exist vars_n (args = params_n /\ body_n)]
 
-    Currently we do not allow defined dynamic relations with negative
-    occurrences to have negative literals (or atoms of defined
-    relations with negative part) in any of [body_i]. (The limitation
-    can be lifted but it would further complicate the implementation.)
-    We therefore allow conjunctions of atoms to be negated (not only
+    (6b1) If the relation has negative subformulas in any of [body_i],
+    we first negate the definition and then expand the negation as in
+    the positive case.
+
+    (6b1a) Eliminate [args = params_i] by substituting-out variables
+    from [params_i] whenever possible.
+
+    Note: the [args] need to be instatiated for the particular
+    solution that is extended (the solution substitution applied).
+
+    (6b1b) We group the positive atoms of body_i together and split
+    the quantifier if each negative subformula and the positive part
+    have disjoint [vars_i] variables; if not, the translation fails;
+    currently, if a negative subformula has free variables in vars_i,
+    the translation also fails.
+
+    (6b1c) So we have two levels of specification-affecting TODOs;
+    working around variables shared between negated subformulas or the
+    positive part -- forbidding pushing quantification inside -- will
+    require major rethinking of implementation; if the quantification
+    can be pushed inside but doesn't disappear around a negated
+    subformula, we will need to extend the universal quantifier
+    handling from only negated to both negated and positive
+    subformulas, which shouldn't be problematic.
+
+    (6b1d) Now push the negation inside the conjunction so that all
+    double negations cancel out (the positive conjuncts are under a
+    single, now negated, quantifier -- see (6b2) about negated
+    conjunctions of atoms). Next we pull the disjunctions out
+    (reducing to DNF-like form), and continue as in the positive case
+    (6a).
+
+    (6b2) We allow conjunctions of atoms to be negated (not only
     literals) in a branch. We expand [not (r, args)] (in general, [not
     (and (...(r args)...))]) into the conjunction of negations, with
     no branch duplication (in general, duplicating the negated
@@ -633,6 +661,12 @@
 (* Type shortcuts (mostly for documentation). *)
 type gdl_atom = string * term list
 type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list
+(* Definition with collected relation branches and negation-local
+   variables found. *)
+type lit_def_branch =
+    term list * gdl_atom list * (Aux.Strings.t * gdl_atom) list
+type lit_def =
+    string * lit_def_branch list
 (* Definition with expanded definitions: expansion of a negated
    relation brings negated (possibly locally existentially quantified)
    conjunctions. *)
@@ -699,13 +733,14 @@
       head, pos_body, neg_body) bodies
   | Atomic (rel, args) -> [(rel, args), [], []]
 
-let add_neg_body_vars global_vars neg_body =
+let add_neg_body_vars global_vars neg_body
+    : (Aux.Strings.t * gdl_atom) list =
   List.map (fun (_, args as a)->
     let local_vs = Aux.Strings.diff (terms_vars args) global_vars in
-    local_vs, [a]) neg_body
+    local_vs, a) neg_body
 
-let defs_of_rules rules
-    : (string * exp_def_branch list) list =
+let lit_defs_of_rules rules
+    : (string * lit_def_branch list) list =
   Aux.map_reduce
     (fun ((drel, params), body, neg_body) ->
       let global_vs =
@@ -714,27 +749,36 @@
             add_neg_body_vars global_vs neg_body))
     (fun x y->y::x) [] rules
 
-(* Only use [rules_of_defs] when sure that no multi-premise negative
-   literal has been expanded. *)
-let rules_of_defs (defs : exp_def list) =
+let rules_of_lit_defs (defs : lit_def list) =
   Aux.concat_map (fun (rel, branches) ->
     List.map (fun (args, body, neg_body) ->
       let neg_body =
-        List.map (function _,[a]->a | _ -> assert false) neg_body in
+        List.map snd neg_body in
       (rel, args), body, neg_body) branches) defs
 
+let exp_brs_of_lit_brs brs =
+  List.map (fun (args, body, neg_body) ->
+    let neg_body =
+      List.map (fun (vs,a) -> vs,[a]) neg_body in
+    args, body, neg_body) brs
+
+let exp_defs_of_lit_defs defs : exp_def list =
+  List.map (fun (rel, branches) ->
+    rel, exp_brs_of_lit_brs branches) defs
+
+
 (* Stratify either w.r.t. the dependency graph ([~def:true]) or its
    subgraph the negation graph ([~def:false]). *)
-let rec stratify ?(def=false) strata (defs : exp_def list) =
+let rec stratify ?(def=false) strata (defs : lit_def list) =
   match
     List.partition (fun (_, branches) ->
       List.for_all (fun (_, body, neg_body) ->
-        let neg_bodies = List.concat (List.map snd neg_body) in
+        let neg_body = List.map snd neg_body in
         List.for_all (fun (rel1,_) ->
           rel1 = "distinct" || rel1 = "true" || rel1 = "does" ||
             not (List.mem_assoc rel1 defs))
-          (if def then body @ neg_bodies
-           else neg_bodies)) branches) defs
+          (if def then body @ neg_body
+           else neg_body)) branches) defs
   with
     | [], [] ->
       (* {{{ log entry *)
@@ -935,6 +979,13 @@
 
 let facts_str facts =
   String.concat " " (List.map fact_str facts)
+let neg_lfacts_str negs =
+  String.concat " "
+    (List.map (fun (vs,d) ->
+      let vs = Aux.Strings.elements vs in
+      let q = if vs = [] then ""
+        else "forall "^String.concat ", " vs in
+      q ^ "(not "^fact_str d^")") negs)
 let neg_facts_str negs =
   String.concat " "
     (List.map (fun (vs,d) ->
@@ -947,9 +998,15 @@
     "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
       " " ^ neg_facts_str neg_body ^ ")"
 
-let def_str (rel, branches) =
+let lit_def_str (rel, branches) =
   String.concat "\n" (List.map (fun (args, body, neg_body) ->
     "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
+      " " ^ neg_lfacts_str neg_body ^ ")"
+  ) branches)
+
+let exp_def_str (rel, branches) =
+  String.concat "\n" (List.map (fun (args, body, neg_body) ->
+    "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
       " " ^ neg_facts_str neg_body ^ ")"
   ) branches)
 (*
@@ -1059,19 +1116,17 @@
       instantiate (inst_stratum [] [] base stratum) strata in
 
   instantiate base
-    (List.map rules_of_defs (stratify [] (defs_of_rules rules)))
+    (List.map rules_of_lit_defs (stratify [] (lit_defs_of_rules rules)))
 
 
 let game_description = ref []
 let player_terms = ref [| |]
 
 let state_of_file s =
-  Printf.printf "GDL: Loading file %s...\n%!" s;
   let f = open_in s in
   let res =
     ArenaParser.parse_game_state Lexer.lex
       (Lexing.from_channel f) in
-  Printf.printf "GDL: File %s loaded.\n%!" s;
   res
 
 (* 6 *)
@@ -1121,12 +1176,61 @@
 let freshen_def_branches =
   List.map freshen_branch
 
+(* [args] are the actual, instatiated, arguments. *)
+let negate_def uni_vs args neg_def =
+  (* 6b1a *)
+  let global_vars = terms_vars args in
+  let aux_br (params, body, neg_body) =
+    let sb = unify [] params args in
+    let body = subst_rels sb body in
+    let neg_body = List.map (fun (vs, conjs) ->
+      vs, subst_rels sb conjs) neg_body in
+    let subforms = (Aux.Strings.empty, body) :: neg_body in
+    (* components of [vars_i] by conjuncts *)
+    let sub_fvars = List.map (fun (_, subphi) ->
+      Aux.Strings.diff (rels_vars subphi) global_vars) subforms in
+    let subvars = List.map2 (fun fvs (qvs,_) ->
+      Aux.Strings.diff fvs qvs) sub_fvars subforms in
+    (* 6b1b *)
+    if List.exists (fun (vs1, vs2) ->
+      not (Aux.Strings.is_empty (Aux.Strings.inter vs1 vs2)))
+      (Aux.pairs subvars)
+    then failwith
+      ("GDL.negate_def: variables shared between negated subformulas" ^
+          " -- long term TODO (params: "^terms_str params^")");
+    (if List.exists (fun (fvs, (qvs,_)) ->
+      (* [fvs - qvs] must be a subset of the "vars_i" quantified vars *)
+      not (Aux.Strings.is_empty (Aux.Strings.diff fvs qvs)))
+        (List.tl (List.combine sub_fvars subforms))
+    then
+      let (fvs,(qvs,_)) = List.find (fun (fvs, (qvs,_)) ->
+        not (Aux.Strings.is_empty (Aux.Strings.diff fvs qvs)))
+        (List.tl (List.combine sub_fvars subforms)) in
+      failwith
+        ("GDL.negate_def: universal quantification escapes negation" ^
+            " -- doable TODO (params: "^terms_str params^") (vars: "^
+            String.concat ", " (Aux.Strings.elements
+                                  (Aux.Strings.diff fvs qvs))^")"));
+    Aux.Right (List.hd sub_fvars, body) ::
+      List.map (fun (_,conjs) -> Aux.Left conjs) neg_body in
+  (* 6b1c *)
+  (* We drop branches whose heads don't match. *)
+  let cnf = Aux.map_try aux_br neg_def in
+  let dnf = Aux.product cnf in
+  List.map (fun conjs ->
+    let pos, neg = Aux.partition_choice conjs in
+    (* since (6b1b), no local universal quantification *)
+    let pos = List.concat pos in
+    pos, neg
+  ) dnf
+
+
 (* assumption: [defs] bodies are already clean of defined relations *)
 let subst_def_branch (defs : exp_def list)
-    (head, body, neg_body as br : exp_def_branch) : exp_def_branch list =
+    (head, body, neg_body as br : lit_def_branch) : exp_def_branch list =
   (* {{{ log entry *)
   if !debug_level > 4 then (
-    Printf.printf "Expanding branch %s\n%!" (def_str ("BRANCH", [br]));
+    Printf.printf "Expanding branch %s\n%!" (lit_def_str ("BRANCH", [br]));
   );
   (* }}} *)
   (* 6a *)
@@ -1137,7 +1241,7 @@
        (* {{{ log entry *)
        if !debug_level > 4 then (
          Printf.printf "Expanding positive %s by %s\n%!" rel
-           (def_str (rel, def))
+           (exp_def_str (rel, def))
        );
        (* }}} *)
        Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
@@ -1158,48 +1262,91 @@
            subst_rel sb atom::pos_sol, neg_sol, sb) sols))
       ([[],[],[]]) body in
   (* 6b *)
+  let neg_body_flat, neg_body_rec =
+    Aux.partition_map (fun (uni_vs, (neg_rel, neg_args) as neg_lit) ->
+      (let try def =
+         freshen_def_branches (List.assoc neg_rel defs) in
+       if not (List.exists (fun (_,_,negb) -> negb<>[]) def)
+       then Aux.Left (neg_lit, Some def)
+       else (
+         (* {{{ log entry *)
+
+         if !debug_level > 3 then (
+           let _,_,def_neg_body =
+             List.find (fun (_,_,negb) -> negb <> []) def in
+           Printf.printf
+             "expand: found recursive negative %s(%s): neg_body= not %s\n%!"
+             neg_rel (terms_str neg_args)
+             (String.concat " and not "
+                (List.map facts_str (List.map snd def_neg_body)))
+         );
+
+         (* }}} *)
+         Aux.Right (neg_lit, def))
+       with Not_found -> Aux.Left (neg_lit, None))
+    ) neg_body in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "Expanding (%s) negative part: flat %s; rec %s\n%!"
+      (terms_str head)
+      (String.concat ", "(List.map (fun ((_,(nr,_)),_) -> nr) neg_body_flat))
+      (String.concat ", "(List.map (fun ((_,(nr,_)),_) -> nr) neg_body_rec))
+  );
+  (* }}} *)
+  (* 6b1 *)
   let sols =
-    (* no branch duplication, but each negation has its own substitution *)
+    List.fold_left (fun sols ((uni_vs, (rel, args)), neg_def) ->
+       (* {{{ log entry *)
+       if !debug_level > 3 then (
+         Printf.printf "Expanding rec-negative %s by %s\n%!" rel
+           (exp_def_str (rel, neg_def))
+       );
+       (* }}} *)
+       (* we don't keep the substitution from the negated match *)
+       Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         let branches = negate_def uni_vs args neg_def in
+         List.map (fun (dbody, dneg_body) ->
+           dbody @ pos_sol, dneg_body @ neg_sol, sb) branches
+       ) sols)
+      sols neg_body_rec in
+
+  (* 6b2 *)
+  let sols =
     List.map (fun (pos_sol, neg_sol, sb) ->
       let more_neg_sol =
-        Aux.concat_map (fun (uni_vs, neg_conjs) ->
-          (* negated subformulas are duplicated instead *)
-          List.fold_left (fun neg_sol (rel, args as atom) ->
-            (let try def =
-               freshen_def_branches (List.assoc rel defs) in
-             Aux.concat_map (fun (uni_vs, neg_acc, sb) ->
-               let args = List.map (subst sb) args in
-               Aux.map_try (fun (dparams, dbody, dneg_body) ->
-                 if dneg_body <> [] then
-                   failwith
-                     ("GDL.subst_def_branch: negation in negatively used" ^
-                         " defined rels not supported yet, relation "^rel);
-                 (let sb1 = unify [] dparams args in
-                  let param_vars = terms_vars dparams in
-                  let body_vars = rels_vars dbody in
-                  let dbody = subst_rels sb1 dbody in
-                  let local_vs =
-                    Aux.Strings.inter (Aux.Strings.diff body_vars param_vars)
-                      (rels_vars dbody) in
-                  let neg_acc = subst_rels sb1 neg_acc in
-                  Aux.Strings.union uni_vs local_vs,
-                  dbody @ neg_acc,
-                  extend_sb sb1 sb)
-               ) def) neg_sol
-             with Not_found ->              (* rel not in defs *)
-               List.map (fun (uni_vs, neg_acc, sb) ->
-                 uni_vs, subst_rel sb atom::neg_acc, sb) neg_sol)
-          ) [uni_vs, [], sb] neg_conjs
-        ) neg_body in
-      let more_neg_sol =
-        List.map (fun (uni_vs, neg_conjs,_) -> uni_vs, neg_conjs)
-          more_neg_sol in
+        Aux.concat_map (fun ((uni_vs, (rel, args as atom)), def_opt) ->
+          (* negated subformulas are duplicated instead of branches *)
+          match def_opt with
+            | Some def ->
+              let args = List.map (subst sb) args in
+              Aux.map_try (fun (dparams, dbody, _) ->
+                (let sb1 = unify [] dparams args in
+                 let param_vars = terms_vars dparams in
+                 let body_vars = rels_vars dbody in
+                 let dbody = subst_rels sb1 dbody in
+                 let local_vs =
+                   Aux.Strings.diff body_vars
+                     (Aux.Strings.diff param_vars uni_vs) in
+                 local_vs, dbody)
+              ) def
+            | None ->              (* rel not in defs *)
+              [uni_vs, [atom]]
+        ) neg_body_flat in
       List.rev pos_sol, List.rev_append neg_sol more_neg_sol, sb
     ) sols in
-  Aux.map_some (fun (pos_sol, neg_sol, sb) ->
-    if List.exists (function _,[] -> true | _ -> false) neg_sol
-    then None
-    else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols
+  let res =
+    Aux.map_some (fun (pos_sol, neg_sol, sb) ->
+      if List.exists (function _,[] -> true | _ -> false) neg_sol
+      then None
+      else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols in
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "Expansion: res =\n%s\nExpansion done.\n%!"
+      (String.concat "\n"(List.map (branch_str "exp-unkn") res))
+  );
+  (* }}} *)
+  res
 
 (* Stratify and expand all relations in the given set. *)
 let expand_def_rules ?(more_defs=[]) rules =
@@ -1218,14 +1365,16 @@
       (* {{{ log entry *)
 if !debug_level > 3 then (
   Printf.printf "expand_def_rules: step result = %s\nexpand_def_rules: end step\n%!"
-    (String.concat "\n" (List.map def_str step))
+    (String.concat "\n" (List.map exp_def_str step))
 );
 (* }}} *)
       loop (base @ step) strata in
-  match stratify ~def:true [] (defs_of_rules rules) with
+  match stratify ~def:true [] (lit_defs_of_rules rules) with
     | [] -> []
-    | [no_defined_rels] when more_defs=[] -> no_defined_rels
-    | def_base::def_strata when more_defs=[] -> loop def_base def_strata
+    | [no_defined_rels] when more_defs=[] ->
+      exp_defs_of_lit_defs no_defined_rels
+    | def_base::def_strata when more_defs=[] ->
+      loop (exp_defs_of_lit_defs def_base) def_strata
     | def_strata -> loop more_defs def_strata
 
 
@@ -1262,6 +1411,11 @@
          (List.rev_append more_neg_body neg_body)))
   with Not_found -> None
 
+let subst_legal_rules def_brs brs =
+  Aux.concat_map (fun br ->
+    List.map snd
+      (Aux.map_some (fun def -> subst_legal_rule def br) def_brs)) brs
+
 (* 1 *)
 
 (* Collect the aggregate playout, but also the actions available in
@@ -1994,27 +2148,21 @@
           | _ -> false) static_rules
     ) static_rules in
   (* {{{ log entry *)
-
   if !debug_level > 0 then (
     Printf.printf "translate_game: expanded static rules: %s\n%!"
       (String.concat ", " (List.map (fun ((r,_),_,_)->r) exp_static_rules));
   );
-
   (* }}} *)
   let static_exp_defs = expand_def_rules exp_static_rules in
-  let static_rules =
-    if static_exp_defs = [] then static_rules
-    else rules_of_defs
-      (List.map (fun (rel,branches) ->
-        rel, Aux.concat_map (subst_def_branch static_exp_defs) branches)
-         (defs_of_rules static_rules)) in
+  let static_rules = Aux.unique_sorted
+    (List.map Aux.fst3 static_rules) in
   let exp_defs =
     expand_def_rules ~more_defs:static_exp_defs dynamic_rules in
 
   (* {{{ log entry *)
   if !debug_level > 0 then (
     Printf.printf "translate_game: All expanded dynamic rules:\n%s\n%!"
-      (String.concat "\n" (List.map def_str exp_defs))
+      (String.concat "\n" (List.map exp_def_str exp_defs))
   );
   (* }}} *)
   (* 3 *)
@@ -2023,15 +2171,13 @@
   let terminal_rules = List.assoc "terminal" exp_defs in
   let goal_rules = List.assoc "goal" exp_defs in
   (* 3b *)
-  let exp_next =
-    Aux.concat_map (subst_def_branch ["does", legal_rules]) next_rules in
+  let exp_next = subst_legal_rules legal_rules next_rules in
+
   (* {{{ log entry *)
-
   if !debug_level > 0 then (
     Printf.printf "translate_game: \"next\" rules with \"does\"<-\"legal\":\n%s\n%!"
-      (def_str ("next", exp_next))
+      (exp_def_str ("next", exp_next))
   );
-
   (* }}} *)
   (* 3c *)
   let masks = List.map (function
@@ -2119,9 +2265,8 @@
     | mask, (sb,_)::_ -> List.map (fun (v,_)->mask, v) sb) elements in
   (* 4a *)
   let static_rels =
-    Aux.unique_sorted
-      (List.map (fun ((rname,args),_,_) ->
-        rname, List.map (fun _ -> ()) args) static_rules) in
+    List.map (fun (rname,args) ->
+      rname, List.map (fun _ -> ()) args) static_rules in
   let static_rels =
     List.map (fun (rel,args) ->
       rel, List.length args,
@@ -2517,7 +2662,9 @@
             );
             (* }}} *)
             (* 7f3 *)
-            let erasure_brs : exp_def_branch list = Aux.concat_map
+            (* TODO: minimize the number of branches by keeping
+               negations over conjunctions like in (6b1) *)
+            let erasure_brs : lit_def_branch list = Aux.concat_map
               (function
                 | [next_arg] as next_args,multi_body ->
                   let mask, _, _, blank_arg = term_to_blank masks next_arg in
@@ -2596,8 +2743,7 @@
                                   List.mem pos neg_conjs) lead_neg_body
                               ) body) &&
                               not (List.exists (fun (_,neg) ->
-                                List.for_all
-                                  (fun neg->List.mem neg lead_body) neg
+                                  List.mem neg lead_body
                               ) neg_body)
                           then Some ([head], body, neg_body)
                           else None
@@ -2612,7 +2758,8 @@
             (* TODO: (7f5) we ignore the possibility that "lead" is
                instantiated by some of erasure substitutions, since
                we already ignore non-maximal "legal" classes *)
-            lead_head, fixed_brs @ expanded_brs @ erasure_brs
+            lead_head, fixed_brs @ expanded_brs @
+              exp_brs_of_lit_brs erasure_brs
           ) rules_brs in
         (* let rules_inds = Array.of_list rules_brs in *)
         rules_brs
@@ -2625,12 +2772,12 @@
       List.iter (fun (lead, brs) ->
         Printf.printf "Rule-precursor: player %s move %s\n%s\n%!"
           (term_str loc_players.(loc)) (term_str lead)
-          (def_str ("action", brs))
+          (exp_def_str ("action", brs))
       ) rules_brs;
     ) loc_next_classes;
   );
   (* }}} *)
-  let static_rnames = List.map (fun ((srel,_),_,_) -> srel) static_rules in
+  let static_rnames = List.map fst static_rules in
   (* 7h *)
   let loc_toss_rules =
     Array.mapi (fun loc rules_brs ->
@@ -2890,7 +3037,8 @@
           List.filter (fun a -> List.exists (fun v->List.mem v disj_vars)
             (FormulaOps.free_vars a)) goal_4b in
         let disj = lift_universal goal_uni_vars (disj_4b @ conjs) in
-        Formula.Ex (FormulaOps.free_vars disj, disj)
+        let disj_vs = FormulaOps.free_vars disj in
+        if disj_vs = [] then disj else Formula.Ex (disj_vs, disj)
       ) brs in
       score, Formula.Or goal_disjs
     ) goals in

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/GGP/GDL.mli	2011-03-03 21:40:00 UTC (rev 1342)
@@ -85,7 +85,7 @@
   gdl_translation * (Arena.game * Arena.game_state)
 
 (* DEBUG intermediate *)
-val defs_of_rules : gdl_rule list -> exp_def list
+(* val exp_defs_of_rules : gdl_rule list -> exp_def list *)
 val expand_def_rules :
   ?more_defs:exp_def list -> gdl_rule list -> exp_def list
 
@@ -109,4 +109,4 @@
 val term_str : term -> string
 val fact_str : string * term list -> string
 val facts_str : (string * term list) list -> string
-val def_str : exp_def -> string
+val exp_def_str : exp_def -> string

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/GGP/GDLTest.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -73,7 +73,7 @@
 ((alpha ?X) <= (rho ?X) (not (and (gamma ?X) (rho ?X))))
 ((zeta ?X) <= (rho ?X) (not (and (gamma ?X))))"
         (String.concat "\n"
-           (List.map GDL.def_str res));
+           (List.map GDL.exp_def_str res));
     );
 
   "connect5" >::
@@ -114,5 +114,5 @@
   let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
   let connect5 = load_rules "./GGP/examples/connect5.gdl" in
   let tictactoe = load_rules "./GGP/examples/tictactoe.gdl" in
-  let gdef = GDL.translate_game (Const "white") breakthrough in
+  let gdef = GDL.translate_game (Const "x") connect5 in
   ignore gdef; ignore connect5; ignore breakthrough; ignore tictactoe

Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Play/GameTest.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -31,12 +31,10 @@
     (Lexing.from_string s)
 
 let state_of_file s =
-  Printf.printf "Loading file %s...\n%!" s;
   let f = open_in s in
   let res =
     ArenaParser.parse_game_state Lexer.lex
       (Lexing.from_channel f) in
-  Printf.printf "File %s loaded.\n%!" s;
   res
 
 module StrMap = Structure.StringMap

Modified: trunk/Toss/Server/Server.ml
===================================================================
--- trunk/Toss/Server/Server.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Server/Server.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -441,12 +441,10 @@
 
 
 let set_state_from_file fn =
-  Printf.printf "Loading file %s...\n%!" fn;
   let f = open_in fn in
   let s = ArenaParser.parse_game_state Lexer.lex (Lexing.from_channel f) in
-  Printf.printf "File %s loaded.\n%!" fn;
   game_modified := true;
-  state := s;
+  state := s
 ;;
 
 let heur_val_white1 = ref "";;

Modified: trunk/Toss/Server/ServerGDLTest.in2
===================================================================
--- trunk/Toss/Server/ServerGDLTest.in2	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Server/ServerGDLTest.in2	2011-03-03 21:40:00 UTC (rev 1342)
@@ -32,7 +32,7 @@
 Content-type: text/acl
 Content-length: 41
 
-(PLAY MATCH.3316980891 (NOOP (MARK 1 1)))
+(PLAY MATCH.3316980891 (NOOP (MARK 2 2)))
 
 POST / HTTP/1.0
 Accept: text/delim
@@ -41,7 +41,7 @@
 Content-type: text/acl
 Content-length: 41
 
-(PLAY MATCH.3316980891 ((MARK 3 2) NOOP))
+(PLAY MATCH.3316980891 ((MARK 1 3) NOOP))
 
 POST / HTTP/1.0
 Accept: text/delim
@@ -50,7 +50,7 @@
 Content-type: text/acl
 Content-length: 41
 
-(PLAY MATCH.3316980891 (NOOP (MARK 2 2)))
+(PLAY MATCH.3316980891 (NOOP (MARK 1 1)))
 
 POST / HTTP/1.0
 Accept: text/delim
@@ -59,7 +59,7 @@
 Content-type: text/acl
 Content-length: 41
 
-(PLAY MATCH.3316980891 ((MARK 3 1) NOOP))
+(PLAY MATCH.3316980891 ((MARK 2 3) NOOP))
 
 POST / HTTP/1.0
 Accept: text/delim

Modified: trunk/Toss/Server/ServerGDLTest.out2
===================================================================
--- trunk/Toss/Server/ServerGDLTest.out2	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Server/ServerGDLTest.out2	2011-03-03 21:40:00 UTC (rev 1342)
@@ -12,7 +12,7 @@
 Content-type: text/acl
 Content-length: 10
 
-(MARK 1 1)
+(MARK 2 2)
 HTTP/1.0 200 OK
 Content-type: text/acl
 Content-length: 4
@@ -22,7 +22,7 @@
 Content-type: text/acl
 Content-length: 10
 
-(MARK 2 2)
+(MARK 1 1)
 HTTP/1.0 200 OK
 Content-type: text/acl
 Content-length: 4

Modified: trunk/Toss/Server/ServerTest.ml
===================================================================
--- trunk/Toss/Server/ServerTest.ml	2011-03-03 18:28:09 UTC (rev 1341)
+++ trunk/Toss/Server/ServerTest.ml	2011-03-03 21:40:00 UTC (rev 1342)
@@ -57,7 +57,7 @@
       let out_ch = open_out "./Server/ServerGDLTest.temp" in
       Game.deterministic_suggest := true;
       let old_effort = !Game.default_effort in
-      Game.default_effort := 2;
+      Game.default_effort := 6;
       (try while true do
           Server.req_handle in_ch out_ch done
        with End_of_file -> ());


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