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

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

Revision: 1507
          http://toss.svn.sourceforge.net/toss/?rev=1507&view=rev
Author:   lukstafi
Date:     2011-07-09 10:28:17 +0000 (Sat, 09 Jul 2011)

Log Message:
-----------
Reimplementation of GDL to Toss translation: untested work in progress.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/AuxTest.ml
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLParser.mly
    trunk/Toss/GGP/Translate.ml
    trunk/Toss/Solver/Structure.ml
    trunk/Toss/Solver/Structure.mli
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/Formula/Aux.ml	2011-07-09 10:28:17 UTC (rev 1507)
@@ -204,10 +204,14 @@
     | 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 _ ->
+let rec fold_n f accu n =
+  if n <= 0 then accu
+  else fold_n f (f accu) (n-1)
+
+let all_ntuples elems arity =
+  fold_n (fun tups ->
     concat_map (fun e -> (List.map (fun tup -> e::tup) tups))
-      elems) [[]] args
+      elems) [[]] arity
 
 let rec remove_one e = function
   | hd::tl when hd = e -> tl
@@ -486,11 +490,7 @@
     | hd::tl ->
         aux (List.map (fun e->[e]) hd) tl
 
-let rec fold_n f accu n =
-  if n <= 0 then accu
-  else fold_n f (f accu) (n-1)
 
-
 (* Character classes. *)
 let is_uppercase c = c >= 'A' && c <= 'Z'
 let is_lowercase c = c >= 'a' && c <= 'z'

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/Formula/Aux.mli	2011-07-09 10:28:17 UTC (rev 1507)
@@ -132,9 +132,8 @@
     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
+(** An [n]th cartesian power of the list. Tail recursive. *)
+val all_ntuples : 'a list -> int -> 'a list list
 
 (** Remove an occurrence of a value (uses structural equality). *)
 val remove_one : 'a -> 'a list -> 'a list

Modified: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/Formula/AuxTest.ml	2011-07-09 10:28:17 UTC (rev 1507)
@@ -140,7 +140,7 @@
         (Aux.map_try f [`A;`B;`C;`D]);
     );  
 
-  "product, all_tuples_for, concat_foldr" >::
+  "product, all_ntuples, concat_foldr" >::
     (fun () ->
       let print_llist l = String.concat "; "
         (List.map (String.concat ", ") l) in
@@ -154,11 +154,11 @@
 
       assert_equal ~printer:print_llist
         [["a"; "a"]; ["a"; "b"]; ["a"; "c"]; ["b"; "a"]; ["b"; "b"]; ["b"; "c"]; ["c"; "a"]; ["c"; "b"]; ["c"; "c"]]
-        (Aux.all_tuples_for [();()] ["a";"b";"c"]);
+        (Aux.all_ntuples ["a";"b";"c"] 2);
 
       assert_equal ~printer:print_llist
         [["a"; "a"; "a"]; ["a"; "a"; "b"]; ["a"; "b"; "a"]; ["a"; "b"; "b"]; ["b"; "a"; "a"]; ["b"; "a"; "b"]; ["b"; "b"; "a"]; ["b"; "b"; "b"]]
-        (Aux.all_tuples_for [();(); ()] ["a";"b"]);
+        (Aux.all_ntuples ["a";"b"] 3);
 
       assert_equal ~printer:print_llist
         [["a1"; "b"; "c"; "a1"; "d"]; ["a2"; "b"; "c"; "a1"; "d"];

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/GGP/GDL.ml	2011-07-09 10:28:17 UTC (rev 1507)
@@ -1,33 +1,40 @@
 (** {2 Game Description Language.}
-    Type definitions, helper functions, game specification. *)
 
+    Type definitions, operations on terms, saturation (i.e. Herbrand
+    model), clause inlining. *)
+
+(* ************************************************************ *)
+(* ************************************************************ *)
+(** {3 Datalog programs: Type definitions and saturation.} *)
+
 open Aux.BasicOperators
 
 let debug_level = ref 0
 let aggregate_drop_negative = ref false
 let aggregate_fixpoint = ref true
 
-(** Expand static relations that do not have ground facts, are not
-    directly recursive, and have arity above the threshold. *)
-let expand_arity_above = ref 0
-
-(** Treat "next" clauses which introduce metavariables only for
-    variable-variable mismatch, as non-erasing frame clauses (to be
-    ignored). ("Wave" refers to the process of "propagating the frame
-    condition" that these clauses are assumed to do, if
-    [nonerasing_frame_wave] is set to [true].) *)
-let nonerasing_frame_wave = ref true
-
 type term =
   | Const of string
   | Var of string
-  | MVar of string                      (* meta-variable, not used in GDL *)
-  | Func of string * term list
+  | Func of string * term array
 
+type rel_atom = string * term list
+(** Positive and negative literals separated, disjunctions expanded-out. *)
+type gdl_rule = rel_atom * rel_atom list * rel_atom list
+(** Collect rules by relations. *)
+type def_branch = term list * rel_atom list * rel_atom list
+type gdl_defs = (string * def_branch list) list
+
+module Terms = Set.Make (
+  struct type t = term let compare = Pervasives.compare end)
+module Atoms = Set.Make (
+  struct type t = rel_atom let compare = Pervasives.compare end)
+
 type atom =
   | Distinct of term list
-  | Rel of string * term list
-  | Currently of term
+  | Rel of rel_atom
+  | Role of term
+  | True of term
   | Does of term * term
 
 type literal =
@@ -35,51 +42,34 @@
   | Neg of atom
   | Disj of literal list
 
-type game_descr_entry =
-  | Datalog of string * term list * literal list
-  | Next of term * literal list
-  | Legal of term * term * literal list
-  | Goal of term * int * literal list
-  | GoalPattern of term * string * literal list
-  | Terminal of literal list
-  | Role of term
-  | Initial of term * literal list
-  | Atomic of string * term list
+type clause = rel_atom * literal list
 
 type request =
-  | Start of string * term * game_descr_entry list * int * int
-  (* prepare game: match id, role, game, startclock, playclock *)
+  | Start of string * term * clause list * int * int
+  (** prepare game: match id, role, game, startclock, playclock *)
   | Play of string * term list
-  (* request a move: match id, actions on previous step *)
+  (** request a move: match id, actions on previous step *)
   | Stop of string * term list
-  (* game ends here: match id, actions on previous step *)
+  (** game ends here: match id, actions on previous step *)
 
 
 let rec term_str = function
   | Const c -> c
   | Var v -> "?"^v
-  | MVar v -> "@"^v
   | Func (f, args) ->
     "(" ^ f ^ " " ^ String.concat " " (List.map term_str args) ^ ")"
 
 let rec term_to_name ?(nested=false) = function
   | Const c -> c
   | Var v -> v
-  | MVar v -> v
   | Func (f, args) ->
     f ^ "_" ^ (if nested then "_S_" else "") ^
       String.concat "_" (List.map (term_to_name ~nested:true) args) ^
       (if nested then "_Z_" else "")
 
-let rec vars ?(meta=false) = function
-  | Const _ -> []
-  | Var x -> [x]
-  | MVar x -> if meta then [x] else []
-  | Func (_, args) -> Aux.concat_map vars args
-
 let rec term_vars = function
   | Const _ -> Aux.Strings.empty
-  | Var v | MVar v -> Aux.Strings.singleton v
+  | Var v -> Aux.Strings.singleton v
   | Func (f, args) -> terms_vars args
 
 and terms_vars args =
@@ -87,166 +77,79 @@
     (List.map term_vars args)
   
 
-let fact_of_atom = function
-  | Distinct args -> assert false
+let rel_of_atom = function
+  | Distinct args -> "distinct", args   (* not a proper relation -- avoid *)
   | Rel (rel, args) -> rel, args
-  | Currently arg -> "true", [arg]
+  | Role arg -> "role", [arg]
+  | True arg -> "true", [arg]
   | Does (arg1, arg2) -> "does", [arg1; arg2]
 
+let atom_of_rel = function
+  | "distinct", args -> Distinct args   (* not a proper relation -- avoid *)
+  | "role", [arg] -> Role arg
+  | "true", [arg] -> True arg
+  | "does", [arg1; arg2] -> Does (arg1, arg2)
+  | rel, args -> Rel (rel, args)
+
 let rec body_of_literal = function
   | Pos (Distinct args) ->
     [Aux.Right ("distinct", args)]        (* not negated actually! *)
   | Neg (Distinct _) -> assert false
-  | Pos atom -> [Aux.Left (fact_of_atom atom)]
-  | Neg atom -> [Aux.Right (fact_of_atom atom)]
+  | Pos atom -> [Aux.Left (rel_of_atom atom)]
+  | Neg atom -> [Aux.Right (rel_of_atom atom)]
   | Disj disjs ->
     Aux.concat_map body_of_literal disjs
 
 let func_graph f terms =
   Aux.map_some (function Func (g, args) when f=g -> Some args | _-> None) terms
 
-(* 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. *)
-type exp_def_branch =
-    term list * gdl_atom list * (Aux.Strings.t * gdl_atom list) list
-type exp_def = string * exp_def_branch list
 
-module Terms = Set.Make (
-  struct type t = term let compare = Pervasives.compare end)
-module Atoms = Set.Make (
-  struct type t = string * term list let compare = Pervasives.compare end)
-
-
-let lit_def_br_vars (head, body, neg_body : lit_def_branch) =
+let gdl_rule_vars (head, body, neg_body) =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map terms_vars
-       (head::List.map snd body @
-          List.map (snd -| snd) neg_body))
+       (head::List.map snd (body @ neg_body)))
 
