[Toss-devel-svn] SF.net SVN: toss:[1509] trunk/Toss/GGP
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1509] trunk/Toss/GGP
|
From: <luk...@us...> - 2011-07-10 19:48:05
|
Revision: 1509
http://toss.svn.sourceforge.net/toss/?rev=1509&view=rev
Author: lukstafi
Date: 2011-07-10 19:47:57 +0000 (Sun, 10 Jul 2011)
Log Message:
-----------
GDL translation work in progress: file changes. Does not compile yet.
Modified Paths:
--------------
trunk/Toss/GGP/TranslateFormula.ml
trunk/Toss/GGP/TranslateGame.ml
Added Paths:
-----------
trunk/Toss/GGP/TranslateFormula.mli
trunk/Toss/GGP/TranslateGame.mli
trunk/Toss/GGP/TranslateGameTest.ml
Removed Paths:
-------------
trunk/Toss/GGP/Translate.ml
trunk/Toss/GGP/Translate.mli
trunk/Toss/GGP/TranslateTest.ml
Deleted: trunk/Toss/GGP/Translate.ml
===================================================================
--- trunk/Toss/GGP/Translate.ml 2011-07-09 12:37:34 UTC (rev 1508)
+++ trunk/Toss/GGP/Translate.ml 2011-07-10 19:47:57 UTC (rev 1509)
@@ -1,3711 +0,0 @@
-open GDL
-
-(** {2 Game Description Language.}
-
- 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. 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
-
-(** 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 tossrule_data = {
- lead_legal : GDL.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 * (GDL.term * (string * string list) list) list) list;
- (* "state" terms indexed by variables that they contain, together
- with the mask-path of the variable *)
- elemvars : GDL.term Aux.StrMap.t;
-(* "state" terms indexed by Toss variable names they generate *)
-}
-
-type gdl_translation = {
- anchor_terms :
- (GDL.term * (string * (GDL.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 : GDL.term Aux.IntMap.t;
- (* element terms (with metavariables only) *)
- playing_as : int;
- (* "active" player *)
- noop_actions : GDL.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 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 ^": "^GDL.term_str noop) gdl.noop_actions));
- Aux.StrMap.iter (fun rname data ->
- Format.fprintf ppf "@ @[<1>RULE@ %s:@ LEGAL=@,%s;@ PRECOND=@,%a;@ "
- rname (GDL.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 ()
-
-
-(* 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 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
-
-let extend_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
-
-
-(* [args] are the actual, instatiated, arguments. *)
-let negate_def uni_vs args neg_def =
- 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
- 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
- (* 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
- 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)
-
-
-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 (vs, neg_conj) =
- let neg_conjs =
- Aux.concat_foldr expand_rel neg_conj [sb, []] in
- List.map (fun (sb, neg_conj) ->
- let vs = List.filter (fun v -> not (List.mem_assoc v sb))
- (Aux.Strings.elements vs) in
- Aux.strings_of_list vs, neg_conj
- ) neg_conjs in
- let brs =
- Aux.concat_map (function ([head],body,neg_body) ->
- Aux.concat_map (fun (sb,head) ->
- let bodies = Aux.concat_foldr expand_rel body [sb, []] in
- Aux.map_some (fun (sb, body) ->
- let head = subst sb head in
- let body = List.map (subst_rel sb) body in
- let neg_body =
- Aux.concat_map (expand_neg sb) neg_body in
- if List.exists (function _, [] -> true | _ -> false)
- neg_body then None
- (* need to pack head into a list for [freshen_branch] *)
- else Some (sb, ([head], body, neg_body))) bodies)
- (if head = Const "_IGNORE_RHS_" then [[], head]
- else expand [] head)
- | _ -> assert false) brs in
- (* {{{ log entry *)
-if !debug_level > 4 then (
- Printf.printf "expand_branch_vars: substitutions=\n%s\n%!"
- (String.concat ";; " (List.map (sb_str -| fst) brs))
-);
-(* }}} *)
- match freshen_unfixed with
- | Aux.Left true ->
- List.map (fun (sb, br) -> sb, freshen_branch br) brs
- | _ -> brs
-
-(* (7l5)-related exception. *)
-exception Failed_branch
-
-let translate_branches ?(conjunctive=false) struc masks playout_terms
- static_rnames dyn_rels
- (brs : exp_def_branch list) =
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "Translating-branches:\n%s\n%!"
- (exp_def_str ("translating", brs));
- );
- (* }}} *)
- (* 7i *)
- (* the state terms are positive, the relation can be positive or
- negative -- negate atoms after generation if the atom was negative *)
- let pos_conjs_4a pos_state_subterms (rel, args) =
- let ptups = List.map (fun arg ->
- Aux.assoc_all arg pos_state_subterms) args in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "pos_conjs_4a: of %s = subterms %s\n%!"
- (fact_str (rel,args)) (String.concat "; " (
- List.map (fun l -> String.concat ", "
- (List.map (fun (_,_,term)->term_str term) l)) ptups))
- );
- (* }}} *)
- let ptups = Aux.product ptups in
- let res =
- List.map (fun ptup ->
- let rname = rel ^ "__" ^ String.concat "__"
- (List.map (fun (mask,v,_)->
- term_to_name mask ^ "_" ^ v) ptup) in
- let tup = List.map (fun (_,_,term) ->
- snd (toss_var masks term)) ptup in
- Formula.Rel (rname, Array.of_list tup)) ptups in
- let res = Aux.unique_sorted res in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "pos_conjs_4a: of %s = %s\n%!"
- (fact_str (rel,args)) (Formula.str (Formula.And res))
- );
- (* }}} *)
- res in
- (* some of the state terms are always negative, the relation can be
- positive or negative but always negate resulting atoms *)
- let neg_conjs_4a pos_state_subterms
- neg_state_terms neg_state_subterms (rel, args) =
- let ptups = List.map (fun arg ->
- Aux.assoc_all arg pos_state_subterms @
- Aux.assoc_all arg neg_state_subterms) args in
- let ptups = Aux.product ptups in
- let ptups = List.filter (fun tup ->
- List.exists (fun (_,_,term) -> Terms.mem term neg_state_terms) tup)
- ptups in
- let res =
- List.map (fun ptup ->
- let rname = rel ^ "__" ^ String.concat "__"
- (List.map (fun (mask,v,_)->
- term_to_name mask ^ "_" ^ v) ptup) in
- let tup = List.map (fun (_,_,term) ->
- snd (toss_var masks term)) ptup in
- Formula.Rel (rname, Array.of_list tup)) ptups in
- let res = Aux.unique_sorted res in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "neg_conjs_4a: of %s = %s\n%!"
- (fact_str (rel,args)) (Formula.str (Formula.And res))
- );
- (* }}} *)
- res in
- (* 7i-4b *)
- (* FIXME: abandon filtering-out rendundant mask variables during
- translation -- this is the job of GameSimplify! *)
- let constrained_vars = ref [] in
- let pos_conjs_4b pos_path_subterms =
- Aux.unique_sorted (Aux.concat_map (fun ((mask, v), terms) ->
- let rname = "EQ___" ^ term_to_name mask ^ "_" ^ v in
- let terms = Aux.collect terms in
- Aux.concat_map (fun (_,terms) ->
- let vars = Aux.unique_sorted
- (List.map (fun t -> snd (toss_var masks t)) terms) in
- constrained_vars := vars @ !constrained_vars;
- let tups =
- match !equivalences_all_tuples with
- | Pairs_all ->
- Aux.concat_map (fun v -> Aux.map_some (fun w ->
- if v=w then None else Some [|v; w|]) vars) vars
- | Pairs_triang ->
- (* generating more relations to faciliate "contraction" of
- co-occurring relations in GameSimpl -- since it
- GameSimpl handles inversion, no need for bidirectional
- links *)
- triang_matrix vars
- | Pairs_star ->
- (* (4b) are equivalences, so we just build a "star" *)
- match vars with [] -> []
- | v::vs -> List.map (fun w -> [|v; w|]) vs in
- if !equivalences_ordered then
- List.iter (Array.sort Pervasives.compare) tups;
- List.map (fun tup -> Formula.Rel (rname, tup)) tups
- ) terms
- ) pos_path_subterms) in
- let neg_conjs_4b pos_path_subterms nterm =
- let nmask, nsb, _, _ = term_to_blank masks nterm in
- let _,ntossvar = toss_var masks nterm in
- Aux.concat_map (fun ((mask, v), terms) ->
- if mask <> nmask then []
- else
- let nval =
- try List.assoc v nsb with Not_found -> assert false in
- match nval with
- | Var nval ->
- let rname = "EQ___" ^ term_to_name mask ^ "_" ^ v in
- let terms =
- Aux.assoc_all nval terms in
- let tossvars = Aux.unique_sorted
- (List.map (fun t -> snd (toss_var masks t)) terms) in
- (* these don't get constrained since they'll occur negatively *)
- let tups =
- match !equivalences_all_tuples with
- | Pairs_all ->
- Aux.concat_map
- (fun v ->
- if v = ntossvar then []
- else [[|v; ntossvar|]; [|ntossvar; v|]]) tossvars
- | Pairs_triang | Pairs_star ->
- Aux.map_some (fun v ->
- if v = ntossvar then None
- else Some [|v; ntossvar|]) tossvars in
- if !equivalences_ordered then
- List.iter (Array.sort Pervasives.compare) tups;
- List.map (fun tup -> Formula.Rel (rname, tup)) tups
- | _ -> []
- ) pos_path_subterms in
- (* calculate state terms twice: before and after filtering branches *)
- let pos_state_terms =
- List.fold_left (fun acc -> function
- | [next_arg], body, _ ->
- let res =
- List.fold_left (fun acc -> function
- | "true", [true_arg] -> Terms.add true_arg acc
- | "true", _ -> assert false
- | _ -> acc) acc body in
- if next_arg = Const "_IGNORE_RHS_"
- then res
- else Terms.add next_arg res
- | _ -> assert false
- ) Terms.empty brs in
- let pos_state_terms = Terms.elements pos_state_terms in
- (* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "pos_state_terms: %s\n%!"
- (String.concat ", " (List.map term_str pos_state_terms))
- );
- (* }}} *)
- let pos_state_subterms =
- Aux.concat_map (fun term ->
- let mask, sb, m_sb, blanked = term_to_blank masks term in
- List.map (fun (v,t) -> t, (mask, v, term)) sb
- ) pos_state_terms in
- let pos_path_subterms =
- Aux.concat_map (fun term ->
- let mask, sb, m_sb, blanked = term_to_blank masks term in
- Aux.map_some (function
- | v, Var t ->
- Some ((mask, v), (t, term))
- | _ -> None) sb
- ) pos_state_terms in
- let pos_path_subterms = Aux.collect pos_path_subterms in
- (* only compute the static part to filter-out inconsistent branches *)
- let pconjs_4b = pos_conjs_4b pos_path_subterms in
- let brs = Aux.map_some (function
- | [next_arg],body,neg_body as br ->
- let phi =
- if next_arg = Const "_IGNORE_RHS_" then []
- else
- let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var masks next_arg in
- (* if List.mem svar !constrained_...
[truncated message content] |