[Toss-devel-svn] SF.net SVN: toss:[1355] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1355] trunk/Toss
|
From: <luk...@us...> - 2011-03-12 19:24:46
|
Revision: 1355
http://toss.svn.sourceforge.net/toss/?rev=1355&view=rev
Author: lukstafi
Date: 2011-03-12 19:24:32 +0000 (Sat, 12 Mar 2011)
Log Message:
-----------
TossFullTest: new test modules, put module tests together. DiscreteRule: remember which LHS tuples required to be absent (useful for analysis); fixes in rule-from-precondition generation. FormulaOps: new partial simplification functions. GGP/tests: targets for GDL translation and GameSimpl simplification tests. GDL translation: much better branch pruning, fixes in erasure branch generation. GameSimpl: specification; removing redundant equivalent relations (still broken effect on rule LHS structures). Various modules: helper functions.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/Arena.mli
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/ContinuousRule.mli
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Arena/DiscreteRule.mli
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/GDLTest.ml
trunk/Toss/GGP/examples/breakthrough.gdl
trunk/Toss/Server/ServerGDLTest.in
trunk/Toss/TossFullTest.ml
trunk/Toss/TossTest.ml
Added Paths:
-----------
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/GGP/GameSimpl.mli
trunk/Toss/GGP/GameSimplTest.ml
trunk/Toss/GGP/tests/
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
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/Arena.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -377,6 +377,20 @@
} in
(game, state), player
+let map_to_formulas f game =
+ {game with
+ rules = List.map (fun (rn, r) ->
+ rn, ContinuousRule.map_to_formulas f r
+ ) game.rules;
+ graph = Array.map (fun loc ->
+ {loc with
+ payoffs =
+ Array.map (FormulaOps.map_to_formulas_expr f) loc.payoffs;
+ }) game.graph;
+ defined_rels = List.map (fun (drel, (args, def)) ->
+ drel, (args, f def)) game.defined_rels;
+ }
+
(* ------------------ REQUESTS TO THE ARENA USED IN OPERATION --------------- *)
(* Location of a structure: either arena or left or right-hand side of a rule *)
Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/Arena.mli 2011-03-12 19:24:32 UTC (rev 1355)
@@ -108,6 +108,8 @@
val process_definition :
?extend_state:game * game_state -> definition list -> game * game_state
+val map_to_formulas : (Formula.formula -> Formula.formula) -> game -> game
+
(** ------------------ REQUESTS TO THE ARENA USED IN OPERATION --------------- *)
(** Location of a structure: either arena or left or right-hand side of a rule *)
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/ContinuousRule.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -41,7 +41,7 @@
-(* ------------------ APPLYING FUNCTIONS TO SIDE STRUCTURES ----------------- *)
+(* ------------------ APPLYING FUNCTIONS TO PARTS OF A RULE ----------------- *)
(* Apply [f] to left (if [to_left]) or right side of the given named rule.
Return the new rule and an additional result which [f] returns. *)
@@ -59,6 +59,16 @@
let lhs r = r.discrete.DiscreteRule.lhs_struc
let rhs r = r.discrete.DiscreteRule.rhs_struc
+let map_to_formulas f r =
+ {r with
+ discrete = {r.discrete with DiscreteRule.pre =
+ f r.discrete.DiscreteRule.pre};
+ compiled = {r.compiled with DiscreteRule.lhs_form =
+ f r.compiled.DiscreteRule.lhs_form};
+ inv = f r.inv;
+ post = f r.post;
+ }
+
(* ---------------------- FINDING APPLICABLE MATCHES ------------------------ *)
(* Find all matches of [r] in [struc] which satisfy [r]'s precondition. *)
Modified: trunk/Toss/Arena/ContinuousRule.mli
===================================================================
--- trunk/Toss/Arena/ContinuousRule.mli 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/ContinuousRule.mli 2011-03-12 19:24:32 UTC (rev 1355)
@@ -54,8 +54,8 @@
val lhs : rule -> Structure.structure
val rhs : rule -> Structure.structure
+val map_to_formulas : (Formula.formula -> Formula.formula) -> rule -> rule
-
(** {2 Finding applicable matches} *)
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/DiscreteRule.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -35,6 +35,10 @@
lhs_elem_names : elem_names;
lhs_elem_inv_names : elem_inv_names;
lhs_elem_vars : string list;
+ lhs_neg_tups : (string * int array list) list;
+ (* Tuples of relations over the LHS structure elements that are
+ required to be absent for embedding; this is "meta-data" not
+ needed for matching and rewriting but useful for other purposes. *)
lhs_form : Formula.formula;
(* gets instantiated in the model *)
(* the precondition [pre] is compiled as part of [lhs_form] *)
@@ -558,21 +562,6 @@
let signat = List.filter (fun (rel,_) ->
special_rel_of rel = None &&
not (List.mem_assoc rel defined_rels)) signat in
- let expand_def_rels rel =
- if List.mem_assoc rel defined_rels then
- let args, rphi = List.assoc rel defined_rels in
- List.map fst (List.filter (fun (rel, ar) ->
- let selector = Structure.free_for_rel rel ar in
- let res = Solver.M.check selector rphi in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "compile_rule.expand_def_rels: %s on %s = %b\n%!"
- rel (Structure.str selector) res
- );
- (* }}} *)
- res
- ) signat)
- else [rel] in
let expand_defrel_tups (drel, tups) =
if List.mem_assoc drel defined_rels
then
@@ -613,7 +602,23 @@
else [drel, tups] in
(* expand defined rels in embedding list *)
let base_emb_rels =
- unique (=) (concat_map expand_def_rels rule_src.emb_rels) in
+ let expand_def_rels rel =
+ if List.mem_assoc rel defined_rels then
+ let args, rphi = List.assoc rel defined_rels in
+ List.map fst (List.filter (fun (rel, ar) ->
+ let selector = Structure.free_for_rel rel ar in
+ let res = Solver.M.check selector rphi in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "compile_rule.expand_def_rels: %s on %s = %b\n%!"
+ rel (Structure.str selector) res
+ );
+ (* }}} *)
+ res
+ ) signat)
+ else [rel] in
+ unique(*_sorted *) (=)
+ (concat_map expand_def_rels rule_src.emb_rels) in
(* {{{ log entry *)
if !debug_level > 1 then (
Printf.printf "compile_rule: emb=%s -- base_emb_rels=%s\n%!"
@@ -723,8 +728,8 @@
let lhs_opt_rels, lhs_pos_tups, lhs_pos_expanded =
compile_opt_rels lhs_rels in
let lhs_all_tups n =
- List.map Array.of_list (Aux.product
- (Aux.fold_n (fun acc -> lhs_elems::acc) [] n)) in
+ List.map Array.of_list (Aux.product (
+ Aux.fold_n (fun acc -> lhs_elems::acc) [] n)) in
(*
let lhs_all_tups n =
List.fold_left (fun tups tup -> STups.add tup tups)
@@ -818,8 +823,8 @@
) tups)
rhs_rels in
let rhs_all_tups n =
- List.map Array.of_list (Aux.product
- (Aux.fold_n (fun acc -> rhs_elems::acc) [] n)) in
+ List.map Array.of_list (Aux.product (
+ Aux.fold_n (fun acc -> rhs_elems::acc) [] n)) in
(* a tuple is negative when it has to be removed: it is in $\tau_e$
and in the LHS, but it does not occur on the RHS even optionally *)
let rhs_neg_tuples =
@@ -861,6 +866,7 @@
lhs_elem_names = lhs_elem_names;
lhs_elem_inv_names = lhs_elem_inv_names;
lhs_elem_vars = lhs_elem_vars;
+ lhs_neg_tups = lhs_neg_tups;
lhs_form = emb;
rhs_elem_names = rule_src.rhs_struc.Structure.names;
rhs_elem_vars = rhs_elem_vars;
@@ -887,26 +893,32 @@
(* Build a rule by translating the "add" list into the RHS structure
directly, and separating out from a precondition the LHS structure
- over the [struc_vars] variables. All relations are
- considered embedded. (Obviously, not all rules can be generated in
- this way.) *)
-let translate_from_precond ~precond ~add ~embed ~struc_elems =
+ over the [struc_vars] variables. Only and all the [emb_rels] relations
+ are embedded (usually the fluents). (Not all rules can be generated
+ using this function.) Caution: simplifies the precondition.
+
+ The partition of embedded relations into positive and negative
+ tuples (literals) is extracted from the precondition. If the
+ partition does not cover all tuples, fail. *)
+let translate_from_precond ~precond ~add ~emb_rels ~signat ~struc_elems =
let rhs_names = Aux.unique_sorted
(Aux.concat_map (fun (_,arg) -> Array.to_list arg) add) in
assert (Aux.list_diff rhs_names struc_elems = []);
let rewritable args =
Aux.array_for_all (fun v -> List.mem (Formula.var_str v) struc_elems)
args in
- let conjs = FormulaOps.flatten_ands precond in
- let literals, conjs = Aux.partition_map (function
+ let conjs =
+ FormulaOps.flatten_ands (FormulaOps.remove_redundant precond) in
+ let posi, conjs = Aux.partition_map (function
| Formula.Rel (rel, args) when rewritable args ->
- Left (Left (rel,args))
- | Not (Formula.Rel (rel, args)) when rewritable args ->
- Left (Right (rel,args))
+ Left (rel,args)
| phi -> Right phi) conjs in
- let posi, nega = Aux.partition_choice literals in
- (* FIXME: TODO: check and at least warn when [nega] is smaller than
- the complement of [posi] over embedded rels *)
+ let nega, conjs = Aux.partition_map (function
+ | Formula.Not (Formula.Rel (rel, args))
+ when List.mem rel emb_rels && rewritable args ->
+ Left (rel,args)
+ | phi -> Right phi) conjs in
+ let lhs_extracted = posi @ nega in
let precond = Formula.And conjs in
let fvars = FormulaOps.free_vars precond in
let local_vars =
@@ -915,12 +927,39 @@
let precond =
if local_vars = [] then precond
else Formula.Ex (local_vars, precond) in
- let emb_rels = Aux.list_inter embed
- (Aux.unique_sorted
- (List.map fst add @ List.map fst (posi @ nega))) in
let posi_s =
List.map (fun (rel, args) -> rel, Array.map Formula.var_str args)
posi in
+ let opt_s =
+ Aux.concat_map (fun rel ->
+ try
+ let arity = signat rel in
+ let tups =
+ List.map
+ Array.of_list
+ (*Aux.array_map_of_list Formula.var_str*)
+ (Aux.product (
+ Aux.fold_n (fun acc -> struc_elems::acc) [] arity)) in
+ let extracted =
+ List.map (Array.map Formula.var_str)
+ (Aux.assoc_all rel lhs_extracted) in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "translate_from_precond: _opt_%s -- extracted %s -- \
+ remaining %s\n%!" rel
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args)) extracted))
+ (String.concat "; "
+ (List.map (fun args ->
+ String.concat " " (Array.to_list args))
+ (Aux.list_diff tups extracted)))
+ );
+ (* }}} *)
+ let tups = Aux.list_diff tups extracted in
+ List.map (fun args -> "_opt_"^rel, args) tups
+ with Not_found -> [])
+ emb_rels in
let rhs_struc, struc_elems =
List.fold_left (fun (rhs_struc, struc_elems) name ->
let rhs_struc, elem =
@@ -933,7 +972,7 @@
let lhs_struc = rhs_struc in
let rhs_struc = add_rels rhs_struc add in
let lhs_struc = add_rels lhs_struc posi_s in
- (* no relations are optional, righ? *)
+ let lhs_struc = add_rels lhs_struc opt_s in
{
lhs_struc = lhs_struc;
rhs_struc = rhs_struc;
@@ -942,6 +981,7 @@
pre = precond;
}
+
(** {2 Printing and parsing.} *)
let matching_str matching =
Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Arena/DiscreteRule.mli 2011-03-12 19:24:32 UTC (rev 1355)
@@ -30,14 +30,19 @@
lhs_elem_names : elem_names;
lhs_elem_inv_names : elem_inv_names;
lhs_elem_vars : string list;
+ lhs_neg_tups : (string * int array list) list;
+ (** Tuples of relations over the LHS structure elements that are
+ required to be absent for embedding; this is "meta-data" not
+ needed for matching and rewriting but useful for other
+ purposes. *)
lhs_form : Formula.formula;
- (* gets instantiated in the model *)
- (* the precondition [pre] is compiled as part of [lhs_form] *)
+ (** gets instantiated in the model *)
+ (** the precondition [pre] is compiled as part of [lhs_form] *)
rhs_elem_names : elem_names;
- rhs_elem_vars : string list; (* replaces the embedding *)
- rhs_pos_tuples : (string * var_tuples) list; (* gets added *)
- rhs_neg_tuples : (string * var_tuples) list; (* gets removed *)
- rlmap : (string * string) list option; (* rule_s on variables (?) *)
+ rhs_elem_vars : string list; (** replaces the embedding *)
+ rhs_pos_tuples : (string * var_tuples) list; (** gets added *)
+ rhs_neg_tuples : (string * var_tuples) list; (** gets removed *)
+ rlmap : (string * string) list option; (** rule_s on variables *)
}
val elemvar_of_elem : elem_inv_names -> int -> string
@@ -113,9 +118,21 @@
val changeable_rels : rule_obj list -> string list
+(** Build a rule by translating the "add" list into the RHS structure
+ directly, and separating out from a precondition the LHS structure
+ over the [struc_vars] variables. Only and all the [emb_rels]
+ relations are embedded (usually the fluents). (Not all rules can be
+ generated using this function.) Caution: simplifies the
+ precondition.
+
+ The partition of embedded relations into positive and negative
+ tuples (literals) is extracted from the precondition. If the
+ partition does not cover all tuples, fail. *)
val translate_from_precond :
precond:Formula.formula -> add:(string * string array) list ->
- embed:string list -> struc_elems:string list -> rule
+ (* del:(string * string array) list -> *)
+ emb_rels:string list -> signat:(string -> int) ->
+ struc_elems:string list -> rule
(** {2 Printing.} *)
val matching_str : matching -> string
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Formula/Aux.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -36,6 +36,14 @@
let intmap_filter p m =
IntMap.fold (fun k v acc -> if p k v then (k,v)::acc else acc) m []
+let int_pow x n =
+ let rec aux acc res n =
+ if n = 0 then res
+ else if n mod 2 = 0 then aux (acc*acc) res (n/2)
+ else aux (acc*acc) (res*acc) (n/2) in
+ if n < 0 then 0
+ else aux x 1 n
+
let is_digit c =
(c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') ||
(c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9')
@@ -44,6 +52,12 @@
let snd3 (_,a,_) = a
let trd3 (_,_,a) = a
+module BasicOperators = struct
+ let (-|) f g x = f (g x)
+end
+
+open BasicOperators
+
(* {2 Helper functions on lists and other functions lacking from the
standard library.} *)
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Formula/Aux.mli 2011-03-12 19:24:32 UTC (rev 1355)
@@ -21,6 +21,14 @@
val intmap_filter :
(int -> 'a -> bool) -> 'a IntMap.t -> (int * 'a) list
+module BasicOperators :
+sig
+ (** Function composition. *)
+ val ( -| ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+end
+
+val int_pow : int -> int -> int
+
val is_digit : char -> bool
val fst3 : 'a * 'b * 'c -> 'a
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Formula/FormulaOps.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -142,7 +142,19 @@
| Sum (vs, phi, r) ->
Sum (vs, map_to_literals f g phi, map_to_literals_expr f g r)
+(* Map [f] to top-level formulas in the real expression ([Char]s and
+ [Sum] guards). *)
+let rec map_to_formulas_expr f = function
+ | RVar _ | Const _ | Fun _ as x -> x
+ | Times (r1, r2) ->
+ Times (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
+ | Plus (r1, r2) ->
+ Plus (map_to_formulas_expr f r1, map_to_formulas_expr f r2)
+ | Char (phi) -> Char (f phi)
+ | Sum (vs, phi, r) ->
+ Sum (vs, f phi, map_to_formulas_expr f r)
+
(* Map [f] to all atoms in the given formula. *)
let map_to_atoms_full f g phi =
map_to_literals (function Not (x) -> Not (f x) | x -> f x) g phi
@@ -673,12 +685,62 @@
| Not phi -> Not (flatten_formula phi)
| (Rel _ | Eq _ | In _ | RealExpr _) as atom -> atom
-(* Formula as a list of conjuncts. *)
+let rec flatten_ors = function
+ | Or disjs -> Aux.concat_map flatten_ors disjs
+ | phi -> [phi]
+
+(* Formula as a list of conjuncts, with one level of distributing
+ negation over disjunction and pushing quantifiers inside. *)
let rec flatten_ands = function
- | Formula.And conjs -> Aux.concat_map flatten_ands conjs
+ | And conjs -> Aux.concat_map flatten_ands conjs
+ | Not (Or disjs) ->
+ List.map (fun d -> Not d)
+ (Aux.concat_map flatten_ors disjs)
+ | All (vs, phi) ->
+ List.map (fun phi -> All (vs, phi)) (flatten_ands phi)
+ | Ex (vs, phi) as arg ->
+ (match flatten_ands phi with
+ | [] -> [] | [_] -> [arg]
+ | conjs ->
+ let free_conjs, bound_conjs = List.partition (fun conj ->
+ Aux.list_inter vs (free_vars conj) = []) conjs in
+ let bound_phi = match bound_conjs with
+ | [phi] -> phi | _ -> And bound_conjs in
+ free_conjs @ [Ex (vs, bound_phi)])
| phi -> [phi]
+(* Remove literals from disjunctions in positive positions
+ (conjunctions in negative positions) that already occur conjoined
+ to the disjucntion. (Does not descend the real part currently.) *)
+let remove_redundant phi =
+ let rec aux base neg = function
+ | And conjs when not neg ->
+ let more_base, subtasks = List.partition (function
+ | Rel _ | Not (Rel _) -> true | _ -> false) conjs in
+ And (more_base @ List.map (aux (more_base @ base) neg) subtasks)
+ | Or conjs when neg ->
+ let more_base, subtasks = List.partition (function
+ | Rel _ | Not (Rel _) -> true | _ -> false) conjs in
+ Or (more_base @ List.map (aux (more_base @ base) neg) subtasks)
+ | Or disjs (* when not neg *) ->
+ let literals, subtasks = List.partition (function
+ | Rel _ | Not (Rel _) -> true | _ -> false) disjs in
+ let disjs =
+ Aux.list_diff literals base @ List.map (aux base neg) subtasks in
+ (match disjs with [disj] -> disj | _ -> Or disjs)
+ | And disjs (* when neg *) ->
+ let literals, subtasks = List.partition (function
+ | Rel _ | Not (Rel _) -> true | _ -> false) disjs in
+ let disjs =
+ Aux.list_diff literals base @ List.map (aux base neg) subtasks in
+ (match disjs with [disj] -> disj | _ -> And disjs)
+ | Not phi -> Not (aux base (not neg) phi)
+ | Ex (vs, phi) -> Ex (vs, aux base neg phi)
+ | All (vs, phi) -> All (vs, aux base neg phi)
+ | phi -> phi in
+ aux [] false (flatten_formula phi)
+
(* Compute size of a formula (currently w/o descending the real part). *)
let rec size = function
| Or js | And js -> List.fold_left (+) 1 (List.map size js)
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/Formula/FormulaOps.mli 2011-03-12 19:24:32 UTC (rev 1355)
@@ -26,6 +26,10 @@
val map_to_literals_expr : (formula -> formula) -> (real_expr -> real_expr) ->
real_expr -> real_expr
+(** Map [f] to top-level formulas in the real expression ([Char]s and
+ [Sum] guards). *)
+val map_to_formulas_expr : (formula -> formula) -> real_expr -> real_expr
+
(** Map [f] to all atoms in the given formula. *)
val map_to_atoms_full : (formula -> formula) -> (real_expr -> real_expr) ->
formula -> formula
@@ -84,9 +88,15 @@
(** Flatten "and"s and "or"s in a formula -- i.e. associativity. *)
val flatten_formula : formula -> formula
-(** Formula as a list of conjuncts. *)
+(** Formula as a list of conjuncts, with one level of distributing
+ negation over disjunction and pushing quantifiers inside. *)
val flatten_ands : formula -> formula list
+(** Remove literals from disjunctions in positive positions
+ (conjunctions in negative positions) that already occur conjoined
+ to the disjucntion. (Does not descend the real part currently.) *)
+val remove_redundant : formula -> formula
+
(** Compute size of a formula (currently w/o descending the real part). *)
val size : formula -> int
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/GGP/GDL.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -320,21 +320,17 @@
negated subformulas are "let free").
(7f4) Drop the erasure branches that contradict the "legal"
- condition of their rule.
+ 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).
- (7g) Instantiate remaining unfixed variables. Implementation TODO.
+ (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.)
- (7g1) 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.)
-
- (7g2) Then, add instantiations of frame rules for each case their
- head term unifies with one from all the non-frame rules.
-
(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
@@ -544,8 +540,10 @@
(** Generate all tuples for equivalences, to faciliate further
transformations of formulas in the game definition (outside of
translation). *)
-let equivalences_all_tuples = ref false
+let equivalences_all_tuples = ref false (* true *)
+open Aux.BasicOperators
+
type term =
| Const of string
| Var of string
@@ -1502,7 +1500,7 @@
if more_state = [] then static_rels, state_rels
else separate static (more_state @ state_rels) in
let static_rels, state_rels =
- separate (List.map (fun ((r,_),_,_)->r) rules)
+ separate (Aux.unique (=) (List.map (fun ((r,_),_,_)->r) rules))
["init"; "does"; "true"; "next"; "terminal"; "goal"] in
let static_rules, dynamic_rules = List.partition
(fun ((rel,_),_,_) -> List.mem rel static_rels) rules in
@@ -1707,32 +1705,7 @@
let translate_branches struc masks playout_terms static_rnames dyn_rels
(brs : exp_def_branch list) =
(* 7i *)
- 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 > 2 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_conjs_4a (rel, args) =
+ 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 *)
@@ -1760,7 +1733,8 @@
);
(* }}} *)
res in
- let neg_conjs_4a neg_state_terms neg_state_subterms (rel, args) =
+ 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
@@ -1785,18 +1759,9 @@
(* }}} *)
res in
(* 7i-4b *)
- 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
let constrained_vars = ref [] in
- let pos_conjs_4b =
- Aux.concat_map (fun ((mask, v), terms) ->
+ 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) ->
@@ -1817,9 +1782,8 @@
| v::vs -> List.map (fun w -> [|v; w|]) vs in
List.map (fun tup -> Formula.Rel (rname, tup)) tups
) terms
- ) pos_path_subterms in
- let pos_conjs_4b = Aux.unique_sorted pos_conjs_4b in
- let neg_conjs_4b nterm =
+ ) 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) ->
@@ -1839,25 +1803,65 @@
if !equivalences_all_tuples
then
Aux.concat_map
- (fun v -> [[|v; ntossvar|]; [|ntossvar; v|]]) tossvars
+ (fun v ->
+ if v = ntossvar then []
+ else [[|v; ntossvar|]; [|ntossvar; v|]]) tossvars
else
- List.map (fun v -> [|v; ntossvar|]) tossvars in
+ Aux.map_some (fun v ->
+ if v = ntossvar then None
+ else Some [|v; ntossvar|]) tossvars in
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 > 2 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 ->
- let phi, lvars =
- if next_arg = Const "_IGNORE_RHS_" then [], ref []
+ | [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_vars then [], ref []
+ if List.mem svar !constrained_vars then []
else
let phi = Formula.Rel (rname, [|svar|]) in
- let lvars = ref [svar] in
- [phi], lvars in
+ [phi] in
let conjs =
Aux.concat_map (fun (rel, args as fact) ->
if rel = "true" then
@@ -1866,7 +1870,6 @@
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
- lvars := svar :: !lvars;
let phi = Formula.Rel (rname, [|svar|]) in
let conjs =
Aux.map_some (function
@@ -1878,12 +1881,12 @@
then conjs else [phi]
else if List.mem rel static_rnames then
(* 7i-4a *)
- pos_conjs_4a fact
+ pos_conjs_4a pos_state_subterms fact
else []
) body in
- (* only to prune early -- we cannot get more than negated
- relations for positive elements, because stuff related to
- negative elements is under common negations/disjunctions *)
+ (* to prune early, we cannot get more than negated relations for
+ positive elements, because stuff related to negative elements
+ is under common negations/disjunctions *)
let neg_conjs =
Aux.concat_map (function
| _, [rel, args as fact] ->
@@ -1892,7 +1895,8 @@
then []
else if List.mem rel static_rnames then
(* 7i-4a *)
- List.map (fun c -> Formula.Not c) (pos_conjs_4a fact)
+ List.map (fun c -> Formula.Not c)
+ (pos_conjs_4a pos_state_subterms fact)
else if rel = "distinct" then
(* 7i0 *)
if Aux.not_unique args then [Formula.Or []]
@@ -1903,42 +1907,137 @@
"translate_game: (7i) unexpected dynamic %s\n%!" rel;
assert false)
| _ -> []) neg_body in
- let all_conjs = phi @ conjs @ neg_conjs in
+ let all_conjs = phi @ conjs @ pconjs_4b @ neg_conjs in
let phi = Formula.And all_conjs in
- let lvars = (!lvars :> Formula.var list) in
- let optim_conjs = List.filter (fun c->
- List.for_all (fun v->List.mem v lvars)
- (FormulaOps.free_vars c)) (pos_conjs_4b @ all_conjs) in
- let rphi = Formula.And optim_conjs in
+ let phi = Formula.Ex (FormulaOps.free_vars phi, phi) in
(* {{{ log entry *)
- if !debug_level > 4 then (
- Printf.printf "evaluating: %s\n%!"
+ if !debug_level > 3 then (
+ Printf.printf "evaluating:\nbranch=%s\nphi=%s\n%!"
+ (exp_def_str ("eval", [br]))
(Formula.str phi)
);
- (* }}} *)
- if Solver.M.check struc rphi
+ (* }}} *)
+ if Solver.M.check struc phi
then (
(* {{{ log entry *)
- if !debug_level > 4 then (
+ if !debug_level > 3 then (
Printf.printf "holds\n%!"
);
- (* }}} *)
- Some (all_conjs, (next_arg,body,neg_body)))
+ (* }}} *)
+ Some (next_arg,body,neg_body))
else None
| _ -> assert false) brs in
(* 7j *)
let check_brs =
expand_branch_vars masks playout_terms
~freshen_unfixed:(Aux.Left false)
- (List.map (fun (_,(head,body,neg_body))->
+ (List.map (fun (head,body,neg_body)->
[head], body, neg_body) brs) in
if List.exists (fun (sb,_)-> sb <> []) check_brs
then failwith
("GDL.translate_game: expanding variables resulting in "^
"duplicating Toss rules not implemented yet");
- (* 7k *)
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "Filtered-branches:\n%s\n%!"
+ (exp_def_str ("filtered",
+ List.map (fun (next_arg,body,neg_body) ->
+ [next_arg], body, neg_body) brs));
+ );
+ (* }}} *)
+
+ (* 7i and 7k *)
+ 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
+ ) Terms.empty brs in
+ let pos_state_terms = Terms.elements pos_state_terms in
+ (* {{{ log entry *)
+ if !debug_level > 2 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
+ let pconjs_4b = pos_conjs_4b pos_path_subterms in
let brs =
- List.map (fun (static_conjs, (next_arg,body,neg_body)) ->
+ List.map (fun (next_arg,body,neg_body) ->
+ 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_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
+ (* 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
+ let phi = Formula.Rel (rname, [|svar|]) in
+ let conjs =
+ Aux.map_some (function
+ | _, Var _ -> None
+ | 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]
+ else if List.mem rel static_rnames then
+ (* 7i-4a *)
+ pos_conjs_4a pos_state_subterms fact
+ else []
+ ) body in
+ (* to prune early, we cannot get more than negated relations for
+ positive elements, because stuff related to negative elements
+ is under common negations/disjunctions *)
+ let neg_conjs =
+ Aux.concat_map (function
+ | _, [rel, args as fact] ->
+ if rel = "true" then []
+ else if 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 *)
+ 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 rhs_pos_preds =
if next_arg = Const "_IGNORE_RHS_" then []
else
@@ -1952,7 +2051,7 @@
let rname = term_to_name (subst_one v_sb mask) in
Some (rname, [|rhs_elem|])
) m_sb in
- let static_conjs = ref static_conjs in
+ let static_conjs = ref (phi @ conjs @ neg_conjs) in
let dyn_conjs =
Aux.concat_map (fun (rel, args) ->
if rel = "true" then
@@ -1961,6 +2060,7 @@
let _, svar = toss_var masks true_arg in
let mask_rname = term_to_name mask in
let mask_phi = Formula.Rel (mask_rname, [|svar|]) in
+ (* the mask formula would be redundant *)
static_conjs := Aux.list_remove mask_phi !static_conjs;
Aux.map_some (fun (v,t as v_sb) ->
if t = Const "_BLANK_" then
@@ -2005,7 +2105,8 @@
Aux.concat_map
(fun (rel,_ as fact) ->
if rel <> "true" && List.mem rel static_rnames
- then neg_conjs_4a neg_state_terms neg_state_subterms fact
+ then neg_conjs_4a pos_state_subterms
+ neg_state_terms neg_state_subterms fact
else []) body in
(* 7k-4b *)
let neg_path_subterms =
@@ -2033,14 +2134,16 @@
if v=w then None else Some [|v; w|]) vars) vars
else
match vars with [] -> []
- | v::vs -> List.map (fun w -> [|v; w|]) vs in
+ | v::vs -> Aux.map_some (fun w ->
+ if v=w then None else Some [|v; w|]) vs in
List.map (fun tup -> Formula.Rel (rname, tup)) tups
) terms
) neg_path_subterms in
let negonly_conjs_4b = Aux.unique_sorted negonly_conjs_4b in
(* the mixed part *)
let mixed_conjs_4b =
- Aux.concat_map neg_conjs_4b neg_state_terml in
+ Aux.concat_map (neg_conjs_4b pos_path_subterms)
+ neg_state_terml in
let nconjs_4b = negonly_conjs_4b @ mixed_conjs_4b in
let disjs =
Aux.concat_map (fun (rel, args as fact) ->
@@ -2056,7 +2159,8 @@
| v, t as v_sb ->
let rname = term_to_name (subst_one v_sb mask) in
Some (Formula.Rel (rname, [|svar|]))) sb in
- let conjs_4b = neg_conjs_4b true_arg in
+ let conjs_4b =
+ neg_conjs_4b pos_path_subterms true_arg in
let conjs_5 =
List.map (fun (v,t as v_sb) ->
if t = Const "_BLANK_" then
@@ -2073,14 +2177,15 @@
else if List.mem rel static_rnames then
(* 7i-4a-2-3 *)
let conjs_4a_2 =
- match pos_conjs_4a fact with
+ match pos_conjs_4a pos_state_subterms fact with
| [] -> []
| [rel_conseq] -> [rel_conseq]
| rel_conseqs ->
(* negation turns it into a conjunction *)
[Formula.Or rel_conseqs] in
let conjs_4a_3 =
- neg_conjs_4a neg_state_terms neg_state_subterms fact in
+ neg_conjs_4a pos_state_subterms
+ neg_state_terms neg_state_subterms fact in
conjs_4a_2 @ conjs_4a_3
else if rel = "distinct" then
(* 7i0 *)
@@ -2105,7 +2210,7 @@
let all_conjs = !static_conjs @ dyn_conjs @ neg_conjs in
(rhs_pos_preds, !static_conjs, all_conjs),
(next_arg, body, neg_body)) brs in
- pos_conjs_4b, brs
+ pconjs_4b, brs
let translate_game player_term game_descr =
@@ -2355,8 +2460,8 @@
| mask, (sb,_)::_ -> List.map (fun (v,_)->mask, v) sb) elements in
(* 4a *)
let static_rels =
- List.map (fun (rname,args) ->
- rname, List.map (fun _ -> ()) args) static_rules in
+ Aux.unique_sorted (List.map (fun (rname,args) ->
+ rname, List.map (fun _ -> ()) args) static_rules) in
let static_rels =
List.map (fun (rel,args) ->
rel, List.length args,
@@ -2678,6 +2783,9 @@
let rules_brs =
List.map (fun ((lead_head, lead_body, lead_neg_body),
branches) ->
+ let lead_does =
+ "_DOES_PLACEHOLDER_", [loc_players.(loc); lead_head] in
+ let lead_body = lead_does::lead_body in
let fixed_vars = term_vars lead_head in
let fixed_brs, other_brs = List.partition
(function
@@ -2698,7 +2806,7 @@
) frame_brs in
let unfixed_brs =
to_expand @ more_to_expand in
- (* 7g1 *)
+ (* 7g *)
let expanded_brs =
expand_branch_vars masks element_terms
~freshen_unfixed:(Aux.Right (Aux.Strings.elements fixed_vars))
@@ -2726,7 +2834,7 @@
| _ -> assert false) l)) frames))
);
(* }}} *)
- (* collect and rename multi-bodies *)
+ (* collect and rename multi-bodies, i.e. form disjunctions *)
let frames = List.map (function
| [] -> assert false
| [head, body, neg_body] -> head, [body, neg_body]
@@ -2754,7 +2862,7 @@
(* 7f3 *)
(* TODO: minimize the number of branches by keeping
negations over conjunctions like in (6b1) *)
- let erasure_brs : lit_def_branch list = Aux.concat_map
+ let erasure_brs = Aux.concat_map
(function
| [next_arg] as next_args,multi_body ->
let mask, _, _, blank_arg = term_to_blank masks next_arg in
@@ -2824,7 +2932,7 @@
(subst_rels sb neg_body) in
let head = subst sb blank_arg in
if
- (* TODO: (7g) instead *)
+ (* TODO: what about expanding as in (7g)? *)
Aux.Strings.subset (term_vars head)
fixed_vars &&
(* (7f4) *)
@@ -2833,9 +2941,27 @@
List.mem pos neg_conjs) lead_neg_body
) body) &&
not (List.exists (fun (_,neg) ->
- List.mem neg lead_body
+ List.mem neg lead_body
) neg_body)
- then Some ([head], body, neg_body)
+ then (
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "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]))
+ );
+ (* }}} *)
+ let neg_body =
+ List.map (fun (vs,lit)->vs,[lit])
+ neg_body in
+ (* we could add "pruning" conditions:*)
+ Some ([head], lead_body @ body,
+ lead_neg_body @ neg_body)
+ (*or not
+ Some ([head], body, neg_body)*)
+ )
else None
with Not_found -> None) erasures in
let erasures = Aux.unique_sorted
@@ -2843,13 +2969,12 @@
head, Aux.unique_sorted body,
Aux.unique_sorted neg_body) erasures) in
erasures
- (* TODO: (7g2) *)
| _ -> assert false) frames in
(* TODO: (7f5) we ignore the possibility that "lead" is
instantiated by some of erasure substitutions, since
we already ignore non-maximal "legal" classes *)
- lead_head, fixed_brs @ expanded_brs @
- exp_brs_of_lit_brs erasure_brs
+ let nonframe_brs = fixed_brs @ expanded_brs in
+ lead_head, nonframe_brs @ erasure_brs
) rules_brs in
(* let rules_inds = Array.of_list rules_brs in *)
rules_brs
@@ -2912,7 +3037,7 @@
let body = List.filter (
function "_DOES_PLACEHOLDER_",_ -> false | _ -> true) body in
lead, (head, body, neg_body)) brs in
- let table = List.map (fun atom ->
+ let table = Aux.map_some (fun atom ->
let positives = Array.mapi (fun i (_,(_,body,_)) ->
if List.mem atom body then Some i else None) brs in
let positives = Aux.map_some (fun x->x)
@@ -2932,9 +3057,15 @@
(String.concat ", "(List.map string_of_int negatives))
);
(* }}} *)
+ (* since artificial branches were introduced for all atoms,
+ if some case isn't specifically selected for, it means
+ that the corresponding literal is not satisfiable *)
+ if negatives = [] || positives = []
+ then None
+ else
(* first those that allow "P" then those that allow "not P" *)
- [Aux.Ints.diff full_set (Aux.ints_of_list negatives);
- Aux.Ints.diff full_set (Aux.ints_of_list positives)]
+ Some [Aux.Ints.diff full_set (Aux.ints_of_list negatives);
+ Aux.Ints.diff full_set (Aux.ints_of_list positives)]
) atoms in
let cases = Aux.product table in
let cases =
@@ -2957,7 +3088,6 @@
Aux.array_existsi (fun ply states ->
if ply mod loc_n = loc then (
(* {{{ log entry *)
-
if !debug_level > 4 then (
let posi =
Aux.map_some (function
@@ -2967,7 +3097,6 @@
"Checking branch at states:\n%s\npositives:\n%s\n"
(terms_str states) (terms_str posi)
);
-
(* }}} *)
let res =
List.for_all (function
@@ -3018,11 +3147,11 @@
Aux.unique_sorted rhs_pos,
static_phis, phis)) cases in
let cases =
- Aux.map_some (
- fun (var_elems,struc_elems,rhs_pos,static_phis,phis) ->
- let rphi = Formula.And static_phis in
+ Aux.map_some (
+ fun (var_elems,struc_elems,rhs_pos,static_phis,phis) ->
+ let rphi = Formula.And static_phis in
(* {{{ log entry *)
- if !debug_level > 4 then (
+ if !debug_level > 4 then (
(* do not print, because it generates too many
answers -- too little constraints per number of
variables when considering a single branch *)
@@ -3033,21 +3162,21 @@
let atups =
AssignmentSet.tuples struc.Structure.elements
avars assgn in *)
- Printf.printf "evaluating: %s\n%!"
- (Formula.str rphi)
+ Printf.printf "evaluating: %s\n%!"
+ (Formula.str rphi)
(* (List.length atups) *)
- );
+ );
(* }}} *)
- let res = Solver.M.check struc rphi in
+ let res = Solver.M.check struc rphi in
(* {{{ log entry *)
- if !debug_level > 4 && res then (
- Printf.printf "holds\n%!"
- );
+ if !debug_level > 4 && res then (
+ Printf.printf "holds\n%!"
+ );
(* }}} *)
- if res then
- let precond = Formula.And phis in
- Some (var_elems, struc_elems, rhs_pos, precond)
- else None) cases in
+ if res then
+ let precond = Formula.And phis in
+ Some (var_elems, struc_elems, rhs_pos, precond)
+ else None) cases in
List.map (fun (var_elems, struc_elems, rhs_pos, precond) ->
lead, (var_elems, struc_elems, rhs_pos, precond)) cases
) rules_brs
@@ -3134,11 +3263,10 @@
) goals in
(* 8c *)
let sized =
- List.map (fun (score,phi) -> FormulaOps.size phi, score) payoff in
- let cmp (s1,v1) (s2,v2) =
- if s2-s1 = 0 then Pervasives.compare v1 v2 else s2-s1 in
+ List.map (fun (score,phi) -> GameSimpl.niceness phi, score) payoff in
+ (* Sort in increasing niceness. *)
let base_score =
- match List.sort cmp sized with [] -> 0.
+ match List.sort Pervasives.compare sized with [] -> 0.
| (_, score)::_ -> score in
let payoff = match payoff with
| [score, guard] ->
@@ -3155,8 +3283,11 @@
);
(* }}} *)
sum)
- else Formula.Plus (sum, Formula.Times (
- Formula.Const (score -. base_score), Formula.Char guard)))
+ else
+ let guarded = Formula.Times (
+ Formula.Const (score -. base_score), Formula.Char guard) in
+ if sum = Formula.Const 0. then guarded
+ else Formula.Plus (sum, guarded))
(Formula.Const base_score) scores in
player, payoff
) player_goals in
@@ -3251,9 +3382,11 @@
rname
);
(* }}} *)
+ let signat rel =
+ Structure.StringMap.find rel struc.Structure.rel_signature in
let discrete =
DiscreteRule.translate_from_precond ~precond
- ~add:rhs_pos ~embed:fluents ~struc_elems in
+ ~add:rhs_pos ~emb_rels:fluents ~signat ~struc_elems in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "Making rule %s of:\n%s\n%!" rname
@@ -3297,6 +3430,18 @@
time = 0.;
cur_loc = 0;
} in
+ (* {{{ log entry *)
+ (* *
+ let file = open_out "./GGP/tests/connect5-raw.toss" in
+ output_string file (Arena.state_str result);
+ close_out file;
+ * *)
+ if !debug_level > 1 then (
+ Printf.printf "\n\nGDL.translate_game: before simplification --\n%s\n%!"
+ (Arena.sprint_state result)
+ );
+ (* }}} *)
+ let result = GameSimpl.simplify result in
let playing_as = find_player player_term in
let noop_actions =
Array.mapi (fun loc noops->
@@ -3305,9 +3450,14 @@
| Some ([_; lead_term], _, _) -> Some lead_term
| _ -> None
) loc_noop_legal in
- (* {{{ log entry *)
+ (* {{{ log entry *)
+ (* *
+ let file = open_out "./GGP/tests/connect5-simpl.toss" in
+ output_string file (Arena.state_str result);
+ close_out file;
+ * *)
if !debug_level > 1 then (
- Printf.printf "\n\nGDL.translate_game:\n%s\n%!"
+ Printf.printf "\n\nGDL.translate_game: after simplification --\n%s\n%!"
(Arena.sprint_state result)
);
(* }}} *)
@@ -3400,9 +3550,11 @@
(Formula.sprint precond)
);
(* }}} *)
+ let signat rel =
+ Structure.StringMap.find rel struc.Structure.rel_signature in
let rule =
DiscreteRule.translate_from_precond ~precond ~add
- ~embed:gdl.fluents ~struc_elems in
+ ~emb_rels:gdl.fluents ~signat ~struc_elems in
let lhs_struc = rule.DiscreteRule.lhs_struc in
let rule = DiscreteRule.compile_rule
(Structure.rel_signature struc) [] rule in
Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml 2011-03-12 17:51:51 UTC (rev 1354)
+++ trunk/Toss/GGP/GDLTest.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -75,22 +75,40 @@
(String.concat "\n"
(List.map GDL.exp_def_str res));
);
+]
+let bigtests = "GDLBig" >::: [
+
"connect5" >::
(fun () ->
- todo "soon";
- (* GDL.debug_level := 3; *)
let connect5 = load_rules "./GGP/examples/connect5.gdl" in
- let gtransl, gdef = GDL.translate_game (Const "x") connect5 in
- ignore (gtransl, gdef)
+ let _, res = GDL.translate_game (Const "x") connect5 in
+ let goalf = open_in "./GGP/tests/connect5-simpl.toss" in
+ let resf = open_out "./GGP/tests/connect5-temp.toss" in
+ let goal_str = Aux.input_file goalf in
+ let res_str = Arena.state_str res in
+ output_string resf res_str;
+ close_in goalf; close_out resf;
+ assert_equal
+ ~msg:"GGP/examples/connect5.gdl to GGP/tests/connect5-simpl.toss, see GGP/tests/connect5-temp.toss"
+ goal_str res_str;
+ Sys.remove "./GGP/tests/connect5-temp.toss"
);
"breakthrough" >::
(fun () ->
- todo "soon";
let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
- let gdef = GDL.translate_game (Const "white") breakthrough in
- ignore gdef;
+ let _, res = GDL.translate_game (Const "white") breakthrough in
+ let goalf = open_in "./GGP/tests/breakthrough-simpl.toss" in
+ let resf = open_out "./GGP/tests/breakthrough-temp.toss" in
+ let goal_str = Aux.input_file goalf in
+ let res_str = Arena.state_str res in
+ output_string resf res_str;
+ close_in goalf; close_out resf;
+ assert_equal
+ ~msg:"GGP/examples/breakthrough.gdl to GGP/tests/breakthrough-simpl.toss, see GGP/tests/breakthrough-temp.toss"
+ goal_str res_str;
+ Sys.remove "./GGP/tests/breakthrough-temp.toss"
);
@@ -100,6 +118,9 @@
let a =
Aux.run_test_if_target "GDLTest" tests
+let a =
+ Aux.run_test_if_target "GDLTest" bigtests
+
let a () =
match test_filter
["GDL:2:masks"]
@@ -110,9 +131,10 @@
let a () =
GDL.debug_level := 4;
+ GameSimpl.debug_level := 4;
DiscreteRule.debug_level := 4;
let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
let connect5 = load_rules "./GGP/examples/connect5.gdl" in
let tictactoe = load_rules "./GGP/examples/tictactoe.gdl" in
- let gdef = GDL.translate_game (Const "x") connect5 in
- ignore gdef; ignore connect5; ignore breakthrough; ignore tictactoe
+ let gdl_def, toss_def = GDL.translate_game (Const "x") connect5 in
+ ignore gdl_def; ignore connect5; ignore breakthrough; ignore tictactoe
Added: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml (rev 0)
+++ trunk/Toss/GGP/GameSimpl.ml 2011-03-12 19:24:32 UTC (rev 1355)
@@ -0,0 +1,292 @@
+(** {2 Simplification of Toss Games.}
+
+ Whole-game simplifications and helper functions that consider both
+ a structure and a formula.
+
+ The simplification of structures, associated formulas and Toss
+ rules is specified by transformations described below. Rules can
+ be refined or new rules added to each stage.
+
+ (1) Identify relations in the structure that are not fluents nor
+ defined relations and that are equal to or are complements of
+ other relations in the structure. Select a single relation / a
+ predicate (called "the original" below), that is smaller than its
+ complement (if the complement is in the signature), and replace
+ all selected relations with it (or its negation), in all formulas
+ of the definition. Remove the other relations from the structure.
+
+ (1a) We need to update LHS structures of rules (for presentation
+ and game modification purposes, since the simple transformation
+ above of the "embedding formula" suffices for the "compiled" rule
+ representation). Replace the identified relations in the "embedded
+ set" with their originals, and add to the embedded set relations
+ that occur positively in the LHS and are complements of their
+ original. Derive all the tuples of embedded relations that are
+ required to be absent for a match (not present, even optionally,
+ in the LHS). Remove the non-optional tuples for relations that are
+ complements of their originals and add tuples of originals that
+ are complements of relations that are required to be
+ absent. Rename relations equivalent to their originals.
+
+ (2) Locate relations that subsume, or are subsumed by others (in
+ terms of inclusion relations between their graphs). Simplify
+ conjunctions and disjunctions of literals by removing literals
+ that are weaker/stronger than another present over the same tuple
+ in the given conjunction/disjunction.
+
+ (3) For each pair of static unary predicates with nonempty
+ intersection, introduce new predicate for their conjunction. For
+ each pair of static binary predicates, introduce two new
+ predicates: one for their conjunction and the other for
+ conjunction of one of the predicates and the inverse of the other.
+
+ (3a) Replace each conjunction of pair of unary/binary predicates
+ over the same variables, with one of introduced predicates. For
+ several possibilities of replacement pick one arbitrarily
+ (currently, in the order of occurrence in the formula).
+*)
+
+open Formula
+open Aux.BasicOperators
+
+let debug_level = ref 0
+
+
+
+(* Collect universally quantified subformulas and compute the size of
+ the "existential" trunk (counting only atomic formulas). *)
+let separate_univ phi =
+ let rec aux neg = function
+ | Or js | And js ->
+ List.fold_left (fun (a,b) (c,d) -> a+c,b@d) (0,[])
+ (List.map (aux neg) js)
+ | All (_, phi) ->
+ if neg then aux neg phi
+ else 0, [phi]
+ | Ex (_, phi) ->
+ if not neg then aux neg phi
+ else 0, [phi]
+ | Not phi -> aux (not neg) phi
+ | Rel _ | Eq _ | In _ | RealExpr _ -> 1, [] in
+ aux false phi
+
+
+(* A heuristic measure of how easy a formula is to solve or provide a
+ good heuristic. Very crude for now, not using the structure yet. *)
+let niceness phi =
+ let trunk, univs = separate_univ phi in
+ trunk - List.fold_left (+) 0 (List.map FormulaOps.size univs)
+
+
+let simplify ?(join_rel_names=fun x _ -> x) (game, state) =
+ let struc = state.Arena.struc in
+ let signat = Structure.rel_signature struc in
+ let nelems = Structure.Elems.cardinal struc.Structure.elements in
+ let tcard tups = Structure.Tuples.cardinal tups in
+ let fluents =
+ Aux.unique_sorted
+ (Aux.concat_map (fun (_,r) ->
+ DiscreteRule.fluents r.ContinuousRule.compiled)
+ game.Arena.rules) in
+ (* {{{ log entry *)
+ if !debug_level > 0 then (
+ Printf.printf "GameSimpl: fluents = %s\n%!"
+ (String.concat ", " fluents)
+ );
+ (* }}} *)
+ (* prepare for (3) and (1) *)
+ let subset_table =
+ List.fold_left (fun table (rel,arity) ->
+ let rel_tups =
+ Structure.StringMap.find rel struc.Structure.relations in
+ let row =
+ List.fold_left (fun row (rel2,arity2) ->
+ if arity2 = arity &&
+ Structure.Tuples.subset rel_tups
+ (Structure.StringMap.find rel2 struc.Structure.relations)
+ then Aux.Strings.add rel2 row
+ else row
+ ) Aux.Str...
[truncated message content] |
