[Toss-devel-svn] SF.net SVN: toss:[1188] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1188] trunk/Toss
|
From: <luk...@us...> - 2010-11-21 21:34:09
|
Revision: 1188
http://toss.svn.sourceforge.net/toss/?rev=1188&view=rev
Author: lukaszkaiser
Date: 2010-11-21 21:34:02 +0000 (Sun, 21 Nov 2010)
Log Message:
-----------
Solver corrections and tests moved to OUnit.
Modified Paths:
--------------
trunk/Toss/Client/SystemDisplay.py
trunk/Toss/Solver/AssignmentSet.ml
trunk/Toss/Solver/AssignmentSet.mli
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/Solver.mli
trunk/Toss/Solver/SolverTest.ml
trunk/Toss/TossTest.ml
Modified: trunk/Toss/Client/SystemDisplay.py
===================================================================
--- trunk/Toss/Client/SystemDisplay.py 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Client/SystemDisplay.py 2010-11-21 21:34:02 UTC (rev 1188)
@@ -43,7 +43,7 @@
suggest_bt = self.toolbar.addAction (QIcon(":/pics/move.svg"),"Hint")
QObject.connect(suggest_bt, SIGNAL("triggered ()"), self.suggest)
- self.__sg_iters = 4
+ self.__sg_iters = 2
self.sg_iters_bt = self.toolbar.addAction ("Depth: " +
str(self.__sg_iters))
QObject.connect(self.sg_iters_bt, SIGNAL("triggered ()"),
Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/AssignmentSet.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -85,14 +85,17 @@
(* List all tuples the first-order assignment [asg] assigns to [vars]
- in order in which [vars] are given. Raise Not_found if the assignment
- is empty. Use [elems] as the set of all elements of the structure. *)
+ in order in which [vars] are given. [elems] are are all elements. *)
let rec tuples elems vars = function
- | Empty -> raise Not_found
+ | Empty -> []
| Any -> List.rev_map Array.of_list
(Aux.product (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
| FO (`FO v, asg_list) ->
- let (idx, vs) = (Aux.find_index v vars, Aux.remove_one v vars) in
+ let (idx, vs) =
+ try
+ (Aux.find_index v vars, Aux.remove_one v vars)
+ with Not_found ->
+ failwith ("assigned var "^ v ^ " not in "^ (String.concat "," vars)) in
let prolong e asg =
Array.of_list (Aux.insert_nth idx e (Array.to_list asg)) in
List.concat (List.rev_map (fun (e, asg) ->
Modified: trunk/Toss/Solver/AssignmentSet.mli
===================================================================
--- trunk/Toss/Solver/AssignmentSet.mli 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/AssignmentSet.mli 2010-11-21 21:34:02 UTC (rev 1188)
@@ -33,6 +33,5 @@
(string * int) list -> assignment_set -> (string * int) list
(* List all tuples the first-order assignment [asg] assigns to [vars]
- in order in which [vars] are given. Raise Not_found if the assignment
- is empty. Use [elems] as the set of all elements of the structure. *)
+ in order in which [vars] are given. [elems] are are all elements. *)
val tuples : Structure.Elems.t -> string list -> assignment_set -> int array list
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/Solver.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -207,15 +207,10 @@
eval_m struc
(RealExpr (Plus (expr, Times (Const (-1.), RVar rvar)), Formula.EQZero))
-let rec remove_dup acc = function
- | [] -> acc
- | [x] -> x :: acc
- | x :: y :: xs when x = y -> remove_dup acc (y :: xs)
- | x :: y :: xs -> remove_dup (x :: acc) (y :: xs)
(* Fast function to get a value of a real expression without free variables
other than those assigned in [asg] explicitely. *)
-let rec get_real_val_a solver asg expr struc =
+let rec get_real_val solver asg expr struc =
let rec check_f = function
Ex (vs, phi) -> check_f phi
| Or (fl) -> List.exists check_f fl
@@ -224,10 +219,10 @@
Char phi -> if check_f phi then 1. else 0.
| Const v -> v
| Times (e1, e2) ->
- (get_real_val_a solver asg e1 struc) *. (get_real_val_a solver asg e2 struc)
+ (get_real_val solver asg e1 struc) *. (get_real_val solver asg e2 struc)
| Plus (e1, e2) ->
- (get_real_val_a solver asg e1 struc) +. (get_real_val_a solver asg e2 struc)
- | Sum (vl, guard, r) -> (* TODO; FIXME; is asg ok down here? *)
+ (get_real_val solver asg e1 struc) +. (get_real_val solver asg e2 struc)
+ | Sum (vl, guard, r) ->
let gd = (
try
let gd_id = List.assoc guard !(solver.reg_formulas) in
@@ -235,13 +230,19 @@
with Not_found ->
Hashtbl.find solver.formulas_eval (register_formula solver guard)
) in
- if !debug_level > 0 then print_endline ("guard " ^ (Formula.str guard));
- let asg = eval_m struc gd in
- let tps = tuples struc.elements (List.map var_str vl) asg in
- let stps = remove_dup [] (List.sort Pervasives.compare tps) in
- let add_val acc tp =
- acc+.(get_real_val_a solver (join asg (asg_of_tuple struc vl tp)) r struc) in
- List.fold_left add_val 0. stps
+ let all_vs = (List.map to_fo (AssignmentSet.assigned_vars [] asg)) @ vl in
+ if !debug_level > 0 then (
+ print_endline ("guard " ^ (Formula.str guard));
+ print_endline ("asg " ^ (AssignmentSet.str asg));
+ print_endline ("sum vars " ^ (Formula.var_list_str vl));
+ print_endline ("all vars " ^ (Formula.var_list_str all_vs));
+ );
+ let asg_gd = join asg (eval_m struc gd) in
+ let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
+ let add_val acc tp =
+ let tp_asg = asg_of_tuple struc all_vs tp in
+ acc +. (get_real_val solver tp_asg r struc) in
+ List.fold_left add_val 0. tps
| _ ->
let rec get_rval = function
| FO (_, [(_, a)]) -> get_rval a
@@ -258,8 +259,6 @@
AssignmentSet.str ev_assgn) in
get_rval (join asg (evaluate_real "#" expr struc))
-let get_real_val expr struc =
- get_real_val_a (new_solver ()) Any expr struc
(* Evaluate i-th formula on j-th structure. *)
let evaluate solver ~formula struc =
@@ -288,7 +287,7 @@
let evaluate struc formula = evaluate solver ~formula struc
let check_formula struc formula =
check solver ~formula struc
- let get_real_val = get_real_val_a solver Any
+ let get_real_val = get_real_val solver Any
let formula_str phi =
let phi = Hashtbl.find solver.formulas_check phi in
Formula.str phi
Modified: trunk/Toss/Solver/Solver.mli
===================================================================
--- trunk/Toss/Solver/Solver.mli 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/Solver.mli 2010-11-21 21:34:02 UTC (rev 1188)
@@ -23,7 +23,8 @@
Assignments.assignment_set
(* Fast function to get a value of a real expression without free variables. *)
-val get_real_val : Formula.real_expr -> Structure.structure -> float
+val get_real_val : solver -> Assignments.assignment_set ->
+ Formula.real_expr -> Structure.structure -> float
(* ------------------------- DEBUGGING ------------------------------------- *)
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/Solver/SolverTest.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -1,4 +1,5 @@
open Solver ;;
+open OUnit ;;
Solver.set_debug_level 0 ;;
Sat.set_debug_level 0;;
@@ -13,129 +14,144 @@
FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
;;
-let nstruc_of_string s =
+let struc_of_string s =
StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
;;
-let struc_of_string s = let struc = nstruc_of_string s in struc ;;
-let test_eval struc_s phi_s =
+let eval_eq struc_s phi_s aset_s =
let (struc, phi) = (struc_of_string struc_s, formula_of_string phi_s) in
let solver = new_solver () in
let f = register_formula solver phi in
- print_string "Evaluating\n ";
- print_endline (Formula.str phi);
- print_string "on\n ";
- print_endline (Structure.str struc);
- print_string "returns:\n ";
- print_endline (AssignmentSet.str (evaluate solver f struc));
- print_endline ""
+ assert_equal ~printer:(fun x -> x)
+ (AssignmentSet.str (evaluate solver f struc)) aset_s
;;
-let test_eval_real struc_s expr_s =
+let eval_real_eq var_s struc_s expr_s aset_s =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
- print_string "Evaluating real expr as r_var\n ";
- print_endline (Formula.real_str expr);
- print_string "on\n ";
- print_endline (Structure.str struc);
- print_string "returns:\n ";
- print_endline (AssignmentSet.str (evaluate_real "r_var" expr struc));
- print_endline ""
+ assert_equal ~printer:(fun x -> x)
+ (AssignmentSet.str (evaluate_real var_s expr struc)) aset_s
;;
-let test_real_val struc_s expr_s =
+let real_val_eq struc_s expr_s x =
let (struc, expr) = (struc_of_string struc_s, real_expr_of_string expr_s) in
- print_string ("Real value of " ^ (Formula.real_str expr) ^ " on\n ");
- print_string ((Structure.str struc) ^ "\nis: ");
- print_endline ((string_of_float (get_real_val expr struc)) ^ "\n");
+ assert_equal ~printer:(fun x -> string_of_float x)
+ (get_real_val (new_solver ()) AssignmentSet.Any expr struc) x
;;
-test_eval "[ | R { (a, b); (a, c) } | ]" "ex x R (x, y)" ;;
-test_eval "[ | R { (a, b); (a, c) } | ]" "x = y" ;;
+let tests = "Solver" >::: [
+ "eval: first-order quantifier free" >::
+ (fun () ->
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "x = y"
+ "{ y->1{ x->1 } , y->2{ x->2 } , y->3{ x->3 } }";
+ eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y"
+ "{ y->2{ x->2 } }";
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "R(x, y) and x = y"
+ "{}";
+ eval_eq "[ | R { (a, a); (a, b) } | ]" "R(x, y) and x = y"
+ "{ y->1{ x->1 } }";
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "not x = y"
+ "{ y->1{ x->2, x->3 } , y->2{ x->1, x->3 } , y->3{ x->1, x->2 } }";
+ eval_eq "[ | R { (a, a); (a, c) } | ]" "R (x, y) and not x = y"
+ "{ y->2{ x->1 } }";
+ );
-test_eval "[ | R { (a, b); (b, c) }; P { b } | ]" "P(x) and x = y" ;;
+ "eval: first-order with quantifiers" >::
+ (fun () ->
+ eval_eq "[ | R { (a, b); (a, c) } | ]" "ex x R (x, y)"
+ "{ y->2, y->3 }";
+ eval_eq "[ | R { (a, b); (b, c) }; P { b } | ]"
+ "ex x ( P(x) and not (ex y R(x, y)) )"
+ "{}";
+ );
-test_eval "[ | R { (a, b); (a, c) } | ]" "R(x, y) and x = y" ;;
+ "eval: mso quantifier free basic" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]" "x in X"
+ "{ x->1{ X->(inc {1} excl {}) } }";
+ eval_eq "[ | P { a } | ]" "not (x in X)"
+ "{ x->1{ X->(inc {} excl {1}) } }";
+ eval_eq "[ | P { a } | ]" "x in X and x in Y"
+ "{ x->1{ Y->(inc {1} excl {}){ X->(inc {1} excl {}) } } }";
+ eval_eq "[ | P { a } | ]" "x in X and not (x in Y)"
+ "{ x->1{ Y->(inc {} excl {1}){ X->(inc {1} excl {}) } } }";
+ eval_eq "[ | P { a } | ]" "x in X and x = y and not (x in X)"
+ "{}";
+ eval_eq "[ | P { a } | ]" "x in X and x in Y and (x = y and not (x in Y))"
+ "{}";
+ eval_eq "[ | P { a } | ]" "x in X and (x in X or x in Y)"
+ "{ x->1{ X->(inc {1} excl {}) } }";
+ );
-test_eval "[ | R { (a, a); (a, b) } | ]" "R(x, y) and x = y" ;;
+ "eval: mso quantifier free" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C)))"
+ ("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
+ " excl {}) }, X->(inc {1} excl {}) } } }");
+ eval_eq "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C) or (t in X)))"
+ ("{ t->1{ X2->(inc {1} excl {}){ X->(inc {} excl {}){ C->(inc {1}" ^
+ " excl {}) }, X->(inc {1} excl {}) } } }");
+ eval_eq "[ | P { a } | ]"
+ "(((t in X2) and ((t in X) or (((t in C) or (t in X)) and ((not t in C)
+ or (not (t in X))))) and ((not (t in X)) or ((t in C) and (t in X)) or
+ ((not (t in C)) and (not (t in X))))))"
+ "{ t->1{ X2->(inc {1} excl {}){ C->(inc {1} excl {}) } } }";
+ );
-test_eval "[ | R { (a, b); (b, c) }; P { b } | ]"
- "ex x ( P(x) and not (ex y R(x, y)) )" ;;
+ "eval: mso with only first-order quantifiers" >::
+ (fun () ->
+ eval_eq "[ | P { a } | ]"
+ "(not t in X2) or ((t in X2) and (t in X3)) and
+ all s (s in X3 or not P(s))"
+ ("{ t->1{ X3->(inc {} excl {}){ X2->(inc {} excl {1}) }," ^
+ " X3->(inc {1} excl {}) } }");
+ );
-test_eval "[ | R { (a, b); (a, c) } | ]" "not x = y" ;;
+ "eval: mso with quantifiers" >::
+ (fun () ->
+ let reach_f =
+ "all X (x in X and (all z,v (z in X and R(z,v)-> v in X))-> y in X)" in
+ eval_eq "[ | R { (a, b); (a, c) } | ]" reach_f
+ "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 } }";
+ eval_eq "[ | R { (a, b); (b, c) } | ]" reach_f
+ "{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
+ eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
+ ("x != y and not R(x, y) and " ^ reach_f)
+ ("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
+ " y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
+ " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 } }");
+ );
-test_eval "[ | R { (a, a); (a, c) } | ]" "R (x, y) and not x = y" ;;
+ "eval: with real values" >::
+ (fun () ->
+ eval_eq "[ | P { x } | ] " "ex :x ((:x^2 + 3*:x + 2 < 0) and (:x < 0))"
+ "T";
+ eval_eq "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]" ":f(x) > 2"
+ "{ x->3 }";
+ eval_eq "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]"
+ "ex :x (:x^2 + :x * :f(x) + 2 < 0)"
+ "{ x->3 }";
+ eval_eq "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y))) > 0"
+ "{ x->1 }";
+ );
-test_eval "[ | P { a } | ]" "x in X" ;;
-
-test_eval "[ | P { a } | ]" "not (x in X)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x in Y" ;;
-
-test_eval "[ | P { a } | ]" "x in X and not (x in Y)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x = y and not (x in X)" ;;
-
-test_eval "[ | P { a } | ]" "x in X and x in Y and (x = y and not (x in Y))" ;;
-
-test_eval "[ | P { a } | ]" "x in X and (x in X or x in Y)" ;;
-
-test_eval "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C)))" ;;
-
-test_eval "[ | P { a } | ]" "(t in X2) and ((t in X) or ((t in C) or (t in X)))" ;;
-
-test_eval "[ | P { a } | ]"
- ("(((t in X2) and ((t in X) or (((t in C) or (t in X)) and ((not (t in C)) or" ^
- " (not (t in X))))) and ((not (t in X)) or ((t in C) and (t in X)) or ((not (t in C)) and (not (t in X))))))") ;;
-
-test_eval "[ | P { a } | ]" "(not t in X2) or ((t in X2) and (t in X3)) and all s (s in X3 or not P(s))" ;;
-
-let reach_f =
- "all X (x in X and ( all z,v (z in X and R (z, v) -> v in X )) -> y in X)" ;;
-
-test_eval "[ | R { (a, b); (a, c) } | ]" reach_f ;;
-
-test_eval "[ | R { (a, b); (b, c) } | ]" reach_f ;;
-
-test_eval "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]"
- ("x != y and not R(x, y) and " ^ reach_f) ;;
-
-test_eval "[ | P { x } | ] " "ex :x ((:x^2 + 3*:x + 2 < 0) and (:x < 0))" ;;
-
-test_eval "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]" ":f(x) > 2" ;;
-
-test_eval "[ | P { x } | f { x -> 1, y -> 2, z -> 3 } ]"
- "ex :x (:x^2 + :x * :f(x) + 2 < 0)" ;;
-
-test_eval "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y))) > 0" ;;
-
-test_eval_real "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y)))" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " ":(ex x (R (x, x))) + 1" ;;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]" "Sum (x | true : :f(x)^2)" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x | true : :(all y (R (x, y))))";;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x | all y (R (x, y)) : 1)";;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]"
- "Sum (x, y | P(x) : :f(x) * :f(y))" ;;
-
-test_real_val "[ | P { x } | f { x->1, y->2, z->3 } ]"
- "Sum (x, y | true : :f(x) * :f(y))" ;;
-
-test_real_val "[ | R { (a, a); (a, b) } | ] " "Sum (x, y | R (x, y) : 1)";;
-
-
-(* Heuristic guard evaluation test. *)
-
-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) and C(w, r) and R(v, r))) or ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w)))) and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(v)) and (not P(w)) and (not P(x)) and (not P(y)) and (not P(z))" ^
- "and (not ex v, w, x, y, z ((((C(y, z) and C(x, y) and C(w, x) and C(v, w)) or (R(y, z) and R(x, y) and R(w, x) and R(v, w)) or ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))) or ex r, s, t, u ((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and R(v, r)))) and P(z) and P(y) and P(x) and P(w) and P(v)))))" ;;
-
-(* Formula.print (FormulaOps.tnf_fv (formula_of_string heur_phi)) ;; *)
-
-test_eval "[ | | ] \"
+ "eval: game heuristic tests" >::
+ (fun () ->
+ let heur_phi = "(((R(v, w) and R(w, x) and R(x, y) and R(y, z)) or
+ (C(v, w) and C(w, x) and C(x, y) and C(y, z)) or ex r, s, t, u
+ ((C(z, u) and R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s)
+ and C(w, r) and R(v, r))) or ex r, s, t, u ((R(y, u) and R(x, t) and
+ R(w, s) and R(v, r) and C(u, z) and C(t, y) and C(s, x) and C(r, w))))
+ and (Q(z) or Q(y) or Q(x) or Q(w) or Q(v)) and (not P(v)) and (not P(w))
+ and (not P(x)) and (not P(y)) and (not P(z))" ^
+ "and (not ex v, w, x, y, z ((((C(y, z) and C(x, y) and C(w, x) and
+ C(v, w)) or (R(y, z) and R(x, y) and R(w, x) and R(v, w)) or
+ ex r, s, t, u ((R(y, u) and R(x, t) and R(w, s) and R(v, r) and C(u, z)
+ and C(t, y) and C(s, x) and C(r, w))) or ex r, s, t, u ((C(z, u) and
+ R(y, u) and C(y, t) and R(x, t) and C(x, s) and R(w, s) and C(w, r) and
+ R(v, r)))) and P(z) and P(y) and P(x) and P(w) and P(v)))))" in
+ let _ () = Formula.print (FormulaOps.tnf_fv (formula_of_string heur_phi)) in
+ eval_eq "[ | | ] \"
... ... ... ...
P ... ... ... ...
... ... ... ...
@@ -152,10 +168,64 @@
...P ... P.. ...
... ... ... ...
... ... ...Q ...
-\"" heur_phi ;;
+\"" heur_phi
+ ("{ z->5{ y->12{ x->19{ w->26{ v->33 } } } } ," ^
+ " z->6{ y->5{ x->4{ w->3{ v->2 } } } } ," ^
+ " z->7{ y->6{ x->5{ w->4{ v->3 } } } } ," ^
+ " z->8{ y->7{ x->6{ w->5{ v->4 } } } } ," ^
+ " z->32{ y->39{ x->46{ w->53{ v->60 } } } } ," ^
+ " z->48{ y->47{ x->46{ w->45{ v->44 } } } } ," ^
+ " z->53{ y->44{ x->35{ w->26{ v->17 } } } } ," ^
+ " z->58{ y->50{ x->42{ w->34{ v->26 } } } } ," ^
+ " z->62{ y->53{ x->44{ w->35{ v->26 } } } } ," ^
+ " z->63{ y->54{ x->45{ w->36{ v->27 } } } } }");
+ );
+ "eval real: basic" >::
+ (fun () ->
+ eval_real_eq "r" "[ | R { (a, a); (a, b) } | ] " ":(all y (R (x, y)))"
+ "{ x->1{ ((1.) + ((-1.)*r) = 0) } , x->2{ ((0.) + ((-1.)*r) = 0) } }";
+ );
+ "get real val" >::
+ (fun () ->
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ ":(ex x (R (x, x))) + 1" 2.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x | true : :f(x)^2)" 14.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | true : :(all y (R (x, y))))" 1.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x | all y (R (x, y)) : 1)" 1.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | P(x) : :f(x) * :f(y))" 6.;
+ real_val_eq "[ | P { x } | f { x->1, y->2, z->3 } ]"
+ "Sum (x, y | true : :f(x) * :f(y))" 36.;
+ real_val_eq "[ | R { (a, a); (a, b) } | ] "
+ "Sum (x, y | R (x, y) : 1)" 2.;
+ );
+] ;;
+
+let a =
+ let file_from_path p =
+ String.sub p (String.rindex p '/'+1)
+ (String.length p - String.rindex p '/' - 1) in
+ let test_fname name =
+ let fname = file_from_path Sys.executable_name in
+ String.length fname >= String.length name &&
+ String.sub fname 0 (String.length name) = name in
+ (* So that the tests are not run twice while building TossTest. *)
+ if test_fname "SolverTest" then
+ match test_filter [""] tests with
+ | Some tests -> ignore (run_test_tt ~verbose:true tests)
+ | None -> ()
+;;
+
+
+
+
+
(* ----------------------- FOUR POINTS PROBLEM --------------------------- *)
(*
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2010-11-21 20:45:43 UTC (rev 1187)
+++ trunk/Toss/TossTest.ml 2010-11-21 21:34:02 UTC (rev 1188)
@@ -1,7 +1,7 @@
open OUnit
let formula_tests = "Formula" >::: [
- AuxTest.tests;
+ (* AuxTest.tests; *)
FormulaTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
@@ -10,6 +10,7 @@
let solver_tests = "Solver" >::: [
StructureTest.tests;
FFSolverTest.tests;
+ SolverTest.tests;
]
let arena_tests = "Arena" >::: [
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
