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

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

Revision: 1434
          http://toss.svn.sourceforge.net/toss/?rev=1434&view=rev
Author:   lukaszkaiser
Date:     2011-05-09 01:19:32 +0000 (Mon, 09 May 2011)

Log Message:
-----------
Playing with Chess heuristic, Chess allowed in WebClient. Moving ServerTest to ReqHandlerTest as it should be, then moving TossTest and TossFullTest to Tests ml in Server, which is now executed from TossServer (one target spares ocamlbuild). Splitting GDL ml to GDL with basic functions and Translate ml with most code.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Makefile
    trunk/Toss/Formula/Makefile
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/GGP/Makefile
    trunk/Toss/Makefile
    trunk/Toss/Play/Makefile
    trunk/Toss/Server/Makefile
    trunk/Toss/Server/ReqHandler.ml
    trunk/Toss/Server/Server.ml
    trunk/Toss/Solver/Makefile
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/WebClient/Handler.py
    trunk/Toss/WebClient/Main.js
    trunk/Toss/examples/Chess.toss

Added Paths:
-----------
    trunk/Toss/GGP/Translate.ml
    trunk/Toss/GGP/Translate.mli
    trunk/Toss/GGP/TranslateTest.ml
    trunk/Toss/Server/ReqHandler.mli
    trunk/Toss/Server/ReqHandlerTest.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Server/Tests.mli

Removed Paths:
-------------
    trunk/Toss/Server/ServerTest.ml
    trunk/Toss/TossFullTest.ml
    trunk/Toss/TossTest.ml

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-05-07 22:30:43 UTC (rev 1433)
+++ trunk/Toss/Arena/Arena.ml	2011-05-09 01:19:32 UTC (rev 1434)
@@ -264,9 +264,10 @@
   (* }}} *)
   let graph = Array.of_list (List.rev locations) in 
   (* TODO; FIXME; JUST THIS List.rev ABOVE WILL NOT ALWAYS BE GOOD, OR?!! *)
