[Toss-devel-svn] SF.net SVN: toss:[1233] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1233] trunk/Toss
|
From: <luk...@us...> - 2010-12-07 16:19:26
|
Revision: 1233
http://toss.svn.sourceforge.net/toss/?rev=1233&view=rev
Author: lukstafi
Date: 2010-12-07 16:19:19 +0000 (Tue, 07 Dec 2010)
Log Message:
-----------
Simple test fixes (mostly adjustments to new FFTNF).
Modified Paths:
--------------
trunk/Toss/Arena/ArenaTest.ml
trunk/Toss/Arena/ContinuousRuleTest.ml
trunk/Toss/Arena/DiscreteRuleTest.ml
trunk/Toss/Play/Game.ml
trunk/Toss/Play/GameTest.ml
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Solver/FFSolverTest.ml
Modified: trunk/Toss/Arena/ArenaTest.ml
===================================================================
--- trunk/Toss/Arena/ArenaTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Arena/ArenaTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -71,8 +71,8 @@
PLAYER black PAYOFF {white: 0.3; black: :(ex x Q(x))}
}
STATE LOC 1" in
- let res1 = "REL Q(x) {ex y R(y, x)}
-REL P(x) {ex y R(x, y)}
+ let res1 = "REL P(x) {ex y R(x, y)}
+REL Q(x) {ex y R(y, x)}
PLAYERS white, black
RULE finish:
[a, b | R (a, b) | ] -> [a, c, b | R {(a, c); (c, b)} | ] emb R
@@ -90,8 +90,8 @@
Arena.equational_def_style := false;
assert_equal ~printer:(fun x->x) ~msg:"curly braces style"
res1 (Arena.sprint_state gs);
- let res2 = "REL Q(x) = ex y R(y, x)
-REL P(x) = ex y R(x, y)
+ let res2 = "REL P(x) = ex y R(x, y)
+REL Q(x) = ex y R(y, x)
PLAYERS white, black
RULE finish:
[a, b | R (a, b) | ] -> [a, c, b | R {(a, c); (c, b)} | ] emb R
Modified: trunk/Toss/Arena/ContinuousRuleTest.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRuleTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Arena/ContinuousRuleTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -26,24 +26,24 @@
"[a, b | R (a, b) | ] -> [c, d | R (c, d) | ] emb R with [c <- a, d <- b] " in
let s = discr ^ " pre true inv true post true" in
let signat = ["R", 2] in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule1" in
assert_equal ~msg:"1. no continuous" ~printer:(fun x->x) s (str r);
let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
let s = discr ^ "\nupdate\n" ^ upd_eq ^ " pre true inv true post true" in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (str r);
let dyn_eq = " f(a)' = (2. * f(a)) + t;\n f(b)' = f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ " pre true inv true post true" in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule3" in
assert_equal ~msg:"3. dynamics" ~printer:(fun x->x) s (str r);
let dyn_eq = " f(a)' = (2. * f(a)) + t;\n f(b)' = f(b)" in
let upd_eq = " f(c) = 2. * f(a);\n f(d) = f(b)\n" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" pre true inv true post true" in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule4" in
assert_equal ~msg:"4. dynamics+update" ~printer:(fun x->x) s (str r);
);
@@ -53,25 +53,25 @@
"[a, b | R (a, b) | ] -> [c, d | R (c, d) | ] emb R with [c <- a, d <- b]" in
let s = discr in
let signat = ["R", 2] in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule1" in
assert_equal ~msg:"1. no continuous" ~printer:(fun x->x) s (sprint r);
let upd_eq1 = " f(c) = 2. * f(a);"
and upd_eq2 = " f(d) = f(b)" in
let upd_eq = upd_eq1 ^ upd_eq2 in
let s = discr ^ "\n update" ^ upd_eq in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (sprint r);
let dyn_eq1 = " f(a)' = 2. * f(a) + t;"
and dyn_eq2 = " f(b)' = f(b)" in
let dyn_eq = dyn_eq1 ^ dyn_eq2 in
let s = discr ^ "\n dynamics" ^ dyn_eq in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule3" in
assert_equal ~msg:"3. dynamics" ~printer:(fun x->x) s (sprint r);
let s = discr ^ "\n dynamics" ^ dyn_eq ^ "\n update" ^ upd_eq in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule4" in
assert_equal ~msg:"4. dynamics+update" ~printer:(fun x->x) s (sprint r);
let dyn_eq = dyn_eq1 ^ "\n" ^ dyn_eq2 ^ ";\n" ^ dyn_eq1 ^ "\n" ^ dyn_eq2
@@ -79,7 +79,7 @@
let upd_eq = upd_eq1 ^ "\n" ^ upd_eq2 ^ ";\n" ^ upd_eq1 ^ "\n" ^ upd_eq2
^ ";\n" ^ upd_eq1 ^ "\n" ^ upd_eq2 in
let s = discr ^ "\n dynamics\n" ^ dyn_eq ^ "\n update\n" ^ upd_eq in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule5" in
assert_equal ~msg:"5. many equations" ~printer:(fun x->x) s (sprint r);
);
@@ -93,7 +93,7 @@
let s = dr ^ " dynamics " ^ dyn_eq ^ " update " ^ upd_eq ^
" pre true inv true post true " in
let struc = struc_of_str "[ | P {a}; Q:1{} | x { a -> 0.0 } ]" in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule1" in
let m = List.hd (matches struc r) in
let res, _, _ =
Aux.unsome (rewrite_single struc 0.0 m r 1. []) in
@@ -113,7 +113,7 @@
" pre true inv true post true " in
let signat = ["P", 1; "Q", 1] in
let struc = struc_of_str "[ | P {a}; Q:1{} | x { a -> 0.0 } ]" in
- let r = rule_of_str s signat [] in
+ let r = rule_of_str s signat [] "rule1" in
let m = List.hd (matches struc r) in
let res, _, _ =
Aux.unsome (rewrite_single struc 0.0 m r 1. []) in
Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -613,7 +613,7 @@
pre = Formula.And [];
rule_s = [1,1]} in
assert_one_of ~msg:"del defrel"
- ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))"]
+ ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))";"((_del_P(b) and O(b) and (not P(b)) and (not Q(b))) or (_del_Q(b) and O(b) and (not P(b)) and (not Q(b))))-> (P(b) and (not O(b)))"]
(rule_obj_str rule_obj);
let lhs_struc = struc_of_str "[ e | _opt_D (e); _diffthan_P(e) | ]" in
Modified: trunk/Toss/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Play/Game.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -251,7 +251,7 @@
(* {{{ log entry *)
if !debug_level > 3 then (
- Printf.printf "default_hauristic: Computing of payoff %s...\n%!"
+ Printf.printf "default_heuristic: Computing of payoff %s...\n%!"
(Formula.sprint_real payoff);
);
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Play/GameTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -467,9 +467,12 @@
let breakthrough_heur =
breakthrough_heur_adv 1.5
-let chess_game =
+let chess_game () =
2.0, state_of_file "./examples/Chess.toss"
+let breakthrough_file_game =
+ 2.0, state_of_file "./examples/Breakthrough.toss"
+
let check_loc_random = function
| Game.Tree_search (_,_,_,evgames) ->
if
@@ -566,7 +569,7 @@
"play: chess suggest first move" >::
(fun () ->
todo "Payoff too difficult for heuristic generation.";
- let state = chess_game in
+ let state = chess_game () in
Game.set_debug_level 7;
Heuristic.debug_level := 7;
FFTNF.debug_level := 4;
@@ -581,7 +584,7 @@
"breakthrough payoff" >::
(fun () ->
- let state = update_game breakthrough_game
+ let state = update_game breakthrough_file_game
"[ | | ] \"
... ... ... ...
B ...B ...B B..B B..
@@ -596,16 +599,16 @@
... ... ... ...
... B.. ... B..
... ... ... ...
- -B ... ...W ...W ...
- ...B ... ... ...
- W..+B W..W W..W W..W
-\"" 1 in
+ ... ...W ...W ...
+ ... ... ... ...
+ W..B W..W W..W W..W
+\"" 0 in
(* Game.set_debug_level 5; *)
let move_opt = (let p,ps = Game.initialize_default (snd state)
~heur_adv_ratio:(fst state)
- ~loc:0 ~effort:5
+ ~loc:0 ~effort:2
~heuristic:breakthrough_heur
- ~search_method:"uct_greedy_playouts" () in
+ ~search_method:"alpha_beta_ord" () in
Game.toss ~grid_size:Game.cGRID_SIZE p ps) in
assert_equal ~msg:"black wins: suggest" ~printer:(function
| Aux.Left (bpos, moves, _, _) ->
@@ -1093,7 +1096,7 @@
);
]
-let a =
+let a () =
Aux.run_test_if_target "GameTest" tests
let a () = run_test_tt ~verbose:true experiments
@@ -1101,14 +1104,14 @@
(* The same content as in .toss files. *)
let a () =
- print_endline ("\n" ^ Arena.sprint_state (snd chess_game))
+ print_endline ("\n" ^ Arena.sprint_state (snd (chess_game ())))
let a () =
Game.set_debug_level 7
-let a () =
+let a =
match test_filter
- ["Game:0:misc:0:play: chess suggest first move"]
+ ["Game:0:misc:2:breakthrough payoff"]
tests
with
| Some tests -> ignore (run_test_tt ~verbose:true tests)
Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Play/HeuristicTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -288,7 +288,7 @@
"of_payoff: tic-tac-toe non monotonic" >::
(fun () -> backtrace (
assert_equal ~printer:(fun x->x) ~msg:"adv_ratio=1.5"
- "(Sum (z | P(z) : ((((0.64 + Sum (y | (R(y, z) and P(y)) : (0.96 + Sum (x | (R(x, y) and P(x)) : 1.44)))) + Sum (y | (C(y, z) and P(y)) : (0.96 + Sum (x | (C(x, y) and P(x)) : 1.44)))) + Sum (u | C(z, u) : (0.29 + Sum (y | (R(y, u) and P(y)) : (0.44 + Sum (v | C(y, v) : (0.66 + Sum (x | (R(x, v) and P(x)) : 1.)))))))) + Sum (u0 | C(u0, z) : (0.29 + Sum (y | (R(y, u0) and P(y)) : (0.44 + Sum (v0 | C(v0, y) : (0.66 + Sum (x | (R(x, v0) and P(x)) : 1.))))))))) + (-1. * Sum (z | Q(z) : ((((0.64 + Sum (y | (R(y, z) and Q(y)) : (0.96 + Sum (x | (R(x, y) and Q(x)) : 1.44)))) + Sum (y | (C(y, z) and Q(y)) : (0.96 + Sum (x | (C(x, y) and Q(x)) : 1.44)))) + Sum (u | C(z, u) : (0.29 + Sum (y | (R(y, u) and Q(y)) : (0.44 + Sum (v | C(y, v) : (0.66 + Sum (x | (R(x, v) and Q(x)) : 1.)))))))) + Sum (u0 | C(u0, z) : (0.29 + Sum (y | (R(y, u0) and Q(y)) : (0.44 + Sum (v0 | C(v0, y) : (0.66 + Sum (x | (R(x, v0) and Q(x)) : 1.)))))))))))"
+ "(Sum (x | P(x) : ((((0.64 + Sum (y | (R(x, y) and P(y)) : (0.96 + Sum (z | (R(y, z) and P(z)) : 1.44)))) + Sum (y | (C(x, y) and P(y)) : (0.96 + Sum (z | (C(y, z) and P(z)) : 1.44)))) + Sum (v0 | R(x, v0) : (0.29 + Sum (y | (C(v0, y) and P(y)) : (0.44 + Sum (u0 | R(y, u0) : (0.66 + Sum (z | (C(u0, z) and P(z)) : 1.)))))))) + Sum (v | R(x, v) : (0.29 + Sum (y | (C(y, v) and P(y)) : (0.44 + Sum (u | R(y, u) : (0.66 + Sum (z | (C(z, u) and P(z)) : 1.))))))))) + (-1. * Sum (x | Q(x) : ((((0.64 + Sum (y | (R(x, y) and Q(y)) : (0.96 + Sum (z | (R(y, z) and Q(z)) : 1.44)))) + Sum (y | (C(x, y) and Q(y)) : (0.96 + Sum (z | (C(y, z) and Q(z)) : 1.44)))) + Sum (v0 | R(x, v0) : (0.29 + Sum (y | (C(v0, y) and Q(y)) : (0.44 + Sum (u0 | R(y, u0) : (0.66 + Sum (z | (C(u0, z) and Q(z)) : 1.)))))))) + Sum (v | R(x, v) : (0.29 + Sum (y | (C(y, v) and Q(y)) : (0.44 + Sum (u | R(y, u) : (0.66 + Sum (z | (C(z, u) and Q(z)) : 1.)))))))))))"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(Heuristic.of_payoff 1.5
@@ -296,7 +296,7 @@
(real_of_str (":("^winPxyz^") - :("^winQxyz^")")))));
assert_equal ~printer:(fun x->x) ~msg:"adv_ratio=10"
- "(Sum (z | P(z) : ((((0.0101 + Sum (y | (R(y, z) and P(y)) : (0.101 + Sum (x | (R(x, y) and P(x)) : 1.01)))) + Sum (y | (C(y, z) and P(y)) : (0.101 + Sum (x | (C(x, y) and P(x)) : 1.01)))) + Sum (u | C(z, u) : (0.001 + Sum (y | (R(y, u) and P(y)) : (0.01 + Sum (v | C(y, v) : (0.1 + Sum (x | (R(x, v) and P(x)) : 1.)))))))) + Sum (u0 | C(u0, z) : (0.001 + Sum (y | (R(y, u0) and P(y)) : (0.01 + Sum (v0 | C(v0, y) : (0.1 + Sum (x | (R(x, v0) and P(x)) : 1.))))))))) + (-1. * Sum (z | Q(z) : ((((0.0101 + Sum (y | (R(y, z) and Q(y)) : (0.101 + Sum (x | (R(x, y) and Q(x)) : 1.01)))) + Sum (y | (C(y, z) and Q(y)) : (0.101 + Sum (x | (C(x, y) and Q(x)) : 1.01)))) + Sum (u | C(z, u) : (0.001 + Sum (y | (R(y, u) and Q(y)) : (0.01 + Sum (v | C(y, v) : (0.1 + Sum (x | (R(x, v) and Q(x)) : 1.)))))))) + Sum (u0 | C(u0, z) : (0.001 + Sum (y | (R(y, u0) and Q(y)) : (0.01 + Sum (v0 | C(v0, y) : (0.1 + Sum (x | (R(x, v0) and Q(x)) : 1.)))))))))))"
+ "(Sum (x | P(x) : ((((0.0101 + Sum (y | (R(x, y) and P(y)) : (0.101 + Sum (z | (R(y, z) and P(z)) : 1.01)))) + Sum (y | (C(x, y) and P(y)) : (0.101 + Sum (z | (C(y, z) and P(z)) : 1.01)))) + Sum (v0 | R(x, v0) : (0.001 + Sum (y | (C(v0, y) and P(y)) : (0.01 + Sum (u0 | R(y, u0) : (0.1 + Sum (z | (C(u0, z) and P(z)) : 1.)))))))) + Sum (v | R(x, v) : (0.001 + Sum (y | (C(y, v) and P(y)) : (0.01 + Sum (u | R(y, u) : (0.1 + Sum (z | (C(z, u) and P(z)) : 1.))))))))) + (-1. * Sum (x | Q(x) : ((((0.0101 + Sum (y | (R(x, y) and Q(y)) : (0.101 + Sum (z | (R(y, z) and Q(z)) : 1.01)))) + Sum (y | (C(x, y) and Q(y)) : (0.101 + Sum (z | (C(y, z) and Q(z)) : 1.01)))) + Sum (v0 | R(x, v0) : (0.001 + Sum (y | (C(v0, y) and Q(y)) : (0.01 + Sum (u0 | R(y, u0) : (0.1 + Sum (z | (C(u0, z) and Q(z)) : 1.)))))))) + Sum (v | R(x, v) : (0.001 + Sum (y | (C(y, v) and Q(y)) : (0.01 + Sum (u | R(y, u) : (0.1 + Sum (z | (C(z, u) and Q(z)) : 1.)))))))))))"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.10000.))/.10000.)
(Heuristic.of_payoff 10.
Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml 2010-12-07 14:35:28 UTC (rev 1232)
+++ trunk/Toss/Solver/FFSolverTest.ml 2010-12-07 16:19:19 UTC (rev 1233)
@@ -91,7 +91,7 @@
"eval: first-order quantifier free more" >::
(fun () ->
eval_eq "[ | R {(a, b); (c, d)}; P {a; b}; Q{a; c} | ]" "P(x) or Q(x)"
- "{ x->b, x->a, x->c }";
+ "{ x->c, x->a, x->b }";
);
"eval: first-order with quantifiers more" >::
@@ -177,11 +177,12 @@
. Q .
\"" heur_phi
- "{ y->b1{ z->c1{ x->a1 } } , y->a2{ z->a3{ x->a1 } } }";
+ "{ z->a3{ y->a2{ x->a1 } } , z->c1{ y->b1{ x->a1 } } }";
);
"eval: gomoku heuristic from SolverTest.ml" >::
(fun () ->
+ todo "Problem: uneliminated Empty inside assignment set";
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)
@@ -215,6 +216,26 @@
\"" heur_phi
"{ y->d6{ z->e7{ x->c5{ w->b4{ v->a3 } } } } , 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{ w->c5{ v->b4 } } } } , y->f7{ x->e6{ z->g8{ w->d5{ v->c4 } } } } }");
+ (*
+
+ {
+ w->f6{} ,
+ w->e6{ v->d6{ x->f6{ y->g6{ z->h6 } } } } ,
+ w->d6{} ,
+ w->d5{ x->e6{ v->c4{ y->f7{ z->g8 } } } } ,
+ w->c5{ x->d6{ v->b4{ y->e7{ z->f8 } } } } ,
+ w->b5{ v->b4{ x->b6{ y->b7{ z->b8 } } } } ,
+ w->e4{} ,
+ w->c4{} ,
+ w->b4{ x->c5{ v->a3{ y->d6{ z->e7 } } } , x->c3{ v->a5{ y->d2{ z->e1 } } } } ,
+ w->c3{} ,
+ w->f1{} ,
+ w->c1{ x->d1{ y->e1{ v->b1{ z->f1 } } } } ,
+ w->d1{ x->e1{ y->f1{ z->g1{ v->c1 } } } } ,
+ w->e1{ x->f1{ y->g1{ v->d1{ z->h1 } } } } ,
+ w->e7{ x->f6{ y->g5{ z->h4{ v->d8 } } } } }
+ *)
+
"get_real_val: tic-tac-toe winning" >::
(fun () ->
let heur = real_of_str
@@ -271,7 +292,7 @@
W..W W..W W..W W..W
\"" in
assert_equal ~printer:(fun x->x)
- "((not ex x ((B(x) and all y ((not C(y, x)))))) and (W(b1) and (not B(b1)) and (C(b1, b2) and (not (b2 = b1)) and (R(a1, b1) and (not (b1 = a1)) and (not (b2 = a1)) and ((not (b1 = a2)) and R(a2, b2) and (not (b2 = a2)) and C(a1, a2) and (not (a2 = a1)) and (not W(a2)))))))"
+ "((not ex x ((B(x) and all y ((not C(y, x)))))) and (W(b1) and (not B(b1)) and (R(a1, b1) and (not (b1 = a1)) and (C(b1, b2) and (not (b2 = b1)) and (not (b2 = a1)) and ((not (b1 = a2)) and C(a1, a2) and (not (a2 = a1)) and R(a2, b2) and (not (b2 = a2)) and (not W(a2)))))))"
(Formula.str (FFSolver.normalize_for_model brkthr_init brkthr_LHS));
);
@@ -290,7 +311,7 @@
. . .
\"" in
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 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))))"
+ "((not ex z ((Q(z) and (ex y ((C(y, z) and Q(y) and ex x ((C(x, y) and Q(x))))) or ex u0 ((C(z, u0) and ex y ((R(y, u0) and Q(y) and ex v0 ((C(y, v0) and ex x ((R(x, v0) 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(u, z) and ex y ((R(y, u) and Q(y) and ex v ((C(v, y) and ex x ((R(x, v) and Q(x))))))))))))) and ((not P(a1)) and (not Q(a1))))"
(Formula.str (FFSolver.normalize_for_model
tictactoe_init tictactoe_LHS));
);
@@ -311,8 +332,9 @@
. . .
\"" in
+ (* not quite completely reviewed, but looks good... *)
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 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)))))))))))"
+"((not ex x0 ((P(x0) and (ex y0 ((R(x0, y0) and P(y0) and ex z0 ((R(y0, z0) and P(z0))))) or ex y0 ((C(x0, y0) and P(y0) and ex z0 ((C(y0, z0) and P(z0))))) or ex v0 ((R(x0, v0) and ex y0 ((C(v0, y0) and P(y0) and ex u0 ((R(y0, u0) and ex z0 ((C(u0, z0) and P(z0))))))))) or ex v ((R(x0, v) and ex y0 ((C(y0, v) and P(y0) and ex u ((R(y0, u) and ex z0 ((C(z0, u) and P(z0))))))))))))) and ((P(z) and (not Q(z)) and (R(y, z) and (not Q(y)) 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(y) and (not Q(y)) and (R(x, y) and (not Q(x)) and (R(y, z) and (not Q(z))))) or (P(z) and (not Q(z)) and (C(y, z) and (not Q(y)) and (C(x, y) and (not Q(x))))) or (P(x) and (not Q(x)) and (C(x, y) and (not Q(y)) and (C(y, z) and (not Q(z))))) or (P(y) and (not Q(y)) and (C(x, y) and (not Q(x)) and (C(y, z) 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 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(y) and (not Q(y)) and ex v0 ((C(y, v0) and ex u0 ((R(y, u0) and (R(x, v0) and (not Q(x)) and (C(z, u0) 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(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(y) and (not Q(y)) and ex u ((R(y, u) and ex v ((C(v, y) and (C(u, z) and (not Q(z)) and (R(x, v) 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
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
