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

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

Revision: 1277
          http://toss.svn.sourceforge.net/toss/?rev=1277&view=rev
Author:   lukstafi
Date:     2011-01-09 20:58:08 +0000 (Sun, 09 Jan 2011)

Log Message:
-----------
GDL translation initial commit, work in progress. Aux.unique_sorted bug fix.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/AuxTest.ml
    trunk/Toss/Play/GDL.ml
    trunk/Toss/Play/GDL.mli
    trunk/Toss/Play/GDLParser.mly
    trunk/Toss/Play/KIFLexer.mll
    trunk/Toss/Solver/Structure.ml
    trunk/Toss/Solver/Structure.mli

Added Paths:
-----------
    trunk/Toss/Play/GDLTest.ml
    trunk/Toss/examples/breakthrough.gdl
    trunk/Toss/examples/checkers.gdl
    trunk/Toss/examples/chess.gdl
    trunk/Toss/examples/connect5.gdl

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-01-07 11:41:28 UTC (rev 1276)
+++ trunk/Toss/Formula/Aux.ml	2011-01-09 20:58:08 UTC (rev 1277)
@@ -24,6 +24,10 @@
   in
   List.rev (cmap_f [] l)
 
+let rec map_prepend tl f = function
+    [] -> tl
+  | a::l -> let r = f a in r :: map_prepend tl f l
+
 let map_some f l =
   let rec maps_f accu = function
     | [] -> accu
@@ -87,8 +91,15 @@
     let tl = map_try f tl in
     try f hd :: tl
     with Not_found -> tl
-  
 
+let rec fold_left_try f accu l =
+  match l with
+      [] -> accu
+    | a::l ->
+      try
+        fold_left_try f (f accu a) l
+      with Not_found -> fold_left_try f accu l
+
 let product l =
   List.fold_right (fun set prod ->
     concat_map (fun el -> List.map (fun tup -> el::tup) prod) set)
@@ -126,13 +137,27 @@
     | [] -> acc in
   List.rev (aux [] l)
 
-(* TODO: that's quadratic, perhaps (sort |> drop_repeating)
-   would be faster in practice *)
+(* Not tail-recursive. *)
+let unique_sorted l =
+  let rec idemp = function
+    | e1::(e2::_ as tl) when e1 = e2 -> idemp tl
+    | e::tl -> e::idemp tl
+    | [] -> [] in
+  idemp (List.sort Pervasives.compare l)
+
+(* TODO: that's quadratic, optimize? *)
 let rec unique eq = function
   | [] -> []
   | x :: xs ->
     x :: unique eq (List.filter (fun y -> not (eq y x)) xs)
 
+let not_unique xs =
+  let rec aux left = function
+    | [] -> false
+    | x :: xs when List.mem x left || List.mem x xs -> true
+    | x :: xs -> aux (x::left) xs in
+  aux [] xs
+
 let take_n n l =
   let rec aux n acc = function
     | hd::tl when n > 0 ->

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-01-07 11:41:28 UTC (rev 1276)
+++ trunk/Toss/Formula/Aux.mli	2011-01-09 20:58:08 UTC (rev 1277)
@@ -15,6 +15,10 @@
 (** Concatenate results of a function. *)
 val concat_map : ('a -> 'b list) -> 'a list -> 'b list
 
+(** Map a second list and prepend the result to the first list, by
+    single traversal. Not tail-recursive. *)
+val map_prepend : 'a list -> ('b -> 'a) -> 'b list -> 'a list
+
 (** Map a list filtering out some elements. *)
 val map_some : ('a -> 'b option) -> 'a list -> 'b list
 
@@ -54,6 +58,12 @@
     raise [Not_found]. Therefore [map_try] call cannot raise [Not_found]. *)
 val map_try : ('a -> 'b) -> 'a list -> 'b list
 
+
+(** Fold [f] over the list collecting results whose computation does
+    not raise [Not_found]. Therefore [fold_left_try] call cannot raise
+    [Not_found]. *)
+val fold_left_try : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+
 (** Cartesian product of lists. Not tail recursive. *)
 val product : 'a list list -> 'a list list
 
@@ -78,12 +88,18 @@
     equal elements only the last one is preserved.) *)
 val maximal : ('a -> 'a -> bool) -> 'a list -> 'a list
 
+(** Return the list of structurally unique elements, in order sorted
+    by {!Pervasives.compare}. Not tail-recursive. *)
+val unique_sorted : 'a list -> 'a list
+
 (** Return the list of unique elements, under the given comparison
     (the input does not need to be sorted). (Currently uses a
-    straightforward [n^2] algorithm, a sorting-based would reduce it to
-    [n log n]. Currently not tail-recursive.) *)
+    straightforward [n^2] algorithm. Currently not tail-recursive.) *)
 val unique : ('a -> 'a -> bool) -> 'a list -> 'a list
 
+(** Check whether the list contains duplicates, using structural equality. *)
+val not_unique : 'a list -> bool
+
 (** Take [n] elements of the given list, or less it the list does not
     contain enough values. *)
 val take_n : int -> 'a list -> 'a list

Modified: trunk/Toss/Formula/AuxTest.ml
===================================================================
--- trunk/Toss/Formula/AuxTest.ml	2011-01-07 11:41:28 UTC (rev 1276)
+++ trunk/Toss/Formula/AuxTest.ml	2011-01-09 20:58:08 UTC (rev 1277)
@@ -198,13 +198,25 @@
            ["a1";"c2"; "b1"; "a3"; "c7"]);
     );  
 
