[Toss-devel-svn] SF.net SVN: toss:[1423] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1423] trunk/Toss
|
From: <luk...@us...> - 2011-04-27 17:44:43
|
Revision: 1423
http://toss.svn.sourceforge.net/toss/?rev=1423&view=rev
Author: lukstafi
Date: 2011-04-27 17:44:35 +0000 (Wed, 27 Apr 2011)
Log Message:
-----------
FormulaOps: satisfiability check in [remove_redundant]. GameSimpl: better glueing, bug fixes. GDL translation: two options for stronger pruning (for experiments); fix translating sets of clauses: when they are interpreted conjunctively, instead of filtering, raise [Unsatisfiable] if any branch is not satisfiable.
Modified Paths:
--------------
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/GDL.mli
trunk/Toss/GGP/GDLTest.ml
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/GGP/GameSimpl.mli
trunk/Toss/GGP/tests/breakthrough-raw.toss
trunk/Toss/GGP/tests/breakthrough-simpl.toss
trunk/Toss/GGP/tests/connect5-raw.toss
trunk/Toss/GGP/tests/connect5-simpl.toss
trunk/Toss/GGP/tests/tictactoe-raw.toss
trunk/Toss/GGP/tests/tictactoe-simpl.toss
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Server/ServerTest.ml
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/Arena/DiscreteRule.ml 2011-04-27 17:44:35 UTC (rev 1423)
@@ -1019,6 +1019,12 @@
let rewritable args =
Aux.array_for_all (fun v -> List.mem (Formula.var_str v) struc_elems)
args in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ FormulaOps.set_debug_level !debug_level;
+ Printf.printf "translate_from_precond:\n%!"
+ );
+ (* }}} *)
let conjs =
FormulaOps.flatten_ands (FormulaOps.remove_redundant precond) in
let posi, conjs = Aux.partition_map (function
@@ -1031,18 +1037,19 @@
Left (rel,args)
| phi -> Right phi) conjs in
let lhs_extracted = posi @ nega in
- let precond = Formula.And conjs in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf
- "translate_from_precond:\nposi=\n%s\nnega=\n%s\nprecond=\n%s\n%!"
+ "translate_from_precond:\nposi:\n%s\nnega:\n%s\norig-precond:\n%s\nsimpl-precond:%s\n%!"
(Formula.sprint (Formula.And (List.map (fun (rel,args) ->
Formula.Rel (rel,args)) posi)))
(Formula.sprint (Formula.And (List.map (fun (rel,args) ->
Formula.Rel (rel,args)) nega)))
(Formula.sprint precond)
+ (Formula.sprint (Formula.And conjs))
);
(* }}} *)
+ let precond = Formula.And conjs in
let fvars = FormulaOps.free_vars precond in
let local_vars =
List.filter (fun v->
@@ -1096,6 +1103,12 @@
let rhs_struc = add_rels rhs_struc add in
let lhs_struc = add_rels lhs_struc posi_s in
let lhs_struc = add_rels lhs_struc opt_s in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ FormulaOps.set_debug_level 0;
+ Printf.printf "translate_from_precond: end\n%!"
+ );
+ (* }}} *)
{
lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/Formula/Aux.ml 2011-04-27 17:44:35 UTC (rev 1423)
@@ -54,6 +54,9 @@
let snd3 (_,a,_) = a
let trd3 (_,_,a) = a
+let map_fst f (a,b) = f a, b
+let map_snd f (a,b) = a, f b
+
module BasicOperators = struct
let (-|) f g x = f (g x)
let (<|) f x = f x
@@ -306,6 +309,24 @@
done;
res
+let array_mapi_some f a =
+ let r = Array.mapi f a in
+ let rl = ref (Array.length r) in
+ for i=0 to Array.length a - 1 do
+ if r.(i) = None then decr rl
+ done;
+ if !rl = 0 then [||]
+ else
+ let pos = ref 0 in
+ while r.(!pos) = None do incr pos done;
+ let res = Array.create !rl (unsome r.(!pos)) in
+ incr pos;
+ for i=1 to !rl -1 do
+ while r.(!pos) = None do incr pos done;
+ res.(i) <- unsome r.(!pos); incr pos
+ done;
+ res
+
let array_map2 f a b =
let l = Array.length a in
if l <> Array.length b then
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/Formula/Aux.mli 2011-04-27 17:44:35 UTC (rev 1423)
@@ -39,6 +39,9 @@
val snd3 : 'a * 'b * 'c -> 'b
val trd3 : 'a * 'b * 'c -> 'c
+val map_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
+val map_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+
(** {2 Helper functions on lists and other functions lacking from the
standard library.} *)
@@ -187,6 +190,7 @@
(** Map an array filtering out some elements. *)
val array_map_some : ('a -> 'b option) -> 'a array -> 'b array
+val array_mapi_some : (int -> 'a -> 'b option) -> 'a array -> 'b array
(** Map a function over two arrays index-wise. Raises
[Invalid_argument] if the arrays are of different lengths. *)
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/Formula/FormulaOps.ml 2011-04-27 17:44:35 UTC (rev 1423)
@@ -954,9 +954,13 @@
track of the sign (variance) of a position. (Does not descend the
real part currently.) [implies] is applied to atoms only. Repeat
the removal till fixpoint since it can "unpack" literals e.g. from
- conjunctions to disjunctions.
+ conjunctions to disjunctions. Also perform a very basic check for
+ satisfiability of disjuncts.
TODO: traverse the real part too. *)
+exception Unsatisfiable
+(* [Unsatisfiable] does not escape the function -- [Or []] is
+ returned instead. *)
let remove_redundant ?(implies=(=)) phi =
let implied_by x y = implies y x in
let literal neg phis =
@@ -983,6 +987,17 @@
(String.concat "; " (List.map Formula.str more_negbase))
);
(* }}} *)
+ (* detect contradiction *)
+ List.iter (fun prem ->
+ List.iter (fun concl ->
+ if implies prem concl
+ then raise Unsatisfiable
+ ) more_negbase) (more_posbase @ posbase);
+ List.iter (fun prem ->
+ List.iter (fun concl ->
+ if implies prem concl
+ then raise Unsatisfiable
+ ) (more_negbase @ negbase)) more_posbase;
(* remove redundant *)
let more_posbase = List.filter
(fun more -> not (List.exists (implied_by more) posbase))
@@ -1038,8 +1053,14 @@
(String.concat "; " (List.map Formula.str neglits))
);
(* }}} *)
- literal neg poslits @ literal (not neg) neglits @
- List.map (aux posbase negbase neg) subtasks
+ let subresults =
+ Aux.map_some (fun disj ->
+ try Some (aux posbase negbase neg disj)
+ with Unsatisfiable -> None) subtasks in
+ let results =
+ literal neg poslits @ literal (not neg) neglits @ subresults in
+ if results = [] then raise Unsatisfiable
+ else results
and aux posbase negbase neg = function
| And conjs when not neg ->
@@ -1065,7 +1086,8 @@
(* }}} *)
let res = aux [] [] false (flatten_formula phi) in
if res = phi then res else fixpoint res in
- fixpoint phi
+ try fixpoint phi
+ with Unsatisfiable -> Or []
(* Compute size of a formula (currently w/o descending the real part). *)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/Formula/FormulaOps.mli 2011-04-27 17:44:35 UTC (rev 1423)
@@ -174,7 +174,9 @@
track of the sign (variance) of a position. (Does not descend the
real part currently.) [implies] is applied to atoms only. Repeat
the removal till fixpoint since it can "unpack" literals e.g. from
- conjunctions to disjunctions. *)
+ conjunctions to disjunctions. Also perform a very basic check for
+ satisfiability. Returns [Or []] if the formula is obviously
+ unsatisfiable (does not do any unification). *)
val remove_redundant :
?implies:(formula -> formula -> bool) -> formula -> formula
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-04-21 00:48:48 UTC (rev 1422)
+++ trunk/Toss/GGP/GDL.ml 2011-04-27 17:44:35 UTC (rev 1423)
@@ -60,8 +60,7 @@
processed in (3a)-(3b) are already expanded by (6).
(3a) Element terms are collected from the aggregate playout: the
- sum of state terms (the "control" function could be dropped but we
- are not taking the effort to identify it).
+ sum of state terms.
(3b) Element masks are generated by generalization from all "next"
rules where the "does" relations are expanded by all unifying
@@ -80,11 +79,19 @@
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
@@ -133,6 +140,9 @@
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
@@ -190,8 +200,9 @@
/\ not exist vars_n (args = params_n /\ body_n)]
(6b1) If the relation has negative subformulas in any of [body_i],
- we first negate the definition and then expand the negation as in
- the positive case.
+ 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.
@@ -298,10 +309,16 @@
contain some fixed variables or no variables at all, and other
containing only unfixed variables.
- (7f1) Branches with (only) 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.
+ (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),
@@ -319,6 +336,10 @@
(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.)
@@ -326,11 +347,11 @@
substituted with the "not distinct" unifier to proper equivalence
classes (remove equivalence classes that become empty).
- (7g) Instantiate remaining unfixed variables: Duplicate non-frame
- rules with unfixed variables for each instantiation of the unfixed
- variables warranted by the aggregate playout. (Perhaps can be done
- "symbolically" to avoid explosion.)
+ (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
@@ -368,9 +389,13 @@
subterms that instantiate (ordinary) variables in the mask
corresponding to the "next"/"true" atom.
- (7i0) Heuristic (reason for unsoundness): for "distinct", only
- check whether its arguments are syntactically equal.
+ (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.
@@ -408,8 +433,12 @@
(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).
+ 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
@@ -420,26 +449,50 @@
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).
+ translated game when making a move). The lattice is built by
+ summing rule bodies.
- (7l1) Since all variables are fixed, the lattice is built by
- summing rule bodies. To avoid contradictions and have a complete
- partition, we construct the set of all bit vectors indexed by all
- atoms occurring in the bodies. 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.
+ (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.
- (7l3) Filter out rule candidates that contradict all states
+ 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).
@@ -537,15 +590,50 @@
let debug_level = ref 0
let aggregate_drop_negative = ref false
let aggregate_fixpoint = ref true
-(** Expand static relations that do not have ground facts and have
- arity above the threshold. *)
+
+(** Expand static relations that do not have ground facts, are not
+ directly recursive, and have arity above the threshold. *)
let expand_arity_above = ref 0
-(** Generate all tuples for equivalences, to faciliate further
+(** Treat "next" clauses which introduce metavariables only for
+ variable-variable mismatch, as non-erasing frame clauses (to be
+ ignored). ("Wave" refers to the process of "propagating the frame
+ condition" that these clauses are assumed to do, if
+ [nonerasing_frame_wave] is set to [true].) *)
+let nonerasing_frame_wave = ref true
+
+(** 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
@@ -658,6 +746,7 @@
and terms_vars args =
List.fold_left Aux.Strings.union Aux.Strings.empty
(List.map term_vars args)
+
let fact_of_atom = function
| Distinct args -> assert false
@@ -722,6 +811,34 @@
module Atoms = Set.Make (
struct type t = string * term list let compare = Pervasives.compare end)
+
+let lit_def_br_vars (head, body, neg_body : lit_def_branch) =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map terms_vars
+ (head::List.map snd body @
+ List.map (snd -| snd) neg_body))
+
+let exp_def_br_vars (head, body, neg_body : exp_def_branch) =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map terms_vars
+ (head::List.map snd body @
+ Aux.concat_map (List.map snd -| snd) neg_body))
+
+let lit_def_brs_vars brs =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map lit_def_br_vars brs)
+
+let exp_def_brs_vars brs =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map exp_def_br_vars brs)
+
+let sdef_br_vars (head, body, neg_body) =
+ exp_def_br_vars ([head], body, neg_body)
+
+let sdef_brs_vars brs =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map sdef_br_vars brs)
+
(*
let branch_vars (args, body, neg_body) =
*)
@@ -935,27 +1052,27 @@
let fresh_count = ref 0 in
let rec loop pf terms1 terms2 =
match terms1, terms2 with
- | [], [] -> (0, 0), []
+ | [], [] -> (0, 0), [], []
| (Const a as cst)::terms1, Const b::terms2 when a=b ->
- let (good_vars, good_csts), gens = loop pf terms1 terms2 in
- (good_vars, good_csts+1), cst::gens
+ let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in
+ (good_vars, good_csts+1), mism, cst::gens
| Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g ->
- let (good_vars1, good_csts1), gen_args = loop f args1 args2 in
- let (good_vars2, good_csts2), gens = loop pf terms1 terms2 in
- (good_vars1+good_vars2, good_csts1+good_csts2),
+ let (good_vars1, good_csts1), mism1, gen_args = loop f args1 args2 in
+ let (good_vars2, good_csts2), mism2, gens = loop pf terms1 terms2 in
+ (good_vars1+good_vars2, good_csts1+good_csts2), mism1 @ mism2,
(Func (f,gen_args))::gens
| (Var x as var)::terms1, Var y::terms2 when x=y ->
- let (good_vars, good_csts), gens = loop pf terms1 terms2 in
- (good_vars+1, good_csts), var::gens
- | _::terms1, _::terms2 ->
- let measure, gens = loop pf terms1 terms2 in
+ let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in
+ (good_vars+1, good_csts), mism, var::gens
+ | t1::terms1, t2::terms2 ->
+ let measure, mism, gens = loop pf terms1 terms2 in
incr fresh_count;
- measure, MVar ("MV"^string_of_int !fresh_count)::gens
+ measure, (t1,t2)::mism, MVar ("MV"^string_of_int !fresh_count)::gens
| _::_, [] | [], _::_ -> raise
(Lexer.Parsing_error
("GDL.generalize: arity mismatch at function "^pf)) in
- let measure, gens = loop "impossible" [term1] [term2] in
- measure, !fresh_count, List.hd gens
+ let measure, mism, gens = loop "impossible" [term1] [term2] in
+ measure, !fresh_count, mism, List.hd gens
(* 3c2 *)
let abstract_consts fresh_count term =
@@ -1215,8 +1332,8 @@
List.map map_rel body,
List.map map_neg neg_body
-let freshen_def_branches =
- List.map freshen_branch
+let freshen_def_branches brs =
+ List.map freshen_branch brs
(* [args] are the actual, instatiated, arguments. *)
let negate_def uni_vs args neg_def =
@@ -1270,8 +1387,10 @@
(* 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 > 4 then (
+ if !debug_level > 3 then (
Printf.printf "Expanding branch %s\n%!" (lit_def_str ("BRANCH", [br]));
);
(* }}} *)
@@ -1281,7 +1400,7 @@
(let try def =
freshen_def_branches (List.assoc rel defs) in
(* {{{ log entry *)
- if !debug_level > 4 then (
+ if !debug_level > 3 then (
Printf.printf "Expanding positive %s by %s\n%!" rel
(exp_def_str (rel, def))
);
@@ -1312,7 +1431,6 @@
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
@@ -1322,11 +1440,50 @@
(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%!"
@@ -1338,19 +1495,19 @@
(* 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)
+ (* {{{ 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 *)
@@ -1374,7 +1531,7 @@
) def
| None -> (* rel not in defs *)
[uni_vs, [atom]]
- ) neg_body_flat in
+ ) (more_neg_flat @ neg_body_flat) in
List.rev pos_sol, List.rev_append neg_sol more_neg_sol, sb
) sols in
let res =
@@ -1419,44 +1576,63 @@
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_args, legal_body, legal_neg_body : exp_def_branch)
- (head, body, neg_body : exp_def_branch)
+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
- Some (
- (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),
- (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)))
+ 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.concat_map (fun br ->
- List.map snd
- (Aux.map_some (fun def -> subst_legal_rule def br) 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 *)
@@ -1666,11 +1842,12 @@
(* Expand branch variables. If [freshen_unfixed=Right fixed], expand
- all variables that don't belong to [fixed]. 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.)
+ 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???
@@ -1681,16 +1858,32 @@
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 is_inst_var =
- match freshen_unfixed with
- | Aux.Left _ ->
- let mask, sb, 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
- (fun v -> List.mem v ivars)
- | Aux.Right fixed -> fun v -> not (List.mem v fixed) 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
@@ -1727,19 +1920,37 @@
(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
-let translate_branches struc masks playout_terms static_rnames dyn_rels
+(* (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 > 3 then (
+ 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 ", "
@@ -1757,12 +1968,14 @@
Formula.Rel (rname, Array.of_list tup)) ptups in
let res = Aux.unique_sorted res in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ 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 ->
@@ -1782,13 +1995,15 @@
Formula.Rel (rname, Array.of_list tup)) ptups in
let res = Aux.unique_sorted res in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ 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) ->
@@ -1813,6 +2028,8 @@
(* (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
@@ -1843,6 +2060,8 @@
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
@@ -1862,7 +2081,7 @@
) Terms.empty brs in
let pos_state_terms = Terms.elements pos_state_terms in
(* {{{ log entry *)
- if !debug_level > 2 then (
+ if !debug_level > 4 then (
Printf.printf "pos_state_terms: %s\n%!"
(String.concat ", " (List.map term_str pos_state_terms))
);
@@ -1891,10 +2110,10 @@
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_vars then []
- else
- let phi = Formula.Rel (rname, [|svar|]) in
- [phi] in
+ (* if List.mem svar !constrained_vars then [] *)
+ (* else *)
+ let phi = Formula.Rel (rname, [|svar|]) in
+ [phi] in
let conjs =
Aux.concat_map (fun (rel, args as fact) ->
if rel = "true" then
@@ -1910,8 +2129,9 @@
| v, t as v_sb ->
let rname = term_to_name (subst_one v_sb mask) in
Some (Formula.Rel (rname, [|svar|]))) sb in
- if conjs <> [] || List.mem svar !constrained_vars
- then conjs else [phi]
+ phi::conjs
+ (* if conjs <> [] || List.mem svar !constrained_vars *)
+ (* then conjs else [phi] *)
else if List.mem rel static_rnames then
(* 7i-4a *)
pos_conjs_4a pos_state_subterms fact
@@ -1923,8 +2143,15 @@
let neg_conjs =
Aux.concat_map (function
| _, [rel, args as fact] ->
- if rel = "true" then []
- else if rel = "_DOES_PLACEHOLDER_"
+ if rel = "true" && !mask_anchors_of_neg = Positive_anch
+ then
+ (* 7i-4c *)
+ let true_arg = List.hd args in
+ let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
+ let rname = term_to_name mask in
+ let _, svar = toss_var masks true_arg in
+ [Formula.Rel (rname, [|svar|])]
+ else if rel = "true" || rel = "_DOES_PLACEHOLDER_"
then []
else if List.mem rel static_rnames then
(* 7i-4a *)
@@ -1932,6 +2159,7 @@
(pos_conjs_4a pos_state_subterms fact)
else if rel = "distinct" then
(* 7i0 *)
+ (* TODO! *)
if Aux.not_unique args then [Formula.Or []]
else []
else (
@@ -1940,27 +2168,43 @@
"translate_game: (7i) unexpected dynamic %s\n%!" rel;
assert false)
| _ -> []) neg_body in
- let all_conjs = phi @ conjs @ pconjs_4b @ neg_conjs in
- let phi = Formula.And all_conjs in
+ let all_conjs = phi @ conjs @ neg_conjs in
+ (* filter 4b not to do unnecessary work in solver *)
+ let used_vars = FormulaOps.free_vars (Formula.And all_conjs) in
+ let local_4b =
+ List.filter (fun f ->
+ List.for_all (fun v->List.mem v used_vars)
+ (FormulaOps.free_vars f)) pconjs_4b in
+ let phi = Formula.And (all_conjs @ local_4b) in
let phi = Formula.Ex (FormulaOps.free_vars phi, phi) in
(* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "evaluating:\nbranch=%s\nphi=%s\n%!"
+ if !debug_level > 4 then (
+ Printf.printf "translate-evaluating:\nbranch=%s\nphi=%s\n%!"
(exp_def_str ("eval", [br]))
- (Formula.str phi)
+ (Formula.sprint phi)
);
(* }}} *)
if Solver.M.check struc phi
then (
(* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "holds\n%!"
+ if !debug_level > 4 then (
+ Printf.printf "translate-holds\n%!"
);
(* }}} *)
Some (next_arg,body,neg_body))
- else None
+ else (
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "translate-doesn't hold\n%!"
+ );
+ (* }}} *)
+ if conjunctive
+ then raise Failed_branch
+ else None)
| _ -> assert false) brs in
+
(* 7j *)
+ (* FIXME: shouldn't the result of expansion be used? *)
let check_brs =
expand_branch_vars masks playout_terms
~freshen_unfixed:(Aux.Left false)
@@ -1971,7 +2215,7 @@
("GDL.translate_game: expanding variables resulting in "^
"duplicating Toss rules not implemented yet");
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "Filtered-branches:\n%s\n%!"
(exp_def_str ("filtered",
List.map (fun (next_arg,body,neg_body) ->
@@ -1994,7 +2238,7 @@
) Terms.empty brs in
let pos_state_terms = Terms.elements pos_state_terms in
(* {{{ log entry *)
- if !debug_level > 2 then (
+ if !debug_level > 4 then (
Printf.printf "pos_state_terms: %s\n%!"
(String.concat ", " (List.map term_str pos_state_terms))
);
@@ -2022,10 +2266,10 @@
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_vars then []
- else
- let phi = Formula.Rel (rname, [|svar|]) in
- [phi] in
+ (* if List.mem svar !constrained_vars then [] *)
+ (* else *)
+ let phi = Formula.Rel (rname, [|svar|]) in
+ [phi] in
let conjs =
Aux.concat_map (fun (rel, args as fact) ->
if rel = "true" then
@@ -2041,8 +2285,9 @@
| v, t as v_sb ->
let rname = term_to_name (subst_one v_sb mask) in
Some (Formula.Rel (rname, [|svar|]))) sb in
- if conjs <> [] || List.mem svar !constrained_vars
- then conjs else [phi]
+ phi::conjs
+ (*if conjs <> [] || List.mem svar !constrained_vars
+ then conjs else [phi] *)
else if List.mem rel static_rnames then
(* 7i-4a *)
pos_conjs_4a pos_state_subterms fact
@@ -2063,6 +2308,7 @@
(pos_conjs_4a pos_state_subterms fact)
else if rel = "distinct" then
(* 7i0 *)
+ (* TODO! *)
if Aux.not_unique args then [Formula.Or []]
else []
else (
@@ -2106,6 +2352,7 @@
then []
else if rel = "distinct" then
(* 7i0 *)
+ (* TODO! *)
if Aux.not_unique args then [Formula.Or []]
else []
else (
@@ -2113,6 +2360,36 @@
(* dynamic relations have been expanded *)
assert false)
) body in
+ let pos_of_neg_conjs =
+ Aux.concat_map (function
+ | _, [rel, args (* as fact *)] ->
+ if rel = "true" && !mask_anchors_of_neg = Positive_anch
+ then
+ (* 7i-4c *)
+ let true_arg = List.hd args in
+ let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
+ let rname = term_to_name mask in
+ let _, svar = toss_var masks true_arg in
+ [Formula.Rel (rname, [|svar|])]
+ else []
+ (* FIXME: is the rest handled properly as [neg_conjs]? *)
+ (*if rel = "true" || rel = "_DOES_PLACEHOLDER_"
+ then []
+ else if List.mem rel static_rnames then
+ (* 7i-4a *)
+ List.map (fun c -> Formula.Not c)
+ (pos_conjs_4a pos_state_subterms fact)
+ else if rel = "distinct" then
+ (* 7i0 *)
+ (* TODO! *)
+ if Aux.not_unique args then [Formula.Or []]
+ else []
+ else (
+ (* dynamic relations have been expanded *)
+ Printf.printf
+ "translate_game: (7i) unexpected dynamic %s\n%!" rel;
+ assert false)*)
+ | _ -> []) neg_body in
let neg_conjs =
Aux.map_some (fun (local_vs, neg_conjs) ->
(* 7k-4a-1 *)
@@ -2170,6 +2447,8 @@
| Pairs_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
) neg_path_subterms in
@@ -2205,7 +2484,9 @@
Formula.Rel (rname, [|svar|])) m_sb in
let conjs =
conjs_4b @ conjs_4c @ conjs_5 in
- if conjs = [] then [phi] else conjs
+ if conjs = [] && !mask_anchors_of_neg = Negative_anch
+ then [phi]
+ else conjs
else if rel = "_DOES_PLACEHOLDER_"
then []
else if List.mem rel static_rnames then
@@ -2223,6 +2504,7 @@
conjs_4a_2 @ conjs_4a_3
else if rel = "distinct" then
(* 7i0 *)
+ (* TODO! *)
if Aux.not_unique args then [Formula.Or []]
else []
else (
@@ -2241,7 +2523,8 @@
else Formula.Not (Formula.Ex (
(uni_toss_vars :> Formula.var list), phi))) res
) neg_body in
- let all_conjs = !static_conjs @ dyn_conjs @ neg_conjs in
+ let all_conjs =
+ !static_conjs @ dyn_conjs @ pos_of_neg_conjs @ neg_conjs in
(rhs_pos_preds, !static_conjs, all_conjs),
(next_arg, body, neg_body)) brs in
pconjs_4b, brs
@@ -2373,7 +2656,9 @@
let static_rules, exp_static_rules =
List.partition (fun ((rel,args), _, _) ->
List.length args <= !expand_arity_above ||
- List.exists (function ((r,_),[],[]) when rel=r-> true
+ List.exists (function
+ | ((r,_),[],[]) when rel=r-> true
+ | ((r,_),body,_) when rel=r && List.mem_assoc r body-> true
| _ -> false) static_rules
) static_rules in
(* {{{ log entry *)
@@ -2385,6 +2670,7 @@
let static_exp_defs = expand_def_rules exp_static_rules in
let static_rules = Aux.unique_sorted
(List.map Aux.fst3 static_rules) in
+ let static_rnames = List.map fst static_rules in
let exp_defs =
expand_def_rules ~more_defs:static_exp_defs dynamic_rules in
@@ -2399,18 +2685,33 @@
let next_rules = List.assoc "next" exp_defs in
let terminal_rules = List.assoc "terminal" exp_defs in
let goal_rules = List.assoc "goal" exp_defs in
+ let legal_rules =
+ Aux.concat_map (function [Const _; _], _, _ as lrule -> [lrule]
+ | [Var v; lterm], body, neg_body ->
+ Array.to_list
+ (Array.map (fun player ->
+ let sb = [v, player] in
+ [player; subst sb lterm],
+ subst_rels sb body,
+ List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body)
+ player_terms)
+ | [Func _; lterm], _, _ ->
+ (* TODO: easy to fix *)
+ failwith "GDL.translate_game: bigger player terms not handled yet"
+ | _ -> assert false) legal_rules in
(* 3b *)
let exp_next = subst_legal_rules legal_rules next_rules in
-
(* {{{ log entry *)
if !debug_level > 0 then (
Printf.printf "translate_game: \"next\" rules with \"does\"<-\"legal\":\n%s\n%!"
- (exp_def_str ("next", exp_next))
+ (exp_def_str ("next", List.map snd exp_next))
);
(* }}} *)
(* 3c *)
- let masks = List.map (function
- | [next_arg], body, neg_body ->
+ (* [remove_orig]: branches with "nasty" fluents, ignoring them
+ (assuming they are nonerasing frame branches) *)
+ let remove_orig, masks = Aux.partition_map (function
+ | orig_br, ([next_arg], body, neg_body) ->
let collect = Aux.map_some
(function "true", [arg] -> Some arg
| "true", _ -> raise
@@ -2423,22 +2724,33 @@
let pos_gens = List.map (generalize next_arg) pos_cands in
let neg_gens = List.map (generalize next_arg) neg_cands in
(* using the fact that Pervasives.compare is lexicographic *)
- let pos_gen = List.fold_left max ((-1,0),0,Const "") pos_gens in
- let neg_gen = List.fold_left max ((-1,0),0,Const "") neg_gens in
- let (_, fresh_count, mask as gen) = max pos_gen neg_gen in
- if gen == pos_gen then mask
- else abstract_consts fresh_count mask
+ let pos_gen = List.fold_left max ((-1,0),0,[],Const "") pos_gens in
+ let neg_gen = List.fold_left max ((-1,0),0,[],Const "") neg_gens in
+ let (_, fresh_count, mism, mask as gen) = max pos_gen neg_gen in
+ (* 3c3 *)
+ if !nonerasing_frame_wave &&
+ List.exists (function Var _, _ -> true | _ -> false) mism
+ then Aux.Left orig_br
+ else if gen == pos_gen then Aux.Right mask
+ (* 3c2 *)
+ else Aux.Right (abstract_consts fresh_count mask)
| _ -> raise
(Lexer.Parsing_error
("GDL.initialize_game: invalid arity of \"next\" atom")))
exp_next in
+ (* exp_next is not used anymore *)
+ (* 3c3 *)
+ let next_rules = Aux.list_diff next_rules remove_orig in
(* {{{ log entry *)
if !debug_level > 1 then (
Printf.printf "translate_game: Generalized element terms (mask candidates):\n%s\n%!"
- (String.concat " " (List.map term_str masks))
+ (String.concat " " (List.map term_str masks));
+ Printf.printf "translate_game: removing \"next\" rules:\n%s\nfiltered \"next\" rules:\n%s\n%!"
+ (exp_def_str ("next", remove_orig)) (exp_def_str ("next", next_rules))
);
(* }}} *)
(* find minimal *)
+ (* TODO: generalize more, like in the paper *)
let masks = Aux.maximal (fun t1 t2->cmp_masks t2 t1) masks in
(* {{{ log entry *)
if !debug_level > 1 then (
@@ -2453,7 +2765,10 @@
Aux.map_try (fun mask ->
mask, match_meta [] [] [term] [mask]) masks
with [mask, (sb, m_sb)] -> mask, sb, m_sb
- | _ -> assert false in (* masks are minimal *)
+ | cur_masks ->
+ Printf.printf "conflicting masks: %s for %s\n%!"
+ (terms_str (List.map fst cur_masks)) (term_str term);
+ assert false in (* masks are minimal *)
let sbs, elements =
try Aux.pop_assoc mask elements
with Not_found -> [], elements in
@@ -2647,20 +2962,6 @@
List.map (fun (path, subts) -> path, Aux.unique_sorted subts)
(Aux.collect dyn_rels) in
(* 7a *)
- let legal_rules =
- Aux.concat_map (function [Const _; _], _, _ as lrule -> [lrule]
- | [Var v; lterm], body, neg_body ->
- Array.to_list
- (Array.map (fun player ->
- let sb = [v, player] in
- [player; subst sb lterm],
- subst_rels sb body,
- List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body)
- player_terms)
- | [Func _; lterm], _, _ ->
- (* TODO: easy to fix *)
- failwith "GDL.translate_game: bigger player terms not handled yet"
- | _ -> assert false) legal_rules in
(* expanded "next" branches indexed by locations, then "legal"
branches, then by MGUs for unifier equivalence classes *)
let loc_lead_legal, loc_noop_legal =
@@ -2705,7 +3006,7 @@
if ply mod loc_n = i then
loc_actions := actions @ !loc_actions) agg_actions;
(* {{{ log entry *)
- if !debug_level > 4 then (
+ if !debug_level > 3 then (
Printf.printf "Possible actions in location %d:\n%s\n%!"
i (String.concat "; "
(List.map (fun a -> term_str (Func ("legal", a))) !loc_actions))
@@ -2771,13 +3072,33 @@
(* now, continue with the lead player *)
let unifs = Aux.map_some (* and substituted legal br-es *)
(fun next_br ->
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "matching-next-legal:\n%s\n%!"
+ (exp_def_str ("orig-br", [next_br]))
+ );
+ (* }}} *)
match
subst_legal_rule lead_legal (freshen_branch next_br)
with None -> None
| Some (([_; lead],lead_body,lead_neg_body), br) ->
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "matching-next-legal-result:\n%s\n%!"
+ (exp_def_str ("matched-br", [br]))
+ );
+ (* }}} *)
Some ((lead,lead_body,lead_neg_body), br)
| _ -> assert false)
next_rules in
+ (* {{{ log entry *)
+ if !debug_level > 1 then (
+ Printf.printf
+ "Rule precursors for loc %d:\nprecursor-branches:\n%s\n%!"
+ loc (exp_def_str ("precursor", List.map snd unifs));
+ );
+ (* }}} *)
+
(* building "Hasse layers" imperatively *)
let unifs = ref unifs in
let hasse_layer () =
@@ -2817,6 +3138,13 @@
let rules_brs =
List.map (fun ((lead_head, lead_body, lead_neg_body),
branches) ->
+ let branches =
+ expand_branch_vars masks element_terms
+ (* ~freshen_unfixed:(Aux.Right fixed_vars) *)
+ (* ~freshen_unfixed:(Aux.Left true) *)
+ ~freshen_unfixed:(Aux.Left false)
+ branches in
+ let branches = List.map snd branches in
let lead_does =
"_DOES_PLACEHOLDER_", [loc_players.(loc); lead_head] in
let lead_body = lead_does::lead_body in
@@ -2826,6 +3154,7 @@
| [next_arg],_,_ ->
Aux.Strings.subset (term_vars next_arg) fixed_vars
| _ -> assert false) branches in
+ (* TODO: see (7f1) TODO *)
let frame_brs, to_expand = List.partition
(function
| [next_arg],_,_ ->
@@ -2838,14 +3167,11 @@
List.exists
(fun (rel, r_args) -> rel="true" && r_args=args) body
) frame_brs in
- let unfixed_brs =
+ (* FIXME: it's called expanded because initially unfixed
+ variables (outside frame branches) were eliminated --
+ clean up *)
+ let expanded_brs =
to_expand @ more_to_expand in
- (* 7g *)
- let expanded_brs =
- expand_branch_vars masks element_terms
- ~freshen_unfixed:(Aux.Right (Aux.Strings.elements fixed_vars))
- unfixed_brs in
- let expanded_brs = List.map snd expanded_brs in
(* 7f2 *)
let leq3 (head1, _, _) (head2, _, _) =
try
@@ -2859,7 +3185,7 @@
List.filter (fun cl->leq3 cl repr) frame_brs)
frame_brs) in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "frames: heads partitioning =\n%s\n%!"
(String.concat "\n"
(List.map (fun l ->
@@ -2887,7 +3213,7 @@
repr_head, multi_body
) frames in
(* {{{ log entry *)
- if !debug_level > 2 then (
+ if !debug_level > 4 then (
Printf.printf "frames: heads = %s\n%!"
(String.concat ", " (List.map (function [h],_ ->term_str h
| _ -> assert false) frames))
@@ -2901,11 +3227,11 @@
| [next_arg] as next_args,multi_body ->
let mask, _, _, blank_arg = term_to_blank masks next_arg in
(* {{{ log entry *)
- if !debug_level > 2 then (
+ if !debug_level > 4 then (
Printf.printf "Blanking-out of %s by %s\n%!"
(term_str next_arg) (term_str mask)
);
- if !debug_level > 2 then (
+ if !debug_level > 4 then (
Printf.printf "Frame multibody:\n%s\n%!"
( String.concat "\n" (List.map (
fun (body, neg_body) ->
@@ -2922,7 +3248,8 @@
then Some (Aux.Left (rel, args))
else None) body in
let neg_body =
- List.map
+ (* we drop failed equality from the disjuction *)
+ Aux.map_try
(function
| _, ["distinct", []] -> assert false
| _, ["distinct", arg::more_args] ->
@@ -2943,9 +3270,21 @@
| _, conj ->
Aux.Right (Aux.Left conj))
neg_body in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "body length = %d; neg_body length = %d\n%!"
+ (List.length body) (List.length neg_body)
+ );
+ (* }}} *)
body @ neg_body) multi_body in
let erasures = List.map Aux.partition_choice
(Aux.unique_sorted (Aux.product multi_body)) in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "initial erasures length = %d\n%!"
+ (List.length erasures)
+ );
+ (* }}} *)
let erasures =
Aux.map_some (fun (neg_body, body) ->
try
@@ -2994,99 +3333,228 @@
Some ([head], lead_body @ body,
lead_neg_body @ neg_body)
(*or not
- Some ([head], body, neg_body)*)
+ Some ([head], body, neg_body)*)
)
- else None
+ else (
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "unsatisfiable-erasure:\n%s\n%s\n%!"
+ (lit_def_str ("erasure", [
+ [head], body, neg_body]))
+ (exp_def_str ("lead", [
+ [lead_head], lead_body, lead_neg_body]))
+ );
+ (* }}} *)
+ None)
with Not_found -> None) erasures in
let erasures = Aux.unique_sorted
(List.map (fun (head, body, neg_body) ->
head, Aux.unique_sorted body,
Aux.unique_sorted neg_body) erasures) in
+ ...
[truncated message content] |
