[Toss-devel-svn] SF.net SVN: toss:[1379] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1379] trunk/Toss
|
From: <luk...@us...> - 2011-03-23 00:41:39
|
Revision: 1379
http://toss.svn.sourceforge.net/toss/?rev=1379&view=rev
Author: lukstafi
Date: 2011-03-23 00:41:31 +0000 (Wed, 23 Mar 2011)
Log Message:
-----------
Generalized folds over formulas and real expressions. Major overhaul of monotonicity (detection and heuristics): distinction of positive, negative and indefinite fluents.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/Arena.mli
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Arena/DiscreteRule.mli
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Formula/FFTNF.mli
trunk/Toss/Formula/FFTNFTest.ml
trunk/Toss/Formula/FormulaOps.ml
trunk/Toss/Formula/FormulaOps.mli
trunk/Toss/GGP/GameSimpl.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Play/Heuristic.mli
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Solver/SolverTest.ml
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Arena/Arena.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -439,6 +439,17 @@
rules = List.map (fun (rn, r) ->
rn, {r with ContinuousRule.discrete =
f r.ContinuousRule.discrete}) game.rules}
+
+let all_fluents game =
+ let drules =
+ List.map (fun r -> (snd r).ContinuousRule.compiled) game.rules in
+ let fluents = List.map DiscreteRule.fluents drules in
+ let frels (posi_frels, nega_frels, indef_frels) =
+ Aux.Strings.union indef_frels
+ (Aux.Strings.union posi_frels nega_frels) in
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map frels fluents)
+
(* Compare two (game, state) pairs and explain the first difference
met. Formulas and expressions are compared for syntactical
Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Arena/Arena.mli 2011-03-23 00:41:31 UTC (rev 1379)
@@ -124,6 +124,8 @@
val map_to_discrete :
(DiscreteRule.rule -> DiscreteRule.rule) -> game -> game
+val all_fluents : game -> Aux.Strings.t
+
(** Compare two (game, state) pairs and explain the first difference
met. Formulas and expressions are compared for syntactical
equality. Players need to be given in the same order. Data is
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Arena/DiscreteRule.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -49,7 +49,13 @@
rlmap : (string * string) list option; (* rule_s on variables (?) *)
}
-(* We call fluents the relations that can be modified by a rule. *)
+(* Fluents are relations that are changed by rules. Distinguish two
+ subclasses of fluents: positive fluents occur only positively on
+ RHSes (are only added) and only negatively on LHSes and in
+ preconditions, and negative fluents only negatively on RHSes (are
+ only deleted) and only positively on LHSes and in
+ preconditions. (Call the remaining fluents indefinite.) See
+ Heuristic.ml. *)
let fluents_make ?(only_pos=false) f r =
let fl_make (s, tp) =
if tp = [] then None else
@@ -61,41 +67,34 @@
let fluents r =
let map_rels =
Aux.map_some (fun (rel,tups)->if tups=[] then None else Some rel) in
- map_rels r.rhs_pos_tuples @ map_rels r.rhs_neg_tuples
-
-(* A relation is monotonic if it cannot remove tuples. *)
-let monotonic r =
- List.for_all (fun (_,tups) -> tups = []) r.rhs_neg_tuples
+ let posi_cands = Aux.strings_of_list (map_rels r.rhs_pos_tuples) in
+ let nega_cands = Aux.strings_of_list (map_rels r.rhs_neg_tuples) in
+ let fluents = Aux.Strings.union posi_cands nega_cands in
+ let posi = Aux.Strings.diff posi_cands nega_cands
+ and nega = Aux.Strings.diff nega_cands posi_cands in
+ let posi_lhs, nega_lhs = FormulaOps.rels_signs r.lhs_form in
+ let posi = Aux.Strings.diff posi posi_lhs in
+ let nega = Aux.Strings.diff nega nega_lhs in
+ posi, nega, Aux.Strings.diff fluents (Aux.Strings.union posi nega)
(* A fluent precondition is an approximation to the condition on a
- structure for the fluent to appear at a position. *)
-let fluent_preconds rules signature fluents =
- (* Remove positive fluents as they could still be added later, also
- remove the fluent under consideration *)
- let module M = struct open Formula
- (* TODO: since OCaml 3.12 *) (* let open Formula in *)
- let rec negative_trace fluent neg = function
- | Rel (rel, _) as atom ->
- if rel = fluent || not neg && List.mem rel fluents
- then raise Not_found
- else atom
- | (Eq _ | In _ | RealExpr _) as atom -> atom
- | Not phi -> Not (negative_trace fluent (not neg) phi)
- | And conjs ->
- And (Aux.map_try (negative_trace fluent neg) conjs)
- | Or disjs ->
- Or (Aux.map_try (negative_trace fluent neg) disjs)
- | Ex (vs, phi) -> Ex (vs, negative_trace fluent neg phi)
- | All (vs, phi) -> All (vs, negative_trace fluent neg phi) end in
- let negative_trace fluent phi =
- try FormulaOps.flatten_formula (M.negative_trace fluent false phi)
- with Not_found -> Formula.And [] in
+ structure for the positive/negative fluent to appear/disappear at a
+ position. We are only interested in expanding preconditions of
+ positive and negative fluents.
+
+ TODO: currently, only a single absence/presence tuple is removed
+ from the precondition: the one from which it "derived"; shouldn't
+ all added and deleted tuples be removed? *)
+let fluent_preconds rules signature posi_frels nega_frels =
+ let fluents =
+ Aux.Strings.elements posi_frels @ Aux.Strings.elements nega_frels in
let fluent_precond rel =
(* rules that produce a fluent, together with its args *)
let rel_prods =
Aux.map_some (fun r ->
- if List.mem_assoc rel r.rhs_pos_tuples then
- let rel_tups = List.assoc rel r.rhs_pos_tuples in
+ let rhs_tuples = r.rhs_pos_tuples @ r.rhs_neg_tuples in
+ if List.mem_assoc rel rhs_tuples then
+ let rel_tups = List.assoc rel rhs_tuples in
if rel_tups <> [] then Some (r, rel_tups)
else None
else None) rules in
@@ -108,7 +107,27 @@
Aux.not_conflicting_names "av__" all_names
(Array.to_list (Array.make (signature rel) ())) in
(* Encapsulate the precondition as a defined relation *)
- let compose_pre r body args =
+ let compose_pre r body args =
+ let lhs_args =
+ match r.rlmap with
+ | None -> (* LHS and RHS vars are the same *)
+ args
+ | Some rlmap ->
+ Array.map (fun e->List.assoc e rlmap) args in
+ (* remove potential condition for absence/presence of the
+ fluent being just added / deleted *)
+ let body = FormulaOps.map_formula
+ {FormulaOps.identity_map with
+ (* remove the absence/presence condition of added/deleted
+ tuple (TODO: see header comment); we know by [rel \in
+ nega_frels/posi_frels] that the occurrence is
+ positive/negative *)
+ FormulaOps.map_Rel = (fun b_rel b_args ->
+ let b = rel = b_rel && lhs_args =
+ Array.map Formula.var_str b_args in
+ if b && Aux.Strings.mem rel nega_frels then Formula.And []
+ else if b && Aux.Strings.mem rel posi_frels then Formula.Or []
+ else Formula.Rel (b_rel, b_args))} body in
let args = Array.to_list args in
let body, other_vars, numap_cstr =
match r.rlmap with
@@ -131,9 +150,8 @@
else Formula.Ex (List.map (fun v-> `FO v) other_vars, body) in
let disjs =
Aux.concat_map
- (fun (r, lhs, args_l)-> List.map (compose_pre r lhs) args_l)
- (List.map (fun (r, args_l)->
- r, negative_trace rel r.lhs_form, args_l) rel_prods) in
+ (fun (r, args_l)-> List.map (compose_pre r r.lhs_form) args_l)
+ rel_prods in
let precond =
match disjs with
| [] -> failwith ("fluent_preconds: not a fluent: "^rel)
Modified: trunk/Toss/Arena/DiscreteRule.mli
===================================================================
--- trunk/Toss/Arena/DiscreteRule.mli 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Arena/DiscreteRule.mli 2011-03-23 00:41:31 UTC (rev 1379)
@@ -47,16 +47,23 @@
val elemvar_of_elem : elem_inv_names -> int -> string
-(* We call fluents the relations that can be modified by a rule. *)
-val fluents : rule_obj -> string list
+(** Fluents are relations that are changed by rules. Distinguish two
+ subclasses of fluents: positive fluents occur only positively on
+ RHSes (are only added) and only negatively on LHSes and in
+ preconditions, and negative fluents only negatively on RHSes (are
+ only deleted) and only positively on LHSes and in
+ preconditions. (Call the remaining fluents indefinite.) See
+ {!Heuristic}. *)
+val fluents : rule_obj -> Aux.Strings.t * Aux.Strings.t * Aux.Strings.t
val fluents_make : ?only_pos : bool -> (string -> int -> 'a) ->
rule_obj -> 'a list
-
-(* A relation is monotonic if it cannot remove tuples. *)
-val monotonic : rule_obj -> bool
+(** A fluent precondition is an approximation to the condition on a
+ structure for the positive/negative fluent to appear/disappear at a
+ position. We are only interested in expanding preconditions of
+ positive and negative fluents. *)
val fluent_preconds :
- rule_obj list -> (string -> int) -> string list ->
+ rule_obj list -> (string -> int) -> Aux.Strings.t -> Aux.Strings.t ->
(string * (string list * Formula.formula)) list
(* Helpers for special relations. *)
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Formula/FFTNF.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -1,143 +1,143 @@
-(* Computing the FF Type Normal Form, and the FF Separation.
+(** Computing the FF Type Normal Form, and the FF Separation.
- {2 Computing the FF Type Normal Form}
+ {2 Computing the FF Type Normal Form}
- Because FFTNF adds considerably to the already high computational
- cost of computing TNF, we turn off some of its flexibility
- depending on the size of the normalized formula:
+ Because FFTNF adds considerably to the already high computational
+ cost of computing TNF, we turn off some of its flexibility
+ depending on the size of the normalized formula:
- (1) at parsimony level 1 (PARL1), we do not move atoms that are
- already protected (in the TNF sense) if that leads to formula
- duplication;
+ (1) at parsimony level 1 (PARL1), we do not move atoms that are
+ already protected (in the TNF sense) if that leads to formula
+ duplication;
- (2) at parsimony level 2 (PARL2), we do not reduce to PNF and do
- not move protected atoms at all.
+ (2) at parsimony level 2 (PARL2), we do not reduce to PNF and do
+ not move protected atoms at all.
- {3 Algorithm for calculating FFTNF(_<_):}
+ {3 Algorithm for calculating FFTNF(_<_):}
- 1: Reduce to partially negation-normal prenex-normal form with
- existential-first minimized alternation -- do not push negation
- inside an existentially quantified ground subformula; collapse
- nonalternating quantifiers into quantifying over sets of
- variables. We call a negated existentially quantified ground
- subformula -- or equivalently a universally quantified ground
- subformula -- a subtask. PARL2: do partial NNF but not PNF.
+ 1: Reduce to partially negation-normal prenex-normal form with
+ existential-first minimized alternation -- do not push negation
+ inside an existentially quantified ground subformula; collapse
+ nonalternating quantifiers into quantifying over sets of
+ variables. We call a negated existentially quantified ground
+ subformula -- or equivalently a universally quantified ground
+ subformula -- a subtask. PARL2: do partial NNF but not PNF.
- 2: Collapse conjunctions and disjunctions using associativity.
+ 2: Collapse conjunctions and disjunctions using associativity.
- 3: The processed part is maintained explicitly; the zipper is
- built during the depth-first search for unprocessed literal and
- is then zipped by pulling-out the selected literal. PARL2: mark
- protected literals as processed.
+ 3: The processed part is maintained explicitly; the zipper is
+ built during the depth-first search for unprocessed literal and
+ is then zipped by pulling-out the selected literal. PARL2: mark
+ protected literals as processed.
- The whole term is searched depth-first for a subtask or the best
- literal to pull-out. A subtask is preferred, otherwise the first
- best literal is selected.
+ The whole term is searched depth-first for a subtask or the best
+ literal to pull-out. A subtask is preferred, otherwise the first
+ best literal is selected.
- A literal that has all variables quantified in the scope of some
- variable of another literal is worse than the other literal. If
- their oldest (quantified with widest scope) variable is the same,
- compare using the ordering _<_. "a _<_ b" means that a is better
- than b -- should be pulled out earlier. "a _<_ b" returns false if
- it is indifferent whether a or b should be first.
+ A literal that has all variables quantified in the scope of some
+ variable of another literal is worse than the other literal. If
+ their oldest (quantified with widest scope) variable is the same,
+ compare using the ordering _<_. "a _<_ b" means that a is better
+ than b -- should be pulled out earlier. "a _<_ b" returns false if
+ it is indifferent whether a or b should be first.
- The subtask or literal to be pulled out is replaced by T = And[],
- forming the initial location (context[],[T]).
+ The subtask or literal to be pulled out is replaced by T = And[],
+ forming the initial location (context[],[T]).
- Note: the literal is treated as "conjoined", as opposed
- to "disjoined", to the surroundings, because disjunctions of
- literals are much rarer than conjunctions.
+ Note: the literal is treated as "conjoined", as opposed
+ to "disjoined", to the surroundings, because disjunctions of
+ literals are much rarer than conjunctions.
- 4: When a subtask/literal is placed in its final location it is
- marked as processed. Denote by Qn, Qn', etc., a quantifier over a
- set of variables, and by -Qn a quantifier that is complementary to
- Qn (e.g. -ex vs.Phi = all vs.Phi). The result of pulling out a
- literal L of a location (context[],[fill-loc]) (denoted also as
- context[][fill-loc]) by cases on context[]:
+ 4: When a subtask/literal is placed in its final location it is
+ marked as processed. Denote by Qn, Qn', etc., a quantifier over a
+ set of variables, and by -Qn a quantifier that is complementary to
+ Qn (e.g. -ex vs.Phi = all vs.Phi). The result of pulling out a
+ literal L of a location (context[],[fill-loc]) (denoted also as
+ context[][fill-loc]) by cases on context[]:
- (a) context'[Qn.[]] where Qn = Qn' union Qn'' for Qn'
- contained in Var(L) and Qn'' disjoint with Var(L)
+ (a) context'[Qn.[]] where Qn = Qn' union Qn'' for Qn'
+ contained in Var(L) and Qn'' disjoint with Var(L)
- (a1) empty Qn': pull-out(context'[],[Qn.[fill-loc]])
+ (a1) empty Qn': pull-out(context'[],[Qn.[fill-loc]])
- (a2) nonempty Qn': context'[Qn'.(L /\ Qn''.[fill-loc])]
+ (a2) nonempty Qn': context'[Qn'.(L /\ Qn''.[fill-loc])]
- (b) context'[[] /\ C]: pull-out(context'[],[[fill-loc] /\ C])
+ (b) context'[[] /\ C]: pull-out(context'[],[[fill-loc] /\ C])
- (c) context'[Qn.([] \/ D)] where Qn1=Qn & Var(L),
- Qn2=Qn & Var(L,[fill-loc]) \ Var(D), Qn3=Qn & Var(L,[fill-loc]) & Var(D)
- Qn4=Qn & Var(D) \ Qn3, Qn5=Qn & Var([fill-loc]) \ Qn1 \ Qn3,
- Qn6=Qn & Var([fill-loc],D)
+ (c) context'[Qn.([] \/ D)] where Qn1=Qn & Var(L),
+ Qn2=Qn & Var(L,[fill-loc]) \ Var(D), Qn3=Qn & Var(L,[fill-loc]) & Var(D)
+ Qn4=Qn & Var(D) \ Qn3, Qn5=Qn & Var([fill-loc]) \ Qn1 \ Qn3,
+ Qn6=Qn & Var([fill-loc],D)
- (c0) PARL1 and Qn1=Qn:
- context[L /\ [fill-loc]]
+ (c0) PARL1 and Qn1=Qn:
+ context[L /\ [fill-loc]]
- (c1) empty Qn3:
- pull-out(context'[Qn2.[] \/ Qn4.D],[fill-loc])
+ (c1) empty Qn3:
+ pull-out(context'[Qn2.[] \/ Qn4.D],[fill-loc])
- (c2) nonempty Qn3 and Qn1, (nonempty Qn1\Qn3 or empty Qn3\Qn1):
- context'[Qn3.(Qn1\Qn3.(L /\ Qn5.[fill-loc]) \/ Qn4.D)]
+ (c2) nonempty Qn3 and Qn1, (nonempty Qn1\Qn3 or empty Qn3\Qn1):
+ context'[Qn3.(Qn1\Qn3.(L /\ Qn5.[fill-loc]) \/ Qn4.D)]
- (c3) Qn existential, nonempty Qn3\Qn1, empty Qn1\Qn3:
- pull-out(context'[Qn2+3.[] \/ Qn3+4.D],[fill-loc])
+ (c3) Qn existential, nonempty Qn3\Qn1, empty Qn1\Qn3:
+ pull-out(context'[Qn2+3.[] \/ Qn3+4.D],[fill-loc])
- (c4) Qn universal, nonempty Qn3\Qn1, empty Qn1\Qn3:
- pull-out(context'[Qn.(([] \/ D) /\ ([fill-loc] \/ D))],[T])
+ (c4) Qn universal, nonempty Qn3\Qn1, empty Qn1\Qn3:
+ pull-out(context'[Qn.(([] \/ D) /\ ([fill-loc] \/ D))],[T])
- (d) context'[Qn.(([] \/ D) /\ C)] where Qn1=Qn & Var(L),
- Qn2=Qn & Var(L,[fill-loc],D) \ Var(C),
- Qn3=Qn & Var(L,[fill-loc],D) & Var(C)
- Qn4=Qn & Var(C) \ Qn3, Qn5=Qn & Var(D,C),
- Qn6=Qn & Var(L,[fill-loc],C)
+ (d) context'[Qn.(([] \/ D) /\ C)] where Qn1=Qn & Var(L),
+ Qn2=Qn & Var(L,[fill-loc],D) \ Var(C),
+ Qn3=Qn & Var(L,[fill-loc],D) & Var(C)
+ Qn4=Qn & Var(C) \ Qn3, Qn5=Qn & Var(D,C),
+ Qn6=Qn & Var(L,[fill-loc],C)
- (d0) PARL1 and Qn1=Qn:
- context[L /\ [fill-loc]]
+ (d0) PARL1 and Qn1=Qn:
+ context[L /\ [fill-loc]]
- (d1) empty Qn3:
- pull-out(context'[Qn2.([] \/ D) /\ Qn4.C],[fill-loc])
+ (d1) empty Qn3:
+ pull-out(context'[Qn2.([] \/ D) /\ Qn4.C],[fill-loc])
- (d2) Qn universal:
- pull-out(context'[Qn2+3.([] \/ D) /\ Qn3+4.C])
+ (d2) Qn universal:
+ pull-out(context'[Qn2+3.([] \/ D) /\ Qn3+4.C])
- (d3) Qn existential, nonempty Qn3:
- pull-out(context'[Qn6.([] /\ C) \/ Qn5.(D /\ C)],[fill-loc])
+ (d3) Qn existential, nonempty Qn3:
+ pull-out(context'[Qn6.([] /\ C) \/ Qn5.(D /\ C)],[fill-loc])
- (e) context'[[] \/ D] when no quantifier in context':
- context[L /\ [fill-loc]]
+ (e) context'[[] \/ D] when no quantifier in context':
+ context[L /\ [fill-loc]]
- (f) context'[([] \/ D) /\ C] when neither case (d) nor (e):
+ (f) context'[([] \/ D) /\ C] when neither case (d) nor (e):
- (f1) If the pulled-out literal is protected in current scope, leave
- it here.
- context[L /\ [fill-loc]]
+ (f1) If the pulled-out literal is protected in current scope, leave
+ it here.
+ context[L /\ [fill-loc]]
- (f2) when the nearest quantifier is existential:
- pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc])
+ (f2) when the nearest quantifier is existential:
+ pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc])
- (f3) context'[(([] \/ D) /\ C) \/ E] (when the nearest q. is universal):
- pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc])
+ (f3) context'[(([] \/ D) /\ C) \/ E] (when the nearest q. is universal):
+ pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc])
- The same rules are applied for subtasks, where we take
- Var(subtask)=empty, and a subtask is protected only when not in
- scope of any quantifier.
+ The same rules are applied for subtasks, where we take
+ Var(subtask)=empty, and a subtask is protected only when not in
+ scope of any quantifier.
- 5: since the literals in conjunctions have been scrambled by the
- zipping process, they are sorted into the order in which they have
- been processed.
+ 5: since the literals in conjunctions have been scrambled by the
+ zipping process, they are sorted into the order in which they have
+ been processed.
- Compact tentative specification of FFTNF(_<_):
+ Compact tentative specification of FFTNF(_<_):
- Consider a graph whose nodes are literals of a formula and two
- nodes are connected by an edge iff the literals share a
- variable. Direct the edges so that there is no edge a->b for
- b_<_a. The formula is in FFTNF(_<_) iff it is in TNF and the number
- of quantifiers a literal is in scope of never decreases along an
- edge, for some such directing of edges.
+ Consider a graph whose nodes are literals of a formula and two
+ nodes are connected by an edge iff the literals share a
+ variable. Direct the edges so that there is no edge a->b for
+ b_<_a. The formula is in FFTNF(_<_) iff it is in TNF and the number
+ of quantifiers a literal is in scope of never decreases along an
+ edge, for some such directing of edges.
- FIXME: the above specification is not correct (too weak).
+ FIXME: the above specification is not correct (too weak).
*)
@@ -1017,87 +1017,90 @@
-(* **************************************************
+(** **************************************************
- {2 Computing the FF Separation}
+ {2 Computing the FF Separation}
- Let FFSEP(F)(Phi) be
- ((V1,F11,...,F1N_1,Guard1), ..., (VM,FM1,...,FMN_M,GuardM))
- where
+ Let FFSEP(PF,NF)(Phi) be
+ ((V1,F11,...,F1N_1,Guard1), ..., (VM,FM1,...,FMN_M,GuardM))
+ where
- * {F1, ..., FMN_M} are all fluent atoms that occur positively in Phi and
- whose free variables are contained in the existential prefix of
- PNF(Phi) (where PNF is "prenex normal, existential-first with
- minimized alternation, form") plus the free variables of Phi
+ * {F1, ..., FMN_M} are all PF atoms that occur positively in Phi
+ and NF atoms that occur negatively in Phi, and whose free variables
+ are contained in the existential prefix of PNF(Phi) (where PNF is
+ "prenex normal, existential-first with minimized alternation,
+ form") plus the free variables of Phi
- * (ex V1 (F11/\.../\F1N_1/\Guard1) \/ ...
- \/ ex VM (FM1/\.../\FMN_M/\GuardM))
- is equivalent to Phi with minimal application of distributivity
- (GuardI can contain disjunctions if they don't contain any of FIj)
+ * (ex V1 (F11/\.../\F1N_1/\Guard1) \/ ...
+ \/ ex VM (FM1/\.../\FMN_M/\GuardM))
+ is equivalent to Phi with minimal application of distributivity
+ (GuardI can contain disjunctions if they don't contain any of FIj)
- {3 Algorithm for computing the FFSEP(F)(Phi):}
+ {3 Algorithm for computing the FFSEP(PF,NF)(Phi):}
- 1: Find the free variables FV and existential prefix variables
- EV. Let "active atoms" be the positive atoms R(tup) with [R \in F]
- and [tup \in EV+FV].
+ 1: Find the free variables FV and existential prefix variables
+ EV. Let "active atoms" be the positive/negative atoms R(tup) with
+ [R \in PF/NF] and [tup \in EV+FV].
- 2: Flatten the formula Phi (using associativity), and push negation
- inside (partial NN) only when there is an active atom in the subformula.
- (Use [TProc (Not ...)] otherwise.)
+ 2: Flatten the formula Phi (using associativity), and push negation
+ inside (partial NN) only when there is an active atom in the subformula.
+ (Use [TProc (Not ...)] otherwise.)
- 3: Loop using a forest initialized with a single tree of
- the formula and empty atoms list. (The "already processed
- literal" tag [TProc] will not be used.) The forest of trees with
- atoms will constitute the answer ((F11,...,F1N_1,Guard1), ...,
- (FM1,...,FMN_M,GuardM)).
+ 3: Loop using a forest initialized with a single tree of
+ the formula and empty atoms list. (The "already processed
+ literal" tag [TProc] will not be used.) The forest of trees with
+ atoms will constitute the answer ((F11,...,F1N_1,Guard1), ...,
+ (FM1,...,FMN_M,GuardM)).
- 4: Find a positive atom R(tup) with [R \in F] and [tup \in EV],
- building a zipper to it. (Preprocessing guarantees that all other
- literals are packed into [TProc] during the main loop.)
+ 4: Find a positive/negative literal R(tup) with [R \in PF/NF] and
+ [tup \in EV], building a zipper to it. (Preprocessing guarantees
+ that all other literals are packed into [TProc] during the main
+ loop.)
- The atom to be pulled out is replaced by T = And[], forming the
- initial location (context[],[T]).
+ The literal to be pulled out is replaced by T = And[] (note the NN
+ form -- T is not under a negation), forming the initial location
+ (context[],[T]).
- 5: In the final location, attach the pulled-out atom to the tree's
- list. For a nonempty context location
- pull-out(context[],[fill-loc]) by cases on context[]:
+ 5: In the final location, attach the pulled-out literal to the tree's
+ list. For a nonempty context location
+ pull-out(context[],[fill-loc]) by cases on context[]:
- (a) context'[Qn.[]]: pull-out(context[],Qn.[fill-loc])
+ (a) context'[Qn.[]]: pull-out(context[],Qn.[fill-loc])
- (b) context'[[] /\ C]: pull-out(context[],[fill-loc] /\ C)
+ (b) context'[[] /\ C]: pull-out(context[],[fill-loc] /\ C)
- (c) context'[Qn.([] \/ D)]:
+ (c) context'[Qn.([] \/ D)]:
- (c1) Qn existential: pull-out(context'[Qn.[] \/ Qn.D], [fill-loc])
+ (c1) Qn existential: pull-out(context'[Qn.[] \/ Qn.D], [fill-loc])
- (c2) Qn universal, FV([fill-loc]) & Qn is empty:
- pull-out(context'[[] \/ Qn.D], [fill-loc])
+ (c2) Qn universal, FV([fill-loc]) & Qn is empty:
+ pull-out(context'[[] \/ Qn.D], [fill-loc])
- (c3) Qn universal, FV([fill-loc]) & Qn is not empty:
- pull-out(context'[([] \/ Qn.D) /\ Qn.([fill-loc] \/ D)],[T])
+ (c3) Qn universal, FV([fill-loc]) & Qn is not empty:
+ pull-out(context'[([] \/ Qn.D) /\ Qn.([fill-loc] \/ D)],[T])
- (d) context'[([] \/ D) /\ C] when the nearest quantifier is
- existential or none:
- pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc])
+ (d) context'[([] \/ D) /\ C] when the nearest quantifier is
+ existential or none:
+ pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc])
- (e) context'[Qn.(([] \/ D) /\ C)] (when Qn is universal):
- pull-out(context'[Qn.([] \/ D) /\ Qn.C], [fill-loc])
+ (e) context'[Qn.(([] \/ D) /\ C)] (when Qn is universal):
+ pull-out(context'[Qn.([] \/ D) /\ Qn.C], [fill-loc])
- (f) context'[(([] \/ D) /\ C) \/ E] (when the nearest q. is universal):
- pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc])
+ (f) context'[(([] \/ D) /\ C) \/ E] (when the nearest q. is universal):
+ pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc])
- (g) [] \/ D: split the tree into [fill-loc] and D trees, sharing
- atom lists, add the new atom to the [fill-loc] tree only
+ (g) [] \/ D: split the tree into [fill-loc] and D trees, sharing
+ atom lists, add the new atom to the [fill-loc] tree only
- 6: V = FV(F11,...,FMN_M), erase quantification over V from
- Guard1,...,GuardM.
+ 6: V = FV(F11,...,FMN_M), erase quantification over V from
+ Guard1,...,GuardM.
*)
(* Steps 1 and 2: Find free vars FV and existential prefix vars EV,
flatten formula, build the tree while pushing negation inside
(flatten if possible) if the subformula contains active atoms. *)
-let ffsep_init frels phi =
+let ffsep_init posi_frels nega_frels phi =
let fvs = FormulaOps.free_vars phi in
let rec aux neg evs = function
| Ex (vs, phi) when not neg ->
@@ -1111,12 +1114,12 @@
| Rel _ | RealExpr _ | Eq _ | In _ -> evs in
let evs = aux false Vars.empty phi in
let fevs = add_vars fvs evs in
- let is_active rel vs =
- Strings.mem rel frels &&
+ let is_active neg rel vs =
+ (neg && Strings.mem rel nega_frels ||
+ (not neg && Strings.mem rel posi_frels)) &&
array_for_all (fun v->Vars.mem v fevs) vs in
let rec has_active neg = function
- | Rel (rel, vs) when neg -> false
- | Rel (rel, vs) -> is_active rel (Formula.var_tup vs)
+ | Rel (rel, vs) -> is_active neg rel (Formula.var_tup vs)
| Not phi -> has_active (not neg) phi
| And js | Or js -> List.exists (has_active neg) js
| Ex (_, phi) | All (_, phi) -> has_active neg phi
@@ -1127,7 +1130,8 @@
t=TProc (0, if neg then Not phi else phi)}
else
match phi with
- | Rel _ as atom -> assert (not neg);
+ | Rel _ as atom ->
+ (* the atom is actually a literal, negative if [rel \in NF] *)
{fvs=vars_of_list (FormulaOps.free_vars atom); t=TLit atom}
| Not phi -> build (not neg) phi
| Ex (vs, phi) ->
@@ -1260,8 +1264,8 @@
(* Step 3, point (g) of step 5, step 6. *)
-let ffsep frels phi =
- let fvs, evs, tree = ffsep_init frels phi in
+let ffsep posi_frels nega_frels phi =
+ let fvs, evs, tree = ffsep_init posi_frels nega_frels phi in
(* step 3 *)
let rec loop solved climbed =
match climbed with [] -> solved
Modified: trunk/Toss/Formula/FFTNF.mli
===================================================================
--- trunk/Toss/Formula/FFTNF.mli 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Formula/FFTNF.mli 2011-03-23 00:41:31 UTC (rev 1379)
@@ -36,5 +36,5 @@
val ffsep :
- Aux.Strings.t -> Formula.formula ->
+ Aux.Strings.t -> Aux.Strings.t -> Formula.formula ->
(Formula.fo_var list * Formula.formula list * Formula.formula) list
Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Formula/FFTNFTest.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -32,8 +32,8 @@
(* Alpha-conversion of the above. *)
let winQvwxyz_idempotent = "ex v ((Q(v) and (ex w2 ((R(v, w2) and Q(w2) and ex x2 ((R(w2, x2) and Q(x2) and ex y2 ((R(x2, y2) and Q(y2) and ex z2 ((R(y2, z2) and Q(z2))))))))) or ex w1 ((C(v, w1) and Q(w1) and ex x1 ((C(w1, x1) and Q(x1) and ex y1 ((C(x1, y1) and Q(y1) and ex z1 ((C(y1, z1) and Q(z1))))))))) or ex r0 ((R(v, r0) and ex w0 ((C(r0, w0) and Q(w0) and ex s0 ((R(w0, s0) and ex x0 ((C(s0, x0) and Q(x0) and ex t0 ((R(x0, t0) and ex y0 ((C(t0, y0) and Q(y0) and ex u0 ((R(y0, u0) and ex z0 ((C(u0, z0) and Q(z0))))))))))))))))) or ex r ((R(v, r) and ex w ((C(w, r) and Q(w) and ex s ((R(w, s) and ex x ((C(x, s) and Q(x) and ex t ((R(x, t) and ex y ((C(y, t) and Q(y) and ex u ((R(y, u) and ex z ((C(z, u) and Q(z))))))))))))))))))))"
-let formula_of_guards frels phi =
- let guards = FFTNF.ffsep frels phi in
+let formula_of_guards posi_frels nega_frels phi =
+ let guards = FFTNF.ffsep posi_frels nega_frels phi in
let parts = List.map (fun (avs, atoms, guard) ->
if avs = [] then Formula.And (atoms @ [guard])
else
@@ -107,14 +107,24 @@
(fun () ->
assert_equal ~printer:(fun x->x)
"true"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (Formula.And [])));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty (Formula.And [])));
assert_equal ~printer:(fun x->x)
"(P(x) and Q(y) and R(x, y))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "R(x, y) and P(x) and Q(y)")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "R(x, y) and P(x) and Q(y)")));
+ assert_equal ~printer:(fun x->x)
+ "(P(x) and Q(y) and R(x, y))"
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"])
+ (Aux.strings_of_list ["Q"])
+ (formula_of_str "R(x, y) and P(x) and not Q(y)")));
+
);
@@ -133,13 +143,17 @@
(fun () ->
assert_equal ~printer:(fun x->x) ~msg:"simple idempotence"
winQzyx
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str winQzyx)));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str winQzyx)));
assert_equal ~printer:(fun x->x) ~msg:"reversing ff_tnf"
"(ex z, y, x ((Q(z) and Q(y) and Q(x) and ex u0 ((ex v0 ((R(x, v0) and C(v0, y))) and R(y, u0) and C(u0, z))))) or ex z, y, x ((Q(z) and Q(y) and Q(x) and ex u ((ex v ((R(x, v) and C(y, v))) and R(y, u) and C(z, u))))) or ex z, y, x ((Q(z) and Q(y) and Q(x) and (R(x, y) and R(y, z)))) or ex z, y, x ((Q(z) and Q(y) and Q(x) and (C(x, y) and C(y, z)))))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "ex z ((Q(z) and (ex y ((C(y, z) and Q(y) and ex x ((C(x, y) and Q(x))))) or ex y ((R(y, z) and Q(y) and ex x ((R(x, y) and Q(x))))) or ex u ((C(z, u) and ex y ((R(y, u) and Q(y) and ex v ((C(y, v) and ex x ((R(x, v) and Q(x))))))))) or ex u0 ((C(u0, z) and ex y ((R(y, u0) and Q(y) and ex v0 ((C(v0, y) and ex x ((R(x, v0) and Q(x))))))))))))")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "ex z ((Q(z) and (ex y ((C(y, z) and Q(y) and ex x ((C(x, y) and Q(x))))) or ex y ((R(y, z) and Q(y) and ex x ((R(x, y) and Q(x))))) or ex u ((C(z, u) and ex y ((R(y, u) and Q(y) and ex v ((C(y, v) and ex x ((R(x, v) and Q(x))))))))) or ex u0 ((C(u0, z) and ex y ((R(y, u0) and Q(y) and ex v0 ((C(v0, y) and ex x ((R(x, v0) and Q(x))))))))))))")));
);
@@ -224,24 +238,64 @@
(* only pulls out positive fluents *)
assert_equal ~printer:(fun x->x) ~msg:"#1"
"(ex y, z (((not R(x, y)) and (not Q(z)))) or ex x ((P(x) and ex y, z ((C(y, z) and (not Q(z)))))))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
assert_equal ~printer:(fun x->x) ~msg:"#2"
"ex z ((Q(z) and ex x, y ((not (R(x, y) and (P(x) or C(y, z)))))))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or not Q(z))")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or not Q(z))")));
(* TODO? simplify the result *)
assert_equal ~printer:(fun x->x) ~msg:"#3"
"(ex y ((C(y, z) and R(x, y))) or ex z ((Q(z) and ex y (true))) or ex x ((P(x) and ex y (R(x, y)))))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
assert_equal ~printer:(fun x->x) ~msg:"#4"
"(ex y ((C(y, z) and R(x, y) and C(x, z))) or ex z ((Q(z) and ex y (C(x, z)))) or ex x ((P(x) and ex y ((R(x, y) and C(x, z))))))"
- (Formula.str (formula_of_guards (Aux.strings_of_list ["P"; "Q"])
- (formula_of_str "ex x, y, z (C(x, z) and ((R(x,y) and (P(x) or C(y,z))) or Q(z)))")));
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"; "Q"])
+ Aux.Strings.empty
+ (formula_of_str "ex x, y, z (C(x, z) and ((R(x,y) and (P(x) or C(y,z))) or Q(z)))")));
+
+ (* interpretation warning: in cases below, pulled-out "Q" in the
+ result represents "not Q" actually (a negative literal) *)
+ assert_equal ~printer:(fun x->x) ~msg:"#5"
+ "(ex z ((Q(z) and ex y ((not R(x, y))))) or ex z, x ((P(x) and Q(z) and ex y (C(y, z)))))"
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"])
+ (Aux.strings_of_list ["Q"])
+ (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
+
+ assert_equal ~printer:(fun x->x) ~msg:"#6"
+ "ex x, y, z ((not ((R(x, y) and (P(x) or C(y, z))) or (not Q(z)))))"
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"])
+ (Aux.strings_of_list ["Q"])
+ (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or not Q(z))")));
+
+ (* distributes to extract P, not because of Q *)
+ assert_equal ~printer:(fun x->x) ~msg:"#7"
+ "(ex y, z ((Q(z) or (C(y, z) and R(x, y)))) or ex x ((P(x) and ex y, z (R(x, y)))))"
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"])
+ (Aux.strings_of_list ["Q"])
+ (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
+
+ assert_equal ~printer:(fun x->x) ~msg:"#8"
+ "(ex y ((C(y, z) and R(x, y) and C(x, z))) or ex z ((Q(z) and ex y (C(x, z)))) or ex x ((P(x) and ex y ((R(x, y) and C(x, z))))))"
+ (Formula.str (
+ formula_of_guards (Aux.strings_of_list ["P"])
+ (Aux.strings_of_list ["Q"])
+ (formula_of_str "ex x, y, z (C(x, z) and ((R(x,y) and (P(x) or C(y,z))) or not Q(z)))")));
+
);
"ff_tnf: simple subtasks" >::
Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Formula/FormulaOps.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -190,6 +190,96 @@
gmap.map_Sum vs (map_formula gmap guard) (map_real_expr gmap expr)
+(* Generalized fold over formula and real expression types. *)
+type 'a formula_and_expr_fold = {
+ fold_Rel : string -> fo_var array -> 'a;
+ fold_Eq : fo_var -> fo_var -> 'a;
+ fold_In : fo_var -> mso_var -> 'a;
+ fold_RealExpr : 'a -> sign_op -> 'a;
+ fold_Not : 'a -> 'a;
+ fold_And : 'a -> 'a -> 'a;
+ fold_Or : 'a -> 'a -> 'a;
+ fold_Ex : var list -> 'a -> 'a;
+ fold_All : var list -> 'a -> 'a;
+
+ fold_RVar : string -> 'a;
+ fold_Const : float -> 'a;
+ fold_Times : 'a -> 'a -> 'a;
+ fold_Plus : 'a -> 'a -> 'a;
+ fold_Fun : string -> fo_var -> 'a;
+ fold_Char : 'a -> 'a;
+ fold_Sum : fo_var list -> 'a -> 'a -> 'a
+}
+
+let make_fold union empty = {
+ fold_Rel = (fun _ _ -> empty);
+ fold_Eq = (fun _ _ -> empty);
+ fold_In = (fun _ _ -> empty);
+ fold_RealExpr = (fun expr _ -> expr);
+ fold_Not = (fun phi -> phi);
+ fold_And = union;
+ fold_Or = union;
+ fold_Ex = (fun _ phi -> phi);
+ fold_All = (fun _ phi -> phi);
+
+ fold_RVar = (fun _ -> empty);
+ fold_Const = (fun _ -> empty);
+ fold_Times = union;
+ fold_Plus = union;
+ fold_Fun = (fun _ _ -> empty);
+ fold_Char = (fun phi -> phi);
+ fold_Sum = (fun _ guard expr -> union guard expr)
+}
+
+open Aux.BasicOperators
+
+let rec fold_formula gfold = function
+ | Rel (rel, args) -> gfold.fold_Rel rel args
+ | Eq (x, y) -> gfold.fold_Eq x y
+ | In (x, ys) -> gfold.fold_In x ys
+ | RealExpr (expr, sign) ->
+ gfold.fold_RealExpr (fold_real_expr gfold expr) sign
+ | Not phi -> gfold.fold_Not (fold_formula gfold phi)
+ | And [] ->
+ gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) GZero
+ | And [conj] -> fold_formula gfold conj
+ | And (conj::conjs) ->
+ List.fold_right (gfold.fold_And -| fold_formula gfold) conjs
+ (fold_formula gfold conj)
+ | Or [] ->
+ gfold.fold_RealExpr (fold_real_expr gfold (Const 1.)) LZero
+ | Or [disj] -> fold_formula gfold disj
+ | Or (disj::disjs) ->
+ List.fold_right (gfold.fold_Or -| fold_formula gfold) disjs
+ (fold_formula gfold disj)
+ | Ex (vs, phi) -> gfold.fold_Ex vs (fold_formula gfold phi)
+ | All (vs, phi) -> gfold.fold_All vs (fold_formula gfold phi)
+
+and fold_real_expr gfold = function
+ | RVar v -> gfold.fold_RVar v
+ | Const c -> gfold.fold_Const c
+ | Times (expr1, expr2) ->
+ gfold.fold_Times (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
+ | Plus (expr1, expr2) ->
+ gfold.fold_Plus (fold_real_expr gfold expr1) (fold_real_expr gfold expr2)
+ | Fun (f, v) -> gfold.fold_Fun f v
+ | Char phi -> gfold.fold_Char (fold_formula gfold phi)
+ | Sum (vs, guard, expr) ->
+ gfold.fold_Sum vs (fold_formula gfold guard) (fold_real_expr gfold expr)
+
+let rels_signs_fold =
+ {make_fold
+ (fun (posi1,nega1) (posi2,nega2) ->
+ Aux.Strings.union posi1 posi2, Aux.Strings.union nega1 nega2)
+ (Aux.Strings.empty, Aux.Strings.empty) with
+ fold_Rel = (fun rel _ ->
+ Aux.Strings.singleton rel, Aux.Strings.empty);
+ fold_Not = (fun (posi,nega) -> nega,posi)}
+
+(* Find all positively and negatively occurring relations. *)
+let rels_signs = fold_formula rels_signs_fold
+let rels_signs_expr = fold_real_expr rels_signs_fold
+
(* Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
formula. Preserves order of subformulas. *)
let rec map_to_literals f g = function
@@ -733,7 +823,13 @@
let sl = subst_l x in Ex (get_fo sl, subst_vars sl f)
| All (x, f) when List.for_all is_fo x ->
let sl = subst_l x in All (get_fo sl, subst_vars sl f)
- | psi -> print_endline ("PSi: " ^ (Formula.str psi)); psi in
+ | psi ->
+ (* {{{ log entry *)
+ if !debug_level > 1 then (
+ print_endline ("PSi: " ^ (Formula.str psi));
+ );
+ (* }}} *)
+ psi in
if do_formula then
Char (simplify ~do_pnf ~do_re:true ~ni new_phi)
else Char new_phi
Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Formula/FormulaOps.mli 2011-03-23 00:41:31 UTC (rev 1379)
@@ -47,6 +47,37 @@
val map_formula : formula_and_expr_map -> formula -> formula
val map_real_expr : formula_and_expr_map -> real_expr -> real_expr
+(** Generalized fold over formula and real expression types. *)
+type 'a formula_and_expr_fold = {
+ fold_Rel : string -> fo_var array -> 'a;
+ fold_Eq : fo_var -> fo_var -> 'a;
+ fold_In : fo_var -> mso_var -> 'a;
+ fold_RealExpr : 'a -> sign_op -> 'a;
+ fold_Not : 'a -> 'a;
+ fold_And : 'a -> 'a -> 'a;
+ fold_Or : 'a -> 'a -> 'a;
+ fold_Ex : var list -> 'a -> 'a;
+ fold_All : var list -> 'a -> 'a;
+
+ fold_RVar : string -> 'a;
+ fold_Const : float -> 'a;
+ fold_Times : 'a -> 'a -> 'a;
+ fold_Plus : 'a -> 'a -> 'a;
+ fold_Fun : string -> fo_var -> 'a;
+ fold_Char : 'a -> 'a;
+ fold_Sum : fo_var list -> 'a -> 'a -> 'a
+}
+
+val make_fold : ('a -> 'a -> 'a) -> 'a -> 'a formula_and_expr_fold
+
+(** Fold the structure using the operations. (Not tail-recursive.) *)
+val fold_formula : 'a formula_and_expr_fold -> formula -> 'a
+val fold_real_expr : 'a formula_and_expr_fold -> real_expr -> 'a
+
+(** Find all positively and negatively occurring relations. *)
+val rels_signs : formula -> Aux.Strings.t * Aux.Strings.t
+val rels_signs_expr : real_expr -> Aux.Strings.t * Aux.Strings.t
+
(** Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
formula. Preserves order of subformulas. *)
val map_to_literals : (formula -> formula) -> (real_expr -> real_expr) ->
Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/GGP/GameSimpl.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -135,15 +135,11 @@
let signat = Structure.rel_signature struc in
let nelems = Structure.Elems.cardinal struc.Structure.elements in
let tcard tups = Tups.cardinal tups in
- let fluents =
- Aux.unique_sorted
- (Aux.concat_map (fun (_,r) ->
- DiscreteRule.fluents r.ContinuousRule.compiled)
- game.Arena.rules) in
+ let fluents = Arena.all_fluents game in
(* {{{ log entry *)
if !debug_level > 0 then (
Printf.printf "GameSimpl: fluents = %s\n%!"
- (String.concat ", " fluents)
+ (String.concat ", " (Aux.Strings.elements fluents))
);
(* }}} *)
(* 1 *)
@@ -175,7 +171,7 @@
let ntups2 = tcard rel2_tups in
if ntups >= ntups2 &&
ntups + ntups2 = Aux.int_pow nelems arity &&
- not (List.mem rel2 fluents) &&
+ not (Aux.Strings.mem rel2 fluents) &&
Tups.is_empty (Tups.inter rel_tups rel2_tups)
then (
(* {{{ log entry *)
@@ -245,7 +241,7 @@
let rel2, _ =
List.find (fun (rel2, arity2) ->
arity = arity2 &&
- not (List.mem rel2 fluents ||
+ not (Aux.Strings.mem rel2 fluents ||
List.mem_assoc rel2 game.Arena.defined_rels) &&
included_in rel1 rel2 && included_in rel2 rel1
) signat in
@@ -259,10 +255,10 @@
| None -> rel
| Some spec -> DiscreteRule.orig_rel_of rel in
rel <> "" &&
- not (List.mem rel fluents) &&
+ not (Aux.Strings.mem rel fluents) &&
not (List.mem_assoc rel game.Arena.defined_rels) &&
not (List.exists (fun (_,(rel2,_)) -> rel2=rel) equivalent) &&
- not (List.mem (fst (List.assoc rel equivalent)) fluents ||
+ not (Aux.Strings.mem (fst (List.assoc rel equivalent)) fluents ||
List.mem_assoc (fst (List.assoc rel equivalent))
game.Arena.defined_rels)
in
@@ -414,8 +410,8 @@
match phi1, phi2 with
| _ when phi1 = phi2 -> true
| Rel (rel1, args1), Rel (rel2, args2) when args1 = args2 ->
- not (List.mem rel1 fluents) &&
- not (List.mem rel2 fluents) &&
+ not (Aux.Strings.mem rel1 fluents) &&
+ not (Aux.Strings.mem rel2 fluents) &&
included_in rel1 rel2
| _ -> false in
let game =
@@ -563,7 +559,7 @@
(* the step of 3d *)
let gluable rel =
- not (List.mem rel fluents) &&
+ not (Aux.Strings.mem rel fluents) &&
not (List.mem_assoc rel game.Arena.defined_rels) in
let glue_phi =
FormulaOps.map_formula {FormulaOps.identity_map with
@@ -748,7 +744,7 @@
else DiscreteRule.orig_rel_of rel in
let res =
(not keep_predicates || List.assoc rel signat > 1) &&
- not (List.mem rel fluents) &&
+ not (Aux.Strings.mem rel fluents) &&
not (List.mem_assoc rel game.Arena.defined_rels) &&
not (Aux.Strings.mem rel used_rels) in
(* {{{ log entry *)
Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml 2011-03-22 18:22:54 UTC (rev 1378)
+++ trunk/Toss/Play/Heuristic.ml 2011-03-23 00:41:31 UTC (rev 1379)
@@ -1,214 +1,238 @@
-(* Generate a heuristic from a payoff.
+(** Generate a heuristic from a payoff.
- Input: a set of relations F whose instances can be altered during a
- game; initial state structure S of the game; payoff of the game for a
- player; advancement value ratio AR; for monotonic games, a mapping
- from fluents to their preconditions (in the form of defined relations).
+ Input: a set of relations F whose instances can be altered during a
+ game; initial state structure S of the game; payoff of the game for a
+ player; advancement value ratio AR; for monotonic games, a mapping
+ from fluents to their preconditions (in the form of defined relations).
- Return a homomorphic image of the payoff which transforms Char(Phi)
- into H(Phi).
+ Return a homomorphic image of the payoff which transforms Char(Phi)
+ into H(Phi).
- The heuristic is generated differently for monotonic and
- nonmonotonic games. General case:
+ The heuristic is generated differently for monotonic and
+ nonmonotonic games. TODO: make the monotonic/nonmonotonic decision
+ at the level of subexpressions instead of the level of the whole
+ game.
- H(Phi) = Alg(FFTNF(promote relations F) of Phi', True)
- where Phi' = ExpandedForm(F, S, FFTNF(promote relations F) of Phi)
+ Fluents are relations that are changed by rules. Distinguish
+ two subclasses of fluents: positive fluents occur only positively on
+ RHSes (are only added) and only negatively on LHSes and in
+ preconditions, and negative fluents only negatively on RHSes (are only
+ deleted) and only positively on LHSes and in preconditions. (Call the
+ remaining fluents indefinite.) A game is monotonic, if its indefinite
+ fluents don't occur in any payoff of the game.
- Since formula transformations involved in generating the heuristic
- are costly, we use the parsimony model from FFTNF:
+ The monotonic-case heuristic is computed by pulling out
+ positive/negative occurrences of positive/negative fluents from
+ the formula; building a guard by substituting these by
+ preconditions (of their addition / deletion) and conjoining with
+ the rest of the formula; and counting the number of
+ positive/negative fluents that are already present/absent (as
+ required) under each match of the guard.
- (1) at parsimony level 1 (PARL1), we do not compute FFTNF prior to
- expanding the formula:
+ General case -- game is not monotonic:
- H(Phi) = Alg(FFTNF(promote relations F) of Phi', True)
- where Phi' = ExpandedForm(F, S, Phi)
+ H(Phi) = Alg(FFTNF(promote relations F) of Phi', True)
+ where Phi' = ExpandedForm(F, S, FFTNF(promote relations F) of Phi)
- (2) at parsimony level 2 (PARL2), we do not expand the formula:
+ Since formula transformations involved in generating the heuristic
+ are costly, we use the parsimony model from FFTNF:
- H(Phi) = Alg(FFTNF(promote relations F) of Phi, True)
+ (1) at parsimony level 1 (PARL1), we do not compute FFTNF prior to
+ expanding the formula:
- Monotonic case (see also the definition of FFSEP(F) in {!FFTNF}
- module):
+ H(Phi) = Alg(FFTNF(promote relations F) of Phi', True)
+ where Phi' = ExpandedForm(F, S, Phi)
- H(Phi) =
- Sum(V1, (F11\/...\/F1N_1) /\ Pre(F11/\.../\F1N_1) /\ Guard1,
- CharSum(F11, ..., F1N_1)) +
- ... +
- Sum(VM, (FM1\/...\/FMN_M) /\ Pre(FM1/\.../\FMN_M) /\ GuardM,
- CharSum(FM1, ..., FMN_M))
- where:
+ (2) at parsimony level 2 (PARL2), we do not expand the formula:
- * CharSum(Fi1, ..., FiN_i) = f(Char(Fi1) + ... + Char(FiN_i), N_i)
- CharSum() = 1 for N_i = 0
+ H(Phi) = Alg(FFTNF(promote relations F) of Phi, True)
- * f(n,N) = (1 + AR + ... + AR^n) / (1+AR+...+AR^N); f(0,N) = 0
- simpler variant: f(n,N) = n^AR/N^AR.
+ Monotonic case (see also the definition of FFSEP(PF,NF) in {!FFTNF}
+ module):
- * Pre() is the substitution of fluent precondition relations for
- fluents
+ H(Phi) =
+ Sum(V1, (F11\/...\/F1N_1) /\ Pre(F11/\.../\F1N_1) /\ Guard1,
+ CharSum(F11, ..., F1N_1)) +
+ ... +
+ Sum(VM, (FM1\/...\/FMN_M) /\ Pre(FM1/\.../\FMN_M) /\ GuardM,
+ CharSum(FM1, ..., FMN_M))
+ where:
- * (V1,F11,...,F1N_1,Guard1; ...; VM,FM1,...,FMN_M,GuardM) = FFSEP(F)(Phi)
+ * CharSum(Fi1, ..., FiN_i) = f(Char(Fi1) + ... + Char(FiN_i), N_i)
+ CharSum() = 1 for N_i = 0
- ** {F1, ..., FMN_M} are all fluent atoms that occur positively in Phi and
- whose free variables are contained in the existential prefix of
- PNF(Phi) (where PNF is "prenex normal, existential-first with
- minimized alternation, form")
+ * f(n,N) = (1 + AR + ... + AR^n) / (1+AR+...+AR^N); f(0,N) = 0
+ simpler variant: f(n,N) = n^AR/N^AR.
- ** (ex V1 (F11/\.../\F1N_1/\Guard1) \/ ...
- \/ ex VM (FM1/\.../\FMN_M/\GuardM))
- is equivalent to Phi with minimal application of distributivity
- (GuardI can contain disjunctions if they don't contain any of FIj)
+ * Pre() is the substitution of preconditions of adding/deleting
+ positive/negative fluents for the fluents
- **********
+ * (V1,F11,...,F1N_1,Guard1; ...; VM,FM1,...,FMN_M,GuardM)
+ = FFSEP(PF,NF)(Phi)
- Algorithm Alg(Ex(V,Phi), Guard0):
+ ** PF are positive fluents, NF are negative fluents of the game
- 1: Segregate Phi into Guard/\Subgoals where Guard is a boolean
- combination of atoms and quantified subformulas
- universal-in-positive / existential-in-negative positions, and each
- conjunct in Subgoals contains a positive occurrence of existential
- quantifier (not in scope of any other quantifier).
+ ** {F1, ..., FMN_M} are all positive/negative fluent atoms that
+ occur positively/negatively in Phi and whose free variables are
+ contained in the existential prefix of PNF(Phi) (where PNF is
+ "prenex normal, existential-first with minimized alternation,
+ form")
- 2: Reduce Subgoals to DNF treating quantified subformulas opaquely.
+ ** (ex V1 (F11/\.../\F1N_1/\Guard1) \/ ...
+ \/ ex VM (FM1/\.../\FMN_M/\GuardM))
+ is equivalent to Phi with minimal application of distributivity
+ (GuardI can contain disjunctions if they don't contain any of FIj)
- 3: Each disjunct Dj is a conjunction of literals and existentially
- quantified formulas. Split the conjuncts into existential
- quantifications {Ex(Vj1,Ej1), ..., Ex(Vjn,Ejn)} and others
- (Gj). Let
+ **********
- Rji=Alg(Ex(Vji,Eji),Gj)
+ Algorithm Alg(Ex(V,Phi), Guard0):
- and Wji be the weight assigned to Vji (see below) and PWji be the
- total weight of each root-leaf path in Rji. Let Rji' be Rji with
- all weights rescaled proportionally (Wji->Wji', but also other
- weights nested deeper in Rji) so that all PWji' are
- equal. Result for a disjunct j:
+ 1: Segregate Phi into Guard/\Subgoals where Guard is a boolean
+ combination of atoms and quantified subformulas
+ universal-in-positive / existential-in-negative positions, and each
+ conjunct in Subgoals contains a positive occurrence of existential
+ quantifier (not in scope of any other quantifier).
- DRj = normalized_mult(Rj1', ..., Rjn')
+ 2: Reduce Subgoals to DNF treating quantified subformulas opaquely.
- where
+ 3: Each disjunct Dj is a conjunction of literals and existentially
+ quantified formulas. Split the conjuncts into existential
+ quantifications {Ex(Vj1,Ej1), ..., Ex(Vjn,Ejn)} and others
+ (Gj). Let
- normalized_mult(x1,..,xn) = n^(n-1)*x1*...*xn / (x1+...+xn)^(n-1)
+ Rji=Alg(Ex(Vji,Eji),Gj)
- In each disjunct n>0, but Subgoals can be empty (m=0).
+ and Wji be the weight assigned to Vji (see below) and PWji be the
+ total weight of each root-leaf path in Rji. Let Rji' be Rji with
+ all weights rescaled proportionally (Wji->Wji', but also other
+ weights nested deeper in Rji) so that all PWji' are
+ equal. Result for a disjunct j:
- 4: Return
+ DRj = normalized_mult(Rj1', ..., Rjn')
- Sum(V, Guard0/\Guard, W + DR1 + ... + DRm)
+ where
- and PW=W+PW11', where W is Max_ji(Wji')/AR; the weights are
- assigned such that each path from root to leaf has the same weight
- (by rescaling Rji->Rji'). The (maximal) ratio of weight change towards
- the leaves (the "advancement value ratio") is a parameter (bigger
- means more stubborn, smaller means more undirected play).
+ normalized_mult(x1,..,xn) = n^(n-1)*x1*...*xn / (x1+...+xn)^(n-1)
- **********
+ In each disjunct n>0, but Subgoals can be empty (m=0).
- Tentative compact specification of ExpandedDescription:
+ 4: Return
- ExpandedDescription(S, T) of a set of substitutions T(x1,...,xn)
- (which can be seen as a set of n-tuples interpreting T in S) over
- elements a structure S is built from minimal sets of atoms Psi over
- variables (x1,...,xn,y1,...,yk) as "\/ ex y1,...,yk /\Psi" such
- that every "ex y1,...,yk /\Psi" is equivalent to T(x1,...,xn) in S
- (minimality means that for no proper subset Psi' of Psi is "ex
- y1,...,yk /\Psi'" equivalent to T(x1,...,xn) in
- S). ExpandedDescription may not exist for some pairs (S,T).
+ Sum(V, Guard0/\Guard, W + DR1 + ... + DRm)
- Maximal expanded description is an expanded description which
- cannot be extended with a disjunct nonequivalent to disjuncts
- actually present in it. The algorithm falls short of maximality
- because of parts marked as GREEDY (for the same reason the
- algorithm is not complete).
+ and PW=W+PW11', where W is Max_ji(Wji')/AR; the weights are
+ assigned such that each path from root to leaf has the same weight
+ (by rescaling Rji->Rji'). The (maximal) ratio of weight change towards
+ the leaves (the "advancement value ratio") is a parameter (bigger
+ means more stubborn, smaller means more undirected play).
- By ExpandedDescription(F, S, psi) (where psi is a formula not
- containing relations from F) we will denote
- ExpandedDescription(S',T) where T is a set of substitutions
- satisfying psi in S', and S' is S truncated to relations outside F.
-
- Algorithm for finding the ExpandedForm(F,S,Phi):
+ **********
- Let Phi=CDE(psi_1,...,psi_m) be a
- conjunctive-disjunctive-existential combination of
- (psi_1,...,psi_m), where each psi_i is either an atom, or has a
- conjunction, a negation or a quantification as its root.
+ Tentative compact specification of ExpandedDescription:
- ExpandedForm(F,S,Phi) = CDE(ED(psi_1), ..., ED(psi_m)), where
- "ED(psi) = ExpandedDescription(F,S,psi)" if psi does not contain
- relations from F and ExpandedDescription(F,S,psi) exists, otherwise
- "ED(psi_1 and ... and psi_n) = ED(psi_1) and ... and ED(psi_n)",
- "ED(ex x psi) = ex x ED(psi)", in other cases "ED(psi) = psi".
- (Where psi is either a formula or a set of all satisfying
- substitutions for psi in S, depending on context.)
-
- Algorithm for finding ExpandedDescription(F, S, T):
+ ExpandedDescription(S, T) of a set of substitutions T(x1,...,xn)
+ (which can be seen as a set of n-tuples interpreting T in S) over
+ elements a structure S is built from minimal sets of atoms Psi over
+ variables (x1,...,xn,y1,...,yk) as "\/ ex y1,...,yk /\Psi" such
+ that every "ex y1,...,yk /\Psi" is equivalent to T(x1,...,xn) in S
+ (minimality means that for no proper subset Psi' of Psi is "ex
+ y1,...,yk /\Psi'" equivalent to T(x1,...,xn) in
+ S). ExpandedDescription may not exist for some pairs (S,T).
- Build a forest of atoms as follows:
+ Maximal expanded description is an expanded description which
+ cannot be extended with a disjunct nonequivalent to disjuncts
+ actually present in it. The algorithm falls short of maximality
+ because of parts marked as GREEDY (for the same reason the
+ algorithm is not complete).
- (0) For a path in a tree, maintain substitutions that satisfy the
- path atoms, partitioned into classes of substitutions extending a
- substitution satisfying T (called "inside classes" below), plus a
- class of substitutions that do not satisfy T (called "outside
- class" below).
-
- (a) To add an atom of a relation R to the forest: Take the
- pre-image (i.e. one-to-many) of the tuples of the relation R
- through a substitution, add new variables if they are not yet in
- substitutions, and take cartesian product.
+ By ExpandedDescription(F, S, psi) (where psi is a formula not
+ containing relations from F) we will denote
+ ExpandedDescription(S',T) where T is a set of substitutions
+ satisfying psi in S', and S' is S truncated to relations outside F.
+
+ Algorithm for finding the ExpandedForm(F,S,Phi):
- (b) Filter the tuples so that if new variables are being added (not
- yet in substitutions), each tuple has some old variable and new
- variables form "triangluar matrix" (reducing "repetition modulo
- renaming variables").
+ Let Phi=CDE(psi_1,...,psi_m) be a
+ conjunctive-disjunctive-existential combination of
+ (psi_1,...,psi_m), where each psi_i is either an atom, or has a
+ conjunction, a negation or a quantification as its root.
- (c) Filter the tuples so that all new variables are present in each
- tuple (even if new variabl...
[truncated message content] |