-  "unique, take_n" >::
+  "unique, unique_soted, not_unique, take_n" >::
     (fun () ->
       assert_equal ~printer:(String.concat "; ")
-        ["a";"c";"b";"d"]
-        (Aux.unique (=) ["a";"c";"b"; "d"; "c"]);
+        ~msg:"should remove duplicates"
+        ["a";"c";"e";"b";"d"]
+        (Aux.unique (=) ["a";"c";"e"; "b"; "d"; "e"; "c"; "e"]);
 
       assert_equal ~printer:(String.concat "; ")
+        ~msg:"should remove duplicates"
+        ["a";"b";"c";"d";"e"]
+        (Aux.unique_sorted ["a";"c";"e"; "b"; "d"; "e"; "c"; "e"]);
+
+      assert_bool "not unique"
+        (Aux.not_unique ["a";"c";"b"; "d"; "c"]);
+
+      assert_bool "unique"
+        (not (Aux.not_unique ["a";"c";"b";"d"]));
+
+      assert_equal ~printer:(String.concat "; ")
         ["a";"c";"b"]
         (Aux.take_n 3 ["a";"c";"b"; "d"; "c"]);
 

Modified: trunk/Toss/Play/GDL.ml
===================================================================
--- trunk/Toss/Play/GDL.ml	2011-01-07 11:41:28 UTC (rev 1276)
+++ trunk/Toss/Play/GDL.ml	2011-01-09 20:58:08 UTC (rev 1277)
@@ -1,10 +1,338 @@
 (** {2 Game Description Language.}
 
-    Type definitions, helper functions, game specification translation. *)
+    Type definitions, helper functions, game specification
+    translation.
 
+    The translation is not complete (yet), and not yet guaranteed to
+    be sound (but aiming at it) -- report any cases where the
+    algorithm does not fail explicitly but does not preserve
+    semantics.
+
+    (1) Aggregate playout: generate successive states as if all moves
+    legal in the previous state were performed. Do not check the
+    termination predicate.
+
+    (1a) Reason for unsoundness: "legal" or "next" preconditions can
+    depend negatively on state, preventing further moves in the
+    aggregate state that would be possible in some of valid game
+    states; the aggregate state does not have enough terms as a
+    result. Workaround: remove negative literals from "legal"/"next"
+    conditions for generating aggregate playout.
+
+    (1b) Saturation works on definitions stratified
+    w.r.t. negation. Positive literals are instantiated one by one,
+    then negative literals are checked over the facts derived from
+    previous strata. To avoid redundancy, new facts and new
+    instantiations are kept separate for the next iteration within a
+    stratum.
+
+    (1c) Heuristic reason for unsoundness: while we check for fixpoint
+    in the playout, we rule out state terms "F(X)" where X is a player
+    (assuming that "F" means "control"). Workaround: turn off fixpoint
+    checking [aggregate_fixpoint].
+
+    (2) Arena graph: currently, only a simple cycle is allowed. The
+    succession of players is determined from the aggregate playout.
+
+    (2a) We need to recognize which player actually makes a move in a
+    state. For this we need to locate the "noop" arguments to "legal"
+    and "does" relations. A noop action in a location is the only
+    action in the corresponding state of an aggregate playout for the
+    player that is additionally constant.
+
+    (2b) We determine the player of a location by requiring that at
+    most one player has a non-noop action in an aggregate
+    state. When all players are noops we select the control player so
+    that the smallest "game cycle" is preserved. Otherwise (more than
+    one no-noop move) we fail (simultaneous moves not supported). We
+    remember the noop actions for each location and player.
+
+    (3) Currently, a constant number of elements is assumed. The rules
+    processed in (3a)-(3b) are already expanded by (6).
+
+    (3a) Element terms are collected from the aggregate playout: the
+    sum of state terms (the "control" function could be dropped but we
+    are not taking the effort to identify it).
+
+    (3b) Element masks are generated by generalization from all "next"
+    rules where the "does" relations are expanded by all unifying
+    "legal" rules (see also (7a)).
+
+    (3c) Generalization in a single expanded "next" rule is by finding
+    for the "next" term the closest "true" term in the lexicographic
+    ordering of (# of matched variables, # of other matched leaves),
+    but in case the closest term is found in the negative part, it is
+    further processed.
+
+    (3c1) Unmatched subterms are replaced by meta-variables.
+    
+    (3c2) When the generalization comes from the negative part, we
+    replace all constant leaves with meta-variables.  Warning: this
+    heuristic is a reason for unsoundness -- search for a workaround
+    once a real counterexample is encountered.
+
+    (3d) The masks are all the minimal w.r.t. matching (substitution)
+    of the generalized terms, with only meta-variable positions of the
+    mask matching meta-variable positions of a generalized
+    term.
+
+    (3e) The elements are the equivalence classes of element terms,
+    where terms are equivalent when they both match a single mask and
+    their matching substitutions differ only at
+    meta-variables. (I.e. for t1 and t2 there exists a mask m and
+    substitutions s1 and s2 such that s1(m)=t1 and s2(m)=t2 and
+    s1(x)=/=s2(x) implies that x is/contains a meta-variable.)
+
+    (Note that there is "nothing wrong" with a given equiv class not
+    having any member in the initial state or some other state. The
+    element is still there in the structure, still participating in
+    the "static" relations, but not in the "dynamic" predicates in
+    that particular state. We use a special _BLANK_ term/predicate to
+    faciliate operations on such "absent" elements.)
+    
+    (4) Static relations (their tuples do not change during the game)
+    are derived from static facts with subterms common with element
+    terms but not below meta-variables.
+
+    Define mask-paths as the set of a mask together with a path in it
+    to a position that is not below (or at) a meta-variable.
+
+    Implementation: currently we approximate paths by only taking the
+    positions of variables in the mask.
+
+    (4a) (Fact relations.) For a static fact (a relation that does not
+    depend on "true" or "init") (unless it is expanded -- see (6)),
+    introduce a relation for each mask-paths tuple with arity of the
+    relation (i.e., introduced relations are a dependent product of
+    static fact relations and a cartesian n-th power of the mask-paths
+    set where n is the arity of the relation). An introduced relation
+    holds over a tuple of elements, iff the corresponding element
+    terms match the respective masks, and the original relation holds
+    over the tuple of subterms selected from the element terms by the
+    corresponding paths.
+
+    (Relations that do not hold for any tuple of element terms in the
+    whole aggregate playout can be removed.)
+
+    (4b) (Equality relations.) For each mask-path, introduce a binary
+    relation that holds over elements which have the same subterm at
+    the mask-path position. (Because of mask-paths definition, same
+    for all element terms in element's equivalence class.)
+
+    (4c) (Anchor predicates.) Collect all terms under "true" and
+    "next" predicates in the game definition. For each mask-path
+    pointing to a constant in some of the terms and that constant,
+    introduce a new predicate with semantics: "matches the mask and
+    has the constant at the path position".
+
+    (5) (Mostly) dynamic relations ("fluents": their tuples change
+    during the game), relations derived from all below-meta-variable
+    subterms of element terms, initialized by those that appear in the
+    initial state. (Some relations introduced in this step might not
+    be fluents.)
+
+    Collect all terms under "true" and "next" predicates in the game
+    definition. For each term, find the element mask it matches, and
+    introduce relations for each meta-variable of the element mask,
+    associated with the subterm that matches the meta-variable. The
+    semantic is that the relation selects the element terms that match
+    the mask with the associated subterm subsituted for the
+    corresponding meta-variable, with existential
+    interpretation. A relation holds initially over an element, if in
+    the initial set of element terms at least one from the element's
+    equivalence class is selected by the relation. An occurrence of
+    "true" or "next" relation is replaced by a conjunction of
+    relations whose substituted-masks match the relation's term.
+
+    When generating predicates that hold over an element term, no
+    predicate is generated for any its meta-variable position that
+    contains _BLANK_.
+
+    (6) Currently how to introduce defined relations in translation is
+    not yet solved in the presented framework. Currently, we simply
+    expand relations that are not static, or (optionally) are static
+    but do not contain ground facts, by duplicating the branch in
+    which body an atom of the relation occurs, for each branch of the
+    relation definition, unifying and applying the unifier. (If the
+    duplication turns out prohibitive, this will be a *huge* TODO for
+    this translation framework.)
+
+    (6a) The definition:
+
+    [(r, params1) <= body1 ... (r, params_n) <= body_n]
+
+    provides a DNF defining formula (using negation-as-failure):
+
+    [(r, args) <=> exist vars1 (args = params1 /\ body1) \/ ...
+    \/ exist vars_n (args = params_n /\ body_n)]
+
+    which expands in a natural way for positive occurrences. We
+    duplicate the branch where [(r, args)] is substitued for each
+    disjunct and apply the unifier of [args = params_i] in the whole
+    [i]th cloned branch. We freshen each [vars_i] to avoid capture. If
+    unification fails, we drop the corresponding branch clone.
+
+    (6b) For negative occurrences we transform the defining formula
+    to:
+
+    [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
+    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
+    subformula inside a branch). We only apply the unifier of [args =
+    params_i] to [body_i] (in general, the whole negated
+    subformula). Still, we freshen each [vars_i] to avoid capture. If
+    unification fails, we drop the corresponding negated
+    subformula. If unification succeeds but the corresponding [body_i]
+    is empty (and, in general, no other disjuncts in the negated
+    subformula are left), we drop the branch.
+
+    (6b1) The general case is not implemented yet since it slightly
+    complicates the code, and expressivity gain is very small.
+
+    (7) Generation of rewrite rules when the dynamic relations are not
+    recursive and are expanded in the GDL definition.
+
+    (7a) We translate each branch of the "legal" relation definition
+    as one or more rewrite rules. Currently, we base availability of
+    rules in a location solely on the player in the location and in
+    the "legal" definition (currently, we do not allow simultaneous
+    moves). Consequently, we define rules on a per-player basis rather
+    than a per-location basis. If the branch of "legal" definition has
+    a variable for a player, it is instantiated for each player in the
+    game, and the variable substituted in the body of the "legal"
+    branch.
+
+    (7b) We collect all the branches of the "next" relation definition
+    for which the selected branch of "legal" unifies with all (usually
+    one, but we allow zero or more) occurrences of "does" with a
+    single unifier per "next" branch. Split the unifiers into
+    equivalence classes (w.r.t. substitution), each class will be a
+    different rewrite rule (or set of rules). Associate negation of
+    equalities specific to the unifiers strictly less general than the
+    equivalence class with it, so that the resulting conditions form a
+    partition of the space of substitutions for the "legal" branch
+    processed.
+
+    (7c) Find a single MGU that unifies the "legal" atom argument and
+    all the "does" atoms arguments into a single instance, and apply
+    it to all "next" branches of the rule. We remember all variables
+    in the "legal"/"does" instantiation as "fixed variables". We
+    replace all occurrences of "does" with the body of the selected
+    "legal" branch.
+
+    (7d) We seggregate "next" atoms into these that contain some fixed
+    variables or no variables at all, and other containing only
+    unfixed variables. Eliminate unfixed variables from "next"
+    atoms with fixed variables by enumerating their domains and
+    duplicating whole "next" branches with each instantiation. (They
+    will not have unfixed variables.)
+
+    (This perhaps could be done in a better way by better integrating
+    (7d) and (7e)...)
+
+    (7e) Branches with (only) unfixed variables in "next" atoms are
+    the "frame" branches. Check that each "frame" branch is an
+    identity: the "next" atom is equal to one of the positive "true"
+    atoms. If not, expand all variables (as they are unfixed)
+    duplicating that branch for each instantiation (the duplicated
+    branches become regular branches -- with constant "next"
+    atoms).
+
+    (7e1) Transform the remaining proper "frame" branches into
+    "erasure" branches: negate the body, push negation inside (using
+    de Morgan laws etc.), reduce to DNF and split into separate
+    "erasure" branch for each disjunct, place the original "next" atom
+    but with meta-variable positions replaced by _BLANK_ as the head
+    of the "erasure" branch, apply (and remove) unification atoms
+    resulting from negating the "distinct" relation.
+
+    (7f) Introduce a new element variable for each class of "next" and
+    "true" terms equal modulo mask (i.e. there is a mask matching them
+    and they differ only at-or-below metavariables). (Remember the
+    atoms "corresponding variable".)
+
+    (7g) Add an appropriate equality relation of (4b) for each case
+    of variable shared by terms corresponding to different element
+    variables (regardless if the element terms are in positive or
+    negative literals).
+
+    (7h) For all subterms of "next" and "true" atoms, identify the
+    sets of <mask-path, element variable> they "inhabit". Replace a
+    static fact relation by relations built over a cartesian product
+    of <mask-path, element variable> sets derived for each static
+    fact's argument by applying corresponding (4a) relations. (For a
+    negative literal the result will be equivalent to a disjunction of
+    negations of generated atoms.)
+
+    (7i) Identify variables in "next" & "true" terms that are
+    at-or-below meta-variables in the corresponding mask. (Most of
+    such variables should be already removed as belonging to "frame"
+    branches.) Expand them by duplicating given branch for all
+    instantiations (all (5) predicates derived from the considered
+    position). (Note that since branches do not have unfixed variables
+    anymore, we do not rename variables during duplication.)
+
+    (7j) Now we build rewrite rules for a refinement of an equivalence
+    class of (7b): from the branches with unifiers in the equiv class,
+    from branches with unifiers more general than the equiv class, and
+    from the disjointness conditions (and the terminal condition, see
+    below). Build a pre-lattice of branch bodies w.r.t. subsumption,
+    in a manner similar to (7b). The subsumption test has to say "no"
+    when there exists a game state where the antecedent holds but the
+    consequent does not, but does not need to always say "yes"
+    otherwise. Build a rewrite rule for each equivalence class
+    w.r.t. subsumption, including also branches that are below the
+    equiv class, and including negation of conditions that make the
+    branches strictly above more specific -- so that the classes form
+    a partition of the nonterminal game states (it is semantically
+    necessary so that all applicable changes are applied in the
+    translated game when making a move).
+
+    (7k) Replace the "next" and "true" atoms by the conjunction of
+    (4c) and (5) predicates over their corresponding variable. (For
+    negative "true" literals this will be equivalent to a disjunction
+    of negations of the predicates.)
+
+    (7l) Include translated negation of the terminal condition.
+
+    The rewrite rule is generated by joining the derived conjunctions
+    from "next" atoms as RHS, and from bodies as the
+    precondition. Exactly the RHS variables are listed in the LHS
+    (other variables are existentially closed in the precondition).
+
+    (8) We use a single payoff matrix for all locations. Goal patterns
+    are expanded to regular goals by instantiating the value variable
+    by all values in its domain (for example, as gathered from the
+    aggregate playout), and expanding all atoms that contained value
+    variables (both static and dynamic) using (6); fail if a goal
+    value cannot be determined. The payoff formula is the sum of
+    "goal" value times the characterisic function of the "goal"
+    body. We do not translate the body if the value is zero (we drop
+    the zero goal branches from the definition). Translate the body
+    using (7f)-(7k), but treating "goal" branches separately -- when
+    (7i) duplicates a branch, new branches add new sum elements.
+
+*)
+
+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 and have
+    arity above the threshold. *)
+let expand_arity_above = ref 0
+
 type term =
   | Const of string
   | Var of string
