[Toss-devel-svn] SF.net SVN: toss:[1210] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1210] trunk/Toss
|
From: <luk...@us...> - 2010-11-30 00:13:33
|
Revision: 1210
http://toss.svn.sourceforge.net/toss/?rev=1210&view=rev
Author: lukstafi
Date: 2010-11-30 00:13:26 +0000 (Tue, 30 Nov 2010)
Log Message:
-----------
Heuristic: clarified handling of quantifiers. FFTNF: subtasks bugfixes and cleanup. FFSolver: extensive diagnostic logging, disjunction rewrite bugfixes.
Modified Paths:
--------------
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Formula/FFTNFTest.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Solver/FFSolver.ml
trunk/Toss/Solver/FFSolverTest.ml
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Formula/FFTNF.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -259,7 +259,7 @@
and tree_node =
| TProc of int * formula (* processed literal *)
| TLit of formula (* unprocessed literal *)
- | TNot_subtask of tree_node
+ | TNot_subtask of formula
(* process recursively separately from the rest, doesn't have free
variables *)
| TAnd of tree list
@@ -344,7 +344,7 @@
let rec aux = function
| {t=TProc (_,lit)} -> lit
| {t=TLit lit} -> lit
- | {t=TNot_subtask subt} -> Not (aux {fvs=Vars.empty; t=subt})
+ | {t=TNot_subtask subt} -> Not subt
| {t=TAnd subts} -> And (List.map aux subts)
| {t=TOr subts} -> Or (List.map aux subts)
| {t=TAll (vs, subt)} -> All (Vars.elements vs, aux subt)
@@ -504,52 +504,12 @@
{fvs=Vars.empty; t=TAnd (subts_proc @ subts)}
| {t=TAll (vs, phi)} ->
- let phi = loop phi in
- begin match phi with
- | {t=TAnd conjs} ->
- let task_conjs, conjs =
- Aux.partition_map (function
- | {t=TNot_subtask _} as subt -> Left subt
- | subt -> Right subt) conjs in
- if task_conjs <> [] then
- {fvs=Vars.empty; t=TAnd (task_conjs @ [
- {fvs=Vars.empty; t=TAll (vs, {fvs=Vars.empty; t=TAnd conjs})}
- ])}
- else
- {fvs=Vars.empty; t=TAll (vs, {fvs=Vars.empty; t=TAnd conjs})}
- | _ ->
- {fvs=Vars.empty; t=TAll (vs, phi)}
- end
+ {fvs=Vars.empty; t=TAll (vs, loop phi)}
| {t=TEx (vs, phi)} ->
- let phi = loop phi in
- begin match phi with
- | {t=TAnd conjs} ->
- let task_conjs, conjs =
- Aux.partition_map (function
- | {t=TNot_subtask _} as subt -> Left subt
- | subt -> Right subt) conjs in
- if task_conjs <> [] then
- {fvs=Vars.empty; t=TAnd (task_conjs @ [
- {fvs=Vars.empty; t=TEx (vs, {fvs=Vars.empty; t=TAnd conjs})}
- ])}
- else
- {fvs=Vars.empty; t=TEx (vs, {fvs=Vars.empty; t=TAnd conjs})}
- | _ ->
- {fvs=Vars.empty; t=TEx (vs, phi)}
- end
+ {fvs=Vars.empty; t=TEx (vs, loop phi)}
- | {t=TNot_subtask phi} ->
- begin
- try
- let phi = loop {fvs=Vars.empty; t=phi} in
- {fvs=Vars.empty; t=TNot_subtask phi.t}
- with
- | Simpl_true -> raise Simpl_false
- | Simpl_false -> raise Simpl_true
- end
-
- | ({t=TLit _} | {t=TProc _}) as lit -> lit in
+ | {t=TNot_subtask _} | ({t=TLit _} | {t=TProc _}) as proc -> proc in
try formula_of_tree (loop tree) with
| Simpl_true -> And []
@@ -575,8 +535,8 @@
prefix Top (p_pn_nnf phi) in
let phi = FormulaOps.flatten_formula phi in
let rec to_tree = function
- | Not (Ex _ as phi) ->
- {fvs=Vars.empty; t=TNot_subtask (to_tree phi).t}
+ | Not (Ex _ as phi) -> (* assumes [phi] is ground! *)
+ {fvs=Vars.empty; t=TNot_subtask phi}
| (Rel _ | Eq _ | In _ | RealExpr _ | Not _) as lit ->
{fvs=vars_of_list (FormulaOps.all_vars lit); t=TLit lit}
| And conjs ->
@@ -707,7 +667,8 @@
match task_lit with
| Left subt ->
Vars.empty,
- lazy {fvs=Vars.empty; t=TProc (task_id, Not (subproc subt))}
+ (* it's a TNot_subtask, the negation is added by [subproc] *)
+ lazy {fvs=Vars.empty; t=TProc (task_id, subproc subt)}
| Right (lit, lit_vs) ->
lit_vs, lazy {fvs=lit_vs; t=TProc (task_id, lit)} in
match loc.x with
@@ -917,8 +878,7 @@
let _ = if !debug_level > 2 then begin
printf "\nfound_subtask-literal: %s\n"
(match subt_lit with
- | Left subt ->
- Formula.str (formula_of_tree {fvs=Vars.empty;t=subt})
+ | Left subt -> Formula.str (Not subt)
| Right (lit,_) -> Formula.str lit);
printf "location: %s\n" (location_str loc) end in
let phi = pull_out subproc (i, subt_lit) loc in
@@ -934,8 +894,12 @@
result
and subproc subt =
- let loc = {x=Top; n={fvs=Vars.empty; t=subt}} in
- flatten_tree_to_formula (loop 0 loc) in
+ let loc = init subt in
+ let _ = if !debug_level > 2 then
+ printf "\ninit_subtask_location: %s\n" (location_str loc) in
+ (* Whatever the recursive call result, it will not spoil the TNF
+ property because we must land outside of quantifiers anyway. *)
+ Not (flatten_tree_to_formula (loop 0 loc)) in
let res = loop 0 loc in
if !debug_level > 1 then
Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Formula/FFTNFTest.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -177,7 +177,7 @@
(formula_of_str "ex x, y, z (C(x, z) and ((R(x,y) and (P(x) or C(y,z))) or Q(z)))")));
);
- "ff_tnf: subtasks" >::
+ "ff_tnf: simple subtasks" >::
(fun () ->
assert_equal ~printer:(fun x->x)
"(not ex z (((not Q(z)) and (ex x, y ((not R(x, y))) or ex y (((not C(y, z)) and ex x ((not P(x)))))))))"
@@ -192,6 +192,24 @@
(formula_of_str "ex x, y (C(x, y) or (P(y) and all z Q(z)))")));
);
+ "ff_tnf: tic-tac-toe subtask" >::
+ (fun () ->
+ let heur_phi = "(((R(x, y) and R(y, z)) or
+ (C(x, y) and C(y, z)) or ex t, u
+ ((C(z, u) and R(y, u) and C(y, t) and R(x, t))) or ex t, u ((R(y, u) and R(x, t) and C(u, z) and C(t, y))))
+ and (Q(z) or Q(y) or Q(x))
+ and (not P(x)) and (not P(y)) and (not P(z))" ^
+ "and (not ex x, y, z ((((C(y, z) and C(x, y)) or (R(y, z) and R(x, y)) or
+ ex t, u ((R(y, u) and R(x, t) and C(u, z)
+ and C(t, y))) or ex t, u ((C(z, u) and
+ R(y, u) and C(y, t) and R(x, t)))) and P(z) and P(y) and P(x)))))" in
+ assert_equal ~printer:(fun x->x)
+ "((not ex x ((P(x) and (ex y ((C(x, y) and P(y) and ex z ((C(y, z) and P(z))))) or ex y ((R(x, y) and P(y) and ex z ((R(y, z) and P(z))))) or ex t ((R(x, t) and ex y ((C(y, t) and P(y) and ex u ((R(y, u) and ex z ((C(z, u) and P(z))))))))) or ex t0 ((R(x, t0) and ex y ((C(t0, y) and P(y) and ex u0 ((R(y, u0) and ex z ((C(u0, z) and P(z))))))))))))) and (not P(x)) and (not P(z)) and (not P(y)) and ((R(y, z) and R(x, y)) or (C(y, z) and C(x, y)) or ex t ((C(t, y) and R(x, t) and ex u ((R(y, u) and C(u, z))))) or ex t0 ((R(x, t0) and C(y, t0) and ex u0 ((C(z, u0) and R(y, u0)))))) and (Q(x) or Q(z) or Q(y)))"
+ (Formula.str (FFTNF.ff_tnf
+ (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
+ (formula_of_str heur_phi)));
+ );
+
]
let a =
Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Play/Heuristic.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -50,15 +50,18 @@
Algorithm Alg(Ex(V,Phi), Guard0):
- 1: Segregate Phi into Guard/\Subgoals where Guard is a conjunction
- of formulas without existential quantifiers and each conjunct in
- Subgoals contains an existential quantifier.
+ 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).
2: Reduce Subgoals to DNF treating quantified subformulas opaquely.
- 3: Each disjunct Dj is a conjunction of literals and quantified
- formulas. Split the conjuncts into existential quantifications
- {Ex(Vj1,Ej1), ..., Ex(Vjn,Ejn)} and others (Gj). Let
+ 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)
@@ -662,15 +665,15 @@
| And conjs ->
gproduct List.append [] (List.map (limited_dnf neg) conjs)
| Or disjs -> Aux.concat_map (limited_dnf neg) disjs
- | Ex (vs, psi) as phi ->
- [[if neg then All (vs, Not psi) else phi]]
+ | Ex _ as phi ->
+ [[if neg then Not phi else phi]]
| All (vs, psi) as phi ->
[[if neg then Ex (vs, Not psi) else phi]]
-let rec has_existential = function
- | Not phi -> has_existential phi
- | And phs | Or phs -> List.exists has_existential phs
- | Ex _ -> true | _ -> false
+let rec has_pos_existential ?(neg=false) = function
+ | Not phi -> has_pos_existential ~neg:(not neg) phi
+ | And phs | Or phs -> List.exists (has_pos_existential ~neg) phs
+ | Ex _ -> not neg | All _ -> neg | _ -> false
let rec map_constants f = function
@@ -714,7 +717,7 @@
let conjs = match phi with
| And conjs | Or [And conjs] -> conjs
| _ -> [phi] in
- let subgoals, guard = List.partition has_existential conjs in
+ let subgoals, guard = List.partition has_pos_existential conjs in
if subgoals = [] then
(* bottoming-out of recursion; [Const 1.] is the weight *)
if vs = [] then
@@ -789,15 +792,6 @@
) guards in
sum_exprs parts
-let has_universal phi=
- let rec aux neg = function
- | Not phi -> aux (not neg) phi
- | And phs | Or phs -> List.exists (aux neg) phs
- | All (_, phi) -> not neg || aux neg phi
- | Ex (_, phi) -> neg || aux neg phi
- | _ -> false in
- aux false phi
-
let of_payoff ?(max_alt_descr=5) ?struc ?fluent_preconds adv_ratio frels expr =
(* FIXME: what [gds] should be doing? it's not doing anything *)
let rec aux gds = function
Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Play/HeuristicTest.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -276,7 +276,7 @@
"of_payoff: non-existential" >::
(fun () ->
assert_equal ~printer:(fun x->x)
- "((0.66 + (1. * :(all x (P(x))))) + Sum (y | (Q(y) and all z (R(y, z))) : 1.))"
+ "((0.66 + (1. * :((not ex x ((not P(x))))))) + Sum (y | (Q(y) and all z (R(y, z))) : 1.))"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(Heuristic.of_payoff 1.5
Modified: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Solver/FFSolver.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -149,7 +149,7 @@
map_try ?catch f tl
let rec fold_try ?catch f accu = function
- | [] -> []
+ | [] -> accu
| hd::tl ->
try
fold_try ?catch f (f accu hd) tl
@@ -212,6 +212,35 @@
failwith "FFSolver: Real/MSO assignments not supported yet" in
aux aset
+let rec aset_fo_vars = function
+ | A.Empty | A.Any -> []
+ | A.FO (v, assgns) ->
+ v :: Aux.concat_map aset_fo_vars (List.map snd assgns)
+ | A.Real _ | A.MSO _ ->
+ failwith "FFSolver: Real/MSO assignments not supported yet"
+
+(* For debugging. Brute force check. *)
+let aset_subsumed all_elems a b =
+ let vars = aset_fo_vars a in
+ let asbs = A.fo_assgn_to_list all_elems vars a in
+ let asbs =
+ Aux.unique (=) (List.map (List.sort Pervasives.compare) asbs) in
+ let bsbs = A.fo_assgn_to_list all_elems vars b in
+ let asbs =
+ Aux.unique (=) (List.map (List.sort Pervasives.compare) bsbs) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ printf "subsumption: test %d <= %d\n%!"
+ (List.length asbs) (List.length bsbs);
+ );
+ (* }}} *)
+ List.for_all (fun asb ->
+ List.exists (fun bsb ->
+ try
+ List.for_all (fun (v,ae) ->
+ List.assoc v bsb = ae) asb
+ with Not_found -> false) bsbs) asbs
+
(* We assume that for every "not ex
psi" subformula, "ex psi" is ground, and that every other
occurrence of negation is in a literal (it is guaranteed by
@@ -284,7 +313,8 @@
(e4) apply the case (c)
*)
-let rec merge all_elems v init_domain sb cur_aset eval_cont =
+(* Model used only for debugging. *)
+let rec merge model all_elems v init_domain sb cur_aset eval_cont =
match cur_aset with
| A.MSO _ | A.Real _ -> failwith
"FFSolver.evaluate: MSO and Real not supported yet"
@@ -329,12 +359,13 @@
e, project_v_on_elem v e cur_aset in
let cur_aset =
A.FO (v, map_try pull_v all_elems) in
- merge all_elems v init_domain sb cur_aset eval_cont
+ merge model all_elems v init_domain sb cur_aset eval_cont
(* "Negate" the second assignment set wrt. [all_elems] and add it to the
first aset. *)
-let rec add_complement all_elems disj_aset = function
+(* Model used only for debugging. *)
+let rec add_complement model all_elems disj_aset = function
| A.Empty -> A.Any
| A.Any ->
if disj_aset = A.Empty then raise Unsatisfiable;
@@ -346,14 +377,21 @@
let cset =
(* Empty will turn into Any on recursive callback *)
try List.assoc e assgns with Not_found -> A.Empty in
- add_complement all_elems dset cset in
- merge all_elems v all_elems [] disj_aset add_cont
+ add_complement model all_elems dset cset in
+ merge model all_elems v all_elems [] disj_aset add_cont
| A.Real _ | A.MSO _ ->
failwith "FFSolver: Real/MSO assignments not supported yet"
let evaluate model ?(sb=[]) ?(disj_aset=A.Empty) phi =
+ (* {{{ log entry *)
+ let guard_number = ref 0 in
+ if !debug_level > 1 then (
+ printf "evaluate: phi=%s; sb=%s; disj_aset=%s\n%!"
+ (Formula.str phi) (sb_str model sb) (AssignmentSet.named_str model disj_aset);
+ );
+ (* }}} *)
let all_elems = Elems.elements model.elements in
let num_elems = Elems.cardinal model.elements in
@@ -369,17 +407,37 @@
Do not return [A.Empty], raise [Unsatisfiable] instead. *)
let rec solve delayed2 delayed1 conj_cont sb cur_aset =
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ printf "solve: remaining=%s\nsolve: sb=%s\nsolve: disj_aset=%s\n%!"
+ (Formula.str (And (conj_cont @ delayed1 @ delayed2))) (sb_str model sb) (AssignmentSet.named_str model cur_aset);
+ );
+ (* }}} *)
(* a *)
- if cur_aset = A.Any then A.Any
- else match conj_cont with
+ if cur_aset = A.Any then (
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "a: cur_aset=Any subsuming phi=%s\n%!"
+ (Formula.str (And (conj_cont @ delayed1 @ delayed2)))
+ );
+ (* }}} *)
+ A.Any
+ ) else match conj_cont with
| [] ->
if delayed1 <> []
then solve delayed2 [] (List.rev delayed1) sb cur_aset
else if delayed2 <> []
then solve [] [] (List.rev delayed2) sb cur_aset
(* b *)
- else A.Any (* subsuming [cur_aset] *)
-
+ else (
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "b: phi=[] subsuming cur_aset=%s\n%!"
+ (AssignmentSet.named_str model cur_aset);
+ );
+ (* }}} *)
+ A.Any (* subsuming [cur_aset] *)
+ )
| Rel (relname, vtup) as atom :: conj_cont ->
let tuples_s =
try StringMap.find relname model.relations
@@ -393,7 +451,7 @@
then solve delayed2 [] (List.rev delayed1) sb cur_aset
else solve [] [] (List.rev delayed2) sb cur_aset
with Not_found ->
- (* we will add new variables one at a time *)
+ (* we will add new variables one at a time *)
let nvi =
Aux.array_argfind (fun v->not (List.mem_assoc v sb)) vtup in
let nvar = vtup.(nvi) in
@@ -404,9 +462,9 @@
if multi_unkn && conj_cont <> [] then (* delay *)
solve delayed2 (atom::delayed1) conj_cont sb cur_aset
else
- (* to narrow the domain, lookup incidence of known vars,
- filter for partial match and project on the nvar
- position *)
+ (* to narrow the domain, lookup incidence of known vars,
+ filter for partial match and project on the nvar
+ position *)
let tuples_i =
try StringMap.find relname model.incidence
with Not_found -> IntMap.empty in
@@ -433,20 +491,28 @@
&& not (List.mem tup.(nvi) dom)
then tup.(nvi)::dom
else dom) tuples [] in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
+ (sb_str model sb) (Formula.str atom)
+ (String.concat ", " (List.map (Structure.elem_str model)
+ init_domain));
+ );
+ (* }}} *)
if init_domain = []
then raise
(Unsatisfiable_FO (vars_of_array (var_tup vtup)))
else if not multi_unkn && conj_cont = [] && delayed1 = [] &&
delayed2 = []
then (* no more vars and conjuncts *)
- merge all_elems nvar init_domain sb cur_aset
+ merge model all_elems nvar init_domain sb cur_aset
(fun _ _ -> A.Any) (* subsume *)
else
let conj_cont =
if multi_unkn then atom::conj_cont else conj_cont in
(* If not [multi_unkn] then for elements in [init_domain]
rel holds *)
- merge all_elems nvar init_domain sb cur_aset
+ merge model all_elems nvar init_domain sb cur_aset
(solve delayed2 delayed1 conj_cont)
)
@@ -458,7 +524,7 @@
then raise (Unsatisfiable_FO (vars_of_list (vtup :> var list)))
else solve delayed2 delayed1 conj_cont sb cur_aset
with Not_found ->
- (* we will add new variables one at a time *)
+ (* we will add new variables one at a time *)
let nvi, nvar =
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
@@ -470,16 +536,29 @@
solve (atom::delayed2) delayed1 conj_cont sb cur_aset
else if multi_unkn then
let conj_cont = atom::conj_cont in
- merge all_elems nvar all_elems sb cur_aset
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS\n%!"
+ (sb_str model sb) (Formula.str atom);
+ );
+ (* }}} *)
+ merge model all_elems nvar all_elems sb cur_aset
(solve delayed2 delayed1 conj_cont)
else
let ovar = if nvi = 1 then x else y in
let e = List.assoc ovar sb in
- merge all_elems nvar [e] sb cur_aset
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
+ (sb_str model sb) (Formula.str atom)
+ (Structure.elem_str model e);
+ );
+ (* }}} *)
+ merge model all_elems nvar [e] sb cur_aset
(solve delayed2 delayed1 conj_cont)
)
- (* by analogy to the [Rel (relname, vtup)] case *)
+ (* by analogy to the [Rel (relname, vtup)] case *)
| Not (Rel (relname, vtup)) as literal :: conj_cont ->
let tuples_s =
try StringMap.find relname model.relations
@@ -494,7 +573,7 @@
then solve delayed2 [] (List.rev delayed1) sb cur_aset
else solve [] [] (List.rev delayed2) sb cur_aset
with Not_found ->
- (* we will add new variables one at a time *)
+ (* we will add new variables one at a time *)
let nvi =
Aux.array_argfind (fun v->not (List.mem_assoc v sb)) vtup in
let nvar = vtup.(nvi) in
@@ -509,9 +588,9 @@
then
solve delayed2 (literal::delayed1) conj_cont sb cur_aset
else if multi_unkn then
- (* we cannot easily optimize *)
+ (* we cannot easily optimize *)
let conj_cont = [literal] in
- merge all_elems nvar all_elems sb cur_aset
+ merge model all_elems nvar all_elems sb cur_aset
(solve delayed2 delayed1 conj_cont)
else
let tuples_i =
@@ -540,12 +619,20 @@
then Elems.add tup.(nvi) dom
else dom) tuples Elems.empty in
Elems.elements (Elems.diff model.elements init_domain_co) in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=%s\n%!"
+ (sb_str model sb) (Formula.str literal)
+ (String.concat ", " (List.map (Structure.elem_str model)
+ init_domain));
+ );
+ (* }}} *)
if init_domain = []
then raise Unsatisfiable
else
(* If not [multi_unkn] then for elements in [init_domain]
rel does not hold *)
- merge all_elems nvar init_domain sb cur_aset
+ merge model all_elems nvar init_domain sb cur_aset
(solve delayed2 delayed1 conj_cont)
)
@@ -557,7 +644,7 @@
then raise (Unsatisfiable_FO (vars_of_list ([x; y] :> var list)))
else solve delayed2 delayed1 conj_cont sb cur_aset
with Not_found ->
- (* we will add new variables one at a time *)
+ (* we will add new variables one at a time *)
let nvi, nvar =
if List.mem_assoc x sb then 1, y else 0, x in
let oldvars =
@@ -569,15 +656,28 @@
solve (literal::delayed2) delayed1 conj_cont sb cur_aset
else if not multi_unkn && conj_cont <> [] then
solve delayed2 (literal::delayed1) conj_cont sb cur_aset
- else if multi_unkn then
- merge all_elems nvar all_elems sb cur_aset
+ else if multi_unkn then begin
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS\n%!"
+ (sb_str model sb) (Formula.str literal);
+ );
+ (* }}} *)
+ merge model all_elems nvar all_elems sb cur_aset
(solve delayed2 delayed1 (literal :: conj_cont))
- else (* optimize *)
+ end else (* optimize *)
let ovar = if nvi = 1 then x else y in
let e = List.assoc ovar sb in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "init_domain: sb=%s; phi=%s; dom=ALL ELEMS - %s\n%!"
+ (sb_str model sb) (Formula.str literal)
+ (Structure.elem_str model e);
+ );
+ (* }}} *)
let init_domain =
Elems.elements (Elems.remove e model.elements) in
- merge all_elems nvar init_domain sb cur_aset
+ merge model all_elems nvar init_domain sb cur_aset
(solve delayed2 delayed1 conj_cont)
)
@@ -593,13 +693,25 @@
(* Propagate implication constraints. *)
| Or fl :: conj_cont when List.exists
(function Not _ -> true | _ -> false) fl ->
+ (* {{{ log entry *)
+ let cur_guard = !guard_number in
+ if !debug_level > 2 then (
+ printf "Computing guard no %d..." cur_guard; incr guard_number;
+ );
+ (* }}} *)
let guard, body = Aux.partition_map
(function Not phi -> Aux.Left phi | phi -> Aux.Right phi) fl in
- (* assignments of the guard alone *)
+ (* assignments of the guard alone *)
let guard_set =
try solve [] [] guard sb A.Empty
with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty in
- let cur_aset = add_complement all_elems cur_aset guard_set in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Guard: no %d guard_set=%s\nBody: %s\n%!" cur_guard
+ (AssignmentSet.named_str model guard_set) (Formula.str (Or body));
+ );
+ (* }}} *)
+ let cur_aset = add_complement model all_elems cur_aset guard_set in
if body = [] || guard_set = A.Empty then
(* the positive part is in effect false -- discard it *)
solve delayed2 delayed1 conj_cont sb cur_aset
@@ -612,34 +724,100 @@
solve delayed2 delayed1 (guard @ [concl] @ conj_cont) sb cur_aset
(* Continue in each branch folding disjuncts; "Or []" is OK. *)
- | Or fl :: conj_cont ->
- List.fold_left (fun dset phi ->
- solve delayed2 delayed1 (phi::conj_cont) sb dset) A.Empty fl
+ | Or fl :: conj_cont ->
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Folding-disjunctively-over: %s\ndisjunct-continuation: %s\n%!"
+ (Formula.str (Or fl)) (Formula.str (And conj_cont));
+ );
+ (* }}} *)
+ fold_try (fun dset phi ->
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ printf "disjunct: %s; prior dset=%s\n%!"
+ (Formula.str phi) (AssignmentSet.named_str model dset);
+ );
+ (* }}} *)
+ solve delayed2 delayed1 (phi::conj_cont) sb dset)
+ cur_aset fl
| Ex ([], phi) :: _ | All ([], phi) :: _ -> assert false
- (* Only project, as the mechanics of existential variables is
- handled at the site of their first occurrence. *)
+ (* Only project, as the mechanics of existential variables is
+ handled at the site of their first occurrence. *)
| Ex (vl, phi) :: conj_cont ->
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solving-for-existential-variables: %s...\n%!"
+ (String.concat ", " (List.map Formula.var_str vl));
+ );
+ (* }}} *)
let aset = solve delayed2 delayed1 (phi::conj_cont) sb cur_aset in
- (* TODO: handle other kinds *)
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solved-variables: %s; aset=%s\n%!"
+ (String.concat ", " (List.map Formula.var_str vl))
+ (AssignmentSet.named_str model aset);
+ );
+ (* }}} *)
+ (* TODO: handle other kinds *)
let vl = List.map to_fo vl in
- List.fold_left (project all_elems) aset vl
+ let aset = List.fold_left (project all_elems) aset vl in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Eliminated-variables: %s; aset=%s\n%!"
+ (String.concat ", " (List.map Formula.var_str vl))
+ (AssignmentSet.named_str model aset);
+ );
+ (* }}} *)
+ aset
- (* Check whether assignment set covers all elements for variables
- [vl]. *)
+ (* Check whether assignment set covers all elements for variables
+ [vl]. *)
| All (vl, phi) :: conj_cont ->
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solving-for-universal-variables: %s...\n%!"
+ (String.concat ", " (List.map Formula.var_str vl));
+ );
+ (* }}} *)
let aset = solve delayed2 delayed1 (phi::conj_cont) sb cur_aset in
- (* TODO: handle other kinds *)
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solved-variables: %s; aset=%s\n%!"
+ (String.concat ", " (List.map Formula.var_str vl))
+ (AssignmentSet.named_str model aset);
+ );
+ (* }}} *)
+ (* TODO: handle other kinds *)
let vl = List.map to_fo vl in
- List.fold_left (universal num_elems all_elems) aset vl
+ let aset =
+ List.fold_left (universal num_elems all_elems) aset vl in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Eliminated-variables: %s; aset=%s\n%!"
+ (String.concat ", " (List.map Formula.var_str vl))
+ (AssignmentSet.named_str model aset);
+ );
+ (* }}} *)
+ aset
- (* By assumption that [Ex (vl, phi)] is ground, check it
- separately and proceed or fail. *)
- | Not (Ex (vl, phi)) :: conj_cont ->
+ (* By assumption that [phi] is ground, check it
+ separately and proceed or fail. *)
+ | Not phi as subtask :: conj_cont ->
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solving-a-subtask: %s...\n" (Formula.str subtask);
+ );
+ (* }}} *)
let aset =
- try solve [] [] [phi] sb cur_aset
+ (* solving in empty context! *)
+ try solve [] [] [phi] [] A.Empty
with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty in
+ if !debug_level > 2 then (
+ printf "Solved-subtask: %s\nsubtask: aset=%s\n%!"
+ (Formula.str subtask) (AssignmentSet.named_str model aset);
+ );
if aset = A.Empty then
solve delayed2 delayed1 conj_cont sb cur_aset
else raise Unsatisfiable
@@ -647,11 +825,7 @@
| RealExpr _ :: _ | In _ :: _ ->
failwith
"FFSolver: MSO and Reals not implemented yet."
- | Not phi :: _ ->
- failwith (
- "FFSolver: formula not in partially-negation-normal form: "
- ^ "negation over " ^ Formula.str phi)
-
+
(*
and solve_db sb delayed2 delayed1 conj_cont =
let count = !debug_count in
Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml 2010-11-29 20:19:39 UTC (rev 1209)
+++ trunk/Toss/Solver/FFSolverTest.ml 2010-11-30 00:13:26 UTC (rev 1210)
@@ -151,8 +151,32 @@
(AssignmentSet.str (FFSolver.evaluate model phi))
);
- "eval: game heuristic tests from SolverTest.ml" >::
+
+ "eval: tic-tac-toe heuristic" >::
(fun () ->
+ let heur_phi = "(((R(x, y) and R(y, z)) or
+ (C(x, y) and C(y, z)) or ex t, u
+ ((C(z, u) and R(y, u) and C(y, t) and R(x, t))) or ex t, u ((R(y, u) and R(x, t) and C(u, z) and C(t, y))))
+ and (Q(z) or Q(y) or Q(x))
+ and (not P(x)) and (not P(y)) and (not P(z))" ^
+ "and (not ex x, y, z ((((C(y, z) and C(x, y)) or (R(y, z) and R(x, y)) or
+ ex t, u ((R(y, u) and R(x, t) and C(u, z)
+ and C(t, y))) or ex t, u ((C(z, u) and
+ R(y, u) and C(y, t) and R(x, t)))) and P(z) and P(y) and P(x)))))" in
+ (* FFSolver.debug_level := 7; *)
+ eval_eq "[ | | ] \"
+
+Q P P
+
+. P .
+
+. Q .
+\"" heur_phi
+ "{ z->a3{ y->a2{ x->a1 } } , z->c1{ y->b1{ x->a1 } } }";
+ );
+
+ "eval: gomoku heuristic from SolverTest.ml" >::
+ (fun () ->
let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or
(C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u
((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s)
@@ -166,6 +190,7 @@
and C(t, y) and C(s, x) and C(r, w))) or ex r, s, t, u ((C(z, u) and
R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and
R(v, r)))) and P(z) and P(y) and P(x) and P(w) and P(v)))))" in
+ (* FFSolver.debug_level := 7; *)
eval_eq "[ | | ] \"
... ... ... ...
P ... ... ... ...
@@ -183,18 +208,8 @@
...P ... P.. ...
... ... ... ...
... ... ...Q ...
-\"" heur_phi
- ("{ z->5{ y->12{ x->19{ w->26{ v->33 } } } } ," ^
- " z->6{ y->5{ x->4{ w->3{ v->2 } } } } ," ^
- " z->7{ y->6{ x->5{ w->4{ v->3 } } } } ," ^
- " z->8{ y->7{ x->6{ w->5{ v->4 } } } } ," ^
- " z->32{ y->39{ x->46{ w->53{ v->60 } } } } ," ^
- " z->48{ y->47{ x->46{ w->45{ v->44 } } } } ," ^
- " z->53{ y->44{ x->35{ w->26{ v->17 } } } } ," ^
- " z->58{ y->50{ x->42{ w->34{ v->26 } } } } ," ^
- " z->62{ y->53{ x->44{ w->35{ v->26 } } } } ," ^
- " z->63{ y->54{ x->45{ w->36{ v->27 } } } } }");
- );
+\"" heur_phi
+ "{ y->d6{ z->e7{ x->c5{ v->a3{ w->b4 } } } } , y->e1{ x->d1{ v->b1{ z->f1{ w->c1 } } } } , y->f1{ x->e1{ v->c1{ z->g1{ w->d1 } } } } , y->g1{ x->f1{ v->d1{ w->e1{ z->h1 } } } } , y->d2{ x->c3{ v->a5{ z->e1{ w->b4 } } } } , y->g5{ x->f6{ v->d8{ w->e7{ z->h4 } } } } , y->g6{ x->f6{ v->d6{ w->e6{ z->h6 } } } } , y->b7{ x->b6{ v->b4{ w->b5{ z->b8 } } } } , y->e7{ x->d6{ z->f8{ v->b4{ w->c5 } } } } , y->f7{ x->e6{ z->g8{ v->c4{ w->d5 } } } } }");
"get_real_val: tic-tac-toe winning" >::
(fun () ->
@@ -273,7 +288,7 @@
\"" in
(* FFTNF.debug_level := 3; *)
assert_equal ~printer:(fun x->x)
- "((not ex x ((Q(x) and (ex y ((C(x, y) and Q(y) and ex z ((C(y, z) and Q(z))))) or ex y ((R(x, y) and Q(y) and ex z ((R(y, z) and Q(z))))) or ex y ((Q(y) and ex z ((Q(z) and (ex v0 ((R(x, v0) and C(y, v0) and ex u0 ((R(y, u0) and C(z, u0))))) or ex v ((R(x, v) and C(v, y) and ex u ((R(y, u) and C(u, z)))))))))))))) and ((not P(a1)) and (not Q(a1))))"
+ "((not ex x ((Q(x) and (ex y ((C(x, y) and Q(y) and ex z ((C(y, z) and Q(z))))) or ex y ((R(x, y) and Q(y) and ex z ((R(y, z) and Q(z))))) or ex v0 ((R(x, v0) and ex y ((C(y, v0) and Q(y) and ex u0 ((R(y, u0) and ex z ((C(z, u0) and Q(z))))))))) or ex v ((R(x, v) and ex y ((C(v, y) and Q(y) and ex u ((R(y, u) and ex z ((C(u, z) and Q(z))))))))))))) and ((not P(a1)) and (not Q(a1))))"
(Formula.str (FFSolver.normalize_for_model
tictactoe_init tictactoe_LHS));
);
@@ -296,7 +311,9 @@
\"" in
(* FFTNF.debug_level := 3; *)
assert_equal ~printer:(fun x->x)
- "((not ex z0 ((P(z0) and (ex y0 ((R(y0, z0) and P(y0) and ex x0 ((R(x0, y0) and P(x0))))) or ex y0 ((C(y0, z0) and P(y0) and ex x0 ((C(x0, y0) and P(x0))))) or ex y0 ((P(y0) and ex x0 ((P(x0) and (ex u ((C(z0, u) and R(y0, u) and ex v ((C(y0, v) and R(x0, v))))) or ex u0 ((C(u0, z0) and R(y0, u0) and ex v0 ((C(v0, y0) and R(x0, v0)))))))))))))) and ((P(z) and (not Q(z)) and (C(y, z) and (not Q(y)) and (C(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (C(y, z) and (not Q(z)) and (C(x, y) and (not Q(x))))) or (P(z) and (not Q(z)) and (R(y, z) and (not Q(y)) and (R(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (R(y, z) and (not Q(z)) and (R(x, y) and (not Q(x))))) or (P(x) and (not Q(x)) and (R(x, y) and (not Q(y)) and (R(y, z) and (not Q(z))))) or (P(x) and (not Q(x)) and (C(x, y) and (not Q(y)) and (C(y, z) and (not Q(z))))) or ((not Q(z)) and ex u ((C(u, z) and (R(y, u) and P(y) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v0 ((R(x, v0) and (C(y, v0) and (not Q(y)) and ex u0 ((R(y, u0) and (C(z, u0) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u0 ((C(z, u0) and (R(y, u0) and (not Q(y)) and ex v0 ((C(y, v0) and (R(x, v0) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v ((R(x, v) and (C(v, y) and (not Q(y)) and ex u ((R(y, u) and (C(u, z) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u ((C(u, z) and (R(y, u) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(y) and (not Q(y)) and ex u0 ((R(y, u0) and ex v0 ((C(y, v0) and (C(z, u0) and (not Q(z)) and (R(x, v0) and (not Q(x)))))))))))"
+"((not ex z0 ((P(z0) and (ex y0 ((R(y0, z0) and P(y0) and ex x0 ((R(x0, y0) and P(x0))))) or ex y0 ((C(y0, z0) and P(y0) and ex x0 ((C(x0, y0) and P(x0))))) or ex u ((C(z0, u) and ex y0 ((R(y0, u) and P(y0) and ex v ((C(y0, v) and ex x0 ((R(x0, v) and P(x0))))))))) or ex u0 ((C(u0, z0) and ex y0 ((R(y0, u0) and P(y0) and ex v0 ((C(v0, y0) and ex x0 ((R(x0, v0) and P(x0))))))))))))) and ((P(z) and (not Q(z)) and (C(y, z) and (not Q(y)) and (C(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (C(y, z) and (not Q(z)) and (C(x, y) and (not Q(x))))) or (P(z) and (not Q(z)) and (R(y, z) and (not Q(y)) and (R(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (R(y, z) and (not Q(z)) and (R(x, y) and (not Q(x))))) or (P(x) and (not Q(x)) and (R(x, y) and (not Q(y)) and (R(y, z) and (not Q(z))))) or (P(x) and (not Q(x)) and (C(x, y) and (not Q(y)) and (C(y, z) and (not Q(z))))) or ((not Q(z)) and ex u ((C(u, z) and (R(y, u) and P(y) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v0 ((R(x, v0) and (C(y, v0) and (not Q(y)) and ex u0 ((R(y, u0) and (C(z, u0) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u0 ((C(z, u0) and (R(y, u0) and (not Q(y)) and ex v0 ((C(y, v0) and (R(x, v0) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v ((R(x, v) and (C(v, y) and (not Q(y)) and ex u ((R(y, u) and (C(u, z) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u ((C(u, z) and (R(y, u) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(y) and (not Q(y)) and ex u0 ((R(y, u0) and ex v0 ((C(y, v0) and (C(z, u0) and (not Q(z)) and (R(x, v0) and (not Q(x)))))))))))"
+(* old variant:
+ "((not ex z0 ((P(z0) and (ex y0 ((R(y0, z0) and P(y0) and ex x0 ((R(x0, y0) and P(x0))))) or ex y0 ((C(y0, z0) and P(y0) and ex x0 ((C(x0, y0) and P(x0))))) or ex y0 ((P(y0) and ex x0 ((P(x0) and (ex u ((C(z0, u) and R(y0, u) and ex v ((C(y0, v) and R(x0, v))))) or ex u0 ((C(u0, z0) and R(y0, u0) and ex v0 ((C(v0, y0) and R(x0, v0)))))))))))))) and ((P(z) and (not Q(z)) and (C(y, z) and (not Q(y)) and (C(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (C(y, z) and (not Q(z)) and (C(x, y) and (not Q(x))))) or (P(z) and (not Q(z)) and (R(y, z) and (not Q(y)) and (R(x, y) and (not Q(x))))) or (P(y) and (not Q(y)) and (R(y, z) and (not Q(z)) and (R(x, y) and (not Q(x))))) or (P(x) and (not Q(x)) and (R(x, y) and (not Q(y)) and (R(y, z) and (not Q(z))))) or (P(x) and (not Q(x)) and (C(x, y) and (not Q(y)) and (C(y, z) and (not Q(z))))) or ((not Q(z)) and ex u ((C(u, z) and (R(y, u) and P(y) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v0 ((R(x, v0) and (C(y, v0) and (not Q(y)) and ex u0 ((R(y, u0) and (C(z, u0) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u0 ((C(z, u0) and (R(y, u0) and (not Q(y)) and ex v0 ((C(y, v0) and (R(x, v0) and (not Q(x))))))))) or (P(x) and (not Q(x)) and ex v ((R(x, v) and (C(v, y) and (not Q(y)) and ex u ((R(y, u) and (C(u, z) and (not Q(z))))))))) or (P(z) and (not Q(z)) and ex u ((C(u, z) and (R(y, u) and (not Q(y)) and ex v ((C(v, y) and (R(x, v) and (not Q(x))))))))) or (P(y) and (not Q(y)) and ex u0 ((R(y, u0) and ex v0 ((C(y, v0) and (C(z, u0) and (not Q(z)) and (R(x, v0) and (not Q(x)))))))))))"*)
(Formula.str (FFSolver.normalize_for_model
ttt heur_phi));
);
@@ -307,7 +324,7 @@
Aux.run_test_if_target "FFSolverTest" tests
let a () =
- match test_filter ["FFSolver:1:evaluate: universal"]
+ match test_filter ["FFSolver:8:eval: gomoku heuristic from SolverTest.ml"]
tests
with
| Some tests -> ignore (run_test_tt ~verbose:true tests)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