-let exp_def_br_vars (head, body, neg_body : exp_def_branch) =
+let gdl_rules_vars brs =
   List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map terms_vars
-       (head::List.map snd body @
-          Aux.concat_map (List.map snd -| snd) neg_body))
+    (List.map gdl_rule_vars brs)
 
-let lit_def_brs_vars brs =
+let rels_vars body =
   List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map lit_def_br_vars brs)
+    (List.map (fun (_,args)->terms_vars args) body)
 
-let exp_def_brs_vars brs =
-  List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map exp_def_br_vars brs)
+let gdl_defs_vars defs =
+  List.fold_left
+    (fun acc rels -> Aux.Strings.union acc (rels_vars rels))
+    Aux.Strings.empty
+    (Aux.concat_map (fun (hd,body,neg_body) ->
+      ("",hd)::body @ neg_body) (Aux.concat_map snd defs))  
 
-let sdef_br_vars (head, body, neg_body) =
-  exp_def_br_vars ([head], body, neg_body)
+let rules_of_clause (head, body) =
+  let body, neg_body =
+    Aux.partition_choice (Aux.concat_map body_of_literal body) in
+  head, body, neg_body
 
-let sdef_brs_vars brs =
-  List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map sdef_br_vars brs)
 
-let rels_vars body =
-  List.fold_left Aux.Strings.union Aux.Strings.empty
-    (List.map (fun (_,args)->terms_vars args) body)
+let clause_vars cl = gdl_rule_vars (rules_of_clause cl)
 
-let rules_of_entry = function
-  | Datalog (rel, args, body) ->
-    let head = rel, args in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Next (head, body) ->
-    let head = "next", [head] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Legal (arg1, arg2, body) ->
-    let head = "legal", [arg1; arg2] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Goal (arg, payoff, body) ->
-    let head = "goal", [arg; Const (string_of_int payoff)] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | GoalPattern (arg, var, body) ->
-    let head = "goal", [arg; Var var] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Terminal body ->
-    let head = "terminal", [] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Role arg -> [("role", [arg]), [], []]
-  | Initial (arg, body) ->
-    let head = "init", [arg] in
-    let bodies = Aux.product (List.map body_of_literal body) in
-    List.map (fun body ->
-      let pos_body, neg_body = Aux.partition_choice body in
-      head, pos_body, neg_body) bodies
-  | Atomic (rel, args) -> [(rel, args), [], []]
+let defs_of_rules rules =
+  Aux.map_reduce (fun ((rel, args), body, neg_body) ->
+    rel, (args, body, neg_body)) (fun y x->x::y) [] rules
 
-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
-
-let lit_defs_of_rules rules : (string * lit_def_branch list) list =
-  Aux.map_reduce
-    (fun ((drel, params), body, neg_body) ->
-      let global_vs =
-        Aux.Strings.union (terms_vars params) (rels_vars body) in
-      drel,(params, body,
-            add_neg_body_vars global_vs neg_body))
-    (fun x y->y::x) [] rules
-
-let rules_of_lit_defs (defs : lit_def list) =
+let rules_of_defs defs =
   Aux.concat_map (fun (rel, branches) ->
     List.map (fun (args, body, neg_body) ->
-      let neg_body =
-        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 : lit_def list) =
+(* Stratify w.r.t. the negation call-graph. *)
+let rec stratify strata defs =
   match
     List.partition (fun (_, branches) ->
-      List.for_all (fun (_, body, neg_body) ->
-        let neg_body = List.map snd neg_body in
+      List.for_all (fun (_, _, neg_body) ->
         List.for_all (fun (rel1,_) ->
           rel1 = "distinct" || rel1 = "true" || rel1 = "does" ||
-            not (List.mem_assoc rel1 defs))
-          (if def then body @ neg_body
-           else neg_body)) branches) defs
+            not (List.mem_assoc rel1 defs)) neg_body)
+        branches) defs
   with
     | [], [] ->
       (* {{{ log entry *)
@@ -269,28 +172,22 @@
       (* }}} *)
       List.rev (stratum::strata)
     | [], _ ->
-      if def then raise
+      raise
         (Lexer.Parsing_error
-           "GDL.stratify: recursive non-static definitions not handled yet")
-      else raise
-        (Lexer.Parsing_error
            "GDL.stratify: cyclic negation dependency")
     | stratum, rules ->
-      if not def then
         let stratum, more_rules = List.partition (fun (_, branches) ->
           List.for_all (fun (_, body, neg_body) ->
             List.for_all (fun (rel1,_) ->
               rel1 = "distinct" || rel1 = "true" || rel1 = "does" ||
                 not (List.mem_assoc rel1 rules))
               body) branches) stratum in
-        stratify ~def (stratum::strata) (more_rules @ rules)
-      else stratify ~def (stratum::strata) rules
+        stratify (stratum::strata) (more_rules @ rules)
       
 
 let rec subst_one (x, term as sb) = function
   | Var y when x=y -> term
-  | MVar y when x=y -> term
-  | (Const _ | Var _ | MVar _ as t) -> t
+  | (Const _ | Var _ as t) -> t
   | Func (f, args) ->
     Func (f, List.map (subst_one sb) args)
 
@@ -321,73 +218,9 @@
     | _ -> raise Not_found
 
 
