[Toss-devel-svn] SF.net SVN: toss:[1740] trunk/Toss/Solver/SolverTest.ml

[<ab...@us...>]

Revision: 1740
          http://toss.svn.sourceforge.net/toss/?rev=1740&view=rev
Author:   abuzaid
Date:     2012-07-02 22:31:54 +0000 (Mon, 02 Jul 2012)
Log Message:
-----------
Updated SO -> QBF and SO evaluation Tests

Modified Paths:
--------------
    trunk/Toss/Solver/SolverTest.ml

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2012-07-02 22:09:09 UTC (rev 1739)
+++ trunk/Toss/Solver/SolverTest.ml	2012-07-02 22:31:54 UTC (rev 1740)
@@ -166,24 +166,19 @@
     );
 
   "convert: second-order to QBF" >::
-    (fun () ->(
+    (fun () ->
       let qbf_str_eq struc_s phi_s qbf_s =
         let phi, struc = formula_of_string phi_s, struc_of_string struc_s in
         LOG 1 "%s" (Formula.str phi);
         assert_equal ~printer:(fun x -> x) qbf_s 
-          (BoolFormula.qbf_str (Solver.so_to_qbf struc phi)) in
-
+          (BoolFormula.qbf_str (Solver.so_to_qbf struc phi)) in(						
       qbf_str_eq "[ a, b | T { a } | ]" "ex |R all x, y (T(x) or |R (x, y))"
-        "which result is ok?";
-      
-      print_endline (Formula.str (formula_of_string "ex |V all |Q ex |R all x, y (T(x) or |R (x, y))"));
-      print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "ex |R all x, y (T(x) or |R (x, y))")));
-			
-      print_endline (Formula.str (formula_of_string "all |Q  all x, y (T(x) or Q(y) or (x = y))")); 
-      print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "all |Q  all x, y (T(x) or Q(y) or (x = y))")));
-      
-      print_endline (Formula.str (formula_of_string "ex x all  y ((T(x) and T(y)) -> x = y)")); 
-      print_endline (BoolFormula.qbf_str (Solver.so_to_qbf (struc_of_string "[ a, b | T { a } | ]") (formula_of_string "ex x all  y ((T(x) and T(y)) -> x = y)")));			)			
+			        "(ex 3, 4 (3 and 4))";            
+			qbf_str_eq "[ a, b | T { a } | ]" "all |Q  all x, y (T(x) or Q(y) or (x = y))"
+        "false";				
+			qbf_str_eq "[ a, b, c | E { (a,b); (b,c); (c,a) } | ]" ("ex |R, |G all x, y ( (|R(x) or |G(x)) and (" ^ " E(x,y) -> not ( (|R(x) and  |R(y)) " ^ " or (|G(x) and |G(y)))))")
+        "(ex 1, 5, 7, 9, 13, 17, 21, 23, 25, 27, 29, 33 (ex 2, 6, 8, 10, 14, 18, 22, 24, 26, 28, 30, 34 (((1 or 2) and ((5 or 6) and (not ((5 and 7) or (6 and 8)))) and (9 or 10)) and ((13 or 14) and (17 or 18) and ((21 or 22) and (not ((21 and 23) or (22 and 24))))) and (((25 or 26) and (not ((25 and 27) or (26 and 28)))) and (29 or 30) and (33 or 34)))))";
+			);	      			
     );
   
   "eval: second-order" >::
@@ -203,6 +198,12 @@
             "      or (|G(x) and |G(y)) or (|B(x) and |B(y)) ) ) )") in
       let triangle = "[ | E { (a, b); (b, c); (c, a) } | ] " in
       eval_eq triangle col3phi "T";
+			
+			let col2phi = ("ex |R, |G all x, y ( (|R(x) or |G(x)) and (" ^
+            " E(x,y) -> not ( (|R(x) and  |R(y)) " ^
+            "      or (|G(x) and |G(y)))))") in
+			let triangle = "[ a,b,c | E { (a, b); (b, c); (c, a) } | ] " in
+			eval_eq triangle col2phi "F";
     );
   
   "eval: game heuristic tests" >::

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.