[Toss-devel-svn] SF.net SVN: toss:[1634] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1634] trunk/Toss
|
From: <luk...@us...> - 2011-11-17 17:12:57
|
Revision: 1634
http://toss.svn.sourceforge.net/toss/?rev=1634&view=rev
Author: lukaszkaiser
Date: 2011-11-17 17:12:44 +0000 (Thu, 17 Nov 2011)
Log Message:
-----------
Cleanups and optimizations in Distinguish, also changing variable order returned by free_vars, adding comments and reference.
Modified Paths:
--------------
trunk/Toss/Formula/FFTNFTest.ml
trunk/Toss/Formula/FormulaSubst.ml
trunk/Toss/Formula/FormulaSubstTest.ml
trunk/Toss/Formula/Makefile
trunk/Toss/Play/HeuristicTest.ml
trunk/Toss/Server/LearnGame.ml
trunk/Toss/Server/LearnGameTest.ml
trunk/Toss/Server/Picture.ml
trunk/Toss/Solver/Distinguish.ml
trunk/Toss/Solver/Distinguish.mli
trunk/Toss/Solver/DistinguishTest.ml
trunk/Toss/www/reference/reference.tex
Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Formula/FFTNFTest.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -17,7 +17,7 @@
let winQxyz =
"ex x, y, z ((((Q(x) and Q(y)) and Q(z)) and ((((R(x, y) and R(y, z)) or (C(x, y) and C(y, z))) or ex u, v ((((R(x, v) and C(v, y)) and R(y, u)) and C(u, z)))) or ex u, v ((((R(x, v) and C(y, v)) and R(y, u)) and C(z, u))))))"
let winQzyx =
- "ex z, y, x (Q(x) and Q(y) and Q(z) and ((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (R(x, v) and C(v, y) and R(y, u) and C(u, z)) or ex u, v (R(x, v) and C(y, v) and R(y, u) and C(z, u))))"
+ "ex x, y, z (Q(x) and Q(y) and Q(z) and ((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (R(x, v) and C(v, y) and R(y, u) and C(u, z)) or ex u, v (R(x, v) and C(y, v) and R(y, u) and C(z, u))))"
let winPxyz =
"ex x, y, z ((((P(x) and P(y)) and P(z)) and ((((R(x, y) and R(y, z)) or (C(x, y) and C(y, z))) or ex u, v ((((R(x, v) and C(v, y)) and R(y, u)) and C(u, z)))) or ex u, v ((((R(x, v) and C(y, v)) and R(y, u)) and C(z, u))))))"
@@ -156,7 +156,7 @@
(formula_of_str winQzyx)));
assert_eq_str ~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))"
+ "ex x, y, z (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 x, y, z (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 x, y, z (Q(z) and Q(y) and Q(x) and R(x, y) and R(y, z)) or ex x, y, z (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"])
Aux.Strings.empty
@@ -275,7 +275,7 @@
(* interpretation warning: in cases below, pulled-out "Q" in the
result represents "not Q" actually (a negative literal) *)
assert_eq_str ~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))"
+ "ex z (Q(z) and ex y not R(x, y)) or ex x, z (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"])
Modified: trunk/Toss/Formula/FormulaSubst.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubst.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Formula/FormulaSubst.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -276,15 +276,6 @@
(* -------------------------- FREE VARIABLES -------------------------------- *)
-(* Helper function: remove duplicates from sorted list of variables. *)
-let rec remove_dup_vars acc = function
- [] -> acc
- | [v] -> v :: acc
- | v1 :: v2 :: vs ->
- match compare_vars v1 v2 with
- 0 -> remove_dup_vars acc (v2::vs)
- | _ -> remove_dup_vars (v1::acc) (v2::vs)
-
let rec all_vars_acc acc = function
| Eq (x, y) -> (x :> var) :: (y :> var) :: acc
| Rel (r, vs) -> List.rev_append ((Array.to_list vs) :> var list) acc
@@ -314,8 +305,7 @@
List.rev_append (List.rev_map var_str (all_vars_acc [] f)) (all_vars_real r)
| RLet (_, def, re) -> List.rev_append (all_vars_real def) (all_vars_real re)
-let all_vars phi =
- remove_dup_vars [] (List.sort compare_vars (all_vars_acc [] phi))
+let all_vars phi = Aux.unique_sorted ~cmp:compare_vars (all_vars_acc [] phi)
let rec free_vars_acc acc = function
| Eq (x, y) -> (x :> var) :: (y :> var) :: acc
@@ -350,8 +340,7 @@
List.filter (fun w -> not (List.mem w vs)) (free_vars_real r)
| RLet _ as r -> free_vars_real (expand_real_expr r)
-let free_vars phi =
- remove_dup_vars [] (List.sort compare_vars (free_vars_acc [] phi))
+let free_vars phi = Aux.unique_sorted ~cmp:compare_vars (free_vars_acc [] phi)
(* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
Modified: trunk/Toss/Formula/FormulaSubstTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubstTest.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Formula/FormulaSubstTest.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -121,9 +121,9 @@
assert_equal ~printer:(fun x -> x)
vs (Formula.var_list_str (
FormulaSubst.free_vars (formula_of_string phi))) in
- fv_eq "not (P(x) and not Q(y))" "y, x";
+ fv_eq "not (P(x) and not Q(y))" "x, y";
fv_eq "Q(x) or (ex x P(x))" "x";
- fv_eq "P(x) or ex y (E(x, y) and y in T)" "x, T";
+ fv_eq "P(x) or ex y (E(x, y) and y in T)" "T, x";
fv_eq "lfp T(x) = (P(x) or ex y (E(x, y) and y in T))" "x";
);
Modified: trunk/Toss/Formula/Makefile
===================================================================
--- trunk/Toss/Formula/Makefile 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Formula/Makefile 2011-11-17 17:12:44 UTC (rev 1634)
@@ -5,6 +5,8 @@
AuxTest:
FormulaTest:
+FormulaMapTest:
+FormulaSubstTest:
BoolFormulaTest:
BoolFunctionTest:
FormulaOpsTest:
Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Play/HeuristicTest.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -275,14 +275,14 @@
"[a | P:1 {}; Q:1 {} | ] -> [ | P:1 {}; Q(a) | ] emb P, Q"] in
assert_eq_str
- "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * 0.33) - Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.33)"
+ "Sum (x, y, z | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * 0.33) - Sum (x, y, z | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.33)"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(default_heuristic 1. rules
(real_of_str (":("^winPxyz^") - :("^winQxyz^")")))));
assert_eq_str
- "Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * (:(P(x)) + :(P(y)) + :(P(z))) * 0.11) - Sum (z, y, x | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.11)"
+ "Sum (x, y, z | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (P(x) or P(y) or P(z)) and (not Q(x) or P(x)) and (not Q(y) or P(y)) and (not Q(z) or P(z))) : (:(P(x)) + :(P(y)) + :(P(z))) * (:(P(x)) + :(P(y)) + :(P(z))) * 0.11) - Sum (x, y, z | (((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v (C(z, u) and C(y, v) and R(y, u) and R(x, v)) or ex u, v (R(y, u) and R(x, v) and C(v, y) and C(u, z))) and (Q(x) or Q(y) or Q(z)) and (not P(x) or Q(x)) and (not P(y) or Q(y)) and (not P(z) or Q(z))) : (:(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(x)) + :(Q(y)) + :(Q(z))) * 0.11)"
(Formula.real_str
(Heuristic.map_constants (fun c->(floor (c*.100.))/.100.)
(default_heuristic 2. rules
@@ -298,14 +298,14 @@
"[a | P:1 {}; Q:1 {} | ] -> [ | P:1 {}; Q(a) | ] emb P, Q"] in
assert_eq_str
- "Sum (z, y, x, w, v | (((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 (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.04 ) - Sum (z, y, x, w, v | (((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(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.04 )"
+ "Sum (v, w, x, y, z | (((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 (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.04 ) - Sum (v, w, x, y, z | (((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(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.04 )"
(Formula.real_str
((* Heuristic.map_constants (fun c->(floor (c*.100.))/.100.) *)
(default_heuristic 2. rules
(real_of_str (":("^winPvwxyz^") - :("^winQvwxyz^")")))));
assert_eq_str
- "Sum (z, y, x, w, v | (((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 (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.008 ) - Sum (z, y, x, w, v | (((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(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.008 )"
+ "Sum (v, w, x, y, z | (((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 (P(z) or P(y) or P(x) or P(w) or P(v)) and (not Q(z) or P(z)) and (not Q(y) or P(y)) and (not Q(x) or P(x)) and (not Q(w) or P(w)) and (not Q(v) or P(v))) : (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * (:(P(v)) + :(P(w)) + :(P(x)) + :(P(y)) + :(P(z))) * 0.008 ) - Sum (v, w, x, y, z | (((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(z) or Q(z)) and (not P(y) or Q(y)) and (not P(x) or Q(x)) and (not P(w) or Q(w)) and (not P(v) or Q(v))) : (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * (:(Q(v)) + :(Q(w)) + :(Q(x)) + :(Q(y)) + :(Q(z))) * 0.008 )"
(Formula.real_str
((* Heuristic.map_constants (fun c->(floor (c*.1000.))/.1000.) *)
(default_heuristic 3. rules
@@ -347,7 +347,7 @@
~advr:4.0 game in
assert_eq_str
- "100. * (Sum (cell_e_y8__BLANK_, cell_d_y8__BLANK_, cell_c1_y8__BLANK_, cell_b_y8__BLANK_, cell_a_y8__BLANK_ | ((cell_2x(cell_a_y8__BLANK_) or cell_2x(cell_b_y8__BLANK_) or cell_2x(cell_c1_y8__BLANK_) or cell_2x(cell_d_y8__BLANK_) or cell_2x(cell_e_y8__BLANK_)) and (cell_2b(cell_a_y8__BLANK_) or cell_2x(cell_a_y8__BLANK_)) and (cell_2b(cell_b_y8__BLANK_) or cell_2x(cell_b_y8__BLANK_)) and (cell_2b(cell_c1_y8__BLANK_) or cell_2x(cell_c1_y8__BLANK_)) and (cell_2b(cell_d_y8__BLANK_) or cell_2x(cell_d_y8__BLANK_)) and (cell_2b(cell_e_y8__BLANK_) or cell_2x(cell_e_y8__BLANK_)) and R2(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and R2(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and R2(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and R2(cell_a_y8__BLANK_, cell_b_y8__BLANK_)) : (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * 0.0016 ) + Sum (cell_x18_y14__BLANK_, cell_x17_y15__BLANK_, cell_x16_y16__BLANK_, cell_x15_y17__BLANK_, cell_x14_y18__BLANK_ | ((cell_2x(cell_x14_y18__BLANK_) or cell_2x(cell_x15_y17__BLANK_) or cell_2x(cell_x16_y16__BLANK_) or cell_2x(cell_x17_y15__BLANK_) or cell_2x(cell_x18_y14__BLANK_)) and (cell_2b(cell_x14_y18__BLANK_) or cell_2x(cell_x14_y18__BLANK_)) and (cell_2b(cell_x15_y17__BLANK_) or cell_2x(cell_x15_y17__BLANK_)) and (cell_2b(cell_x16_y16__BLANK_) or cell_2x(cell_x16_y16__BLANK_)) and (cell_2b(cell_x17_y15__BLANK_) or cell_2x(cell_x17_y15__BLANK_)) and (cell_2b(cell_x18_y14__BLANK_) or cell_2x(cell_x18_y14__BLANK_)) and R1(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and R1(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and R1(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and R1(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_)) : (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * 0.0016 ) + Sum (cell_x9_y9__BLANK_, cell_x13_y13__BLANK_, cell_x12_y12__BLANK_, cell_x11_y11__BLANK_, cell_x10_y10__BLANK_ | ((cell_2x(cell_x10_y10__BLANK_) or cell_2x(cell_x11_y11__BLANK_) or cell_2x(cell_x12_y12__BLANK_) or cell_2x(cell_x13_y13__BLANK_) or cell_2x(cell_x9_y9__BLANK_)) and (cell_2b(cell_x10_y10__BLANK_) or cell_2x(cell_x10_y10__BLANK_)) and (cell_2b(cell_x11_y11__BLANK_) or cell_2x(cell_x11_y11__BLANK_)) and (cell_2b(cell_x12_y12__BLANK_) or cell_2x(cell_x12_y12__BLANK_)) and (cell_2b(cell_x13_y13__BLANK_) or cell_2x(cell_x13_y13__BLANK_)) and (cell_2b(cell_x9_y9__BLANK_) or cell_2x(cell_x9_y9__BLANK_)) and R0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and R0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and R0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and R0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_)) : (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * 0.0016 ) + Sum (cell_x8_e0__BLANK_, cell_x8_d0__BLANK_, cell_x8_c2__BLANK_, cell_x8_b0__BLANK_, cell_x8_a0__BLANK_ | ((cell_2x(cell_x8_a0__BLANK_) or cell_2x(cell_x8_b0__BLANK_) or cell_2x(cell_x8_c2__BLANK_) or cell_2x(cell_x8_d0__BLANK_) or cell_2x(cell_x8_e0__BLANK_)) and (cell_2b(cell_x8_a0__BLANK_) or cell_2x(cell_x8_a0__BLANK_)) and (cell_2b(cell_x8_b0__BLANK_) or cell_2x(cell_x8_b0__BLANK_)) and (cell_2b(cell_x8_c2__BLANK_) or cell_2x(cell_x8_c2__BLANK_)) and (cell_2b(cell_x8_d0__BLANK_) or cell_2x(cell_x8_d0__BLANK_)) and (cell_2b(cell_x8_e0__BLANK_) or cell_2x(cell_x8_e0__BLANK_)) and R(cell_x8_d0__BLANK_, cell_x8_e0__BLANK_) and R(cell_x8_c2__BLANK_, cell_x8_d0__BLANK_) and R(cell_x8_b0__BLANK_, cell_x8_c2__BLANK_) and R(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_)) : (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * 0.0016 )) + 50. * Sum ( | false : 0. * 0. * 0. * 0. * inf)"
+ "100. * (Sum (cell_a_y8__BLANK_, cell_b_y8__BLANK_, cell_c1_y8__BLANK_, cell_d_y8__BLANK_, cell_e_y8__BLANK_ | ((cell_2x(cell_a_y8__BLANK_) or cell_2x(cell_b_y8__BLANK_) or cell_2x(cell_c1_y8__BLANK_) or cell_2x(cell_d_y8__BLANK_) or cell_2x(cell_e_y8__BLANK_)) and (cell_2b(cell_a_y8__BLANK_) or cell_2x(cell_a_y8__BLANK_)) and (cell_2b(cell_b_y8__BLANK_) or cell_2x(cell_b_y8__BLANK_)) and (cell_2b(cell_c1_y8__BLANK_) or cell_2x(cell_c1_y8__BLANK_)) and (cell_2b(cell_d_y8__BLANK_) or cell_2x(cell_d_y8__BLANK_)) and (cell_2b(cell_e_y8__BLANK_) or cell_2x(cell_e_y8__BLANK_)) and R2(cell_d_y8__BLANK_, cell_e_y8__BLANK_) and R2(cell_c1_y8__BLANK_, cell_d_y8__BLANK_) and R2(cell_b_y8__BLANK_, cell_c1_y8__BLANK_) and R2(cell_a_y8__BLANK_, cell_b_y8__BLANK_)) : (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * (:(cell_2x(cell_a_y8__BLANK_)) + :(cell_2x(cell_b_y8__BLANK_)) + :(cell_2x(cell_c1_y8__BLANK_)) + :(cell_2x(cell_d_y8__BLANK_)) + :(cell_2x(cell_e_y8__BLANK_))) * 0.0016 ) + Sum (cell_x14_y18__BLANK_, cell_x15_y17__BLANK_, cell_x16_y16__BLANK_, cell_x17_y15__BLANK_, cell_x18_y14__BLANK_ | ((cell_2x(cell_x14_y18__BLANK_) or cell_2x(cell_x15_y17__BLANK_) or cell_2x(cell_x16_y16__BLANK_) or cell_2x(cell_x17_y15__BLANK_) or cell_2x(cell_x18_y14__BLANK_)) and (cell_2b(cell_x14_y18__BLANK_) or cell_2x(cell_x14_y18__BLANK_)) and (cell_2b(cell_x15_y17__BLANK_) or cell_2x(cell_x15_y17__BLANK_)) and (cell_2b(cell_x16_y16__BLANK_) or cell_2x(cell_x16_y16__BLANK_)) and (cell_2b(cell_x17_y15__BLANK_) or cell_2x(cell_x17_y15__BLANK_)) and (cell_2b(cell_x18_y14__BLANK_) or cell_2x(cell_x18_y14__BLANK_)) and R1(cell_x17_y15__BLANK_, cell_x18_y14__BLANK_) and R1(cell_x16_y16__BLANK_, cell_x17_y15__BLANK_) and R1(cell_x15_y17__BLANK_, cell_x16_y16__BLANK_) and R1(cell_x14_y18__BLANK_, cell_x15_y17__BLANK_)) : (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * (:(cell_2x(cell_x14_y18__BLANK_)) + :(cell_2x(cell_x15_y17__BLANK_)) + :(cell_2x(cell_x16_y16__BLANK_)) + :(cell_2x(cell_x17_y15__BLANK_)) + :(cell_2x(cell_x18_y14__BLANK_))) * 0.0016 ) + Sum (cell_x10_y10__BLANK_, cell_x11_y11__BLANK_, cell_x12_y12__BLANK_, cell_x13_y13__BLANK_, cell_x9_y9__BLANK_ | ((cell_2x(cell_x10_y10__BLANK_) or cell_2x(cell_x11_y11__BLANK_) or cell_2x(cell_x12_y12__BLANK_) or cell_2x(cell_x13_y13__BLANK_) or cell_2x(cell_x9_y9__BLANK_)) and (cell_2b(cell_x10_y10__BLANK_) or cell_2x(cell_x10_y10__BLANK_)) and (cell_2b(cell_x11_y11__BLANK_) or cell_2x(cell_x11_y11__BLANK_)) and (cell_2b(cell_x12_y12__BLANK_) or cell_2x(cell_x12_y12__BLANK_)) and (cell_2b(cell_x13_y13__BLANK_) or cell_2x(cell_x13_y13__BLANK_)) and (cell_2b(cell_x9_y9__BLANK_) or cell_2x(cell_x9_y9__BLANK_)) and R0(cell_x9_y9__BLANK_, cell_x10_y10__BLANK_) and R0(cell_x12_y12__BLANK_, cell_x13_y13__BLANK_) and R0(cell_x11_y11__BLANK_, cell_x12_y12__BLANK_) and R0(cell_x10_y10__BLANK_, cell_x11_y11__BLANK_)) : (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * (:(cell_2x(cell_x10_y10__BLANK_)) + :(cell_2x(cell_x11_y11__BLANK_)) + :(cell_2x(cell_x12_y12__BLANK_)) + :(cell_2x(cell_x13_y13__BLANK_)) + :(cell_2x(cell_x9_y9__BLANK_))) * 0.0016 ) + Sum (cell_x8_a0__BLANK_, cell_x8_b0__BLANK_, cell_x8_c2__BLANK_, cell_x8_d0__BLANK_, cell_x8_e0__BLANK_ | ((cell_2x(cell_x8_a0__BLANK_) or cell_2x(cell_x8_b0__BLANK_) or cell_2x(cell_x8_c2__BLANK_) or cell_2x(cell_x8_d0__BLANK_) or cell_2x(cell_x8_e0__BLANK_)) and (cell_2b(cell_x8_a0__BLANK_) or cell_2x(cell_x8_a0__BLANK_)) and (cell_2b(cell_x8_b0__BLANK_) or cell_2x(cell_x8_b0__BLANK_)) and (cell_2b(cell_x8_c2__BLANK_) or cell_2x(cell_x8_c2__BLANK_)) and (cell_2b(cell_x8_d0__BLANK_) or cell_2x(cell_x8_d0__BLANK_)) and (cell_2b(cell_x8_e0__BLANK_) or cell_2x(cell_x8_e0__BLANK_)) and R(cell_x8_d0__BLANK_, cell_x8_e0__BLANK_) and R(cell_x8_c2__BLANK_, cell_x8_d0__BLANK_) and R(cell_x8_b0__BLANK_, cell_x8_c2__BLANK_) and R(cell_x8_a0__BLANK_, cell_x8_b0__BLANK_)) : (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * (:(cell_2x(cell_x8_a0__BLANK_)) + :(cell_2x(cell_x8_b0__BLANK_)) + :(cell_2x(cell_x8_c2__BLANK_)) + :(cell_2x(cell_x8_d0__BLANK_)) + :(cell_2x(cell_x8_e0__BLANK_))) * 0.0016 )) + 50. * Sum ( | false : 0. * 0. * 0. * 0. * inf)"
(Formula.real_str loc_heurs.(0).(0));
);
Modified: trunk/Toss/Server/LearnGame.ml
===================================================================
--- trunk/Toss/Server/LearnGame.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Server/LearnGame.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -19,7 +19,13 @@
let winFormula winningStates notWinningStates =
- Distinguish.distinguish winningStates notWinningStates
+ if !debug_level > 0 then
+ print_endline (
+ "Searching WIN:\n" ^
+ (String.concat "\n" (List.map Structure.str winningStates)) ^ "\nNOT\n"^
+ (String.concat "\n" (List.map Structure.str notWinningStates)));
+ FormulaOps.tnf_fv
+ (Aux.unsome (Distinguish.distinguish winningStates notWinningStates))
let cleanStructure struc =
let funs = ref [] in
Modified: trunk/Toss/Server/LearnGameTest.ml
===================================================================
--- trunk/Toss/Server/LearnGameTest.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Server/LearnGameTest.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -6,43 +6,6 @@
let struc_of_string s =
StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
-let formula_eq ?(flatten_sort=true) phi1 phi2 =
- if flatten_sort then
- assert_equal ~printer:(fun x -> Formula.sprint x)
- (Formula.flatten_sort (formula_of_string phi1))
- (Formula.flatten_sort phi2)
- else
- assert_equal ~printer:(fun x -> Formula.sprint x)
- (formula_of_string phi1) phi2
-
-let formula_list_eq ?(flatten_sort=true) l1 l2 =
- List.iter2 (formula_eq ~flatten_sort) l1 l2
-
-let formula_option_eq ?(flatten_sort=true) fopt1 fopt2 =
- let fopt_str = function None -> "None" | Some f -> Formula.str f in
- if fopt1 = "None" then
- assert_equal ~printer:fopt_str None fopt2
- else match fopt2 with
- | None -> assert_equal ~printer:(fun x -> x) fopt1 "None"
- | Some f -> formula_eq ~flatten_sort fopt1 f
-
-let hashtbl_eq struc list ht =
- let str_pair (tuple, phi) =
- (Structure.tuple_str struc tuple) ^ "->" ^ (Formula.str phi) in
- let str ps = String.concat "; " (List.map str_pair ps) in
- let hashtbl_to_list ht =
- let res = ref [] in
- Hashtbl.iter (fun k v -> res := (k, v) :: !res) ht; !res in
- let lst = List.map (fun (tp, fs) -> (tp, formula_of_string fs)) list in
- let simp l = List.sort Pervasives.compare
- (List.map (fun (t, f) -> (t, Formula.flatten f)) l) in
- assert_equal ~printer:str (simp lst) (simp (hashtbl_to_list ht))
-
-let array_list_str f a = "[| [" ^ (String.concat "]; [" (
- List.map (fun l -> String.concat ";" (List.map f l))
- (Array.to_list a))) ^ "] |]"
-
-
let tests = "LearnGame" >::: [
"simple test game" >::
(fun () ->
@@ -76,8 +39,8 @@
\"" ;]] in
let res_game =
"PLAYERS 1, 2
-REL Win1() = ex x0, x1 (Q(x1) and R(x1, x0))
-REL Win2() = ex x0, x1 (Q(x1) and R(x0, x1))
+REL Win1() = ex x1 (Q(x1) and ex x0 R(x1, x0))
+REL Win2() = ex x1 (Q(x1) and ex x0 R(x0, x1))
RULE Mv1:
[1 | P:1 {}; Q:1 {}; R:2 {} | ] -> [1 | P (1); Q:1 {}; R:2 {} | ]
emb R,Q,P pre not Win2()
Modified: trunk/Toss/Server/Picture.ml
===================================================================
--- trunk/Toss/Server/Picture.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Server/Picture.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -362,7 +362,7 @@
Format.eprintf "@[%a@]@ \n%!" Formula.fprint (Formula.And (basic :: mw));
if !debug_level > -1 then
Format.eprintf "@[%a@]@ \n%!" Formula.fprint
- (Aux.unsome (Distinguish.distinguish_by_type ~qr:1 ~k:2 [right] [wrong]));
+ (Aux.unsome (Distinguish.distinguish_upto ~qr:1 ~k:2 [right] [wrong]));
Formula.flatten (Formula.Ex (ex_vars, Formula.And (basic :: mw)))
)
Modified: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Solver/Distinguish.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -3,10 +3,9 @@
let debug_level = ref 0
let set_debug_level i = (debug_level := i)
-type distinguish_method = Types | Guarded
+type logic = FO | GuardedFO
-
(* Helper functions to construct variables for indices. *)
let varname i = "x" ^ string_of_int i
let varnames k = List.map varname (Aux.range k)
@@ -76,8 +75,9 @@
(* - Guards and Guarded Types - *)
(* Generate all guarded substitutions of [tuple] with the guards.
+ A subst-tuple is a substitution of [tuple] if it has the same length.
A subst-tuple is a guarded substitution of [tuple] if a permuted
- sub-tuple a of subst-tuple containig at least one element of
+ sub-tuple of subst-tuple containig at least one element of
the original [tuple] is in some relation R in the structure [struc].
The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
@@ -206,39 +206,50 @@
| All (vs, f) -> All (vs, greedy_remove (fun x -> cond (All (vs, x))) f)
| phi -> phi
+(* Order on types that we use to select the minimal one. *)
+let compare_types tp1 tp2 =
+ let tp_lits = function And fl -> List.filter Formula.is_literal fl | _-> [] in
+ let c = Formula.compare (And (tp_lits tp1)) (And (tp_lits tp2)) in
+ if c <> 0 then c else Formula.compare tp1 tp2
-let distinguish_by_type ?(how=Guarded) ?(skip_outer_exists=false)
- ~qr ~k pos_struc neg_struc =
- let types s = match how with
- | Guarded -> guarded_types s ~qr ~k
- | Types -> ntypes s ~qr ~k in
- let (pos_tp, neg_tp) = (List.map types pos_struc, List.map types neg_struc) in
- let candidates = List.rev_append (List.concat pos_tp)
- (List.map (fun f -> Not f) (List.concat neg_tp)) in
- let fails_neg f = not (List.exists (fun s -> check s [||] f) neg_struc) in
- let fail_neg = List.filter fails_neg (Aux.unique_sorted candidates) in
- let fail_neg =
- List.rev_map (fun f -> Formula.flatten_sort (FormulaOps.nnf f)) fail_neg in
- let tp_lits = function And fl -> List.filter Formula.is_literal fl | _-> [] in
- let cmp_tp tp1 tp2 =
- let c = Formula.compare (And (tp_lits tp1)) (And (tp_lits tp2)) in
- if c <> 0 then c else Formula.compare tp1 tp2 in
- let fail_neg = Aux.unique_sorted ~cmp:cmp_tp fail_neg in
- let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_struc in
+let compare_types = ref compare_types
+
+(* Find the minimal [logic]-type of [struc] not included in [neg_types]
+ and with at most [qr] quantifiers and [k] variables. *)
+let min_type_omitting ?(logic = GuardedFO) ~qr ~k neg_types struc =
+ let pos_types = match logic with
+ | GuardedFO -> guarded_types struc ~qr ~k
+ | FO -> ntypes struc ~qr ~k in
+ let ok_types = List.filter (fun f -> not (List.mem f neg_types)) pos_types in
+ let ok_types = List.sort !compare_types ok_types in
+ if ok_types = [] then None else Some (List.hd ok_types)
+
+(* Find a [logic]-formula with at most [qr] quantifiers and [k] variables
+ which holds on all [pos_strucs] and on no [neg_strucs]. *)
+let distinguish_upto ?(logic = GuardedFO) ~qr ~k pos_strucs neg_strucs =
+ let types s = match logic with
+ | GuardedFO -> guarded_types s ~qr ~k
+ | FO -> ntypes s ~qr ~k in
+ let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
+ let pos_tps = Aux.unique_sorted ~cmp:!compare_types (
+ Aux.map_some (min_type_omitting ~logic ~qr ~k neg_tps) pos_strucs) in
+ let fails_neg f = not (List.exists (fun s -> check s [||] f) neg_strucs) in
+ let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_strucs in
let rec find_type acc = function
| [] -> []
| x :: xs -> if succ_pos (x::acc) then x :: acc else
find_type (x::acc) xs in
- let dtypes = find_type [] fail_neg in
+ let dtypes = find_type [] pos_tps in
if dtypes = [] then None else
let is_ok f = fails_neg f && succ_pos [f] in
let mintp = greedy_remove is_ok (Or dtypes) in
let fv = FormulaSubst.free_vars mintp in
- let t = FormulaOps.rename_quant_avoiding fv mintp in
- if skip_outer_exists then Some t else
- Some (Ex (List.sort Formula.compare_vars fv, t))
+ Some (FormulaOps.rename_quant_avoiding fv mintp)
-let distinguish ?(how=Guarded) ?(skip_outer_exists=false) strucs1 strucs2 =
+
+(* Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+ Leaves free variables (existential) if [skip_outer_exists] is set. *)
+let distinguish ?(how=GuardedFO) ?(skip_outer_exists=false) strucs1 strucs2 =
if !debug_level > 0 then
Printf.printf "distinguishing:\n\n%s\n\n and\n\n %s\n%!"
(String.concat "\n" (List.map Structure.str strucs1))
@@ -246,8 +257,10 @@
let rec diff qr k =
if qr > k then diff 0 (k+1) else (
if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
- match distinguish_by_type ~how ~skip_outer_exists ~qr ~k strucs1 strucs2 with
- | Some f -> f
+ match distinguish_upto ~logic:how ~qr ~k strucs1 strucs2 with
+ | Some f ->
+ if skip_outer_exists then Some f else
+ Some (Ex (FormulaSubst.free_vars f, f))
| None -> diff (qr+1) k
) in
diff 0 1
Modified: trunk/Toss/Solver/Distinguish.mli
===================================================================
--- trunk/Toss/Solver/Distinguish.mli 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Solver/Distinguish.mli 2011-11-17 17:12:44 UTC (rev 1634)
@@ -1,6 +1,6 @@
(** Distinguish sets of structures by formulas. *)
-type distinguish_method = Types | Guarded
+type logic = FO | GuardedFO
(** {2 Atoms and FO Types} *)
@@ -19,6 +19,7 @@
(** {2 Guards and Guarded Types} *)
(** Generate all guarded substitutions of [tuple] with the guards.
+ A subst-tuple is a substitution of [tuple] if it has the same length.
A subst-tuple is a guarded substitution of [tuple] if a permuted
sub-tuple a of subst-tuple containig at least one element of
the original [tuple] is in some relation R in the structure [struc].
@@ -45,14 +46,26 @@
(** {2 Distinguishing Structure Sets} *)
-val distinguish_by_type: ?how: distinguish_method -> ?skip_outer_exists: bool ->
- qr: int -> k: int -> Structure.structure list -> Structure.structure list ->
- Formula.formula option
-
-val distinguish: ?how: distinguish_method -> ?skip_outer_exists: bool ->
- Structure.structure list -> Structure.structure list -> Formula.formula
+(** Order on types that we use to select the minimal ones. *)
+val compare_types : (Formula.formula -> Formula.formula -> int) ref
+(** Find the minimal [logic]-type of [struc] not included in [neg_types]
+ and with at most [qr] quantifiers and [k] variables. *)
+val min_type_omitting: ?logic: logic -> qr: int -> k: int ->
+ Formula.formula list -> Structure.structure -> Formula.formula option
+(** Find a [logic]-formula with at most [qr] quantifiers and [k] variables
+ which holds on all [pos_strucs] and on no [neg_strucs].
+ Leaves free variables which are implicitly quantified existentially. *)
+val distinguish_upto: ?logic: logic -> qr: int -> k: int ->
+ Structure.structure list -> Structure.structure list -> Formula.formula option
+
+(** Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+ Leaves free variables (existential) if [skip_outer_exists] is set. *)
+val distinguish: ?how: logic -> ?skip_outer_exists: bool ->
+ Structure.structure list -> Structure.structure list -> Formula.formula option
+
+
(** {2 Debugging} *)
val set_debug_level: int -> unit
Modified: trunk/Toss/Solver/DistinguishTest.ml
===================================================================
--- trunk/Toss/Solver/DistinguishTest.ml 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/Solver/DistinguishTest.ml 2011-11-17 17:12:44 UTC (rev 1634)
@@ -208,39 +208,38 @@
(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
);
- "distinguish_by_type" >::
+ "distinguish_upto" >::
(fun () ->
let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
formula_option_eq "None"
- (Distinguish.distinguish_by_type ~qr:2 ~k:1 [struc1] [struc2]);
+ (Distinguish.distinguish_upto ~qr:2 ~k:1 [struc1] [struc2]);
formula_option_eq "None" (* we use guarded types - so None here *)
- (Distinguish.distinguish_by_type ~qr:0 ~k:2 [struc1] [struc2]);
+ (Distinguish.distinguish_upto ~qr:0 ~k:2 [struc1] [struc2]);
formula_option_eq "not R(x0, x1) and not x0 = x1 and not R(x1, x0)"
- (Distinguish.distinguish_by_type ~how:Types ~skip_outer_exists:true
- ~qr:0 ~k:2 [struc1] [struc2]);
+ (Distinguish.distinguish_upto ~logic:FO ~qr:0 ~k:2 [struc1] [struc2]);
formula_option_eq "None" (* we use guarded types - so None here *)
- (Distinguish.distinguish_by_type ~qr:0 ~k:3 [struc1] [struc2]);
+ (Distinguish.distinguish_upto ~qr:0 ~k:3 [struc1] [struc2]);
formula_option_eq "R(x0, x1) and ex x2 R(x2, x0)"
- (Distinguish.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2
- [struc1] [struc2]);
+ (Distinguish.distinguish_upto ~qr:1 ~k:2 [struc1] [struc2]);
let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
- formula_option_eq "ex x0 P(x0)"
- (Distinguish.distinguish_by_type ~qr:0 ~k:1 [struc1] [struc2]);
+ formula_option_eq "P(x0)"
+ (Distinguish.distinguish_upto ~qr:0 ~k:1 [struc1] [struc2]);
);
"distinguish" >::
(fun () ->
let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
- formula_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x2, x0))"
+ formula_option_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x2, x0))"
(Distinguish.distinguish [struc1] [struc2]);
let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
- formula_eq "ex x0 P(x0)" (Distinguish.distinguish [struc1] [struc2]);
+ formula_option_eq "ex x0 P(x0)"
+ (Distinguish.distinguish [struc1] [struc2]);
let struc1 = struc_of_string "[ | | ] \"
...
@@ -254,7 +253,7 @@
...
...
\"" in
- formula_eq "ex x0, x1 (P(x0) and C(x0, x1))"
+ formula_option_eq "ex x0, x1 (P(x0) and C(x0, x1))"
(Distinguish.distinguish [struc1] [struc2]);
);
]
@@ -293,7 +292,7 @@
P..
... ...
...P ...
-\"" in formula_eq
+\"" in formula_option_eq
"P(x0) and P(x1) and C(x0, x1) and ex x2 (P(x2) and C(x2, x0))"
(Distinguish.distinguish ~skip_outer_exists:true
[strucP] [strucN1; strucN2; strucN3]);
@@ -337,7 +336,7 @@
... ... ... ...
...W ... ... ...
\"" in (* Distinguish.set_debug_level 1; *)
- formula_eq "W(x1) and all x0 not C(x1, x0)"
+ formula_option_eq "W(x1) and all x0 not C(x1, x0)"
(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
);
]
Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex 2011-11-16 21:58:12 UTC (rev 1633)
+++ trunk/Toss/www/reference/reference.tex 2011-11-17 17:12:44 UTC (rev 1634)
@@ -1,4 +1,4 @@
-\documentclass{scrbook}
+\documentclass[oneside,fleqn]{scrbook}
% Font choice
\usepackage[sc]{mathpazo}
@@ -94,6 +94,7 @@
\newcommand{\TrST}{\ensuremath{\mathrm{TrST}}}
\newcommand{\lfp}{\mathrm{lfp}}
\newcommand{\gfp}{\mathrm{gfp}}
+\newcommand{\tp}{\mathrm{tp}}
% Theorem environments
\theoremstyle{plain}
@@ -1101,11 +1102,12 @@
\section{Solver Techniques}
-We used a SAT solver (MiniSAT) to operate on symbolic representations
-of MSO variables. We decided in favor of CNF representation instead of
-the more standard BDD approach as it seems to scale in a more consistent way.
+We use a SAT solver (from The Decision Procedure Toolkit, DPT) to operate on
+symbolic representations of MSO variables. We decided in favor of CNF
+representation instead of the more standard BDD approach as it seems to
+scale in a more consistent way.
-For handling real arithmetic, we implemented a quantifier elimination
+For handling real arithmetic, we implement a quantifier elimination
procedure based on Muchnik's proof. It is not as efficient as CAD
(cylindrical algebraic decomposition) but works very consistently
for many cases.
@@ -1113,7 +1115,156 @@
The main formula optimization is just performing the TNF, later we
only push predicates to the front.
+\chapter{Formula and Game Induction}
+In this chapter we present a method for constructing formulas that
+separate sets of structures from such sets given as input, and we
+describe how games can be learned from example plays using this method.
+
+\section{Fragments of First-Order Logic}
+
+The $k$-variable fragment of FO consists of all formulas which use only
+the variables $x_1, \ldots, x_{k-1}$, both as free ones and under quantifiers.
+
+The guarded fragment of FO is defined inductively by
+\[ \phi\ ::= \ R(\ol{x}) \ \mid \ x = x \ \mid \ \neg \phi \ \mid \
+ \phi \land \phi \ \mid \ \phi \lor \phi \ \mid \]
+\[ \phantom{\phi\ :==}\
+ \exists \ol{y} \big( R(\ol{x},\ol{y}) \land \phi(\ol{x},\ol{y}) \big)
+ \quad \mid \quad
+ \forall \ol{y} \big( \neg R(\ol{x},\ol{y}) \lor \phi(\ol{x},\ol{y})\big),\]
+where in the line above $\phi(\ol{x},\ol{y})$ means that all free variables
+of $\phi$ must be included in the set $\{\ol{x}\} \cup \{\ol{y}\}$.
+
+\begin{example}
+Formulas of modal logic translate to guarded first-order logic with two
+variables, so \eg a formula with one free variable $x$ expressing that
+``every $E$-sucessor of $x$ has an $R$-successor in which $P$ holds'' can be
+written in the guarded fragment with two variables as follows:
+\[ \exists y \big( E(x, y) \land \forall x (R(y, x) \to P(y)) \big). \]
+\end{example}
+
+
+\section{Types}
+
+Let $\calL$ be any set of formulas, \eg a fragment of first-order logic.
+The $\calL$-type of a tuple $\ol{a}$ in a structure $\frakA$ is the subset
+of $\calL$ of formulas with as many free variables as $|\ol{a}|$ which are
+satisified by $\ol{a}$ in $\frakA$, \ie
+\[ \calL-\mathrm{type}(\frakA, \ol{a}) =
+ \{ \phi(\ol{x}) \in \calL \mid |\ol{x}| = |\ol{a}| \text{ and }
+ \frakA \models \phi(\ol{a}) \}. \]
+
+The set described above is most often infinite even for trivial reasons, \eg
+it might contain formulas $P(x), P(x) \land P(x), P(x) \land P(x) \land P(x)$,
+and so on -- something which could be described just by $P(x)$. And since in
+many cases there exists one formula describing this set, we will often abuse
+the terminology and say that the $\calL$-type of $\ol{a}$ in $\frakA$ is one
+formula $\tau \in \calL$, denoted $\tau = \tp^\calL(\frakA, \ol{a})$, such that
+\[ \frakA \models \tau(\ol{a}) \text{ and for all } \phi \in
+ \calL-\mathrm{type}(\frakA, \ol{a}) \text{ holds }
+ \tau(\ol{x}) \Rightarrow \phi(\ol{x}). \]
+
+Note that, in principle, such a formula $\tau$ might not exist in $\calL$.
+But it does exist for fragments of FO with bounded quantifier rank,
+additionally bounded number of variables, and additionally guarded.
+The proof of existence is done by inductive construction, and the same
+constructions are also used in our algorithms to compute the types.
+
+\subsubsection{Type in FO with Bounded Rank and Variable Number}
+
+Let $n$ be the bound on the number of quantifiers and let us fix $\frakA$
+and $\ol{a}$ and assume that $|\ol{a}| = k$ is also the bound on the number
+of variables we are allowed to use. We denote the FO type with quantifier rank
+bounded by $n$ and variable number bounded by $k$ by $\tp^{n,k}(\frakA,\ol{a})$.
+
+For $n = 0$, the formula $\tp^{n,k}(\frakA,\ol{a})$ is simply a conjunction of
+all literals satisfied by $\ol{a}$ in $\frakA$, which we compute exhaustively.
+
+For $n > 0$, the formula $\tp^{n,k}(\frakA,\ol{a})$ is given by
+\[ \tp^{n-1,k}(\frakA,\ol{a}) \ \land\ \Land_{i < |\ol{a}|} \left(
+ \forall x_i \left( \Lor_{b \in \frakA}
+ \tp^{n-1,k}(\frakA,\ol{a}[a_i \ot b]) \right) \ \land \
+ \Land_{b \in \frakA} \exists x_i \left(
+ \tp^{n-1,k}(\frakA,\ol{a}[a_i \ot b]) \right) \right). \]
+We omit the proof of correctness for this formula.
+
+
+\subsubsection{Type in Guarded FO with Bounded Rank and Variable Number}
+
+Let $n$ be the bound on the number of quantifiers and let us fix $\frakA$
+and $\ol{a}$ and assume that $|\ol{a}| = k$ is also the bound on the number
+of variables we are allowed to use. We denote the guarded-FO type with
+quantifier rank bounded by $n$ and variable number bounded by $k$ by
+$\tp_g^{n,k}(\frakA,\ol{a})$.
+
+For $n = 0$, $\tp^{n,k}(\frakA,\ol{a})$ is again a conjunction of
+all literals satisfied by $\ol{a}$ in $\frakA$.
+
+For $n > 0$, we first need to consider all \emph{guarded substitutions} of
+the tuple $\ol{a}$. We say that $\ol{b}$ is a guarded substitution of $\ol{a}$
+in $\frakA$ if $|\ol{b}| = |\ol{a}|$, and there is a subset $\{b_1,\ldots,b_k\}$
+of $\ol{b}$ such that $(b_1, \ldots, b_k) \in R^\frakA$ for some $R$, at least
+one $b_i \in \ol{a}$, and on all positions $j < |b|$ either
+$b[j] = a[j]$ or $b[j] = b_i$ for some $i$.
+
+Let now $S$ be the set of all guarded substitutions of $\ol{a}$ and
+$V$ the set of all proper subsets of variables $x_0, \ldots, x_{|a|-1}$.
+For each non-empty set $\sfx \in V$ let $G_\sfx$ denote proper guards
+for $\sfx$, \ie formulas $R(\ol{x}, \ol{y})$ such that $\{\ol{x}\} = \sfx$
+and $\ol{y}$ is not empty. For each such $g \in G_\sfx$ let us denote by
+$S_g$ the subset of $S$ for which the guard $g$ holds, \ie
+$S_g = \{ \ol{b} \in S \mid \frakA \models g(\ol{b}) \}.$
+We will now construct the next type for $\sfx$ and $g \in G_\sfx$ as
+\[ \tau_{\sfx, g} =
+ \forall \sfx \left(g \to
+ \Lor_{\ol{b} \in S_g}\tp_g^{n-1,k}(\frakA,\ol{b}) \right) \ \land \
+ \Land_{\ol{b} \in S_g} \exists \sfx \left(
+ g \land \tp_g^{n-1,k}(\frakA,\ol{b}) \right). \]
+
+Finally, the guarded type $\tp_g^{n,k}(\frakA,\ol{a})$ is given by
+\[ \tp^{n-1,k}(\frakA,\ol{a}) \ \land\
+ \Land_{\sfx \in V} \Land_{g \in G_\sfx} \tau_{\sfx, g}. \]
+
+
+\section{Learning Games}
+
+Let us start by showing how to learn two-player zero-sum games with payoffs only
+$1$, $0$, and $-1$. First, we say that an abstract \emph{play} is a sequence
+\[ \frakA_0 \to_{p_0} \frakA_1 \to_{p_1} \dots \to_{p_{n-1}} \frakA_n, \]
+where each $\frakA_i$ is a structure (the state of the play) and each
+$p_i$ is the player who made that move, \ie $p_i \in \{0,1\}$.
+The input for learning a game as above consists of four sets of plays:
+\begin{enumerate}
+\item[$\Pi_1$] -- plays after which Player~$0$ gets payoff $1$,
+\item[$\Pi_0$] -- plays after which both players get payoff $0$,
+\item[$\Pi_{-1}$] -- plays after which Player~$0$ gets payoff $-1$,
+\item[$\Pi_W$] -- plays in which the last move is incorrect.
+\end{enumerate}
+
+To learn the game, we induce the winning conditions for both players and
+the termination condition, and the rules for moves of the players.
+
+\subsubsection{Termination Condition and Payoffs}
+
+To learn this, we apply the distinguish function described above $3$ times,
+to induce formulas for the last structures in $\Pi_1, \Pi_0$ and $\Pi_{-1}$.
+
+\subsubsection{Inducing Moves}
+
+First, we create for each of the two players two list of pairs
+$(\frakL, \frakR)$ -- one with all his correct moves in the sets $\Pi_*$ and
+the other with incorrect moves of this player, \ie the last ones from $\Pi_W$.
+We create the general move rules by taking the positive list and cutting
+each $(\frakL, \frakR)$ to only the elements that differ. If the list of
+wrong moves is empty, this is the end, we have the moves.
+
+If the list of wrong moves is not empty, we match each general move to
+the right and wrong move pairs in which it could have been applied,
+and use the function distinguish from above to learn a precondition or
+postcondition which will restrict the move only to the correct structures.
+
+
\chapter{GDL to Toss Translation}
\section{Game Description Language}
@@ -1167,28 +1318,20 @@
(init (cell c c b))
(init (control x))
(<= (next (control ?r)) (does ?r noop))
-(<= (next (cell ?x ?y ?r))
- (does ?r (mark ?x ?y)))
-(<= (next (cell ?x ?y ?c))
- (true (cell ?x ?y ?c))
- (does ?r (mark ?x1 ?y1))
+(<= (next (cell ?x ?y ?r)) (does ?r (mark ?x ?y)))
+(<= (next (cell ?x ?y ?c)) (true (cell ?x ?y ?c)) (does ?r (mark ?x1 ?y1))
(or (distinct ?x ?x1) (distinct ?y ?y1)))
-(<= (legal ?r (mark ?x ?y))
- (true (control ?r))
- (true (cell ?x ?y b)))
-(<= (legal ?r noop) (role ?r)
- (not (true (control ?r))))
+(<= (legal ?r (mark ?x ?y)) (true (control ?r)) (true (cell ?x ?y b)))
+(<= (legal ?r noop) (role ?r) (not (true (control ?r))))
(<= (goal ?r 100) (conn3 ?r))
-(<= (goal ?r 50) (role ?r)
- (not exists_line3))
+(<= (goal ?r 50) (role ?r) (not exists_line3))
(<= (goal x 0) (conn3 o))
(<= (goal o 0) (conn3 x))
(<= terminal exists_line3)
(<= terminal (not exists_blank))
(<= exists_blank (true (cell ?x ?y b)))
(<= exists_line3 (role ?r) (conn3 ?r))
-(<= (conn3 ?r) (or (col ?r) (row ?r)
- (diag1 ?r) (diag2 ?r)))
+(<= (conn3 ?r) (or (col ?r) (row ?r) (diag1 ?r) (diag2 ?r)))
(<= (row ?r)
(true (cell ?a ?y ?r)) (nextcol ?a ?b)
(true (cell ?b ?y ?r)) (nextcol ?b ?c)
@@ -2496,10 +2639,8 @@
-\chapter{Design}
+\chapter{Implementation}
-\section{Organization of Code}
-
Toss consists of the main \emph{TossServer} which is built from several
main modules explained in the sections below and corresponding to
directories in the code tree. The main modules contain OCaml modules
@@ -2512,7 +2653,7 @@
specification of available server requests and the response format.
-\section{Formula}
+\subsubsection{Formula}
This most basic directory implements formulas as described above and various
operations on formulas which are necessary for other modules. It also
@@ -2521,28 +2662,28 @@
simplification.
-\section{Solver}
+\subsubsection{Solver}
This directory contains the module which represents relational structures,
and the full Solver, including the elimination-based solver for the theory
of reals and the SAT-based solving algorithm for monadic second-order logic.
-\section{Arena}
+\subsubsection{Arena}
This directory contains modules which implement the game definition,
including discrete and continuous structure rewriting, game file parser
and client-server communication parser and request type.
-\section{Play}
+\subsubsection{Play}
This directory contains modules responsible for automatic play, including
the heuristic generation module, the abstract game tree module and its
instantiations to Maximax and UCT.
-\section{GGP}
+\subsubsection{GGP}
This directory contains the code which translates GDL files into Toss
format together with various needed simplifications. Multiple tests
@@ -2550,19 +2691,14 @@
of the Toss-GGP code.
-\section{Server}
+\subsubsection{Server}
In this directory we simply keep the implementation of TossServer
together with several high-level tests to check that it works ok.
-\section{Client}
+\subsubsection{WebClient}
-This stand-alone Toss client is written in python using the Qt4 library.
-
-
-\section{WebClient}
-
The browser-based client does not currently interface TossServer directly,
but uses a python request Handler.py as an intermediate step. This handler
also manages a database of users and games.
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