-(* Match the first argument as term against the second argument as
-   pattern. Allow nonlinear (object) variables. *)
-let rec match_meta ?(ignore_meta=false) sb m_sb terms1 terms2 =
-  match terms1, terms2 with
-    | [], [] -> sb, m_sb
-    | (Const _ (* | Var _ *) as a)::terms1,
-      (Const _ (* | Var _ *) as b)::terms2
-        when a=b -> match_meta ~ignore_meta sb m_sb terms1 terms2
-    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
-      match_meta ~ignore_meta sb m_sb (args1 @ terms1) (args2 @ terms2)
-    | term::terms1, MVar x::terms2 ->
-      (* we don't substitute because metavariables are linear *)
-      match_meta ~ignore_meta sb ((x, term)::m_sb) terms1 terms2
-    | MVar _::terms1, _::terms2 ->
-      if ignore_meta then match_meta ~ignore_meta sb m_sb terms1 terms2
-      else raise Not_found
-    | term::terms1, Var x::terms2 ->
-      let sb1 = x, term in
-      let sb = 
-        if List.mem_assoc x sb then
-          if List.assoc x sb = term then sb
-          else raise Not_found
-        else sb1::sb in
-      match_meta ~ignore_meta sb m_sb terms1 terms2
-    | _ ->
-      (* {{{ log entry *)
-      if !debug_level > 4 then (
-        Printf.printf "match_meta: unmatched (%s) against pattern (%s)\n%!"
-          (String.concat ", " (List.map term_str terms1))
-          (String.concat ", " (List.map term_str terms2))
-      );
-      (* }}} *)
-      raise Not_found
-
-
-let generalize term1 term2 =
-  let fresh_count = ref 0 in
-  let rec loop pf terms1 terms2 =
-  match terms1, terms2 with
-    | [], [] -> (0, 0), [], []
-    | (Const a as cst)::terms1, Const b::terms2 when a=b ->
-      let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in
-      (good_vars, good_csts+1), mism, cst::gens
-    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
-      let (good_vars1, good_csts1), mism1, gen_args = loop f args1 args2 in
-      let (good_vars2, good_csts2), mism2, gens = loop pf terms1 terms2 in
-      (good_vars1+good_vars2, good_csts1+good_csts2), mism1 @ mism2,
-      (Func (f,gen_args))::gens
-    | (Var x as var)::terms1, Var y::terms2 when x=y ->
-      let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in
-      (good_vars+1, good_csts), mism, var::gens
-    | t1::terms1, t2::terms2 ->
-      let measure, mism, gens = loop pf terms1 terms2 in
-      incr fresh_count;
-      measure, (t1,t2)::mism, MVar ("MV"^string_of_int !fresh_count)::gens
-    | _::_, [] | [], _::_ -> raise
-      (Lexer.Parsing_error
-         ("GDL.generalize: arity mismatch at function "^pf)) in
-  let measure, mism, gens = loop "impossible" [term1] [term2] in
-  measure, !fresh_count, mism, List.hd gens
-
-
 let rec subst sb = function
   | Var y as t ->
     (try List.assoc y sb with Not_found -> t)
-  | MVar y as t ->
-    (try List.assoc y sb with Not_found -> t)
   | Const _ as t -> t
   | Func (f, args) ->
     Func (f, List.map (subst sb) args)
@@ -409,6 +242,10 @@
   if rel1 = rel2 then unify [] args1 args2
   else raise Not_found
 
+let rels_unify atom1 atom2 =
+  try ignore (unify_rels atom1 atom2); true
+  with Not_found -> false
+
 let subst_rel sb (rel, args) = rel, List.map (subst sb) args
 let subst_rels sb body = List.map (subst_rel sb) body
 
@@ -418,12 +255,28 @@
   let var_terms = List.map (fun v->Var v) (vars1 @ vars2) in
   unify [] var_terms (terms1 @ terms2)
 
-let subst_br sb (head, body, neg_body) =
-  List.map (subst sb) head,
+let subst_br sb (args, body, neg_body) =
+  List.map (subst sb) args,
   subst_rels sb body,
   List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body
 
-let fact_str (rel, args) =
+
+let subst_atom sb = function
+  | Distinct args -> Distinct (List.map (subst sb) args)
+  | Rel rel_atom -> Rel (subst_rel sb rel_atom)
+  | Role arg -> Role (subst sb arg)
+  | True arg -> True (subst sb arg)
+  | Does (arg1, arg2) -> Does (subst sb arg1, subst sb arg2)
+
+let rec subst_literal sb = function
+  | Pos atom -> Pos (subst_atom sb atom)
+  | Neg atom -> Neg (subst_atom sb atom)
+  | Disj disjs -> Disj (List.map (subst_literal sb) disjs)
+
+let subst_clause sb (head, body) =
+  subst_rel sb head, List.map (subst_literal sb) body
+
+let rel_atom_str (rel, args) =
   "(" ^ rel ^ " " ^ String.concat " " (List.map term_str args) ^ ")"
 
 let tuples_str tups =
@@ -434,40 +287,22 @@
 let terms_str facts =
   String.concat ", " (List.map term_str facts)
 
-let facts_str facts = String.concat " " (List.map fact_str facts)
+let rel_atoms_str body = String.concat " " (List.map rel_atom_str body)
 
-let neg_lfacts_str negs =
+let neg_rel_atoms_str neg_body =
   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)
+    (List.map (fun a -> "(not " ^ rel_atom_str a ^")") neg_body)
 
-let neg_facts_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 (and "^facts_str d^"))") negs)
-
 let branch_str rel (args, body, neg_body) =
-    "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
-      " " ^ neg_facts_str neg_body ^ ")"
+    "("^ rel_atom_str (rel, args) ^ " <= " ^ rel_atoms_str body ^
+      " " ^ neg_rel_atoms_str neg_body ^ ")"
 
-let lit_def_str (rel, branches) =
+let 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)
+    "("^ rel_atom_str (rel, args) ^ " <= " ^ rel_atoms_str body ^
+      " " ^ neg_rel_atoms_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)
-
 let sb_str sb =
   String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
 
@@ -486,7 +321,11 @@
         if List.mem head tot_base then []
         else if List.exists (fun (rel,args as neg_atom) ->
           rel = "distinct" && Aux.not_unique args ||
-            List.mem neg_atom tot_base) neg_body then []
+            (* faster option: *)
+            (* List.mem neg_atom tot_base *)
+            (* accurate option: *)
+            List.exists (unifies neg_atom) tot_base
+        ) neg_body then []
         else [Aux.Left head]
       | head, cond1::body, neg_body ->
         Aux.map_try (fun fact ->
@@ -494,7 +333,7 @@
 
           if !debug_level > 5 then (
             Printf.printf "instantiate_one: trying to unify %s and %s\n%!"
-              (fact_str fact) (fact_str cond1)
+              (rel_atom_str fact) (rel_atom_str cond1)
           );
 
           (* }}} *)