+  let pats = List.rev_map (FormulaOps.subst_rels_expr def_rels_pure) patterns in
   {
     rules = rules;
-    patterns = List.rev patterns;
+    patterns = pats;
     graph = graph;
     num_players = num_players;
     player_names = player_names;

Modified: trunk/Toss/Arena/Makefile
===================================================================
--- trunk/Toss/Arena/Makefile	2011-05-07 22:30:43 UTC (rev 1433)
+++ trunk/Toss/Arena/Makefile	2011-05-09 01:19:32 UTC (rev 1434)
@@ -1,7 +1,7 @@
 all: tests
 
 %Test:
-	make -C .. Arena/$@
+	make -C .. Arena/$@Verbose
 
 TermTest:
 DiscreteRuleTest:

Modified: trunk/Toss/Formula/Makefile
===================================================================
--- trunk/Toss/Formula/Makefile	2011-05-07 22:30:43 UTC (rev 1433)
+++ trunk/Toss/Formula/Makefile	2011-05-09 01:19:32 UTC (rev 1434)
@@ -1,7 +1,7 @@
 all: tests
 
 %Test:
-	make -C .. Formula/$@
+	make -C .. Formula/$@Verbose
 
 AuxTest:
 FormulaTest:

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-05-07 22:30:43 UTC (rev 1433)
+++ trunk/Toss/GGP/GDL.ml	2011-05-09 01:19:32 UTC (rev 1434)
@@ -1,592 +1,8 @@
-
 (** {2 Game Description Language.}
+    Type definitions, helper functions, game specification. *)
 
-    Type definitions, helper functions, game specification
-    translation.
+open Aux.BasicOperators
 
-    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. To avoid ungrounded player variables, add
-    "role" filter to "legal" rules.
-
-    (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.
-
-    In case of problems, it should be relatively easy to expand the
-    translation to use a single location per player, and for rules to
-    determine which player is active after the rule takes effect
-    (i.e. the target location.) Once Toss has a good system for
-    simultaneous moves, we can simplify by translating into a single
-    location game, obsoleting this "chapter".
-
-    (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 also 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.
-
-    (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.
-
-    (3c3) When [nonerasing_frame_wave] is set to [true], remove
-    branches that have a variable/variable mismatch at proposed fluent
-    position.(TODO)
-
-    (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.
-
-    TODO: this is wrong! Generates too many masks compared to the
-    paper method (using fluent paths). Should generalize masks that
-    do not differ at constant/functor-constant/functor positions.
-
-    (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.
-
-    (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.) Add a predicate for being derived from a
-    mask (which is applied in (7i-4c) only if not adding mask-path
-    predicates, fact or equivalence relations from which it can be
-    inferred). For each mask-path pointing to a constant in some of
-    the elements and that constant, introduce a new predicate with
-    semantics: "matches the mask and has the constant at the path
-    position".
-
-    Optionally, also include a positive mask predicate for negative
-    state terms (rather than a negative one).
-
-    (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.)
-
-    (See also (7k).) For each element 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.)
-
-    First, we expand all uses of the built-in "role" predicate.
-
-    (6a) The definition:
-
-    [(r, params1) <= body1 ... (r, params_n) <= body_n]
-
-    provides a DNF defining formula (using negation-as-failure):
-
-    [(r, args) <=> exist vars1 (params1 = args /\ body1) \/ ...
-    \/ exist vars_n (params_n = args /\ 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 [params_i = args] in the whole
-    [i]th cloned branch, eliminating the [params] (rather than the
-    [args]) when possible. 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)]
-
-    (6b1) If the relation has negative subformulas in any of [body_i],
-    unless all the negative subformulas are just "distinct" checks
-    that become ground, we first negate the definition and then expand
-    the negation as in the positive case.
-
-    (6b1a) Eliminate [args = params_i] by substituting-out variables
-    from [params_i] whenever possible.
-
-    Note: the [args] need to be instatiated for the particular
-    solution that is extended (the solution substitution applied).
-
-    (6b1b) We group the positive atoms of body_i together and split
-    the quantifier if each negative subformula and the positive part
-    have disjoint [vars_i] variables; if not, the translation fails;
-    currently, if a negative subformula has free variables in vars_i,
-    the translation also fails.
-
-    (6b1c) So we have two levels of specification-affecting TODOs;
-    working around variables shared between negated subformulas or the
-    positive part -- forbidding pushing quantification inside -- will
-    require major rethinking of implementation; if the quantification
-    can be pushed inside but doesn't disappear around a negated
-    subformula, we will need to extend the universal quantifier
-    handling from only negated to both negated and positive
-    subformulas, which shouldn't be problematic.
-
-    (6b1d) Now push the negation inside the conjunction so that all
-    double negations cancel out (the positive conjuncts are under a
-    single, now negated, quantifier -- see (6b2) about negated
-    conjunctions of atoms). Next we pull the disjunctions out
-    (reducing to DNF-like form), and continue as in the positive case
-    (6a).
-
-    (6b2) We allow conjunctions of atoms to be negated (not only
-    literals) in a branch. We expand [not (r, args)] (in general, [not
-    (and (...(r args)...))]) into the conjunction of negations, with
-    no branch duplication (in general, duplicating the negated
-    subformula inside a branch). We only apply the unifier of [args =
-    params_i] to [body_i] (in general, the whole negated subformula),
-    eliminating the [params] (rather than the [args]) when
-    possible. Still, we freshen each [vars_i] to avoid capture. We
-    remember the (uneliminated) [vars_i] in the set of variables
-    quantified existentially under the negation (since the free
-    variables occurring only under the negation are quantified
-    universally there -- it is a positive position). 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.
-
-    (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 on the player in the location and noop actions
-    of other players in it, compared to the "legal" definition
-    branch (currently, we do not allow simultaneous moves). 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. A rewrite rule is
-    associated with a single "lead legal" branch of the location's
-    player.
-
-    (7a1) Filter "lead legal" rules by satisfiability in the current
-    location plys of the aggregate playout.
-
-    (7b) We collect all the branches of the "next" relation definition
-    for which the selected branches of "lead legal" and "noop legal"
-    (the "joint legal" actions) unify with all (usually one, but we
-    allow zero or more) occurrences of "does" with a single unifier
-    per "next" branch. (A "noop legal" actually only matches and
-    substitutes the local variables of "next" branches.) Split the
-    unifiers into equivalence classes (w.r.t. substitution), each
-    class will be a different rewrite rule (or set of rules). (Note
-    that equivalent unifiers turn out to be those that when truncated
-    to variables of the "legal" branch are renamings of each other.)
-
-    (7b1) Since the "noop legals" are constants (by current
-    assumption), we do not need to construct equivalence classes for
-    them. Their branches will join every rule generated for the "joint
-    legal" choice.
-
-    (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 (i.e. after applying the
-    original unifier, apply a renaming that makes the unifier equal to
-    all other unifiers in the equiv. class). We replace all
-    occurrences of "does" with the body of the selected "legal"
-    branch.
-
-    (7d) Add all branches of equiv classes smaller than a given equiv
-    class to its branch set.
-
-    Implementation TODO (reason for unsoundness): currently, we
-    discard non-maximal equivalence classes, because negation (7e) is
-    not implemented, and with negation it would still be preferable to
-    have exhaustiveness check so as to not generate spurious
-    (unapplicable) rules. TODO: rethink, compare with (7f2).
-
-    (7e) 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.
-
-    (7f) We remember all variables in the "legal"/"does" instantiation
-    as "fixed variables". We seggregate "next" atoms into these that
-    contain some fixed variables or no variables at all, and other
-    containing only unfixed variables.
-
-    (7f1) Branches with only (TODO: some? (x)) unfixed variables in "next"
-    atoms that are "identities" are the "frame" branches. "Identity"
-    here means the "next" atom is equal to one of the positive "true"
-    atoms.
-
-    (x) It is probably better to not expand "identity" branches that
-    have both fixed and unfixed variables in the head, as they will be
-    correctly handled (translated to erasure branches) in the
-    following code.
-
-    (7f2) Transform the "frame" branches into "erasure" branches:
-    distribute them into equivalence classes of head terms
-    (w.r.t. substitution but treating fixed variables as constants),
-    add smaller elements and negation of larger elements (in the same
-    manner as in (7b) and (7d) for the "legal" term), disjoin bodies
-    in each class (a "multi-body"), then:
-
-    (7f3) negate the multi-body, push negation inside (using de Morgan
-    laws etc.), 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. The local variables of newly created negated
-    subformulas become existentially-quantified-under-negation
-    (i.e. universally quantified) (while the local variables of old
-    negated subformulas are "let free").
-
-    FIXME: it is probably wrongly assumed in the implementation that
-    negated "distinct" unifies all terms, instead of disjunction of
-    pairwise unification, check that.
-
-    (7f4) Drop the erasure branches that contradict the "legal"
-    condition of their rule. (Add the "legal" condition for early pruning.)
-
-    (7f5) Redistribute the erasure branches in case they were
-    substituted with the "not distinct" unifier to proper equivalence
-    classes (remove equivalence classes that become empty).
-
-    (7f6) Filter-out branches that are not satisfiable by their static
-    part (in the initial structure).
-
-    (7g) NOOP (Was eliminating unfixed variables.)
-
-    (7h) 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".) From now on until (7l1) we keep
-    both the (partially) Toss-translated versions and the (complete)
-    GDL-originals of branches (so to use GDL atoms for "subsumption
-    checking" in (7l)).
-
-    (7i-7k) Variables corresponding to negated "true" atoms
-    that contain locally existentially quantified variables are
-    quantified universally (with a scope containing all their
-    occurrences).
-
-    Implementation: we only introduce universal quantification after
-    filtering (7m), is it OK?
-
-    (7i-4a) 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. Only
-    build the relation over positive elements, deferring negated ones
-    to (7k-4a) so that they are included under common
-    disjunction. Relations over elements coming from different
-    negations are not introduced, which agrees with negation-as-failure.
-
-    (7i-4c) Include the (4c) relations for "next" and "true" positive
-    atoms.
-
-    (7i-4b) (4b) is essentially a special case of (4a). Add an
-    appropriate equality relation of (4b) for each case of subterm
-    shared by terms corresponding to different positive elements.
-
-    Implementation: instead of all subterms we currently only consider
-    subterms that instantiate (ordinary) variables in the mask
-    corresponding to the "next"/"true" atom.
-
-    (7i0) For "distinct", negate the anchors of the constants at mask
-    paths of the variables, and equivalences of the variables (if
-    there are multiple variables).
-
-    TODO: currently only checks whether "distinct" arguments are
-    syntactically equal.
-
-    (7i1) Remove branches that are unsatisfiable by their static
-    relations (4a), (4b) and (positive) (4c) alone.
-
-    (7j) 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.) Such fixed variables should be expanded by duplicating
-    the whole set of branches together with the "lead legal" term.
-
-    Implementation: TODO; currently, we check for such fixed
-    variables and fail if they're present.
-
-    (7k) Replace the "next" and "true" atoms by the conjunction of
-    (4b), (4c) and (5) predicates over their corresponding variable. (For
-    negative "true" literals this will be equivalent to a disjunction
-    of negations of the predicates.) Note that positive static
-    relations are already added in (7i-4b,4c). Handle negative subformula
-    translations of (4a, 4b, 4c, 5) together.
-
-    (7k-4a-1) Add to the disjunction a negation of all what (7i-4a)
-    would generate (i.e. for positive facts), but over tuples with at
-    least one of the negated elements of current negation (no elements
-    from other negations).
-
-    (7k-4a-2) For a negative fact generate result equivalent to a
-    *conjunction* of negations of generated atoms if all elements are
-    positive,
-
-    (7k-4a-3) but add a *disjunction* of negations (i.e. a negated
-    conjunction) of tuples with at least one negated element.
-
-    (7k-4c) Include the (4c) relations for "next" and "true" negative
-    atoms.
-
-    (7k-4b) It is essentially a special case of (7k-4a-1). Introduce
-    equivalences as in (7i-4b), but with tuples containing at least
-    one element from the current negation (no elements from other
-    negations). Generate the same set of equivalence tuples as a
-    positive occurrence would so that they can be pruned when
-    possible.
-
-    TODO: handle "distinct" that contains variable(s)!
-
-    (7l) 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). The lattice is built by
-    summing rule bodies.
-
-    (7l0) To avoid contradictions and have a complete partition, we
-    construct the set of all bit vectors indexed by all atoms
-    occurring in the bodies (optionally, all atoms in bodies of
-    branches containing "does" atoms). We collapse atoms that have the
-    same pattern of occurrence in the branches as single index.
-
-    (7l1) With every index-bit value we associate the set of branches
-    that do not allow such literal. For every vector we calculate the
-    complement of the sum of branch sets associated with every
-    bit. The unique resulting sets are exactly the Toss rules
-    precursors. Heuristic (FIXME: needed?): We only use atoms that are
-    deterministically present or absent in at least some branch for
-    indexing.
-
-    (7l2) Filter rule candidates so that each has a "does"-specific
-    branch.
-
-    TODO: perhaps should be optional -- perhaps there are "default
-    all noop rules" in some games.
-
-    (7l3) Optionally, remove synthetic branches that do not have (a)
-    gdl variables (i.e. Toss equivalence relations) or (b) state terms
-    (i.e. Toss variables) in common with the non-synthetic branches of
-    the rule candidate.
-
-    Only translate the formulas after (7l3).
-
-    (7l3b) In this optional case, only keep synthetic branches that
-    either have non-state-term atoms with gdl variables common with
-    base branches, or actually have state terms in common with base
-    branches. (E.g. do not keep a branch with "(R ?x ?y) (true (ST ?v ?x))
-    (true (ST ?v ?y))" when only "v" is in common with base branches.)
-
-    (7l4) Filter out rule candidates that contradict all states
-    from the current location plys of aggregate playout (by their
-    "true" atoms -- "not true" are not valid in the aggregate playout).
-
-    (7l5) Here a set of branches has conjunctive interpretation, since
-    they are the "next" clauses that simultaneously match. If a branch
-    fails, the whole case fails.
-
-    (7m) Filter the final rule candidates by satisfiability of the
-    static part (same as (7i1) conjoined).
-
-    (7n) Include translated negation of the terminal condition. (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.)
-
-    (7n1) Prior to translation, expand all variables under
-    meta-variables in "terminal" branches, as in (7j).
-
-    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). All the relations that appear in either LHS or RHS
-    are considered embedded.
-
-    (7o) After the rules are translated, perform an aggregated playout
-    of the Toss variant of the game. Remove the rules that were never
-    applied.
-
-    (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.
-
-    (8a) Filter-out goal branches that are contradictory with the
-    terminal condition (using resolution on the GDL
-    side). Implementation TODO.
-
-    (8b) For each goal value we collect bodies to form a disjunction.
-
-    (8c) The payoff formula is the sum of "goal" value times the
-    characterisic function of the corresponding "goal" bodies. To
-    simplify the result, we find the longest formula, and center the
-    payoff around it: for the goal value V_i if i-th formula phi_i and
-    phi_K being the longest formula, we translate the payoff into "K +
-    (V_1 - V_K) :(phi_1) + ... (V_n - V_K) :(phi_n)" thus removing
-    phi_K from translation.
-
-    (8d) Finally, we simplify the result. Unused predicates are not
-    removed, because some of them will be needed for action translation.
-
-    (9) To translate an incoming action, we:
-
-    (9a) find the "lead legal" term to which the "does move" ground
-    term of the current player matches;
-
-    (9b) earlier, remember which Toss variables of a rule contain which
-    fixed variables at which positions in their masks;
-
-    (9c) find anchor predicates corresponding to instantiations of the
-    "lead legal" variables, anchoring positions found by (9b) "fixed
-    var" - "mask + mask var" correspondence;
-
-    (9d) build a conjunction of anchor predicates over variables that
-    contain the fixed variable which is "instantiated" by the anchor
-    of the corresponding position, as established by (9c);
-
-    (9e) conjoin the (9d) with the "matching" formula of a rule, and
-    evaluate the result for all rules (of the located "lead legal"
-    class); only a single rule should have a match, and only a single
-    assignment should be returned; this rule with this assignment is
-    the translated move.
-
-    (10) To translate an outgoing action, we:
-
-    (10a) associate the rule with its corresponding data: the "lead
-    legal" term, the fixed variables corresponding to rule elements,
-    ...
-
-    (10b) earlier, return/store the mapping from an element to the
-    mask and subsitution that define the element;
-
-    (10c) earlier, for each rule store a mapping from fixed variables
-    to rule variables and the mask variables that in the rule variable
-    are instantiated by the fixed variables;
-
-    (10d) to determine how to instantiate the fixed variables in the
-    "lead legal" term, find the (10b) substitutions of assigned
-    elements and (10c) mask variables for fixed variables; compose the
-    maps to get fixed variable to GDL ground term mapping, each
-    "route" should give the same term.
-
-    Implementation TODO: once the LHS-RHS structures are removed from
-    the backbone and formula registration is removed, some
-    simplifications can be done in (9) and (10).
-
-*)
-
 let debug_level = ref 0
 let aggregate_drop_negative = ref false
 let aggregate_fixpoint = ref true
@@ -602,44 +18,6 @@
     [nonerasing_frame_wave] is set to [true].) *)
 let nonerasing_frame_wave = ref true
 
-(** Include mask predicates (first part of (4c)) of negative state
-    term atoms as either positive or negated atoms. *)
-type mask_anchors_of_neg = Positive_anch | Negative_anch | No_anch
-let mask_anchors_of_neg = ref (* Positive_anch *) Negative_anch
-
-(** Approximate rule preconditions by dropping parts of "partition
-    guards" of (7l) -- parts of conditions introduced merely to
-    distinguish rules that should not be available at the same time. *)
-type approximate_rule_preconds =
-  | Exact                               (** keep all conditions *)
-  | Connected                           (** keep all connected to
-                                            variables appearing in the
-                                            rest, i.e. containing
-                                            common gdl variables *)
-  | TightConnected                      (** keep connected but
-                                            ignoring equivalence
-                                            links, i.e. containing
-                                            common gdl state terms *)
-  | DropAll
-let approximate_rule_preconds = ref (* Connected *) Exact
-
-(** Filter rule candidates by the stable part of precondition either
-    before or after game simplification. *)
-type prune_rulecands = Before_simpl | After_simpl | Never
-let prune_rulecands_at = ref (* Before_simpl *) Never
-
-(** Perhaps generate all tuples for equivalences, to faciliate further
-    transformations of formulas in the game definition (outside of
-    translation). *)
-type pair_matrix = Pairs_all | Pairs_triang | Pairs_star
-let equivalences_all_tuples = ref Pairs_triang
-let equivalences_ordered = ref true
-
-(** Generate test case for the given game name. *)
-let generate_test_case = ref None
-
-open Aux.BasicOperators
-
 type term =
   | Const of string
   | Var of string
@@ -676,47 +54,7 @@
   | Stop of string * term list
   (* game ends here: match id, actions on previous step *)
 
-type tossrule_data = {
-  lead_legal : term;
-  (* the "legal"/"does" term of the player that performs the move, we
-     call its parameters "fixed variables" as they are provided externally *)
-  precond : Formula.formula;
-  (* the LHS match condition (the LHS structure and the precondition) *)
-  rhs_add : (string * string array) list;
-  (* the elements of LHS/RHS structures, corresponding to the "next"
-     terms *)
-  struc_elems : string list;
-  fixvar_elemvars :
-    (string * (term * (string * string list) list) list) list;
-  (* "state" terms indexed by variables that they contain, together
-     with the mask-path of the variable *)
-  elemvars : term Aux.StrMap.t;
-(* "state" terms indexed by Toss variable names they generate *)
-}
 
-type gdl_translation = {
-  anchor_terms :
-  (term * (string * (term * string) list) list) list;
-  (* mask path (i.e. mask+var) and a ground term to anchor predicate *)
-  tossrule_data : tossrule_data Aux.StrMap.t;
-  (* rule name to rule translation data *)
-  t_elements : term Aux.IntMap.t;
-  (* element terms (with metavariables only) *)
-  playing_as : int;
-  (* "active" player *)
-  noop_actions : term option array;
-  (* NOOP actions of "active" player indexed by locations *)
-  fluents : string list;
-}
-
-let empty_gdl_translation =
-  {anchor_terms = [];
-   tossrule_data = Aux.StrMap.empty;
-   t_elements = Aux.IntMap.empty;
-   playing_as = 0;
-   noop_actions = [||];
-   fluents = []}
-
 let rec term_str = function
   | Const c -> c
   | Var v -> "?"^v
@@ -743,6 +81,7 @@
   | Const _ -> Aux.Strings.empty
   | Var v | MVar v -> Aux.Strings.singleton v
   | Func (f, args) -> terms_vars args
+
 and terms_vars args =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map term_vars args)
@@ -754,33 +93,6 @@
   | Currently arg -> "true", [arg]
   | Does (arg1, arg2) -> "does", [arg1; arg2]
 
-let fprint_gdl_transl_data ?(details=false) ppf gdl =
-  (* TODO: print more data if needed *)
-  Format.fprintf ppf
-    "GDL_DATA@,{@[<1>FLUENTS@ %a;@ PLAYING_AS@ %d;@ NOOPS@ %a;"
-    (Aux.fprint_sep_list "," Format.pp_print_string) gdl.fluents
-    gdl.playing_as
-    (Aux.fprint_sep_list "," Format.pp_print_string)
-    (Array.to_list (Array.mapi (fun i -> function
-      | None -> string_of_int i ^": None"
-      | Some noop -> string_of_int i ^": "^term_str noop) gdl.noop_actions));
-  Aux.StrMap.iter (fun rname data ->
-    Format.fprintf ppf "@ @[<1>RULE@ %s:@ LEGAL=@,%s;@ PRECOND=@,%a;@ "
-      rname (term_str data.lead_legal) Formula.fprint data.precond;
-    Format.fprintf ppf "{@[<1>RHS ADD:@ ";
-    Aux.fprint_sep_list ";" Format.pp_print_string ppf
-      (List.map (fun (rel,args) -> rel^"("^String.concat ", "
-        (Array.to_list args)^")") data.rhs_add);
-    Format.fprintf ppf "@]}@]"
-  ) gdl.tossrule_data;
-  Format.fprintf ppf "@]}"
-
-let sprint_gdl_transl_data ?(details=false) gdl =
-  ignore (Format.flush_str_formatter ());
-  Format.fprintf Format.str_formatter "@[%a@]"
-    (fprint_gdl_transl_data ~details) gdl;
-  Format.flush_str_formatter ()
-
 let rec body_of_literal = function
   | Pos (Distinct args) ->
     [Aux.Right ("distinct", args)]        (* not negated actually! *)
@@ -791,8 +103,7 @@
     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
+  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
@@ -801,15 +112,13 @@
    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
+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
+type exp_def = string * exp_def_branch list
 
 module Terms = Set.Make (
   struct type t = term let compare = Pervasives.compare end)
@@ -844,9 +153,6 @@
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map sdef_br_vars brs)
 
-(*
-  let branch_vars (args, body, neg_body) =
-*)  
 let rels_vars body =
   List.fold_left Aux.Strings.union Aux.Strings.empty
     (List.map (fun (_,args)->terms_vars args) body)
@@ -897,14 +203,12 @@
       head, pos_body, neg_body) bodies
   | Atomic (rel, args) -> [(rel, args), [], []]
 
-let add_neg_body_vars global_vars neg_body
-    : (Aux.Strings.t * gdl_atom) list =
+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 =
+let lit_defs_of_rules rules : (string * lit_def_branch list) list =
   Aux.map_reduce
     (fun ((drel, params), body, neg_body) ->
       let global_vs =
@@ -1016,7 +320,7 @@
         (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 ?(ignore_meta=false) sb m_sb terms1 terms2 =
@@ -1052,7 +356,6 @@
       raise Not_found
 
 
-(* 3c1 *)
 let generalize term1 term2 =
   let fresh_count = ref 0 in
   let rec loop pf terms1 terms2 =
@@ -1079,14 +382,6 @@
   let measure, mism, gens = loop "impossible" [term1] [term2] in
   measure, !fresh_count, mism, 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 ->
@@ -1097,8 +392,6 @@
   | Func (f, args) ->
     Func (f, List.map (subst sb) args)
 
-let extend_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
-
 let rec unify_all sb = function
   | [] | [_] -> sb
   | t1::t2::tl ->
@@ -1131,7 +424,7 @@
   List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body
 
 let fact_str (rel, args) =
-  "("^rel^" "^String.concat " " (List.map term_str args) ^")"
+  "(" ^ rel ^ " " ^ String.concat " " (List.map term_str args) ^ ")"
 
 let tuples_str tups =
   let tup_str tup =
@@ -1141,8 +434,8 @@
 let terms_str facts =
   String.concat ", " (List.map term_str facts)
 
-let facts_str facts =
-  String.concat " " (List.map fact_str facts)
+let facts_str facts = String.concat " " (List.map fact_str facts)
+
 let neg_lfacts_str negs =
   String.concat " "
     (List.map (fun (vs,d) ->
@@ -1150,6 +443,7 @@
       let q = if vs = [] then ""
         else "forall "^String.concat ", " vs in
       q ^ "(not "^fact_str d^")") negs)
+
 let neg_facts_str negs =
   String.concat " "
     (List.map (fun (vs,d) ->
@@ -1173,21 +467,13 @@
     "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
       " " ^ neg_facts_str neg_body ^ ")"
   ) branches)
-(*
-let rule_str (head, body, neg_body) =
-  String.concat "\n" (List.map (fun (args, body, neg_body) ->
-    "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
-      " " ^ String.concat " "
-      (List.map (fun f->"not "^fact_str f) neg_body) ^ ")"
-  ) branches)
-*)
+
 let sb_str sb =
   String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
 
 let proto_rel_str (rel, args) =
   rel ^"(" ^ String.concat ", " (Array.to_list args) ^")"
 
-(* 1b *)
 
 (* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
    TODO: optimize by using constant-time append data structure. *)
@@ -1227,7 +513,6 @@
 
   let rec inst_stratum old_base old_irules cur_base cur_irules =
     (* {{{ 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);
@@ -1235,7 +520,6 @@
         "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
@@ -1283,367 +567,10 @@
     (List.map rules_of_lit_defs (stratify [] (lit_defs_of_rules rules)))
 
 
-let game_description = ref []
-let player_terms = ref [| |]
-
-let state_of_file s =
-  let f = open_in s in
-  let res =
-    ArenaParser.parse_game_state Lexer.lex
-      (Lexing.from_channel f) in
-  res
-
-(* 6 *)
-
-(* Need a global access so that the support can be reset between
-   different translations. (Generalization uses a local [fresh_count]
-   state.) *)
-let var_support = ref Aux.Strings.empty
-
-let freshen_branch (args, body, neg_body) =
-  let sb = ref [] in
-  let rec map_vnames = function
-    | Var x ->
-      if List.mem_assoc x !sb then Var (List.assoc x !sb)
-      else
-        let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
-        var_support := Aux.Strings.add x1 !var_support;
-        sb := (x,x1)::!sb;
-        Var x1
-    | MVar x ->
-      if List.mem_assoc x !sb then MVar (List.assoc x !sb)
-      else
-        let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
-        var_support := Aux.Strings.add x1 !var_support;
-        sb := (x,x1)::!sb;
-        MVar x1
-    | 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
-  let map_neg (vs, atoms) =
-    let vs =
-      List.map (fun x ->
-        if List.mem_assoc x !sb then List.assoc x !sb
-        else
-          let x1 = Aux.not_conflicting_name ~truncate:true !var_support x in
-          var_support := Aux.Strings.add x1 !var_support;
-          sb := (x,x1)::!sb; x1
-      ) (Aux.Strings.elements vs) in
-    Aux.strings_of_list vs,
-    List.map map_rel atoms in
-  List.map map_vnames args,
-  List.map map_rel body,
-  List.map map_neg neg_body
-
-let freshen_def_branches brs =
-  List.map freshen_branch brs
-
-(* [args] are the actual, instatiated, arguments. *)
-let negate_def uni_vs args neg_def =
-  (* 6b1a *)
-  let global_vars = terms_vars args in
-  let aux_br (params, body, neg_body) =
-    let sb = unify [] params args in
-    let body = subst_rels sb body in
-    let neg_body = List.map (fun (vs, conjs) ->
-      vs, subst_rels sb conjs) neg_body in
-    let subforms = (Aux.Strings.empty, body) :: neg_body in
-    (* components of [vars_i] by conjuncts *)
-    let sub_fvars = List.map (fun (_, subphi) ->
-      Aux.Strings.diff (rels_vars subphi) global_vars) subforms in
-    let subvars = List.map2 (fun fvs (qvs,_) ->
-      Aux.Strings.diff fvs qvs) sub_fvars subforms in
-    (* 6b1b *)
-    if List.exists (fun (vs1, vs2) ->
-      not (Aux.Strings.is_empty (Aux.Strings.inter vs1 vs2)))
-      (Aux.pairs subvars)
-    then failwith
-      ("GDL.negate_def: variables shared between negated subformulas" ^
-          " -- long term TODO (params: "^terms_str params^")");
-    (if List.exists (fun (fvs, (qvs,_)) ->
-      (* [fvs - qvs] must be a subset of the "vars_i" quantified vars *)
-      not (Aux.Strings.is_empty (Aux.Strings.diff fvs qvs)))
-        (List.tl (List.combine sub_fvars subforms))
-    then
-      let (fvs,(qvs,_)) = List.find (fun (fvs, (qvs,_)) ->
-        not (Aux.Strings.is_empty (Aux.Strings.diff fvs qvs)))
-        (List.tl (List.combine sub_fvars subforms)) in
-      failwith
-        ("GDL.negate_def: universal quantification escapes negation" ^
-            " -- doable TODO (params: "^terms_str params^") (vars: "^
-            String.concat ", " (Aux.Strings.elements
-                                  (Aux.Strings.diff fvs qvs))^")"));
-    Aux.Right (List.hd sub_fvars, body) ::
-      List.map (fun (_,conjs) -> Aux.Left conjs) neg_body in
-  (* 6b1c *)
-  (* We drop branches whose heads don't match. *)
-  let cnf = Aux.map_try aux_br neg_def in
-  let dnf = Aux.product cnf in
-  List.map (fun conjs ->
-    let pos, neg = Aux.partition_choice conjs in
-    (* since (6b1b), no local universal quantification *)
-    let pos = List.concat pos in
-    pos, neg
-  ) dnf
-
-
-(* assumption: [defs] bodies are already clean of defined relations *)
-let subst_def_branch (defs : exp_def list)
-    (head, body, neg_body as br : lit_def_branch) : exp_def_branch list =
-  var_support := Aux.Strings.union !var_support
-    (lit_def_br_vars br);
-  (* {{{ log entry *)
-  if !debug_level > 3 then (
-    Printf.printf "Expanding branch %s\n%!" (lit_def_str ("BRANCH", [br]));
-  );
-  (* }}} *)
-  (* 6a *)
-  let sols =
-    List.fold_left (fun sols (rel, args as atom) ->
-      (let try def =
-         freshen_def_branches (List.assoc rel defs) in
-       (* {{{ log entry *)
-       if !debug_level > 3 then (
-         Printf.printf "Expanding positive %s by %s\n%!" rel
-           (exp_def_str (rel, def))
-       );
-       (* }}} *)
-       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 (fun (vs,bs)->vs, subst_rels sb1 bs)
-                 (dneg_body @ neg_sol),
-               extend_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 neg_body_flat, neg_body_rec =
-    Aux.partition_map (fun (uni_vs, (neg_rel, neg_args) as neg_lit) ->
-      (let try def =
-         freshen_def_branches (List.assoc neg_rel defs) in
-       if not (List.exists (fun (_,_,negb) -> negb<>[]) def)
-       then Aux.Left (neg_lit, Some def)
-       else (
-         (* {{{ log entry *)
-         if !debug_level > 3 then (
-           let _,_,def_neg_body =
-             List.find (fun (_,_,negb) -> negb <> []) def in
-           Printf.printf
-             "expand: found recursive negative %s(%s): neg_body= not %s\n%!"
-             neg_rel (terms_str neg_args)
-             (String.concat " and not "
-                (List.map facts_str (List.map snd def_neg_body)))
-         );
-         (* }}} *)
-         Aux.Right (neg_lit, def))
-       with Not_found -> Aux.Left (neg_lit, None))
-    ) neg_body in
-  (* checking if all negative bodies are just already satisfied
-     "distinct" atoms; we could refine the split per-solution, but it
-     isn't worth the effort *)
-  let more_neg_flat, neg_body_rec =
-    Aux.partition_map (fun (_, (_, args) as neg_lit, def as neg_case) ->
-      if List.for_all (function
-        | _,_,[] -> true
-        |_,_,neg_body ->
-          List.for_all (function
-            | _, ["distinct", _] -> true | _ -> false) neg_body
-      ) def
-      then
-        if List.for_all (function
-          | _,_,[] -> true
-          |params,_,neg_body ->
-            List.for_all (function
-              | _, ["distinct", terms] ->
-                List.for_all (fun (_,_,sb) ->
-                  let args = List.map (subst sb) args in
-                  let sb1 = unify [] params args in
-                  let terms = List.map (subst sb1) terms in
-                  (* {{{ log entry *)
-                  if !debug_level > 4 then (
-                    Printf.printf
-                      "Checking distinctness of %s after sb=%s; sb1=%s\n%!"
-                      (terms_str terms)
-                      (sb_str sb) (sb_str sb1)
-                  );
-                  (* }}} *)
-                  Aux.Strings.is_empty (terms_vars terms)
-                  && List.length (Aux.unique_sorted terms) > 1
-                ) sols
-              | _ -> false) neg_body) def
-        then
-          let def = List.map (fun (params, body, neg_body) ->
-            params, body, []) def in
-          Aux.Left (neg_lit, Some def)
-        else Aux.Right neg_case
-      else Aux.Right neg_case
-    ) neg_body_rec in
-  (* {{{ log entry *)
-  if !debug_level > 3 then (
-    Printf.printf "Expanding (%s) negative part: flat %s; rec %s\n%!"
-      (terms_str head)
-      (String.concat ", "(List.map (fun ((_,(nr,_)),_) -> nr) neg_body_flat))
-      (String.concat ", "(List.map (fun ((_,(nr,_)),_) -> nr) neg_body_rec))
-  );
-  (* }}} *)
-  (* 6b1 *)
-  let sols =
-    List.fold_left (fun sols ((uni_vs, (rel, args)), neg_def) ->
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        Printf.printf "Expanding rec-negative %s by %s\n%!" rel
-          (exp_def_str (rel, neg_def))
-      );
-      (* }}} *)
-      (* we don't keep the substitution from the negated match *)
-      Aux.concat_map (fun (pos_sol, neg_sol, sb) ->
-        let args = List.map (subst sb) args in
-        let branches = negate_def uni_vs args neg_def in
-        List.map (fun (dbody, dneg_body) ->
-          dbody @ pos_sol, dneg_body @ neg_sol, sb) branches
-      ) sols)
-      sols neg_body_rec in
-
-  (* 6b2 *)
-  let sols =
-    List.map (fun (pos_sol, neg_sol, sb) ->
-      let more_neg_sol =
-        Aux.concat_map (fun ((uni_vs, (rel, args as atom)), def_opt) ->
-          (* negated subformulas are duplicated instead of branches *)
-          match def_opt with
-            | Some def ->
-              let args = List.map (subst sb) args in
-              Aux.map_try (fun (dparams, dbody, _) ->
-                (let sb1 = unify [] dparams args in
-                 let param_vars = terms_vars dparams in
-                 let body_vars = rels_vars dbody in
-                 let dbody = subst_rels sb1 dbody in
-                 let local_vs =
-                   Aux.Strings.diff body_vars
-                     (Aux.Strings.diff param_vars uni_vs) in
-                 local_vs, dbody)
-              ) def
-            | None ->              (* rel not in defs *)
-              [uni_vs, [atom]]
-        ) (more_neg_flat @ neg_body_flat) in
-      List.rev pos_sol, List.rev_append neg_sol more_neg_sol, sb
-    ) sols in
-  let res =
-    Aux.map_some (fun (pos_sol, neg_sol, sb) ->
-      if List.exists (function _,[] -> true | _ -> false) neg_sol
-      then None
-      else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols in
-  (* {{{ log entry *)
-  if !debug_level > 3 then (
-    Printf.printf "Expansion: res =\n%s\nExpansion done.\n%!"
-      (String.concat "\n"(List.map (branch_str "exp-unkn") res))
-  );
-  (* }}} *)
-  res
-
-(* Stratify and expand all relations in the given set. *)
-let expand_def_rules ?(more_defs=[]) rules =
-  let rec loop base = function
-    | [] -> base
-    | stratum::strata ->
-      (* {{{ log entry *)
-      if !debug_level > 3 then (
-        Printf.printf "expand_def_rules: step base rels = %s\n%!"
-          (String.concat ", " (List.map fst base))
-      );
-      (* }}} *)
-      let step = List.map (fun (rel, branches) ->
-        rel, Aux.concat_map
-          (subst_def_branch (more_defs@base)) branches) stratum in
-      (* {{{ log entry *)
-if !debug_level > 3 then (
-  Printf.printf "expand_def_rules: step result = %s\nexpand_def_rules: end step\n%!"
-    (String.concat "\n" (List.map exp_def_str step))
-);
-(* }}} *)
-      loop (base @ step) strata in
-  match stratify ~def:true [] (lit_defs_of_rules rules) with
-    | [] -> []
-    | [no_defined_rels] when more_defs=[] ->
-      exp_defs_of_lit_defs no_defined_rels
-    | def_base::def_strata when more_defs=[] ->
-      loop (exp_defs_of_lit_defs def_base) def_strata
-    | def_strata -> loop more_defs def_strata
-
-(* As [subst_def_branch], but specifically for "legal" definition and
-   result structured by "legal" definition branches. *)
-(* 7b *)
-let subst_legal_rule legal
-    (head, body, neg_body as br)
-    : (exp_def_branch * exp_def_branch) option =
-  var_support := Aux.Strings.union !var_support
-    (exp_def_br_vars br);
-  let legal = freshen_branch legal in
-  let legal_args, legal_body, legal_neg_body = legal in
-  (* {{{ log entry *)
-  if !debug_level > 3 then (
-    Printf.printf "subst_legal_rule:\n%s\n%s\n%!"
-      (exp_def_str ("legal", [legal]))
-      (exp_def_str ("branch", [br]))
-  );
-  (* }}} *)
-  if List.exists (fun (_,neg_conjs) ->
-    List.exists (fun (rel,_)->rel="does") neg_conjs) neg_body
-  then failwith
-    "GDL.translate_game: negated \"does\" conditions not implemented yet";
-  try
-    let body, more_neg_body, sb =
-      List.fold_left (fun (body,more_neg_body,sb) (rel, args as atom) ->
-        if rel = "does" then
-          ("_DOES_PLACEHOLDER_", args) :: List.rev_append legal_body body,
-          List.rev_append legal_neg_body more_neg_body,
-          unify sb legal_args args
-        else atom::body, more_neg_body, sb) ([],[],[]) body in
-    let legal_res =
-      List.map (subst sb) legal_args,
-      subst_rels sb legal_body,
-      List.map (fun (uni_vs,neg_conjs) ->
-        (* local variables so cannot be touched *)
-        uni_vs, subst_rels sb neg_conjs)
-        legal_neg_body in
-    let br_res =
-      List.map (subst sb) head,
-      subst_rels sb (List.rev body),
-      List.map (fun (uni_vs, neg_conjs) ->
-        uni_vs, subst_rels sb neg_conjs)
-        (List.rev_append more_neg_body neg_body) in
-    (* {{{ log entry *)
-if !debug_level > 3 then (
-  Printf.printf "%s\n%s\n"
-    (exp_def_str ("legal-res", [legal_res]))
-    (exp_def_str ("br-res", [br_res]))
-);
-(* }}} *)
-    Some (legal_res, br_res)
-  with Not_found -> None
-
-let subst_legal_rules def_brs brs =
-  Aux.unique_sorted
-    (Aux.concat_map (fun br ->
-      List.map (fun (_,x) -> br, x)
-        (Aux.map_some (fun def -> subst_legal_rule def br) def_brs)) brs)
-
-(* 1 *)
-
 (* Collect the aggregate playout, but also the actions available in
    the state. *)
 exception Playout_over
+
 let aggregate_ply players static current rules =
   let base =
     Aux.map_prepend static (fun term -> "true", [term]) current in
@@ -1717,7 +644,6 @@
     (fun ((rel,_),_,_) -> List.mem rel static_rels) rules in
   let static_base = saturate [] static_rules in
   let state_rules =
-    (* 1, 1a *)
     List.map (function
       | ("legal", [player; _] as head), body, neg_body ->
         head, ("role", [player])::body,
@@ -1808,2956 +734,3 @@
     );
     (* }}} *)
     false
-
-let rec blank_out = function
-  | Const a as c, Const b when a = b -> c
-  | (*Var _ as*) v, Var _ -> v
-  | t, MVar _ -> Const "_BLANK_"
-  | Func (f, f_args), Func (g, g_args) when f = g ->
-    Func (f, List.map blank_out (List.combine f_args g_args))
-  | a, b ->
-    Printf.printf "blank_out mismatch: term %s, mask %s\n%!"
-      (term_str a) (term_str b);
-    assert false
-
-
-let triang_matrix elems =
-  let rec aux acc = function
-    | [] -> acc
-    | hd::tl -> aux (List.map (fun e->[|hd; e|]) tl @ acc) tl in
-  aux [] elems
-
-
-let term_to_blank masks next_arg =
-  let mask_cands =
-    Aux.map_try (fun mask ->
-      mask, match_meta [] [] [next_arg] [mask]
-    ) masks in
-  let mask, sb, m_sb = match mask_cands with
-    | [mask, (sb, m_sb)] -> mask, sb, m_sb
-    | _ ->
-      Printf.printf "GDL.term_to_blank: bad state term %s\n%!"
-        (term_str next_arg);
-      assert false in
-  mask, sb, m_sb, blank_out (next_arg, mask)
-
-let toss_var masks term =
-  let mask, _, _, blank = term_to_blank masks term in
-  mask, Formula.fo_var_of_string (String.lowercase (term_to_name blank))
-
-
-(* Expand branch variables. If [freshen_unfixed=Right fixed], expand
-   all variables that don't belong to [fixed] and appear in the head
-   of some branch. If [freshen_unfixed=Left freshen], then expand all
-   variables below meta-variables of masks. If [freshen] is true,
-   rename other (i.e. non-expanded) variables while duplicating
-   branches. (When [freshen] is false, all remaining variables should
-   be fixed.)
-
-   With each branch, also return the instantiation used to derive it???
-
-   As in the expansion of relation definitions, branches are
-   duplicated for instantiations of positive literals, and
-   additionally of heads. For instantiations of atoms in negated
-   subformulas, the subformulas are duplicated within a branch, with
-   instantiations kept local to the subformula. Final substitution is
-   re-applied to catch up with later instantiations. *)
-let expand_branch_vars masks playout_terms ~freshen_unfixed brs =
-  let head_vars = List.fold_left (fun acc -> function [head],_,_ ->
-    Aux.Strings.union acc (term_vars head)
-    | _ -> assert false) Aux.Strings.empty  brs in
-  let use_fixed, fixed =
-    match freshen_unfixed with
-      | Aux.Left _ -> false, Aux.Strings.empty
-      | Aux.Right fixed -> true, fixed in
-(* {{{ log entry *)
-if !debug_level > 4 then (
-  Printf.printf "expand_branch_vars: head_vars: %s; fixed vars: %s; before=\n%s\n%!"
-    (String.concat ","(Aux.Strings.elements head_vars))
-    (String.concat ","(Aux.Strings.elements fixed))
-    (exp_def_str ("before", brs))
-);
-(* }}} *)
-  let expand sb arg =
-    let arg = subst sb arg in
-    let mask, _, m_sb, blank = term_to_blank masks arg in
-    let ivars = Aux.concat_map (fun (_,t) ->
-      Aux.Strings.elements (term_vars t)) m_sb in
-    let is_inst_var v =
-      (*if use_fixed
-      then
-        (Aux.Strings.mem v head_vars || List.mem v ivars)
-        && not (Aux.Strings.mem v fixed)
-      else*) List.mem v ivars in
-    Aux.unique_sorted
-      (Aux.map_try (fun term ->
-        let sb1, _ = match_meta [] [] [term] [arg] in
-        let sb1 = List.sort Pervasives.compare
-          (List.filter (fun (v,_)->is_inst_var v) sb1) in
-        extend_sb sb1 sb, subst sb1 arg
-       ) playout_terms) in
-  let expand_rel atom (sb, acc) =
-    match atom with
-      | "true", [arg] ->
-        List.map (fun (sb,arg) -> sb, ("true",[arg])::acc) (expand sb arg)
-      | rel, args -> [sb, (rel, List.map (subst sb) args)::acc] in
-  let expand_neg sb (v...
 
[truncated message content]