+  | MVar of string                      (* meta-variable, not used in GDL *)
   | Func of string * term list
 
 type atom =
@@ -16,18 +344,19 @@
 type literal =
   | Pos of atom
   | 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 request =
   | Start of string * term * game_descr_entry list * int * int
   (* prepare game: match id, role, game, startclock, playclock *)
@@ -36,11 +365,369 @@
   | Stop of string * term list
   (* game ends here: match id, actions on previous step *)
 
-let compile_game_descr entries = entries
+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 fact_of_atom = function
+  | Distinct args -> assert false
+  | Rel (rel, args) -> rel, args
+  | Currently arg -> "true", [arg]
+  | Does (arg1, arg2) -> "does", [arg1; arg2]
+
+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)]
+  | 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 expanded definitions: expansion of a negated
+   relation brings negated conjunctions. *)
+type exp_def_branch =
+    term list * gdl_atom list * gdl_atom list list
+type exp_def =
+    string * exp_def_branch list
+
+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 : (string * exp_def_branch list) list =
+  Aux.map_reduce
+    (fun ((drel, params), body, neg_body) ->
+      drel,(params, body, List.map (fun a->[a]) 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) =
+  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
+      (rel, args), body, neg_body) 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) =
+  match
+    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 defs))
+          (if def then body @ List.concat neg_body
+           else List.concat neg_body)) branches) defs
+  with
+    | [], [] -> List.rev strata
+    | stratum, [] -> List.rev (stratum::strata)
+    | [], _ ->
+      if def then 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 -> stratify (stratum::strata) rules
+      
+
+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 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
+  | Func (f, args) ->
+    Func (f, List.map (subst_one sb) args)
+
+let rec unify sb terms1 terms2 =
+  match terms1, terms2 with
+    | [], [] -> sb
+    | Const a::terms1, Const b::terms2 when a=b ->
+      unify sb terms1 terms2
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      unify sb (args1 @ terms1) (args2 @ terms2)
+    | Var x::terms1, Var y::terms2 when x=y ->
+      unify sb terms1 terms2
+    | (Var x::terms1, (Var _ | Const _ as term)::terms2
+          | (Const _ as term)::terms1, Var x::terms2) ->
+      let sb1 = x, term in
+      unify (sb1::List.map (fun (x,t)->x, subst_one sb1 t) sb)
+        (List.map (subst_one sb1) terms1)
+        (List.map (subst_one sb1) terms2)
+    | (Var x::_, term::_ | term::_, Var x::_)
+        when List.mem x (vars term) ->
+      raise Not_found
+    | Var x::terms1, term::terms2 | term::terms1, Var x::terms2 ->
+      let sb1 = x, term in
+      unify (sb1::List.map (fun (x,t)->x, subst_one sb1 t) sb)
+        (List.map (subst_one sb1) terms1)
+        (List.map (subst_one sb1) terms2)
+    | _ -> raise Not_found
+
+(* 3d *)
+(* Match the first argument as term against the second argument as
+   pattern. Allow nonlinear (object) variables. *)
+let rec match_meta sb m_sb terms1 terms2 =
+  match terms1, terms2 with
+    | [], [] -> sb, m_sb
+    | (Const a | Var a)::terms1, (Const b | Var b)::terms2 when a=b ->
+      match_meta sb m_sb terms1 terms2
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      match_meta sb m_sb (args1 @ terms1) (args2 @ terms2)
+    | term::terms1, MVar x::terms2 ->
+      (* we don't substitute because metavariables are linear *)
+      match_meta sb ((x, term)::m_sb) terms1 terms2
+    | MVar _::_, _ -> 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 sb m_sb terms1 terms2
+    | _ -> raise Not_found
+
+
+(* 3c1 *)
+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), gens = loop pf terms1 terms2 in
+      (good_vars, good_csts+1), cst::gens
+    | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
+      let (good_vars1, good_csts1), gen_args = loop f args1 args2 in
+      let (good_vars2, good_csts2), gens = loop pf terms1 terms2 in
+      (good_vars1+good_vars2, good_csts1+good_csts2),
+      (Func (f,gen_args))::gens
+    | (Var x as var)::terms1, Var y::terms2 when x=y ->
+      let (good_vars, good_csts), gens = loop pf terms1 terms2 in
+      (good_vars+1, good_csts), var::gens
+    | _::terms1, _::terms2 ->
+      let measure, gens = loop pf terms1 terms2 in
+      incr fresh_count;
+      measure, MVar ("MV"^string_of_int !fresh_count)::gens
+    | _::_, [] | [], _::_ -> raise
+      (Lexer.Parsing_error
+         ("GDL.generalize: arity mismatch at function "^pf)) in
+  let measure, gens = loop "impossible" [term1] [term2] in
+  measure, !fresh_count, List.hd gens
+
+(* 3c2 *)
+let abstract_consts fresh_count term =
+  let fresh_count = ref fresh_count in
+  let rec loop = function
+    | Const _ -> incr fresh_count; MVar ("MV"^string_of_int !fresh_count)
+    | Func (f,args) -> Func (f, List.map loop args)
+    | term -> term in
+  loop term
+
+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)
+
+let unify_rels (rel1, args1) (rel2, args2) =
+  if rel1 = rel2 then unify [] args1 args2
+  else raise Not_found
+
+let subst_rel sb (rel, args) = rel, List.map (subst sb) args
+let subst_rels sb body = List.map (subst_rel sb) body
+let compose_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
+
+let fact_str (rel, args) =
+  "("^rel^" "^String.concat " " (List.map term_str args) ^")"
+
+let tuples_str tups =
+  let tup_str tup =
+    "("^String.concat " " (List.map term_str tup) ^")" in
+  String.concat " " (List.map tup_str tups)
+
+let facts_str facts =
+  String.concat " " (List.map fact_str facts)
+
+let def_str (rel, branches) =
+  let neg_facts_str negs =
+    String.concat " "
+      (List.map (fun d -> "(not (and "^facts_str d^"))") negs) in
+  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)
+
+(* 1b *)
+
+(* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
+   TODO: optimize by using constant-time append data structure. *)
+let saturate base rules =
+
+  let instantiate_one tot_base cur_base irules =
+    Aux.concat_map (function
+      | head, [], neg_body ->
+        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 []
+        else [Aux.Left head]
+      | head, cond1::body, neg_body ->
+        Aux.map_try (fun fact ->
+          (* {{{ log entry *)
+          if !debug_level > 4 then (
+            Printf.printf "instantiate_one: trying to unify %s and %s\n%!"
+              (fact_str fact) (fact_str cond1)
+          );
+          (* }}} *)
+          let sb = unify_rels fact cond1 in
+          (* {{{ log entry *)
+          if !debug_level > 4 then (
+            Printf.printf "instantiate_one: succeeded with %s\n%!"
+              (sb_str sb)
+          );
+          (* }}} *)
+          let irule =
+            subst_rel sb head,
+            subst_rels sb body, subst_rels sb neg_body in
+          Aux.Right irule
+        ) cur_base) irules in
+
+  let rec inst_stratum old_base old_irules cur_base cur_irules =
+    (* {{{ log entry *)
+    if !debug_level > 3 then (
+      Printf.printf "inst_stratum: old_base = %s; cur_base = %s\n%!"
+        (facts_str old_base) (facts_str cur_base);
+      Printf.printf
+        "inst_stratum: #old_irules = %d, #cur_irules = %d\n%!"
+        (List.length old_irules) (List.length cur_irules)
+    );
+    (* }}} *)
+    let base = Aux.unique_sorted (cur_base @ old_base)
+    and irules = Aux.unique_sorted (cur_irules @ old_irules) in
+    let new_base1, new_irules1 =
+      Aux.partition_choice (instantiate_one base cur_base cur_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 3 then (
+      Printf.printf "inst_stratum: cur-cur = %s\n%!"
+        (facts_str new_base1)  
+    );
+    (* }}} *)
+    let new_base2, new_irules2 =
+      Aux.partition_choice (instantiate_one base cur_base old_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 3 then (
+      Printf.printf "inst_stratum: cur-old = %s\n%!"
+        (facts_str new_base2)  
+    );
+    (* }}} *)
+    let new_base3, new_irules3 =
+      Aux.partition_choice (instantiate_one base old_base cur_irules) in
+    (* {{{ log entry *)
+    if !debug_level > 3 then (
+      Printf.printf "inst_stratum: old-cur = %s\n%!"
+        (facts_str new_base3)  
+    );
+    (* }}} *)
+    let new_base = Aux.unique_sorted (new_base1 @ new_base2 @ new_base3)
+    and new_irules = Aux.unique_sorted
+      (new_irules1 @ new_irules2 @ new_irules3) in
+    let new_base =
+      List.filter (fun f->not (List.mem f base)) new_base in
+    let new_irules =
+      List.filter (fun f->not (List.mem f irules)) new_irules in    
+    if new_base = [] && new_irules = []
+    then base
+    else inst_stratum base irules new_base new_irules in
+  
+  let rec instantiate base = function
+    | [] -> base
+    | stratum::strata ->
+      instantiate (inst_stratum [] [] base stratum) strata in
+
+  instantiate base
+    (List.map rules_of_defs (stratify [] (defs_of_rules rules)))
+
+
 let playing_as = ref (Const "uninitialized")
 let game_description = ref []
