[Toss-devel-svn] SF.net SVN: toss:[1207] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1207] trunk/Toss
|
From: <luk...@us...> - 2010-11-29 09:49:08
|
Revision: 1207
http://toss.svn.sourceforge.net/toss/?rev=1207&view=rev
Author: lukstafi
Date: 2010-11-29 09:49:01 +0000 (Mon, 29 Nov 2010)
Log Message:
-----------
FFTNF bug fixes (recent missing negation, older implementation of c3 of FFTNF spec).
Modified Paths:
--------------
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Formula/FFTNFTest.ml
trunk/Toss/Solver/FFSolverTest.ml
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2010-11-28 17:05:43 UTC (rev 1206)
+++ trunk/Toss/Formula/FFTNF.ml 2010-11-29 09:49:01 UTC (rev 1207)
@@ -50,7 +50,7 @@
(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])
@@ -93,6 +93,7 @@
(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])
@@ -658,8 +659,8 @@
Left subt, {loc with n={fvs=Vars.empty; t=TAnd[]}}
| {fvs=lit_vs; t=TLit lit} ->
let _ = if !debug_level > 3 then
- printf "find_unprot: processing literal, loc %s\n"
- (location_str loc) in
+ printf "find_unprot: processing literal %s, loc %s\n"
+ (Formula.str lit) (location_str loc) in
let best_loc = (* store if first *)
match best_loc with
| Some ((lit2,lit_vs2), _)
@@ -706,7 +707,7 @@
match task_lit with
| Left subt ->
Vars.empty,
- lazy {fvs=Vars.empty; t=TProc (task_id, subproc subt)}
+ lazy {fvs=Vars.empty; t=TProc (task_id, Not (subproc subt))}
| Right (lit, lit_vs) ->
lit_vs, lazy {fvs=lit_vs; t=TProc (task_id, lit)} in
match loc.x with
@@ -717,18 +718,21 @@
| ExNode (ctx', vs) ->
let vs' = Vars.inter vs lit_vs in
let vs'' = Vars.diff vs vs' in
- (* a1 *)
+ (* a1
+ pull-out(context'[],[Qn.[fill-loc]]) *)
if Vars.is_empty vs' then
let _ = if !debug_level > 2 then printf "a1\n" in
pull_out subproc task {x=ctx'; n=qT loc.x (vs,loc.n)}
- (* a2 *)
+ (* a2
+ context'[Qn'.(L /\ Qn''.[fill-loc])] *)
else
let _ = if !debug_level > 2 then printf "a2\n" in
zip {x=ctx'; n=qT loc.x (vs', conj_flat (
Lazy.force put_result, qT loc.x (vs'', loc.n)))}
- (* b *)
+ (* b
+ pull-out(context'[],[[fill-loc] /\ C]) *)
| AndNode (ctx', subts) ->
let _ = if !debug_level > 2 then printf "b\n" in
pull_out subproc task
@@ -749,14 +753,16 @@
let disj = {fvs=vsSibl; t=TOr subts} in
let vs1_3 = Vars.diff vs1 vs3 in
- (* c1 *)
+ (* c1
+ pull-out(context'[Qn2.[] \/ Qn4.D],[fill-loc]) *)
if Vars.is_empty vs3 then
let _ = if !debug_level > 2 then printf "c1\n" in
pull_out subproc task
{loc with x= qNode qN (
orNode_flat (ctx', [qT qN (vs4, disj)]), vs2)}
- (* c2 *)
+ (* c2
+ context'[Qn3.(Qn1\Qn3.(L /\ Qn5.[fill-loc]) \/ Qn4.D)] *)
else if not (Vars.is_empty vs1) &&
(not (Vars.is_empty vs1_3) ||
Vars.is_empty (Vars.diff vs3 vs1))
@@ -769,14 +775,17 @@
qT qN (vs4, disj)) in
zip {x=ctx'; n=qT qN (vs3, subt)}
- (* c3 *)
+ (* c3
+ pull-out(context'[Qn2+3.[] \/ Qn3+4.D],[fill-loc]) *)
else if match qN with ExNode _ -> true | _ -> false then
let _ = if !debug_level > 2 then printf "c3\n" in
pull_out subproc task
- {x=orNode_flat (ctx', [qT qN (vsD, disj)]);
- n= qT qN (vs0, loc.n)}
+ {loc with x=qNode qN
+ (orNode_flat (ctx', [qT qN (vsD, disj)]), vs0)}
- (* c4 *)
+ (* c4
+ pull-out(context'[Qn.(([] \/ D) /\ ([fill-loc] \/
+ D))],[T]) *)
else
let _ = if !debug_level > 2 then printf "c4\n" in
pull_out subproc task
@@ -809,7 +818,8 @@
let conj = {fvs=vsSiblAnd; t=TAnd and_subts} in
- (* d1 *)
+ (* d1
+ pull-out(context'[Qn2.([] \/ D) /\ Qn4.C],[fill-loc]) *)
if Vars.is_empty vs3 then
let _ = if !debug_level > 2 then printf "d1\n" in
pull_out subproc task
@@ -818,7 +828,8 @@
ctx', qT qN (vs4, conj)), vs2),
or_subts)}
- (* d2 *)
+ (* d2
+ pull-out(context'[Qn2+3.([] \/ D) /\ Qn3+4.C]) *)
else if match qN with AllNode _ -> true | _ -> false then
let _ = if !debug_level > 2 then printf "d2\n" in
pull_out subproc task
@@ -826,7 +837,9 @@
qNode qN (andNode_flat (ctx', qT qN (vsC, conj)), vsFLD)
, or_subts)}
- (* d3 *)
+ (* d3
+ pull-out(context'[Qn6.([] /\ C) \/ Qn5.(D /\
+ C)],[fill-loc]) *)
else
let vs5 = Vars.union vsD vsC in
let vs6 = Vars.union vsFL vsC in
@@ -841,7 +854,8 @@
| OrNode (OrNode _,_) ->
failwith "pull_out: malformed context (nonflat disjunction)"
- (* e *)
+ (* e
+ context[fill-loc] *)
| OrNode (Top, _) ->
let _ = if !debug_level > 2 then printf "e\n" in
zip {loc with n=conj_flat (Lazy.force put_result, loc.n)}
@@ -849,7 +863,8 @@
let _ = if !debug_level > 2 then printf "e\n" in
zip {loc with n=conj_flat (Lazy.force put_result, loc.n)}
- (* f1 *)
+ (* f1
+ context[L /\ [fill-loc]] *)
| OrNode (AndNode (Top, _), _) ->
let _ = if !debug_level > 2 then printf "f1\n" in
zip {loc with n=
@@ -860,7 +875,9 @@
zip {loc with n=
conj_flat (Lazy.force put_result, loc.n)}
- (* f2 *) (* same as (d) of FFSEP *)
+ (* f2
+ pull-out(context'[([] /\ C) \/ (D /\ C)], [fill-loc]) *)
+ (* same as (d) of FFSEP *)
| OrNode (AndNode (ctx', conjs), disjs)
when not (univ_next_in_scope ctx') ->
let _ = if !debug_level > 2 then printf "f2\n" in
@@ -872,7 +889,9 @@
{loc with x= andNode_flat (
orNode_flat (ctx', [conj_flat (d,c)]), c)}
- (* f3 *) (* same as (f) of FFSEP *)
+ (* f3
+ pull-out(context'[([] \/ D \/ E) /\ (C \/ E)], [fill-loc]) *)
+ (* same as (f) of FFSEP *)
| OrNode (AndNode (OrNode (ctx', esjs), conjs), disjs) ->
let _ = if !debug_level > 2 then printf "f3\n" in
let e = List.fold_right (fun a b->disj_flat (a,b)) esjs
Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml 2010-11-28 17:05:43 UTC (rev 1206)
+++ trunk/Toss/Formula/FFTNFTest.ml 2010-11-29 09:49:01 UTC (rev 1207)
@@ -151,7 +151,20 @@
"ff_tnf: deep" >::
(fun () ->
+ (* FFTNF.debug_level := 7; *)
assert_equal ~printer:(fun x->x)
+ "ex z (((not Q(z)) and (ex x, y ((not R(x, y))) or ex y ((C(y, z) and ex x (P(x)))))))"
+ (Formula.str (FFTNF.ff_tnf
+ (FFTNF.promote_rels (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))")));
+
+ assert_equal ~printer:(fun x->x)
+ "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))))))))"
+ (Formula.str (FFTNF.ff_tnf
+ (FFTNF.promote_rels (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 Q(z))")));
+
+ assert_equal ~printer:(fun x->x)
"ex z ((Q(z) or ex x ((P(x) and ex y (R(x, y)))) or ex y ((C(y, z) and ex x (R(x, y))))))"
(Formula.str (FFTNF.ff_tnf
(FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
@@ -164,6 +177,21 @@
(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" >::
+ (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)))))))))"
+ (Formula.str (FFTNF.ff_tnf
+ (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
+ (formula_of_str "all x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
+
+ assert_equal ~printer:(fun x->x)
+ "(((not ex z ((not Q(z)))) and ex y (P(y))) or ex x, y (C(x, y)))"
+ (Formula.str (FFTNF.ff_tnf
+ (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
+ (formula_of_str "ex x, y (C(x, y) or (P(y) and all z Q(z)))")));
+ );
+
]
let a =
Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml 2010-11-28 17:05:43 UTC (rev 1206)
+++ trunk/Toss/Solver/FFSolverTest.ml 2010-11-29 09:49:01 UTC (rev 1207)
@@ -273,7 +273,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 Q(a1)) and (not P(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 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))))"
(Formula.str (FFSolver.normalize_for_model
tictactoe_init tictactoe_LHS));
);
@@ -296,56 +296,11 @@
\"" 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)))))))))))"
(Formula.str (FFSolver.normalize_for_model
ttt heur_phi));
);
- "ff_tnf: gomoku heuristic with negative subtask" >::
- (fun () ->
- skip_if true "ttt enough";
- let heur_phi = formula_of_str
- "(((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)
- and C(w, r) and R(v, r))) or ex r, s, t, u ((R(y, u) and R(x, t) and
- R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))))
- and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(v)) and (not P(w))
- and (not P(x)) and (not P(y)) and (not P(z))
- and (not ex v, w, x, y, z ((((C(y, z) and C(x, y) and C(w, x) and
- C(v, w)) or (R(y, z) and R(x, y) and R(w, x) and R(v, w)) or
- ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z)
- 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
- Printf.printf "heur_phi=%s\n%!"(Formula.str heur_phi);
- let gomoku8x8 = struc_of_str
-"[ | P:1 { }; Q:1 { } | ] \"
- ... ... ... ...
- ... ... ... ...
-... ... ... ...
-... ... ... ...
- ... ... ... ...
- ... ... ... ...
-... ... ... ...
-... ... ... ...
- ... ... ... ...
- ... ... ... ...
-... ... ... ...
-... ... ... ...
- ... ... ... ...
- ... ... ... ...
-... ... ... ...
-... ... ... ...
-\"" in
- (* FFTNF.debug_level := 3; *)
- assert_equal ~printer:(fun x->x)
- ""
- (Formula.str (FFSolver.normalize_for_model
- gomoku8x8 heur_phi));
- );
-
]
let a =
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
