[Toss-devel-svn] SF.net SVN: toss:[1211] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1211] trunk/Toss
|
From: <luk...@us...> - 2010-11-30 15:31:52
|
Revision: 1211
http://toss.svn.sourceforge.net/toss/?rev=1211&view=rev
Author: lukstafi
Date: 2010-11-30 15:31:45 +0000 (Tue, 30 Nov 2010)
Log Message:
-----------
FFSolver: rewrite of existential quantification.
Modified Paths:
--------------
trunk/Toss/Play/GameTest.ml
trunk/Toss/Solver/FFSolver.ml
trunk/Toss/Solver/FFSolverTest.ml
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2010-11-30 00:13:26 UTC (rev 1210)
+++ trunk/Toss/Play/GameTest.ml 2010-11-30 15:31:45 UTC (rev 1211)
@@ -675,9 +675,9 @@
]
let search_tests algo randomize effort_easy effort_medium effort_hard =
- let easy_case = compute_try algo randomize effort_easy 120
- and medium_case = compute_try algo randomize effort_medium 240
- and hard_case = compute_try algo randomize effort_hard 600 in
+ let easy_case = compute_try algo randomize effort_easy 240
+ and medium_case = compute_try algo randomize effort_medium 600
+ and hard_case = compute_try algo randomize effort_hard 1200 in
algo >::: [
"tictactoe suggest tie" >:: (fun () ->
@@ -950,7 +950,6 @@
"gomoku8x8 more pieces" >::
(fun () ->
- skip_if true "takes too long -- uncheck later";
let state = update_game gomoku8x8_game
"[ | | ] \"
... ... ... ...
Modified: trunk/Toss/Solver/FFSolver.ml
===================================================================
--- trunk/Toss/Solver/FFSolver.ml 2010-11-30 00:13:26 UTC (rev 1210)
+++ trunk/Toss/Solver/FFSolver.ml 2010-11-30 15:31:45 UTC (rev 1211)
@@ -51,8 +51,7 @@
| A.Real _ | A.MSO _ ->
failwith "Real/MSO assignments not supported yet"
-(* Use a bigger assignment set as the first argument. TODO: obsolete
- this function by optimizations of disjunction and existential q. *)
+(* Use a bigger assignment set as the first argument. *)
let sum_assignment_sets all_elems aset1 aset2 =
let sbs2 = invert_aset [[]] aset2 in
let rec aux sb = function
@@ -75,8 +74,7 @@
failwith "Real/MSO assignments not supported yet" in
List.fold_right aux sbs2 aset1
-(* Remove existentially quantified variables from the solution. TODO:
- obsolete this function by optimizing treatment of ex. q. variables. *)
+(* Remove existentially quantified variables from the solution. *)
let rec project all_elems aset v =
match aset with
| A.Empty -> A.Empty
@@ -226,7 +224,7 @@
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 =
+ let bsbs =
Aux.unique (=) (List.map (List.sort Pervasives.compare) bsbs) in
(* {{{ log entry *)
if !debug_level > 3 then (
@@ -241,10 +239,12 @@
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
- {!ff_tnf}).
+(* 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 {!FFTNF.ff_tnf}). We assume that every
+ existentially quantified single disjunct [Ex (vs, Or [phi])] marks
+ the fact that the body [phi] does not have universal quantifiers
+ (guaranteed by {!FFSolver.add_locvar_info}).
We use the structure of the formula to organize search and build
the result on the recursive stack. Accumulated substitution stores
@@ -258,7 +258,9 @@
position, delayed2: would have to split on all elements. We fold
over disjunctive constraints by keeping the aset subtree to which
we merge from the current context to produce the final answer. (It
- is initialized with Empty aset.)
+ is initialized with Empty aset.) In the same way we fold over
+ assignments for local variables: existentially quantified variables
+ that do not have a universal quantifier in their scope.
The rules to merge (disjoin) the current aset (cur-aset) and the
current position (cur-pos):
@@ -314,8 +316,9 @@
(e4) apply the case (c)
*)
(* Model used only for debugging. *)
-let rec merge model all_elems v init_domain sb cur_aset eval_cont =
- match cur_aset with
+let merge model all_elems is_local v init_domain sb cur_aset
+ eval_cont =
+ let rec aux = function (* v not in local_vars *)
| A.MSO _ | A.Real _ -> failwith
"FFSolver.evaluate: MSO and Real not supported yet"
(* a *)
@@ -357,11 +360,20 @@
| _ -> (* when A.mem_assoc v cur_aset *)
let pull_v e =
e, project_v_on_elem v e cur_aset in
- let cur_aset =
- A.FO (v, map_try pull_v all_elems) in
- merge model all_elems v init_domain sb cur_aset eval_cont
+ aux (A.FO (v, map_try pull_v all_elems)) in
+ if is_local then
+ (* similar to case (d), but fold instead of mapping *)
+ let choose cur_aset e =
+ eval_cont ((v, e)::sb) cur_aset in
+ let pos_assgns =
+ fold_try ~catch:(v :> var) choose cur_aset init_domain in
+ if pos_assgns = A.Empty then raise Unsatisfiable
+ else pos_assgns
+ else aux cur_aset
+
+
(* "Negate" the second assignment set wrt. [all_elems] and add it to the
first aset. *)
(* Model used only for debugging. *)
@@ -378,7 +390,7 @@
(* Empty will turn into Any on recursive callback *)
try List.assoc e assgns with Not_found -> A.Empty in
add_complement model all_elems dset cset in
- merge model all_elems v all_elems [] disj_aset add_cont
+ merge model all_elems false v all_elems [] disj_aset add_cont
| A.Real _ | A.MSO _ ->
failwith "FFSolver: Real/MSO assignments not supported yet"
@@ -406,7 +418,7 @@
optimize]. Check universally quantified variables for coverage.
Do not return [A.Empty], raise [Unsatisfiable] instead. *)
- let rec solve delayed2 delayed1 conj_cont sb cur_aset =
+ let rec solve local_vars 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%!"
@@ -425,9 +437,9 @@
) else match conj_cont with
| [] ->
if delayed1 <> []
- then solve delayed2 [] (List.rev delayed1) sb cur_aset
+ then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
else if delayed2 <> []
- then solve [] [] (List.rev delayed2) sb cur_aset
+ then solve local_vars [] [] (List.rev delayed2) sb cur_aset
(* b *)
else (
(* {{{ log entry *)
@@ -446,10 +458,10 @@
if not (Tuples.mem tup tuples_s)
then raise (Unsatisfiable_FO (vars_of_array (var_tup vtup)))
else if conj_cont <> []
- then solve delayed2 delayed1 conj_cont sb cur_aset
+ then solve local_vars delayed2 delayed1 conj_cont sb cur_aset
else if delayed1 <> []
- then solve delayed2 [] (List.rev delayed1) sb cur_aset
- else solve [] [] (List.rev delayed2) sb cur_aset
+ then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
+ else solve local_vars [] [] (List.rev delayed2) sb cur_aset
with Not_found ->
(* we will add new variables one at a time *)
let nvi =
@@ -460,7 +472,7 @@
let multi_unkn = Aux.array_existsi
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && conj_cont <> [] then (* delay *)
- solve delayed2 (atom::delayed1) conj_cont sb cur_aset
+ solve local_vars 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
@@ -505,15 +517,15 @@
else if not multi_unkn && conj_cont = [] && delayed1 = [] &&
delayed2 = []
then (* no more vars and conjuncts *)
- merge model all_elems nvar init_domain sb cur_aset
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) 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 model all_elems nvar init_domain sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar init_domain sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
)
(* by analogy to the [Rel (relname, vtup)] case *)
@@ -522,7 +534,7 @@
(try
if not (List.assoc x sb = List.assoc y sb)
then raise (Unsatisfiable_FO (vars_of_list (vtup :> var list)))
- else solve delayed2 delayed1 conj_cont sb cur_aset
+ else solve local_vars delayed2 delayed1 conj_cont sb cur_aset
with Not_found ->
(* we will add new variables one at a time *)
let nvi, nvar =
@@ -533,7 +545,7 @@
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
- solve (atom::delayed2) delayed1 conj_cont sb cur_aset
+ solve local_vars (atom::delayed2) delayed1 conj_cont sb cur_aset
else if multi_unkn then
let conj_cont = atom::conj_cont in
(* {{{ log entry *)
@@ -542,8 +554,8 @@
(sb_str model sb) (Formula.str atom);
);
(* }}} *)
- merge model all_elems nvar all_elems sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar all_elems sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
else
let ovar = if nvi = 1 then x else y in
let e = List.assoc ovar sb in
@@ -554,8 +566,8 @@
(Structure.elem_str model e);
);
(* }}} *)
- merge model all_elems nvar [e] sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar [e] sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
)
(* by analogy to the [Rel (relname, vtup)] case *)
@@ -568,10 +580,10 @@
then raise
(Unsatisfiable_FO (vars_of_array (var_tup vtup)))
else if conj_cont <> []
- then solve delayed2 delayed1 conj_cont sb cur_aset
+ then solve local_vars delayed2 delayed1 conj_cont sb cur_aset
else if delayed1 <> []
- then solve delayed2 [] (List.rev delayed1) sb cur_aset
- else solve [] [] (List.rev delayed2) sb cur_aset
+ then solve local_vars delayed2 [] (List.rev delayed1) sb cur_aset
+ else solve local_vars [] [] (List.rev delayed2) sb cur_aset
with Not_found ->
(* we will add new variables one at a time *)
let nvi =
@@ -583,15 +595,15 @@
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
- solve (literal::delayed2) delayed1 conj_cont sb cur_aset
+ solve local_vars (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
+ solve local_vars delayed2 (literal::delayed1) conj_cont sb cur_aset
else if multi_unkn then
(* we cannot easily optimize *)
let conj_cont = [literal] in
- merge model all_elems nvar all_elems sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar all_elems sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
else
let tuples_i =
try StringMap.find relname model.incidence
@@ -632,8 +644,8 @@
else
(* If not [multi_unkn] then for elements in [init_domain]
rel does not hold *)
- merge model all_elems nvar init_domain sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar init_domain sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
)
(* by analogy to both [Eq] and [not Rel] cases *)
@@ -642,7 +654,7 @@
(try
if List.assoc x sb = List.assoc y sb
then raise (Unsatisfiable_FO (vars_of_list ([x; y] :> var list)))
- else solve delayed2 delayed1 conj_cont sb cur_aset
+ else solve local_vars delayed2 delayed1 conj_cont sb cur_aset
with Not_found ->
(* we will add new variables one at a time *)
let nvi, nvar =
@@ -653,9 +665,9 @@
(fun i v->i>nvi && not (List.mem v oldvars)) vtup in
if multi_unkn && (conj_cont <> [] || delayed1 <> [])
then (* delay *)
- solve (literal::delayed2) delayed1 conj_cont sb cur_aset
+ solve local_vars (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
+ solve local_vars delayed2 (literal::delayed1) conj_cont sb cur_aset
else if multi_unkn then begin
(* {{{ log entry *)
if !debug_level > 2 then (
@@ -663,8 +675,8 @@
(sb_str model sb) (Formula.str literal);
);
(* }}} *)
- merge model all_elems nvar all_elems sb cur_aset
- (solve delayed2 delayed1 (literal :: conj_cont))
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar all_elems sb cur_aset
+ (solve local_vars delayed2 delayed1 (literal :: conj_cont))
end else (* optimize *)
let ovar = if nvi = 1 then x else y in
let e = List.assoc ovar sb in
@@ -677,19 +689,18 @@
(* }}} *)
let init_domain =
Elems.elements (Elems.remove e model.elements) in
- merge model all_elems nvar init_domain sb cur_aset
- (solve delayed2 delayed1 conj_cont)
+ merge model all_elems (Vars.mem (nvar :> var) local_vars) nvar init_domain sb cur_aset
+ (solve local_vars delayed2 delayed1 conj_cont)
)
+ | Or [_] :: _ | And [_] :: _ -> assert false
+
(* use associativity, but don't invert the order *)
| And conj :: conj_cont ->
let conj_cont =
if conj_cont = [] then conj else conj @ conj_cont in
- solve delayed2 delayed1 conj_cont sb cur_aset
+ solve local_vars delayed2 delayed1 conj_cont sb cur_aset
- | Or [phi] :: conj_cont ->
- solve delayed2 delayed1 (phi::conj_cont) sb cur_aset
-
(* Propagate implication constraints. *)
| Or fl :: conj_cont when List.exists
(function Not _ -> true | _ -> false) fl ->
@@ -703,7 +714,7 @@
(function Not phi -> Aux.Left phi | phi -> Aux.Right phi) fl in
(* assignments of the guard alone *)
let guard_set =
- try solve [] [] guard sb A.Empty
+ try solve local_vars [] [] guard sb A.Empty
with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty in
(* {{{ log entry *)
if !debug_level > 2 then (
@@ -714,14 +725,14 @@
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
+ solve local_vars delayed2 delayed1 conj_cont sb cur_aset
else
(* hopefully more constrained
(TODO: don't redo the guard?) *)
let concl =
match body with
| [concl] -> concl | _ -> Or body in
- solve delayed2 delayed1 (guard @ [concl] @ conj_cont) sb cur_aset
+ solve local_vars delayed2 delayed1 (guard @ [concl] @ conj_cont) sb cur_aset
(* Continue in each branch folding disjuncts; "Or []" is OK. *)
| Or fl :: conj_cont ->
@@ -738,11 +749,34 @@
(Formula.str phi) (AssignmentSet.named_str model dset);
);
(* }}} *)
- solve delayed2 delayed1 (phi::conj_cont) sb dset)
+ solve local_vars delayed2 delayed1 (phi::conj_cont) sb dset)
cur_aset fl
| Ex ([], phi) :: _ | All ([], phi) :: _ -> assert false
+ (* Local variables -- handled by merging online. *)
+ | Ex (vl, Or [phi]) :: conj_cont ->
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solving-for-local-variables: %s...\n%!"
+ (String.concat ", " (List.map Formula.var_str vl));
+ );
+ (* }}} *)
+ let local_vars = add_vars vl local_vars in
+ (* FIXME: after debugging return to tail call *)
+ let aset =
+ solve local_vars delayed2 delayed1 (phi::conj_cont) sb
+ cur_aset in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ printf "Solved-local-variables: %s; aset=%s\n%!"
+ (String.concat ", " (List.map Formula.var_str vl))
+ (AssignmentSet.named_str model aset);
+ );
+ (* }}} *)
+ (* TODO: handle other kinds *)
+ aset
+
(* Only project, as the mechanics of existential variables is
handled at the site of their first occurrence. *)
| Ex (vl, phi) :: conj_cont ->
@@ -752,7 +786,7 @@
(String.concat ", " (List.map Formula.var_str vl));
);
(* }}} *)
- let aset = solve delayed2 delayed1 (phi::conj_cont) sb cur_aset in
+ let aset = solve local_vars delayed2 delayed1 (phi::conj_cont) sb cur_aset in
(* {{{ log entry *)
if !debug_level > 2 then (
printf "Solved-variables: %s; aset=%s\n%!"
@@ -781,7 +815,7 @@
(String.concat ", " (List.map Formula.var_str vl));
);
(* }}} *)
- let aset = solve delayed2 delayed1 (phi::conj_cont) sb cur_aset in
+ let aset = solve local_vars delayed2 delayed1 (phi::conj_cont) sb cur_aset in
(* {{{ log entry *)
if !debug_level > 2 then (
printf "Solved-variables: %s; aset=%s\n%!"
@@ -812,14 +846,14 @@
(* }}} *)
let aset =
(* solving in empty context! *)
- try solve [] [] [phi] [] A.Empty
+ try solve local_vars [] [] [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
+ solve local_vars delayed2 delayed1 conj_cont sb cur_aset
else raise Unsatisfiable
| RealExpr _ :: _ | In _ :: _ ->
@@ -839,7 +873,7 @@
aset
*)
in
- try solve [] [] [phi] sb disj_aset
+ try solve Vars.empty [] [] [phi] sb disj_aset
with Unsatisfiable_FO _ | Unsatisfiable -> A.Empty
(* Assignments of a single variable that are supported by all
@@ -965,7 +999,34 @@
| Sum (vl, gd, e) -> Sum (vl, norm gd, aux e) in
aux expr
+let add_locvar_info phi =
+ let rec has_univ = function
+ | All _ -> true
+ | Or js | And js -> List.exists has_univ js
+ | Ex (_, phi) -> has_univ phi
+ | _ -> false in (* assumes (partial) NNF *)
+ let rec aux = function
+ | Ex (vs, phi) when not (has_univ phi) ->
+ Ex (vs, Or [aux phi])
+ | Ex (vs, phi) -> Ex (vs, aux phi)
+ | All (vs, phi) -> All (vs, aux phi)
+ | Not phi -> Not (aux phi) (* subtasks also apply *)
+ | Or [phi] -> aux phi
+ | And [phi] -> aux phi
+ | Or djs -> Or (List.map aux djs)
+ | And cjs -> And (List.map aux cjs)
+ | atom -> atom in
+ aux phi
+let rec add_locvar_info_expr = function
+ | Times (a,b) ->
+ Times (add_locvar_info_expr a, add_locvar_info_expr b)
+ | Plus (a,b) ->
+ Plus (add_locvar_info_expr a, add_locvar_info_expr b)
+ | Char (phi) -> Char (add_locvar_info phi)
+ | Sum (vs, guard, expr) ->
+ Sum (vs, add_locvar_info guard, add_locvar_info_expr expr)
+ | simple -> simple
(* Interface to {!SolverIntf}. *)
module M = struct
@@ -978,26 +1039,32 @@
let evaluate_partial struc sb reg_phi =
if not (snd !reg_phi) then
reg_phi :=
- normalize_for_model struc
- ((* FormulaOps.simplify *) (fst !reg_phi)), true;
+ add_locvar_info
+ (normalize_for_model struc
+ ((* FormulaOps.simplify *) (fst !reg_phi))), true;
evaluate struc ~sb (fst !reg_phi)
let evaluate struc reg_phi =
if not (snd !reg_phi) then
reg_phi :=
- normalize_for_model struc
- ((* FormulaOps.simplify *) (fst !reg_phi)), true;
+ add_locvar_info
+ (normalize_for_model struc
+ ((* FormulaOps.simplify *) (fst !reg_phi))), true;
evaluate struc (fst !reg_phi)
let check_formula struc reg_phi =
if not (snd !reg_phi) then
- reg_phi := normalize_for_model struc (fst !reg_phi), true;
+ reg_phi :=
+ add_locvar_info
+ (normalize_for_model struc (fst !reg_phi)), true;
check_formula struc (fst !reg_phi)
let get_real_val reg_expr struc =
if not (snd !reg_expr) then
reg_expr :=
- normalize_expr_for_model struc (fst !reg_expr), true;
+ add_locvar_info_expr
+ (normalize_expr_for_model struc (fst !reg_expr)), true;
get_real_val (fst !reg_expr) struc
let formula_str reg_phi =
if not (snd !reg_phi) then
+ (* TODO: inconsistent with other defs *)
(* to increase consistency of display *)
reg_phi := FormulaOps.simplify (fst !reg_phi), false;
Formula.str (fst !reg_phi)
Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml 2010-11-30 00:13:26 UTC (rev 1210)
+++ trunk/Toss/Solver/FFSolverTest.ml 2010-11-30 15:31:45 UTC (rev 1211)
@@ -32,18 +32,17 @@
let eval_eq struc_s phi_s aset_s =
let struc = struc_of_str struc_s in
- let f =
- FFSolver.normalize_for_model struc (formula_of_str phi_s) in
+ let f = FFSolver.M.register_formula (formula_of_str phi_s) in
assert_equal ~printer:(fun x -> x) aset_s
- (AssignmentSet.named_str struc (FFSolver.evaluate struc f))
+ (AssignmentSet.named_str struc (FFSolver.M.evaluate struc f))
;;
let real_val_eq struc_s expr_s x =
let struc = struc_of_str struc_s in
let expr =
- FFSolver.normalize_expr_for_model struc (real_of_str expr_s) in
+ FFSolver.M.register_real_expr (real_of_str expr_s) in
assert_equal ~printer:(fun x -> string_of_float x) ~msg:expr_s
- x (FFSolver.get_real_val expr struc)
+ x (FFSolver.M.get_real_val expr struc)
let tests = "FFSolver" >::: [
"eval: first-order quantifier free from SolverTest.ml" >::
@@ -96,7 +95,16 @@
);
"eval: first-order with quantifiers more" >::
- (fun () -> ()
+ (fun () ->
+ eval_eq "[ | R {(a,a); (a,b); (a,c); (a,d)}; S {(a,b); (b,c); (c,d); (d,d)}; P(d) | ]"
+ "ex x all y ex z (R(x,y) and S(y,z) and v=x)"
+ "{ v->a }";
+ eval_eq "[ | R {(a,a); (a,b); (a,c); (a,d)}; S {(a,b); (b,c); (c,d); (d,d)}; P(d) | ]"
+ "ex z all y ex x (R(x,y) and S(y,z) and v=z)"
+ "{}";
+ eval_eq "[ | R {(a,a); (a,b); (a,c); (a,d)}; S {(a,b); (b,c); (c,d); (d,d)}; P(d) | ]"
+ "ex x all y ex z (R(x,y) and S(y,z))"
+ "T";
);
"evaluate: negation" >::
@@ -172,7 +180,7 @@
. Q .
\"" heur_phi
- "{ z->a3{ y->a2{ x->a1 } } , z->c1{ y->b1{ x->a1 } } }";
+ "{ y->b1{ z->c1{ x->a1 } } , y->a2{ z->a3{ x->a1 } } }";
);
"eval: gomoku heuristic from SolverTest.ml" >::
@@ -209,7 +217,7 @@
... ... ... ...
... ... ...Q ...
\"" 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 } } } } }");
+ "{ 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 } } } } }");
"get_real_val: tic-tac-toe winning" >::
(fun () ->
@@ -324,7 +332,7 @@
Aux.run_test_if_target "FFSolverTest" tests
let a () =
- match test_filter ["FFSolver:8:eval: gomoku heuristic from SolverTest.ml"]
+ match test_filter ["FFSolver:4:eval: first-order with quantifiers more"]
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.
|