@@ -515,7 +354,7 @@
     (* {{{ log entry *)
     if !debug_level > 4 then (
       Printf.printf "inst_stratum: old_base = %s; cur_base = %s\n%!"
-        (facts_str old_base) (facts_str cur_base);
+        (rel_atoms_str old_base) (rel_atoms_str cur_base);
       Printf.printf
         "inst_stratum: #old_irules = %d, #cur_irules = %d\n%!"
         (List.length old_irules) (List.length cur_irules)
@@ -528,7 +367,7 @@
     (* {{{ log entry *)
     if !debug_level > 4 then (
       Printf.printf "inst_stratum: cur-cur = %s\n%!"
-        (facts_str new_base1)  
+        (rel_atoms_str new_base1)  
     );
     (* }}} *)
     let new_base2, new_irules2 =
@@ -536,7 +375,7 @@
     (* {{{ log entry *)
     if !debug_level > 4 then (
       Printf.printf "inst_stratum: cur-old = %s\n%!"
-        (facts_str new_base2)  
+        (rel_atoms_str new_base2)  
     );
     (* }}} *)
     let new_base3, new_irules3 =
@@ -544,7 +383,7 @@
     (* {{{ log entry *)
     if !debug_level > 4 then (
       Printf.printf "inst_stratum: old-cur = %s\n%!"
-        (facts_str new_base3)  
+        (rel_atoms_str new_base3)  
     );
     (* }}} *)
     let new_base = Aux.unique_sorted (new_base1 @ new_base2 @ new_base3)
@@ -564,9 +403,117 @@
       instantiate (inst_stratum [] [] base stratum) strata in
 
   instantiate base
-    (List.map rules_of_lit_defs (stratify [] (lit_defs_of_rules rules)))
+    (List.map rules_of_defs (stratify [] (defs_of_rules rules)))
 
+(* ************************************************************ *)
+(* ************************************************************ *)
+(** {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 =
+  let used_vars = ref (gdl_defs_vars (("",brs)::defs)) in
+  let freshen_brs brs =
+    let br_vars = gdl_defs_vars ["",brs] in
+    let sb = List.map
+      (fun v ->
+        v, Aux.not_conflicting_name ~truncate:true !used_vars v)
+      (Aux.Strings.elements br_vars) in
+    used_vars := Aux.add_strings (List.map snd sb) !used_vars;
+    List.map (subst_br sb) brs in
+  let expand_atom (rel, args as atom) result =
+    (let try def_brs = freshen_brs (List.assoc rel defs) in
+     Aux.concat_map (fun (sb, (head, r_body, r_neg_body)) ->
+       let args = subst_terms sb args in
+       List.map (fun (params,d_body,d_neg_body) ->
+         let sb = unify sb params args in
+         let r_br =
+           head, d_body @ r_body, d_neg_body @ r_neg_body in
+         sb, subst_br sb r_br
+       ) def_brs
+     ) result
+     with Not_found ->
+       List.map (fun (sb,(head,r_body,r_neg_body)) ->
+         sb, atom::r_body, r_neg_body) result) in
+  let expand_br (head, body, neg_body) =
+    let init = [[], (head, [], neg_body)] in
+    Aux.concat_foldr expand_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
+    if new_n_brs > n_brs && i > 0 then fix new_n_brs brs (i-1)
+    else brs in
+  fix (List.length brs) brs 5
+
+
+(** Form clause bodies whose disjunction is equivalent to the
+    negation of disjunction of given clause bodies. *)
+let negate_bodies conjs =
+  let placeholder = "", [] in
+  let clauses = List.map (fun body -> placeholder, body) conjs in
+  let clauses = List.map rules_of_clause clauses in
+  let clauses = List.map (fun (_,body,neg_body) ->
+    List.map (fun a -> Pos (atom_of_clause a)) body @
+      List.map (fun a -> Neg (atom_of_clause 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) -> Left terms
+        | Neg atom -> Pos atom
+        | Pos atom -> Neg atom
+        | Disjunction _ -> assert false) body in
+    let sb = List.fold_left unify_all [] uniterms in
+    List.map (subst_literal sb) lits in
+  Aux.map_try nclause negated
+
+
+(** Rename clauses so that they have disjoint variables. Return a cell
+    storing all variables. *)
+let rename_clauses clauses =
+  let used_vars = ref Aux.Strings.empty in
+  let clauses = List.map (fun cl ->
+    let cl_vars = clause_vars cl in
+    let sb =
+      List.map (fun v ->
+        let nv = Aux.not_conflicting_name ~truncate:true !used_vars v in
+        used_vars := Aux.Strings.add nv !used_vars;
+        v, nv
+      ) cl_vars in
+    subst_clause sb cl
+  ) clauses in
+  used_vars, clauses    
+
+
+let flatten_disjs body =
+  let rec aux = function
+    | (Pos _ | Neg _) as lit -> [lit]
+    | Disj lits -> Aux.concat_map aux lits in
+  List.map (function
+    | (Pos _ | Neg _) as lit -> lit
+    | Disj _ as disj -> Disj (aux disj)) body
+
+
+let nnf_dnf body =
+  List.map (function
+    | Pos a -> [Neg a]
+    | Neg a -> [Pos a]
+    | Disj lits ->
+      List.map (function
+        | Pos a -> Neg a
+        | Neg a -> Pos a
+        | _ -> assert false) lits
+  ) (List.map flatten_disjs body)
+
+
+(* ************************************************************ *)
+(* ************************************************************ *)
+(** {3 GDL whole-game operations.}
+
+    Aggregate playout, player-denoting variable elimination. *)
+
 (* Collect the aggregate playout, but also the actions available in
    the state. *)
 exception Playout_over
@@ -578,7 +525,7 @@
   (* {{{ log entry *)
   if !debug_level > 4 then (
     Printf.printf "GDL.aggregate_ply: updated base -- %s\n%!"
-      (String.concat " " (List.map fact_str base))
+      (rel_atoms_str base)
   );
   (* }}} *)
   let does = Aux.map_some (fun (rel, args) ->
@@ -714,23 +661,258 @@
         loop cycle trav [] cycle tail in
   loop [] [] [] [] cands
 
-let cmp_masks t1 t2 =
-  (* {{{ log entry *)
-  if !debug_level > 4 then (
-    Printf.printf "cmp_masks: %s <= %s .. " (term_str t1) (term_str t2);
-  );
-  (* }}} *)
-  try ignore (match_meta [] [] [t2] [t1]);
-      (* {{{ log entry *)
-      if !debug_level > 4 then (
-        Printf.printf "true\n%!";
-      );
-      (* }}} *)
-      true
-  with Not_found ->
-    (* {{{ log entry *)
-    if !debug_level > 4 then (
-      Printf.printf "false\n%!";
-    );
-    (* }}} *)
-    false
+
+let expand_players clauses =
+  let players =
+    Aux.map_some (function
+      | ("role", [player]), _ -> Some player
+      | _ -> None
+    ) clauses in
+  let exp_clause (rel, _ as head, body as clause) =
+    (* determine variables standing for players *)
+    let plvars =
+      let head = if rel = "role" then [] else [head] in
+      Aux.concat_map player_vars_of
+        (head @ List.map rel_of_atom body) in
+    if plvars = [] then [clause]
+    else
+      let sbs = List.map (fun v ->
+        List.map (fun pl -> v, pl) players) plvars in
+      List.map (fun sb -> subst_clause sb clause) sbs in
+  Aux.concat_map exp_clause clauses
+
+(** Partition relations into stable (not depending, even indirectly,
+    on "true") and remaining ones. *)
+let stable_rels defs =
+  let rec aux nonstable remaining =
+    let more = Aux.map_some (fun (rel, branches) ->
+      if List.exists
+        (fun (_, body, neg_body) ->
+          let called = List.map fst (body @ neg_body) in
+          List.exists (fun rel -> rel = "true" ||
+              List.mem rel nonstable) called
+        ) branches
+      then Some rel else None
+    ) remaining in
+    if more = [] then List.map fst remaining, nonstable
+    else aux (more @ nonstable)
+      (List.filter (fun (rel,_) -> not (List.mem rel more)) remaining)
+    in
+  aux [] remaining
+
+
+let state_terms body =
+  let rec aux = function
+    | Pos (True t) -> [t]
+    | Neg (True t) -> [t]
+    | Disj ls -> Aux.concat_map aux ls
+    | _ -> [] in
+  Aux.concat_map aux body
+
+let rec term_arities =
+  function
+    | Func (rel, args) ->
+      (rel, Array.length args)::
+        Aux.concat_map term_arities (Array.to_list args)
+    | _ -> []
+
+
+(* ************************************************************ *)
+(* ************************************************************ *)
+(** {3 Paths and operations involving terms and paths.} *)
+
+(** A path is a position in a tree together with labels on nodes from
+    the root to that position (but excluding the position). *)
+type path = (string * int) list
+
+(** A trie representing a set of paths. *)
+type path_set =
+  | Empty
+  | Here                              (** Singleton $\{\epsilon\}$. *)
+  | Below of (string * path_set array) list
+  | Here_and_below of (string * path_set array) list
+(* Subtries are in sorted order. *)
+
+let path_str p =
+  String.concat "_" (List.map (fun (rel, arg) ->
+    rel ^ "_" ^ string_of_int arg) p)
+
+let paths_union ps1 ps2 =
+  let rec aux = function
+    | Empty, p | p, Empty -> p
+    | Here, Below ps | Below ps, Here -> Here_and_below ps
+    | Below ps1, Below ps2 -> Below (merge (ps1, ps2))
+    | Below ps1, Here_and_below ps2
+    | Here_and_below ps2, Below ps1
+    | Here_and_below ps1, Here_and_below ps2
+      -> Here_and_below (merge (ps1, ps2))
+  and merge = function
+    | [], ps | ps, [] -> ps
+    | ((rel1, args1)::ps1), ((rel2, args2)::ps2) when rel1 = rel2 ->
+      let args = Aux.array_map2 aux args1 args2 in
+      (rel1, args)::merge (ps1, ps2)
+    | ((rel1, _ as rel_ps)::ps1), ((rel2, _)::_ as ps2) when rel1 < rel2 ->
+      rel_ps::merge (ps1, ps2)
+    | ((rel1, _)::_ as ps1), ((rel2, _ as rel_ps)::ps2) ->
+      rel_ps::merge (ps1, ps2) in
+  aux (ps1, ps2)
+
+let add_path arities p ps =
+  let rec aux = function
+    | [], Empty -> Here
+    | [], (Below ps | Here_and_below ps) -> Here_and_below ps
+    | (rel, pos)::suffix, Below ps ->
+      Below (add suffix rel pos ps)
+    | (rel, pos)::suffix, Here_and_below ps ->
+      Here_and_below (add suffix rel pos ps)
+  and add p rel pos ps =
+    (let try args, ps = Aux.pop_assoc rel ps in
+     (* Keeping functional... *)
+     let args = Array.copy args in
+     args.(pos) <- aux (p, args.(pos));
+     (rel, args)::ps
+     with Not_found ->
+       let args = Array.make (arities rel) Empty in
+       args.(pos) <- aux (p, args.(pos));
+       (rel, args)::ps)
+  in
+  aux (p, ps)
+
+(** Find a path in a term and substitute, raise [Not_found] if path
+    not present. [subst_at_path p s t] is $t[p \ot s]$. *)
+let subst_at_path 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)
+    | _ -> raise Not_found in
+  aux (p, t)
+
+(** [simult_subst ps s t] substitutes [s] at all [t] paths that belong
+    to the set [ps], returns $t[ps \ot s]$. *)
+let simult_subst ps s t =
+  let rec aux = function
+    | Empty, t -> t
+    | (Here | Here_and_below _), _ -> s
+    | Below subps, (Func (rel, args) as t) ->
+      (let try argps = List.assoc rel subps in
+       Func (rel, Aux.array_map2 (fun ps t -> aux (ps,t)) argps args)
+       with Not_found -> t)
+    | Below _, t -> t in
+  aux (ps, t)
+
+(** Find the subterm at given path, if the term does not have the
+    path, return [Not_found]; [at_path p t] is $t \tpos p$. *)
+let at_path t p =
+  let rec aux = function
+    | [], t -> t
+    | (rel1, pos)::p, Func (rel2, args) when rel1 = rel2 ->
+      aux (p, args.(pos))
+    | _ -> raise Not_found in
+  aux (p, t)
+
+(** Find the list of subterms at paths from the given set, if the term
+    does not have some of the paths, ignore them if [~fail_at_missing:false],
+    raise [Not_found] if [~fail_at_missing:true]. *)
+let at_paths ?(fail_at_missing=false) ps t =
+  let miss () =
+    if fail_at_missing then raise Not_found else [] in
+  let rec aux = function
+    | Empty, t -> []
+    | Here, t -> [t]
+    | Here_and_below subps, t -> t::(aux (Below subps, t))
+    | Below subps, (Func (rel, args) as t)
+      when not fail_at_missing ->
+      (let try argps = List.assoc rel subps in
+       let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in
+       List.concat (Array.to_list res)
+       with Not_found -> [])
+    | Below [rel1, argps], (Func (rel2, args) as t)
+      when rel1 = rel2 (* && fail_at_missing *) ->
+       let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in
+       List.concat (Array.to_list res)
+    | Below _, t -> miss () in
+  aux (ps, t)
+
+(** Find the list of results of a function applied to paths from the
+    given set that are in the term, and to subterms at these paths. *)
+let map_paths f ps t =
+  let rec aux revp = function
+    | Empty, t -> []
+    | Here, t -> [f (List.rev revp) t]
+    | Here_and_below subps, t ->
+      f (List.rev revp) t::(aux path (Below subps, t))
+    | Below subps, (Func (rel, args) as t) ->
+      (let try argps = List.assoc rel subps in
+       let res =
+         Array.mapi (fun i ps -> aux ((rel,i)::revp) (ps,args.(i))) argps in
+       List.concat (Array.to_list res)
+       with Not_found -> [])
+    | Below _, t -> [] in
+  aux [] (ps, t)
+
+(** All paths in a term pointing to subterms that satisfy a
+    predicate. With [~prefix_only:true], paths that contain a path
+    that has been included, are not included. *)
+let rec term_paths ?(prefix_only=false) cond = function
+  | Func (rel, args) as t ->
+    let subps = Array.map (term_paths p) args in
+    let no_sub = Array.for_all (fun subp -> subp = Empty) subps in
+    let here =  cond t in
+    if no_sub && not here then Empty
+    else if here && not no_sub && not prefix_only then Here_and_below subps
+    else if here then Here
+    else Below subps
+  | t -> if cond t then Here else Empty
+      
+(** The number of nodes in a term tree. *)
+let rec term_size = function
+  | Const _ | Var _ -> 1
+  | Func (_, args) ->
+    Array.fold_left (fun acc t -> acc + term_size t) 1 args
+
+(** The set of paths that merges two terms, the cardinality of this
+    set, and the size of the largest common subtree. *)
+let rec merge_terms s t =
+  match s, t with
+    | s, t when s = t -> Empty, 0, term_size t
+    | Func (rel1, args1), Func (rel2, args2) when rel1 = rel2 ->
+      let subr = Aux.array_map2 merge_terms args1 args2 in
+      let subps = Array.map Aux.fst3 subr
+      and subcard = Array.map Aux.snd3 subr
+      and subsize = Array.map Aux.trd3 subr in
+      Below [rel1, subps], Array.fold_left (+) 0 subcard,
+      Array.fold_left (+) 1 subsize
+    | _ -> Here, 1, 0
+
+
+(** List the paths in a set. *)
+let paths_to_list ps =
+  let rec subpaths subps =
+    Aux.concat_map (fun (rel, subps) ->
+      Array.to_list
+        (Array.mapi (fun i ps ->
+          let sub_res = aux ps in
+          List.map (fun p -> (rel, i)::p) sub_res) subps)) subps
+  and aux = function
+    | Empty -> []
+    | Here -> [[]]
+    | Here_and_below subps -> []::(subpaths subps)
+    | Below subps -> subpaths subps in
+  aux ps
+
+
+(** Toss relations hold between subterms of GDL state terms: generate
+    Toss relation name. *)
+let rel_on_paths rel paths_tup =
+  rel ^ "__" ^ String.concat "__" (List.map path_str paths_tup)
+
+(** Some Toss predicates are generated from a path and an expected
+    subterm at that path. *)
+let pred_on_path_subterm path subterm =
+  path_str path ^ term_to_name subterm
+
+(** A "blank" term. *)
+let blank = Const "_BLANK_"

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/GGP/GDL.mli	2011-07-09 10:28:17 UTC (rev 1507)
@@ -19,13 +19,23 @@
 type term =
   | Const of string
   | Var of string
-  | MVar of string
   | Func of string * term list
 
+type rel_atom = string * term list
+(** Positive and negative literals separated, disjunctions expanded-out. *)
+type gdl_rule = rel_atom * rel_atom list * rel_atom list
+(** Collect rules by relations. *)
+type def_branch = term list * rel_atom list * rel_atom list
+type gdl_defs = (string * def_branch list) list
+
+module Terms : Set.S with type elt = term
+module Atoms : Set.S with type elt = rel_atom
+
 type atom =
   | Distinct of term list
-  | Rel of string * term list
-  | Currently of term
+  | Rel of rel_atom
+  | Role of term
+  | True of term
   | Does of term * term
 
 type literal =
@@ -33,71 +43,37 @@
   | Neg of atom
   | Disj of literal list
 
-type game_descr_entry =
-  | Datalog of string * term list * literal list
-  | Next of term * literal list
-  | Legal of term * term * literal list
-  | Goal of term * int * literal list
-  | GoalPattern of term * string * literal list
-  | Terminal of literal list
-  | Role of term
-  | Initial of term * literal list
-  | Atomic of string * term list
+type clause = rel_atom * literal list
 
 type request =
-  | Start of string * term * game_descr_entry list * int * int
+  | Start of string * term * clause list * int * int
   (** prepare game: match id, role, game, startclock, playclock *)
   | Play of string * term list
   (** request a move: match id, actions on previous step *)
   | Stop of string * term list
   (** game ends here: match id, actions on previous step *)
 
-(** 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 conjunctions. *)
-type exp_def_branch =
-    term list * gdl_atom list * (Aux.Strings.t * gdl_atom list) list
-type exp_def = string * exp_def_branch list
-
-module Terms : Set.S with type elt = term
-module Atoms : Set.S with type elt = gdl_atom
-
 val term_str : term -> string
 val terms_str : term list -> string
 val sb_str : (string * term) list -> string
-val fact_str : string * term list -> string
-val facts_str : (string * term list) list -> string
-val exp_def_str : exp_def -> string
+val rel_atom_str : rel_atom -> string
+val rel_atoms_str : rel_atom list -> string
+val def_str :
+  string * (term list * rel_atom list * rel_atom list) -> string
 val tuples_str : term list list -> string
 val proto_rel_str : string * string array -> string
 
-val lit_def_br_vars : lit_def_branch -> Aux.Strings.t
-val lit_def_str : lit_def -> string
-val neg_facts_str : (Aux.Strings.t * gdl_atom list) list -> string
+val gdl_rule_vars : gdl_rule -> Aux.Strings.t
+val gdl_rules_vars : gdl_rule list -> Aux.Strings.t
 
+val branch_str : string -> def_branch -> string
 
-val exp_def_br_vars : exp_def_branch -> Aux.Strings.t
-val branch_str : string -> exp_def_branch -> string
-
-val sdef_br_vars : term * gdl_atom list * (Aux.Strings.t * gdl_atom list) list->
-  Aux.Strings.t
-val sdef_brs_vars : 
-  (term * gdl_atom list * (Aux.Strings.t * gdl_atom list) list) list ->
-  Aux.Strings.t
-
 val func_graph : string -> term list -> term list list
 
-val rules_of_entry : game_descr_entry -> gdl_rule list
+val rules_of_clause : clause -> gdl_rule list
 
 val terms_vars : term list -> Aux.Strings.t
-val rels_vars : gdl_atom list -> Aux.Strings.t
+val rels_vars : rel_atom list -> Aux.Strings.t
 
 val term_to_name : ?nested:bool -> term -> string
 val term_vars : term -> Aux.Strings.t
@@ -107,40 +83,24 @@
 
 val subst_one : string * term -> term -> term
 val subst : (string * term) list -> term -> term
-val subst_rel : (string * term) list -> gdl_atom -> gdl_atom
-val subst_rels : (string * term) list -> gdl_atom list -> gdl_atom list
-val subst_br : (string * term) list -> exp_def_branch -> exp_def_branch
+val subst_rel : (string * term) list -> rel_atom -> rel_atom
+val subst_rels : (string * term) list -> rel_atom list -> rel_atom list
+val subst_br : (string * term) list -> def_branch -> def_branch
 
-val add_neg_body_vars : Aux.Strings.t -> gdl_atom list ->
-  (Aux.Strings.t * gdl_atom) list
+val defs_of_rules : gdl_rule list -> gdl_defs
 
-val lit_defs_of_rules : 
-  ((string * term list) * gdl_atom list * (string * term list) list) list ->
-  lit_def list
-
-val exp_defs_of_lit_defs : lit_def list -> exp_def list
-
-val match_meta : ?ignore_meta:bool -> (string * term) list ->
-  (string * term) list -> term list -> term list ->
-  (string * term) list * (string * term) list
-
 val unify :
   (string * term) list -> term list -> term list -> (string * term) list
 
 val unifies : term -> term -> bool
 
-val generalize : term -> term -> (int * int) * int * (term * term) list * term
+val saturate : rel_atom list -> gdl_rule list -> rel_atom list
 
-val saturate : gdl_atom list -> gdl_rule list -> gdl_atom list
+val stratify : gdl_defs list -> gdl_defs -> gdl_defs list
 
-val stratify : ?def:bool -> lit_def list list ->
-  lit_def list -> lit_def list list
-
 val aggregate_playout :
   term array -> int -> gdl_rule list ->
   gdl_rule list * gdl_rule list * (string * term list) list * 
     term list * (term list list list * term list list)
 
 val find_cycle : term option list -> term option list
-
-val cmp_masks : term -> term -> bool

Modified: trunk/Toss/GGP/GDLParser.mly
===================================================================
--- trunk/Toss/GGP/GDLParser.mly	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/GGP/GDLParser.mly	2011-07-09 10:28:17 UTC (rev 1507)
@@ -17,7 +17,7 @@
 %start parse_game_description parse_request parse_term
 %type <GDL.request> parse_request request
 %type <GDL.term> parse_term
-%type <GDL.game_descr_entry list> parse_game_description game_description
+%type <GDL.clause list> parse_game_description game_description
 
 
 %%
@@ -44,11 +44,11 @@
       | (Const "distinct" | Const "DISTINCT")::args ->
         Distinct args
       | [(Const "true" | Const "TRUE"); arg] ->
-        Currently arg
+        True arg
       | [(Const "does" | Const "DOES"); player; action] ->
         Does (player, action)
       | (Const "role" | Const "ROLE")::player ->
-        Rel ("role", player)
+        Role player
       | (Const "init" | Const "INIT")::state ->
         Rel ("init", state)
       | (Const "next" | Const "NEXT")::state ->
@@ -71,38 +71,12 @@
 | OPEN NOT a=atom CLOSE { Neg a }
 | OPEN OR disjs=list (literal) CLOSE { Disj disjs }
 
-game_descr_entry:
+clause:
 | OPEN REVIMPL head=atom body=list (literal) CLOSE
     { match head with
-      | Rel ("next", [t]) -> Next (t, body)
-      | Rel ("next", _) ->
-        raise (Lexer.Parsing_error "GDL next: not unary")
-      | Rel ("init", [arg]) -> Initial (arg, body)
-      | Rel ("init", _) ->
-        raise (Lexer.Parsing_error "GDL init: not unary")
-      | Rel ("terminal", []) -> Terminal body
-      | Rel ("terminal", _) ->
-        raise (Lexer.Parsing_error "GDL terminal: not nullary")
-      | Rel ("legal", [t1; t2]) ->
-        Legal (t1, t2, body)
-      | Rel ("legal", _) ->
-        raise (Lexer.Parsing_error "GDL legal: not binary")
-      | Rel ("goal", [t; Const gv]) ->
-        (try
-          let gv = int_of_string gv in
-          Goal (t, gv, body)
-        with Failure _ | Invalid_argument _ ->
-          raise (Lexer.Parsing_error "GDL goal: value not a constant int"))
-      | Rel ("goal", [t; Var gv]) ->
-        (try
-          GoalPattern (t, gv, body)
-        with Failure _ | Invalid_argument _ ->
-          raise (Lexer.Parsing_error "GDL goal: value not a constant int"))
-      | Rel ("goal", _) | Rel ("GOAL", _) ->
-        raise (Lexer.Parsing_error
-                 "GDL goal: not binary or value not constant")
-      | Rel (r, args) -> Datalog (r, args, body)
-      | Currently _ ->
+      | Rel rel_atom -> rel_atom, body
+      | Role player -> ("role", [player]), body
+      | True _ ->
         raise (Lexer.Parsing_error "GDL rule: \"true\" in head")
       | Distinct _ ->
         raise (Lexer.Parsing_error "GDL rule: \"distinct\" in head")
@@ -111,13 +85,8 @@
     }
 | a=atom
     { match a with
-      | (Rel ("init", [arg])) -> Initial (arg, [])
-      | (Rel ("init", _)) ->
-        raise (Lexer.Parsing_error "GDL init: not unary")
-      | (Rel ("role", [arg])) -> Role arg
-      | (Rel ("role", _) | Rel ("ROLE", _)) ->
-        raise (Lexer.Parsing_error "GDL role: not unary")
-      | Rel (r, args) -> Atomic (r, args)
+      | Role player -> ("role", [player]), []
+      | Rel rel_atom -> rel_atom, []
       | _ ->
         raise (Lexer.Parsing_error
                  "GDL atomic entry: not init, role nor fact")
@@ -125,7 +94,7 @@
 
 
 %public game_description:
-| descr=list(game_descr_entry)
+| descr=list(clause)
     { descr }
 
 %public request:

Modified: trunk/Toss/GGP/Translate.ml
===================================================================
--- trunk/Toss/GGP/Translate.ml	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/GGP/Translate.ml	2011-07-09 10:28:17 UTC (rev 1507)
@@ -2072,8 +2072,8 @@
       rname, List.map (fun _ -> ()) args) static_rules) in
   let static_rels =
     List.map (fun (rel,args) ->
-      rel, List.length args,
-      Aux.all_tuples_for args mask_paths) static_rels in
+      let ar = List.length args in
+      rel, ar, Aux.all_ntuples mask_paths ar) static_rels in
   let static_base = Aux.collect static_base in
   (* TODO: optimize by indexing elements by path position
      terms (currently, substitution values) *)
@@ -3696,7 +3696,7 @@
       
   
 let translate_last_action gdl_translation state actions =
-  if actions = [] then (* start of game -- Server will handle this as NOOP *)
+  if actions = [] then (* start of game -- Server will not perform a move *)
     "", []
   else translate_incoming_move gdl_translation state actions
 

Modified: trunk/Toss/Solver/Structure.ml
===================================================================
--- trunk/Toss/Solver/Structure.ml	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/Solver/Structure.ml	2011-07-09 10:28:17 UTC (rev 1507)
@@ -261,7 +261,32 @@
   let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
     { new_struc with relations = new_rel ; incidence = new_incidence }
 
+(* Add tuple [tp] to relation [rn] in structure [struc]. *)
+let add_rel_named_elems struc rn tp =
+  let new_struc, tp =
+    Array.fold_right (fun (struc, tp) e ->
+      let struc, e = find_or_new_elem struc e in
+      struc, e::tp)
+      (add_rel_name rn (Array.length tp) struc) tp in
+  let tp = Array.of_list tp in
+  let add_to_relmap rmap = 
+    let tps = StringMap.find rn rmap in
+    StringMap.add rn (Tuples.add tp tps) rmap in
+  let new_rel = add_to_relmap new_struc.relations in
+  let add_to_imap imap e = 
+    try
+      IntMap.add e (Tuples.add tp (IntMap.find e imap)) imap
+    with Not_found -> 
+      IntMap.add e (Tuples.singleton tp) imap  in
+  let new_incidence_imap = 
+    try
+      Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
+    with Not_found -> 
+      Array.fold_left add_to_imap IntMap.empty tp in
+  let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
+    { new_struc with relations = new_rel ; incidence = new_incidence }
 
+
 (* Return a structure with a single relation, over a single tuple, of
    different elements. *)
 let free_for_rel rel arity =

Modified: trunk/Toss/Solver/Structure.mli
===================================================================
--- trunk/Toss/Solver/Structure.mli	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/Solver/Structure.mli	2011-07-09 10:28:17 UTC (rev 1507)
@@ -167,6 +167,9 @@
 (** Add tuple [tp] to relation [rn] in structure [struc]. *)
 val add_rel : structure -> string -> int array -> structure
 
+(** Add tuple [tp] to relation [rn] in structure [struc]. *)
+val add_rel_named_elems : structure -> string -> string array -> structure
+
 (** Add tuple [tp] to relation [rn] in structure [struc] without
     checking whether it and its elements already exist in the structure
     and without checking arity. *)

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-07-06 22:13:35 UTC (rev 1506)
+++ trunk/Toss/www/reference/reference.tex	2011-07-09 10:28:17 UTC (rev 1507)
@@ -1343,11 +1343,13 @@
 of $s$ and $t$, the bigger its size the more similar $s$ and $t$ are.
 \end{definition}
 
-Let $\mathrm{Next}_{e}$ be the set of \texttt{next} clauses in $G$ with all
-atoms of \texttt{does} expanded (inlined) by the \texttt{legal}
-clause definitions, duplicating the \texttt{next} clause when more
-than one head of \texttt{legal} unifies with the \texttt{does} atom.
-Intuitively, these are expanded forms of clauses defining game state change.
+Let $\mathrm{Next}_{e}$ be the set of \texttt{next} clauses in $G$
+with all atoms of relations whose definitions use \texttt{true}
+expanded (inlined) by their clause definitions, duplicating the
+\texttt{next} clause when more than one clause of a relation unifies
+with its atom. We expand \texttt{does} atoms by \texttt{legal}
+clauses. We also expand disjunctions. Intuitively, these are expanded
+forms of clauses defining game state change.
 
 For each clause $\calC \in \mathrm{Next}_{e}$, we select two terms
 $s_\calC$ and $t_\calC$ in the following way. The term $s_\calC$ is
@@ -1420,7 +1422,7 @@
 \begin{definition}
 We define the \emph{element mask equivalence} $\sim$ by:
 \[ t \sim s \quad \Leftrightarrow \quad
-   t[P_f \ot c] = s[P_f \ot c] \text{ for all terms } c.\]
+   t[\calP_f \ot c] = s[\calP_f \ot c] \text{ for all terms } c.\]
 The set of elements $A$ of the initial Toss structure $\frakA$ consists
 of equivalence classes of $\sim$. For $a \in A$ we write $\lsem a \rsem$
 to denote the corresponding subset of equivalent terms from $\calS$.
@@ -1488,19 +1490,21 @@
 $p \in \calP_f$ and subterms $s = t\tpos_p, t \in \calS$,
 we introduce the \emph{fluent predicate} $Flu^s_p(a)$:
 \[ Flu^s_p(a) \ \  \iff \ \ t\tpos_p\ =\ s \text{ for some }
-     t \in \lsem a \rsem \cap \calS^{\text{init}}. \]
+t \in \lsem a \rsem \cap \calS^{\text{init}}.
+\]
+Currently in the implementation, the string representing the path $p$
+alone is used as the predicate name, we use the prefixes $Anch$ and
+$Flu$ in the reference for clarity.
 
 \noindent \textbf{Mask predicates.}
-We say that a term $m$ is a \emph{mask term} if the paths to all variables
-of $m$ are contained in $\calP_m \cup \calP_f$ and for each
-$p \in \calP_m \cup \calP_f$ if $p$ exists in $m$ then $m \tpos_p$ is
-a variable. We say that $m$ \emph{masks} a term $t$ if $m$ is a mask term
-and there exists
-a substitution $\sigma$ such that $\sigma(m) = t$. For all mask terms
-$m \in \calS$ we introduce  the \emph{mask predicate} $Mask_m$.
+We define the mask root relation $\sim_m$ by:
+\[ t \sim_m s \quad \Leftrightarrow \quad t[\calP_f \cup \calP_m \ot
+c] = s[\calP_f \cup \calP_m \ot c] \text{ for all terms } c.\] We call
+an equivalence class of $\sim_m$ a \emph{mask root}. For all mask
+roots $m$ we introduce the \emph{mask predicate} $Mask_m$.
 Mask predicates are similar to the anchor predicates, but instead of
-matching against a subterm, they match against the mask.
-\[ Mask_m(a) \ \ \iff \ \ m \text{ masks all } t \in \lsem a \rsem. \]
+matching against a subterm, they match against the mask root.
+\[ Mask_m(a) \ \ \iff \ \ \lsem a \rsem \subset m. \]
 
 %Elements $a \in A$ can be represented as tuples consisting of a mask
 %term $m_a$ such that $Mask_{m_a}(a)$ and terms $s_p = a\tpos^m_p$ for
@@ -1570,8 +1574,8 @@
   \text{ and } \ \ Flu^{\mathtt{x}}_{(\mathtt{control},1)} = \{a_{ctrl}\}. \]
 
 \emph{Mask predicates.}
-For the specification we consider, there are two mask terms:
-$m_1 = (\mathtt{control}\ x)$ and $m_2 = (\mathtt{cell}\ x\ y\ z)$.
+For the specification we consider, there are two mask roots:
+$m_1 = \big\{(\mathtt{control}\ x) \ \big| \ (\mathtt{control}\ x) \in \calS \big\}$ and $m_2 = \big\{(\mathtt{cell}\ x\ y\ z) \ \big|\  (\mathtt{cell}\ x\ y\ z) \in \calS \big\}$.
 The predicate $Mask_{m_1} \ = \ \{ a_{ctrl} \}$ holds exactly for
 the control element, and $Mask_{m_2} = A \setminus \{a_{ctrl}\}$ contains these
 elements of $A$ which are not the control element, \ie the board elements.
@@ -1690,8 +1694,13 @@
 then for correctness, we need to preclude application of the first
 (more general) rule when the more concrete rule is applicable, adding
 \texttt{distinct} conditions to clauses of the otherwise more general
-rule. In the current implementation, we only consider maximal sets of
-\texttt{next} clauses.
+rule. In the current implementation, we select a minimal covering
+family of maximal sets of \texttt{next} clauses, where covering
+means that every clause occurs in at least one set of the
+family. (While in Section~\ref{subsec-rules} we describe additional
+partition of the substituted clauses, in unlikely scenarios the
+generated $\sigma_{\ol{\calC},\ol{\calN}}$ might be too specific to
+capture all possible moves.)
 
 \begin{example}
 Let $\calC_1 = \mathtt{noop}$ and  $\calC_2 = (\mathtt{mark}\ x\ y)$.
@@ -1723,16 +1732,24 @@
 will keep track of the elements that possibly lose fluents and ensure
 correct translation.
 
+We determine which clauses are frame clauses prior to partitioning
+into the rule clauses and computing the substitution
+$\sigma_{\ol{\calC},\ol{\calN}}$ -- at the point where fluent paths
+are computed.
+
 From the frame clauses in $\sigma_{\ol{\calC}, \ol{\calN}}(\calN_1), \dots,
-\sigma_{\ol{\calC}, \ol{\calN}}(\calN_m)$, we select all (maximal) subsets $J$
+\sigma_{\ol{\calC}, \ol{\calN}}(\calN_m)$, we select subsets $J$
 such that, clauses in $J$ having the form $\mathtt{(<= (next\ s_i)\ b_i)}$,
 it holds
-\[ s_1 \ \dot{=}_f \ \ldots \ \dot{=}_f \ s_{|J|}, \]
-\ie the arguments of \texttt{next} unify. Note that we use $\dot{=}_f$
-instead of the standard unification, and by that we mean that the variables
-shared with the \texttt{legal} clauses $\ol{\calC}$ are treated as constants.
-The reason is that these variables are not local to the clauses and must
-therefore remain intact.
+\[ s_1 \ \dot{=}_f \ \ldots \ \dot{=}_f \ s_{|J|}, \] \ie the
+arguments of \texttt{next} unify. Note that we use $\dot{=}_f$ instead
+of the standard unification, and by that we mean that the variables
+shared with the \texttt{legal} clauses $\ol{\calC}$ are treated as
+constants.  The reason is that these variables are not local to the
+clauses and must therefore remain intact. As before, we select a
+minimal covering family of maximal such subsets (possibly resulting,
+in unlikely cases, in rules that do not remove fluent predicates over
+elements that do not gain fluent predicates during rewriting.)
 
 Intuitively, the selected sets $J$ describe a partition of the state terms
 that could possibly be copied without change by the rule we will generate
@@ -1751,8 +1768,8 @@
 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. The
-erasure clauses $\calE_{\ol{\calC}, \ol{\calN}}(J) = \{ \mathtt{(<=\
-  h\ e_1)} \dots \mathtt{(<=\ h\ e_l)} \},$ and we write
+erasure clauses
+$\calE_{\ol{\calC}, \ol{\calN}}(J) = \{ \mathtt{(<=\  h\ e_1)} \dots \mathtt{(<=\ h\ e_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.
@@ -1797,9 +1814,15 @@
 rule clauses, and generate a Toss rule candidate for every partition
 of the groups into true and false ones: we collect the rule clauses
 that agree with the given partition. The selected atoms, some negated
-according to the partition, form the separation condition.
+according to the partition, form the separation condition. Currently,
+we do not consider atoms under disjunction (mostly for simplicity
+considerations; would this cause problems, the definition can be
+extended to include disjunctions in making the partition).
 
-For each candidate, we will construct the Toss rule in two steps.
+We filter the rule candidates by checking for satisfiability (in the
+same GDL model as used for building the initial Toss structure) of the
+stable part of their clause bodies. For each remaining candidate,
+we will construct the Toss rule in two steps.
 
 In the first step we generate the \emph{matching condition}: we
 translate the conjunction of the bodies of rule clauses and the
@@ -1807,10 +1830,6 @@
 atomic relations presented in Section~\ref{subsec-rels} and is
 described in Section~\ref{subsec-translate}.
 
-Later we \emph{filter} the rule candidates by checking for
-satisfiability in the initial structure of the stable part of the
-matching condition.
-
 In the second step, we build a Toss rewrite rule it...
 
[truncated message content]