-let player_name_terms = ref [| |]
+let player_terms = ref [| |]
 
 let state_of_file s =
   Printf.printf "GDL: Loading file %s...\n%!" s;
@@ -51,99 +738,603 @@
   Printf.printf "GDL: File %s loaded.\n%!" s;
   res
 
-let initialize_game_gomoku state player game_descr startcl =
-  state := state_of_file "./examples/Gomoku.toss";
-  playing_as := player;
-  game_description := game_descr;
-  player_name_terms := [|Const "X"; Const "O"|];
-  let effort, horizon, heur_adv_ratio =
-    2, 100, 4.0 in
-  effort, horizon, heur_adv_ratio
+(* 6 *)
 
-let initialize_game_breakthrough state player game_descr startcl =
-  state := state_of_file "./examples/Breakthrough.toss";
+(* TODO: do proper elegant renaming... *)
+let freshen_def_branches =
+  let fresh_count = ref 0 in
+  let map_branch (args, body, neg_body) =
+    incr fresh_count;
+    let rec map_vnames = function
+      | Var x -> Var (x^string_of_int !fresh_count)
+      | MVar x -> MVar (x^string_of_int !fresh_count)
+      | Const _ as t -> t
+      | Func (f, args) ->
+        Func (f, List.map map_vnames args) in
+    let map_rel (rel, args) =
+      rel, List.map map_vnames args in
+    List.map map_vnames args,
+    List.map map_rel body,
+    List.map (List.map map_rel) neg_body in
+  List.map map_branch
+
+(* assumption: [defs] bodies are already clean of defined relations *)
+let subst_def_branch (defs : exp_def list)
+    (head, body, neg_body : exp_def_branch) : exp_def_branch list =
+  (* 6a *)
+  let sols =
+    List.fold_left (fun sols (rel, args as atom) ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         Aux.map_some (fun (dparams, dbody, dneg_body) ->
+           try
+             let sb1 = unify [] dparams args in
+             Some (
+               subst_rels sb1 (dbody @ pos_sol),
+               List.map (subst_rels sb1) (dneg_body @ neg_sol),
+               compose_sb sb1 sb)
+           with Not_found -> None
+         ) def
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           subst_rel sb atom::pos_sol, neg_sol, sb) sols))
+      ([[],[],[]]) body in
+  (* 6b *)
+  let sols =
+    List.fold_left (fun sols -> function [rel, args as atom] ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       List.map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         let more_neg =
+           Aux.map_some (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);
+             try
+               let sb1 = unify [] dparams args in
+               Some (subst_rels sb1 dbody)
+             with Not_found -> None
+           ) def in
+         pos_sol, more_neg @ neg_sol, sb
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           pos_sol, [subst_rel sb atom]::neg_sol, sb) sols)
+      | _ -> failwith
+        "GDL.subst_def_branch: unimplemented, see (6b1) of spec")
+      sols neg_body in
+  Aux.map_some (fun (pos_sol, neg_sol, sb) ->
+    if List.mem [] neg_sol then None
+    else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols
+
+(* Stratify and expand all relations in the given set. *)
+let expand_def_rules ?(more_defs=[]) rules =
+  let rec loop base = function
+    | [] -> base
+    | stratum::strata ->
+      let step = List.map (fun (rel, branches) ->
+        rel, Aux.concat_map
+          (subst_def_branch (more_defs@base)) branches) stratum in
+      loop (base @ step) strata in
+  match stratify ~def:true [] (defs_of_rules rules) with
+    | [] -> []
+    | [no_defined_rels] ->
+      if more_defs = [] then no_defined_rels
+      else List.map (fun (rel, branches) ->
+        rel, Aux.concat_map (subst_def_branch more_defs) branches)
+        no_defined_rels
+    | def_base::def_strata -> loop def_base def_strata
+
+
+(* As [subst_def_branch], but specifically for "legal" definition and
+   result structured by "legal" definition branches. *)
+      (*
+let subst_legal_rule (legal_defs : exp_def_branch list)
+    (head, body, neg_body : exp_def_branch) : exp_def_branch list =
+  (* 6a *)
+  let sols =
+    List.fold_left (fun sols (rel, args as atom) ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         Aux.map_some (fun (dparams, dbody, dneg_body) ->
+           try
+             let sb1 = unify [] dparams args in
+             Some (
+               subst_rels sb1 (dbody @ pos_sol),
+               List.map (subst_rels sb1) (dneg_body @ neg_sol),
+               compose_sb sb1 sb)
+           with Not_found -> None
+         ) def
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           subst_rel sb atom::pos_sol, neg_sol, sb) sols))
+      ([[],[],[]]) body in
+  (* 6b *)
+  let sols =
+    List.fold_left (fun sols -> function [rel, args as atom] ->
+      (let try def =
+         freshen_def_branches (List.assoc rel defs) in
+       List.map (fun (pos_sol, neg_sol, sb) ->
+         let args = List.map (subst sb) args in
+         let more_neg =
+           Aux.map_some (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);
+             try
+               let sb1 = unify [] dparams args in
+               Some (subst_rels sb1 dbody)
+             with Not_found -> None
+           ) def in
+         pos_sol, more_neg @ neg_sol, sb
+       ) sols
+       with Not_found ->
+         List.map (fun (pos_sol, neg_sol, sb) ->
+           pos_sol, [subst_rel sb atom]::neg_sol, sb) sols)
+      | _ -> failwith
+        "GDL.subst_def_branch: unimplemented, see (6b1) of spec")
+      sols neg_body in
+  Aux.map_some (fun (pos_sol, neg_sol, sb) ->
+    if List.mem [] neg_sol then None
+    else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols
+      *)
+(* 1 *)
+
+(* Collect the aggregate playout, but also the actions available in
+   the state. *)
+let aggregate_ply players static current rules =
+  let base =
+    Aux.map_prepend static (fun term -> "true", [term]) current in
+  let base = saturate (base @ static) rules in
+  let does = Aux.map_some (fun (rel, args) ->
+    if rel = "legal" then Some ("does", args) else None) base in
+  if                                    (* no move *)
+    Aux.array_existsi (fun _ player ->
+      List.for_all (function _, (actor::_) -> player <> actor | _ -> true)
+        does) players
+  then raise Not_found
+  else
+    let step = saturate (does @ base) rules in
+    let step = Aux.map_some (function ("next", [arg]) -> Some arg
+      | _ -> None) step in
+    if !aggregate_fixpoint &&           (* fixpoint reached *)
+      List.for_all (function
+        | Func (_,[arg]) when
+            Aux.array_existsi (fun _ player -> arg=player) players -> true
+        | term -> List.mem term current
+      ) step
+    then raise Not_found
+    else
+      List.map snd does, step
+
+(* Besides the aggregate playout, also return the separation of rules
+   into static and dynamic. Note that the list of playout states is
+   one longer than that of playout actions. *)
+let aggregate_playout players horizon rules =
+  (* separate and precompute the static part *)
+  let rec separate static_rels state_rels =
+    let static, more_state =
+      List.partition (fun rel ->
+        List.for_all (fun ((rule,_), body, neg_body) ->
+          rule <> rel || List.for_all (fun srel ->
+            not (List.mem_assoc srel (neg_body @ body))) state_rels)
+          rules) static_rels in
+    if more_state = [] then static_rels, state_rels
+    else separate static (more_state @ state_rels) in
+  let static_rels, state_rels =
+    separate (List.map (fun ((r,_),_,_)->r) rules)
+      ["init"; "does"; "true"; "next"; "terminal"; "goal"] in
+  let static_rules, dynamic_rules = List.partition
+    (fun ((rel,_),_,_) -> List.mem rel static_rels) rules in
+  let static_base = saturate [] static_rules in
+  let state_rules =
+    (* 1a *)
+    if !aggregate_drop_negative then
+      List.map (function
+        | ("legal", _ as head), body, _ -> head, body, []
+        | ("does", _ as head), body, _ -> head, body, []
+        | rule -> rule) dynamic_rules
+    else dynamic_rules in    
+  let rec loop actions_accu state_accu step state =
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      Printf.printf "aggregate_playout: step %d...\n%!" step
+    );
+    (* }}} *)
+    (let try actions, next =
+       aggregate_ply players static_base state state_rules in
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      Printf.printf "aggregate_playout: state %s\n%!"
+        (String.concat " " (List.map term_str next))
+    );
+    (* }}} *)
+    if step < horizon then
+      loop (actions::actions_accu) (state::state_accu) (step+1) next
+    else 
+      List.rev (actions::actions_accu),
+      List.rev (next::state::state_accu)
+     with Not_found ->
+       List.rev actions_accu, List.rev (state::state_accu)) in
+  (* FIXME: this is identity, right? remove *)
+  let init_base = saturate static_base state_rules in
+  let init_state =
+    Aux.map_some (function ("init", [arg]) -> Some arg
+      | _ -> None) init_base in
+  (* {{{ log entry *)
+  if !debug_level > 0 then (
+    Printf.printf "aggregate_playout: init %s\n%!"
+      (String.concat " " (List.map term_str init_state))
+  );
+  (* }}} *)
+  static_rules, dynamic_rules, static_base, loop [] [] 0 init_state
+
+
+let find_cycle cands =
+  let rec loop cycle trav pref rem path =
+    if cycle = [] then
+      let ini = [List.hd path] in
+      loop ini ini ini [] (List.tl path)
+    else match path, rem with
+      | _, [] -> loop cycle trav [] cycle path
+      | [], _ -> cycle                  (* consumed the whole path *)
+      | x::tail, y::rem when x=y || x = None->
+        (* either elements agree or indifferent path element *)
+        loop cycle (x::trav) (y::pref) rem tail
+      | x::tail, None::rem ->
+        (* instantiating undecided cycle element *)
+        loop (List.rev pref @ [x] @ rem) (x::trav) (x::pref) rem tail
+      | x::tail, _::_ ->
+        (* mismatch: grow the cycle to current point *)
+        let trav = x::trav in
+        let cycle = List.rev trav in
+        loop cycle trav [] cycle tail in
+  loop [] [] [] [] cands
+
+
+let translate_game game_descr =
+  let player_terms =
+    Array.of_list
+      (Aux.map_some (function Role p -> Some p | _ -> None) game_descr) in
+  let rules = Aux.concat_map rules_of_entry game_descr in
+  let static_rules, dynamic_rules, static_base, (agg_actions, agg_states) =
+    aggregate_playout player_terms 30 rules in
+  (* (8) -- drop zero goal branches, "first round" *)
+  let dynamic_rules = List.filter
+    (function ("goal", [_; Const "0"]), _, _ -> false | _ -> true)
+    dynamic_rules in
+  let element_terms : term list =
+    List.fold_left (fun acc st -> Aux.unique_sorted (st @ acc)) []
+      agg_states in
+  let noop_cands = List.map (fun actions ->
+    let actions = Aux.map_reduce
+      (function [player; action] -> player, action
+        | _ -> assert false) (fun y x->x::y) [] actions in
+    (* 2a *)
+    List.map (function
+      | player, [Const _ as noop] -> player, Some noop
+      | player, _ -> player, None) actions) agg_actions in
+  let control_cands = List.map (fun noop_cands ->
+    List.fold_left (fun accu -> function
+      | player, None ->
+        if accu = None then Some player
+        else raise
+          (Lexer.Parsing_error
+             ("GDL.initialize_game: branching arena graphs"^
+                 " or simultaneous moves not supported yet"))
+      | _, Some _ -> accu) None noop_cands) noop_cands in
+  (* 2b *)
+  let cycle = find_cycle control_cands in
+  (* {{{ log entry *)
+  if !debug_level > 0 then (
+    Printf.printf "translate_game: location players %s\n%!"
+      (String.concat " "
+         (List.map (function Some t->term_str t | None->"None") cycle))
+  );
+  (* }}} *)
+  (* 6 *)
+  let static_rules, exp_static_rules =
+    List.partition (fun ((rel,args), _, _) ->
+      List.length args <= !expand_arity_above ||
+        List.exists (function ((r,_),[],[]) when rel=r-> true
+          | _ -> 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 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))
+  );
+  (* }}} *)
+  (* 3 *)
+  let legal_rules = List.assoc "legal" exp_defs in
+  let next_rules = List.assoc "next" exp_defs in
+  (* 3b *)
+  let exp_next =
+    Aux.concat_map (subst_def_branch ["does", 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))
+  );
+  (* }}} *)
+  (* 3c *)
+  let masks = List.map (function
+    | [next_arg], body, neg_body ->
+      let collect = Aux.map_some
+        (function "true", [arg] -> Some arg
+          | "true", _ -> raise
+            (Lexer.Parsing_error
+               ("GDL.initialize_game: invalid arity of \"true\" atom"))
+          | _ -> None) in
+      let pos_cands = collect body in
+      let neg_cands = Aux.concat_map collect neg_body in
+      let pos_gens = List.map (generalize next_arg) pos_cands in
+      let neg_gens = List.map (generalize next_arg) neg_cands in
+      (* using the fact that Pervasives.compare is lexicographic *)
+      let pos_gen = List.fold_left max ((-1,0),0,Const "") pos_gens in
+      let neg_gen = List.fold_left max ((-1,0),0,Const "") neg_gens in
+      let (_, fresh_count, mask as gen) = max pos_gen neg_gen in
+      if gen == pos_gen then mask
+      else abstract_consts fresh_count mask
+    | _ -> raise
+      (Lexer.Parsing_error
+         ("GDL.initialize_game: invalid arity of \"next\" atom")))
+    exp_next in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: Generalized element terms (mask candidates):\n%s\n%!"
+      (String.concat " " (List.map term_str masks))
+  );
+  (* }}} *)
+  let cmp_masks t1 t2 =
+    Printf.printf "cmp_masks: %s <= %s .. " (term_str t1) (term_str t2);
+    try ignore (match_meta [] [] [t1] [t2]); Printf.printf "true\n%!"; true
+    with Not_found -> Printf.printf "false\n%!"; false in
+  let masks = Aux.maximal cmp_masks masks in
+  (* {{{ log entry *)
+  if !debug_level > 1 then (
+    Printf.printf "translate_game: Masks:\n%s\n%!"
+      (String.concat " " (List.map term_str masks))
+  );
+  (* }}} *)
+  (* 3e *)
+  let elements = List.fold_left (fun elements term ->
+    let mask, sb, m_sb =
+      match
+        Aux.map_try (fun mask ->
+          mask, match_meta [] [] [term] [mask]) masks
+      with [mask, (sb, m_sb)] -> mask, sb, m_sb
+        | _ -> assert false in          (* masks are minimal *)
+    let sbs, elements =
+      try Aux.pop_assoc mask elements
+      with Not_found -> [], elements in
+    (mask, if List.mem sb sbs then sbs else sb::sbs)::elements
+  ) [] element_terms in
+  let struc = Structure.empty_structure () in
+  let struc, elements =
+    List.fold_left (fun (struc, elements) (mask, sbs) ->
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf "mask-elements:";
+      );
+      (* }}} *)
+      let struc, m_elements =
+        List.fold_left (fun (struc, m_elements) sb ->
+          let e_term = subst sb mask in
+          (* {{{ log entry *)
+          if !debug_level > 2 then (
+            Printf.printf ", %s%!" (term_to_name e_term)
+          );
+          (* }}} *)
+          let struc, elem =
+            Structure.add_new_elem struc ~name:(term_to_name e_term) () in
+          struc, (sb, elem)::m_elements
+        ) (struc, []) sbs in
+      (* {{{ log entry *)
+      if !debug_level > 2 then (
+        Printf.printf "\n%!";
+      );      
+      (* }}} *)
+      struc, (mask, m_elements)::elements
+    ) (struc, []) elements in
+  (* 4 *)
+  (* currently, position paths are approximated by variables
+     (non-variable positions are ignored) *)
+  let mask_paths = Aux.concat_map (function _, [] -> assert false
+    | mask, (sb,_)::_ -> List.map (fun (v,_)->mask, v) sb) elements in
+  (* 4a *)
+  (* TODO: move generation of static rels graphs to the end and
+     filter to only generate used relations *)
+  let static_rels =
+    Aux.unique_sorted
+      (List.map (fun ((rname,args),_,_) ->
+        rname, List.map (fun _ -> ()) args) static_rules) in
+  let static_rels =
+    List.map (fun (rel,args) ->
+      rel,
+      Aux.all_tuples_for args mask_paths) static_rels in
+  let static_base =
+    Aux.map_reduce (fun x->x) (fun x y->y::x) [] static_base in
+  (* TODO: optimize by indexing elements by path position
+     terms (currently, substitution values) *)
+  let struc = List.fold_left (fun struc (brel, path_tups) ->
+    let brel_tups = List.assoc brel static_base in
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      Printf.printf "Translating static relation %s with %d tuples:\n%s\n%!"
+        brel (List.length brel_tups) (tuples_str brel_tups);
+    );
+    (* }}} *)
+    List.fold_left (fun struc ptup ->
+      let rname = brel ^ "__" ^ String.concat "__"
+        (List.map (fun (mask,v)->
+          term_to_name mask ^ "_" ^ v) ptup) in
+      let struc =
+        Structure.add_rel_name rname (List.length ptup) struc in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf "static-rel: %s, of... %!" rname;
+      );
+      (* }}} *)
+      let elem_sets =
+        List.map (fun (mask,v)->
+          List.map (fun (sb,elem)->
+            try List.assoc v sb, elem
+            with Not_found -> assert false)
+            (List.assoc mask elements)) ptup in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf "%s ... %!" (String.concat "x" (
+          List.map (fun x-> string_of_int (List.length x)) elem_sets));
+      );
+      (* }}} *)
+      let elem_tups =
+        Aux.concat_map (fun ttup ->
+          let elem_sets = List.map2 (fun term elems ->
+            Aux.map_some (fun (tcand, e) ->
+              if tcand=term then Some e else None) elems
+          ) ttup elem_sets in
+          List.map Array.of_list (Aux.product elem_sets)
+        ) brel_tups in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf "%d tuples, adding to struc...%!" (List.length elem_tups);
+      );
+      (* }}} *)
+      let res = Structure.unsafe_add_rels struc rname elem_tups in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf " done\n%!";
+      );
+      (* }}} *)
+      res
+    ) struc path_tups) struc static_rels in
+  (* 4b *)
+  let struc = List.fold_left (fun struc (mask,v) ->
+    let rname = "EQ___" ^ term_to_name mask ^ "_" ^ v in
+    let struc =
+      Structure.add_rel_name rname 2 struc in
+    let elems = List.assoc mask elements in
+    (* {{{ log entry *)
+    if !debug_level > 0 then (
+      Printf.printf "Adding static EQ relation %s over %d elements.\n%!"
+        rname (List.length elems);
+    );
+    (* }}} *)
+    let elem_tups =
+      List.fold_left (fun tups (sb1, e1) ->
+        List.fold_left (fun tups (sb2, e2) ->
+          try
+            if List.assoc v sb1 = List.assoc v sb2
+            then [|e1; e2|]::[|e2; e1|]::tups
+            else tups
+          with Not_found -> assert false
+        ) tups elems      
+      ) [] elems in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf "%d tuples, adding to struc...%!" (List.length elem_tups);
+      );
+      (* }}} *)
+      let res = Structure.unsafe_add_rels struc rname elem_tups in
+      (* {{{ log entry *)
+      if !debug_level > 1 then (
+        Printf.printf " done\n%!";
+      );
+      (* }}} *)
+      res    
+  ) struc mask_paths in
+  (* 4c: TODO -- see laziness TODO 4 *)
+
+  (* 5: TODO *)
+  
+  (* 7a *)
+  let legal_rules =
+    Aux.concat_map (function [Const _; _], _, _ as lrule -> [lrule]
+      | [Var v; lterm], body, neg_body ->
+        Array.to_list
+          (Array.map (fun player -> [player; lterm], body, neg_body)
+             player_terms)
+      | [Func _; lterm], _, _ ->
+        (* TODO: easy to fix *)
+        failwith "GDL.translate_game: bigger player terms not handled yet"
+      | _ -> assert false) legal_rules in
+  (* indexed by players, then "legal" branches, then by MGUs for
+     unifier equivalence classes *)
+  (*
+  let player_next =
+    Aux.map_reduce (fun ()) in
+  *)
+  struc
+
+(*
+  let paths = collect_paths element_terms in
+  let static_facts =
+    Array.of_list
+      (Aux.map_some (function Atomic p -> Some p | _ -> None) game_descr) in
+  let element_names = List.map term_to_name element_terms in
+
+  let struc = List.fold_left (fun acc name ->
+    fst (Structure.add_new_elem acc ~name ()))
+    Structure.empty_structure element_names in
+      *)  
+
+let initialize_game state player game_descr startcl =
   playing_as := player;
-  game_description := game_descr;
-  player_name_terms := [|Const "WHITE"; Const "BLACK"|];
-  let effort, horizon, heur_adv_ratio =
-    3, 100, 2.0 in
-  effort, horizon, heur_adv_ratio
+  let struc = translate_game game_descr in
+  ignore struc;
+  (* state := Arena.process_definition ~extend_state:(!state) defs; *)
+  2, 100, 2.0
 
-let initialize_game =
-  initialize_game_breakthrough
-  
-let translate_last_action_gomoku actions =
-  let number_of_letter c = 
-    string_of_int ((Char.code (Char.lowercase c)) - 96) in
+
+let translate_last_action actions =
   match actions with
     | [] ->
       (* start of game -- Server will handle this answer as NOOP *)
       "", []
     | [Func ("MARK", [Const col; Const row]); Const "NOOP"] ->
-      "Cross", ["a1", ((String.lowercase col) ^ (number_of_letter row.[0]))]
+      "Cross", ["...
 
[truncated message content]