[Toss-devel-svn] SF.net SVN: toss:[1427] trunk/Toss

[<luk...@us...>]

Revision: 1427
          http://toss.svn.sourceforge.net/toss/?rev=1427&view=rev
Author:   lukaszkaiser
Date:     2011-05-01 00:33:55 +0000 (Sun, 01 May 2011)

Log Message:
-----------
Complete moving ClassTest to OUnit, merge with PresbTest; many cleanups in Formula ml and tests, among others str = sprint now; start implementing functions for fixed-points.

Modified Paths:
--------------
    trunk/Toss/Arena/DiscreteRuleTest.ml
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Formula/BoolFormulaTest.ml
    trunk/Toss/Formula/BoolFunctionTest.ml
    trunk/Toss/Formula/FFTNFTest.ml
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Formula/FormulaTest.ml
    trunk/Toss/Play/HeuristicTest.ml
    trunk/Toss/Server/PictureTest.ml
    trunk/Toss/Server/Server.ml
    trunk/Toss/Solver/Class.ml
    trunk/Toss/Solver/ClassTest.ml
    trunk/Toss/TossFullTest.ml
    trunk/Toss/TossTest.ml

Removed Paths:
-------------
    trunk/Toss/Solver/PresbTest.ml

Modified: trunk/Toss/Arena/DiscreteRuleTest.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRuleTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Arena/DiscreteRuleTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -590,7 +590,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_equal ~printer:(fun x->x) ~msg:"one not opt"
-        "(not O(b))-> true"
+        "not O(b)-> true"
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | _opt_D (e); O(e) | ]" in
@@ -604,7 +604,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_equal ~printer:(fun x->x) ~msg:"del one not opt"
-        "O(b)-> (not O(b))"
+        "O(b)-> not O(b)"
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | D (e); _opt_O(e) | ]" in
@@ -618,7 +618,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_one_of ~msg:"match defined"
-        ["(P(b) or Q(b))-> O(b)"; "(Q(b) or P(b))-> O(b)"]
+        ["P(b) or Q(b)-> O(b)"; "Q(b) or P(b)-> O(b)"]
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | D (e); _opt_O(e) | ]" in
@@ -632,14 +632,14 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_one_of ~msg:"match defined 2"
-        ["(P(b) or Q(b))-> (O(b) and (not P(b)) and (not Q(b)))";"(Q(b) or P(b))-> (O(b) and (not P(b)) and (not Q(b)))"]
+        ["P(b) or Q(b)-> (O(b) and not P(b) and not Q(b))";
+	 "Q(b) or P(b)-> (O(b) and not P(b) and not Q(b))"]
 	(rule_obj_str rule_obj);
 
     ); 
 
   "compile_rule: special relations" >::
     (fun () ->
-
       let lhs_struc = struc_of_str "[ e | _diffthan_D (e); _any_ (e) | ]" in
       let rhs_struc = struc_of_str "[ b | _opt_O (b) | ]" in
       let signat = ["O", 1; "P", 1; "Q", 1] in
@@ -651,7 +651,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_equal ~printer:(fun x->x) ~msg:"defrel: diffthan P Q"
-        "((not P(b)) and (not Q(b)))-> true"
+        "(not P(b) and not Q(b))-> true"
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | _del_D (e); O(e) | ]" in
@@ -665,7 +665,10 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_one_of ~msg:"del defrel"
-        ["(O(b) and (not P(b)) and (not Q(b)) and (_del_P(b) or _del_Q(b)))-> (P(b) and (not O(b)))";"((_del_Q(b) or _del_P(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))";"((_del_P(b) and O(b) and (not P(b)) and (not Q(b))) or (_del_Q(b) and O(b) and (not P(b)) and (not Q(b))))-> (P(b) and (not O(b)))";"((_del_P(b) or _del_Q(b)) and O(b) and (not P(b)) and (not Q(b)))-> (P(b) and (not O(b)))"]
+        ["(O(b) and not P(b) and not Q(b) and (_del_P(b) or _del_Q(b)))-> (P(b) and not O(b))";
+	 "((_del_Q(b) or _del_P(b)) and O(b) and not P(b) and not Q(b))-> (P(b) and not O(b))";
+	 "((_del_P(b) and O(b) and not P(b) and not Q(b)) or (_del_Q(b) and O(b) and not P(b) and not Q(b)))-> (P(b) and not O(b))";
+	 "((_del_P(b) or _del_Q(b)) and O(b) and not P(b) and not Q(b))-> (P(b) and not O(b))"]
 	(rule_obj_str rule_obj);
 
       let lhs_struc = struc_of_str "[ e | _opt_D (e); _diffthan_P(e) | ]" in
@@ -679,7 +682,7 @@
         pre = Formula.And [];
         rule_s = [1,1]} in
       assert_equal ~printer:(fun x->x) ~msg:"diffthan override"
-        "((not O(b)) and (not P(b)))-> (O(b) and (not Q(b)))"
+        "(not O(b) and not P(b))-> (O(b) and not Q(b))"
 	(rule_obj_str rule_obj);
 
     ); 

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/Aux.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -589,6 +589,12 @@
   (* So that the tests are not run twice while building TossTest. *)
   run_if_target target_name f
 
+let set_optimized_gc () =
+  Gc.set { (Gc.get()) with
+    Gc.space_overhead = 300;  (* 300% instead of 80% std *)
+    Gc.minor_heap_size = 160*1024; (* 4*std, opt ~= L2 cache/proc *)
+    Gc.major_heap_increment = 8*124*1024 (* 8*std ok *) 
+  }
 
 let rec input_file file =
   let buf = Buffer.create 256 in

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/Aux.mli	2011-05-01 00:33:55 UTC (rev 1427)
@@ -289,6 +289,9 @@
 (** Run a test suite if the executable name matches the given prefix. *)
 val run_test_if_target : string -> OUnit.test -> unit
 
+(** Set more agressive Gc values optimized for heavier computations. *)
+val set_optimized_gc : unit -> unit
+
 (** Input a file to a string. *)
 val input_file : in_channel -> string
 

Modified: trunk/Toss/Formula/BoolFormulaTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFormulaTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/BoolFormulaTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -20,8 +20,11 @@
   let b_flat = BoolFormula.flatten_sort b_nnf in
   BoolFormula.to_reduced_form b_flat
 
-let assert_eq_string arg msg x y = 
+let assert_eq_string arg msg x_in y_in = 
   let full_msg = msg ^ " (argument: " ^ arg ^ ")" in
+  let ws = Str.regexp "[ \n\t]+" in
+  let x = Str.global_replace ws " " (" " ^ x_in ^ " ") in
+  let y = Str.global_replace ws " " (" " ^ y_in ^ " ") in
   assert_equal ~printer:(fun x -> x) ~msg:full_msg 
     ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
 
@@ -56,7 +59,7 @@
       test_cnf_bool "P(x)" "P(x)";
 
       test_bool_auxcnf "not P(x)" "-1" "-1" "1";
-      test_cnf_bool "not P(x)" "(not P(x))";
+      test_cnf_bool "not P(x)" "not P(x)";
 
       test_bool_auxcnf "P(x) and (P(y) or P(z))"
 	"((3 or 2) and 1)" "(not (-1 or (not (2 or 3))))"
@@ -73,8 +76,8 @@
 	    " and (7 or 6) and (7 or 3) and (-5 or -4 or -6) and (6 or 5) " ^ 
 	    "and (6 or 4))");
       test_cnf_bool "not (A(x) and B(x)) or (not P(x) or (C(x) and D(y)))"
-	("((D(y) or (not P(x)) or (not B(x)) or (not A(x))) and " ^ 
-	    "(C(x) or (not P(x)) or (not B(x)) or (not A(x))))");
+	("((D(y) or not P(x) or not B(x) or not A(x)) and " ^ 
+	    "(C(x) or not P(x) or not B(x) or not A(x)))");
 	
       test_bool_auxcnf "(P(x) and P(y)) or (not P(x) and not P(y))"
 	"((-2 and -1) or (2 and 1))" "((not (-1 or -2)) or (not (1 or 2)))"
@@ -82,7 +85,7 @@
 	    "(-2 or -1 or -4) and (4 or 2) and (4 or 1) and (2 or 1 or -3) " ^ 
 	    "and (3 or -2) and (3 or -1))");
       test_cnf_bool "(P(x) and P(y)) or (not P(x) and not P(y))"
-	"((P(y) or (not P(x))) and ((not P(y)) or P(x)))";
+	"((P(y) or not P(x)) and (not P(y) or P(x)))";
     );
 
   "Plaisted Greenbaum auxcnf and cnf" >::
@@ -153,14 +156,14 @@
 	"not ((P(x) and P(x)) and Q(x)) or (P(y) or Q(z))"
 	"-1 | -2 | 3 | 4";
       test_cnf_bool "not ((P(x) and P(x)) and Q(x)) or (P(y) or Q(z))" 
-	"(Q(z) or P(y) or (not Q(x)) or (not P(x)))";
+	"Q(z) or P(y) or not Q(x) or not P(x)";
 
       test_flat_reduced_cnf_list 
 	"not (A(x) and B(x)) or (not P(x) or (C(x) and D(y)))"
 	"-1 | -2 | -3 | 4 & -1 | -2 | -3 | 5";
       test_cnf_bool "not (A(x) and B(x)) or (not P(x) or (C(x) and D(y)))"
-	("((D(y) or (not P(x)) or (not B(x)) or (not A(x))) and " ^ 
-	    "(C(x) or (not P(x)) or (not B(x)) or (not A(x))))");
+	("((D(y) or not P(x) or not B(x) or not A(x)) and " ^ 
+	    "(C(x) or not P(x) or not B(x) or not A(x)))");
 
       test_flat_reduced_cnf_list 
 	("(P(x) and P(a)) or (P(x) and P(b)) or (P(x) and P(c))" ^ 
@@ -170,7 +173,7 @@
       test_cnf_bool ("(P(x) and P(a)) or (P(x) and P(b)) or (P(x) and P(c))" ^ 
 			" or (P(x) and P(d)) or (not P(x) and Q(a))" ^ 
 			" or (not P(x) and Q(b)) or (not P(x) and Q(c))")
-	("((P(d) or P(c) or P(b) or P(a) or (not P(x))) " ^ 
+	("((P(d) or P(c) or P(b) or P(a) or not P(x)) " ^ 
 	    "and (Q(c) or Q(b) or Q(a) or P(x)))");
     );
 
@@ -413,10 +416,7 @@
 
 
 let main () =
-  Gc.set { (Gc.get()) with
-    Gc.space_overhead = 300;  (* 300% instead of 80% std *)
-    Gc.minor_heap_size = 160*1024; (* 4*std, opt ~= L2 cache/proc *)
-    Gc.major_heap_increment = 8*124*1024 (* 8*std ok *) };
+  Aux.set_optimized_gc ();
   let (file) = (ref "") in
   let opts = [
     ("-v", Arg.Unit (fun () -> set_debug_elim true), "be verbose");

Modified: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/BoolFunctionTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -107,10 +107,7 @@
 
 
 let main () =
-  Gc.set { (Gc.get()) with
-    Gc.space_overhead = 300;  (* 300% instead of 80% std *)
-    Gc.minor_heap_size = 160*1024; (* 4*std, opt ~= L2 cache/proc *)
-    Gc.major_heap_increment = 8*124*1024 (* 8*std ok *) };
+  Aux.set_optimized_gc ();
   let (file, print_bool, debug_level) = (ref "", ref false, ref 0) in
   let dbg_level i = (debug_level := i; BoolFunction.set_debug_level i) in
   let (only_inline, only_fp, nf) = (ref false, ref false, ref 0) in
@@ -128,7 +125,7 @@
      "do not compute the goal, but resolve the fixed-points");
   ] in
   Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
-  if !file = "" then ignore (OUnit.run_test_tt tests) else
+  if !file = "" then ignore (OUnit.run_test_tt ~verbose:true tests) else
     let f = open_in !file in
     let file_s = Aux.input_file f in
     close_in f;

Modified: trunk/Toss/Formula/FFTNFTest.ml
===================================================================
--- trunk/Toss/Formula/FFTNFTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/FFTNFTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -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 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))))"
 
 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))))))"
@@ -25,12 +25,12 @@
 let winQvwxyz =
   "ex v, w, x, y, z ((((((Q(v) and Q(w)) and Q(x)) and Q(y)) and Q(z)) and ((((((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 ((((((((R(v, r) and C(r, w)) and R(w, s)) and C(s, x)) and R(x, t)) and C(t, y)) and R(y, u)) and C(u, z)))) or ex r, s, t, u ((((((((R(v, r) and C(w, r)) and R(w, s)) and C(x, s)) and R(x, t)) and C(y, t)) and R(y, u)) and C(z, u))))))"
 
-let breakW_expanded = "ex y8 ((W(y8) and ex y7 ((C(y7, y8) and ex y6 ((C(y6, y7) and ex y5 ((C(y5, y6) and ex y4 ((C(y4, y5) and ex y3 ((C(y3, y4) and ex y2 ((C(y2, y3) and ex y1 (C(y1, y2))))))))))))))))"
+let breakW_expanded = "ex y8 (W(y8) and ex y7 (C(y7, y8) and ex y6 (C(y6, y7) and ex y5 (C(y5, y6) and ex y4 (C(y4, y5) and ex y3 (C(y3, y4) and ex y2 (C(y2, y3) and ex y1 C(y1, y2))))))))"
 
-let winQvwxyz_expanded = "ex v ((Q(v) and (ex w ((R(v, w) and Q(w) and ex x ((R(w, x) and Q(x) and ex y ((R(x, y) and Q(y) and ex z ((R(y, z) and Q(z))))))))) or ex w ((C(v, w) and Q(w) and ex x ((C(w, x) and Q(x) and ex y ((C(x, y) and Q(y) and ex z ((C(y, z) and Q(z))))))))) or ex r0 ((R(v, r0) and ex w ((C(r0, w) and Q(w) and ex s0 ((R(w, s0) and ex x ((C(s0, x) and Q(x) and ex t0 ((R(x, t0) and ex y ((C(t0, y) and Q(y) and ex u0 ((R(y, u0) and ex z ((C(u0, z) and Q(z))))))))))))))))) or ex r ((R(v, r) and ex w ((C(w, r) and Q(w) and ex s ((R(w, s) and ex x ((C(x, s) and Q(x) and ex t ((R(x, t) and ex y ((C(y, t) and Q(y) and ex u ((R(y, u) and ex z ((C(z, u) and Q(z))))))))))))))))))))"
+let winQvwxyz_expanded = "ex v (Q(v) and (ex w (R(v, w) and Q(w) and ex x (R(w, x) and Q(x) and ex y (R(x, y) and Q(y) and ex z (R(y, z) and Q(z))))) or ex w (C(v, w) and Q(w) and ex x (C(w, x) and Q(x) and ex y (C(x, y) and Q(y) and ex z (C(y, z) and Q(z))))) or ex r0 (R(v, r0) and ex w (C(r0, w) and Q(w) and ex s0 (R(w, s0) and ex x (C(s0, x) and Q(x) and ex t0 (R(x, t0) and ex y (C(t0, y) and Q(y) and ex u0 (R(y, u0) and ex z (C(u0, z) and Q(z))))))))) or ex r (R(v, r) and ex w (C(w, r) and Q(w) and ex s (R(w, s) and ex x (C(x, s) and Q(x) and ex t (R(x, t) and ex y (C(y, t) and Q(y) and ex u (R(y, u) and ex z (C(z, u) and Q(z)))))))))))"
 
 (* Alpha-conversion of the above. *)
-let winQvwxyz_idempotent = "ex v ((Q(v) and (ex w2 ((R(v, w2) and Q(w2) and ex x2 ((R(w2, x2) and Q(x2) and ex y2 ((R(x2, y2) and Q(y2) and ex z2 ((R(y2, z2) and Q(z2))))))))) or ex w1 ((C(v, w1) and Q(w1) and ex x1 ((C(w1, x1) and Q(x1) and ex y1 ((C(x1, y1) and Q(y1) and ex z1 ((C(y1, z1) and Q(z1))))))))) or ex r0 ((R(v, r0) and ex w0 ((C(r0, w0) and Q(w0) and ex s0 ((R(w0, s0) and ex x0 ((C(s0, x0) and Q(x0) and ex t0 ((R(x0, t0) and ex y0 ((C(t0, y0) and Q(y0) and ex u0 ((R(y0, u0) and ex z0 ((C(u0, z0) and Q(z0))))))))))))))))) or ex r ((R(v, r) and ex w ((C(w, r) and Q(w) and ex s ((R(w, s) and ex x ((C(x, s) and Q(x) and ex t ((R(x, t) and ex y ((C(y, t) and Q(y) and ex u ((R(y, u) and ex z ((C(z, u) and Q(z))))))))))))))))))))"
+let winQvwxyz_idempotent = "ex v (Q(v) and (ex w2 (R(v, w2) and Q(w2) and ex x2 (R(w2, x2) and Q(x2) and ex y2 (R(x2, y2) and Q(y2) and ex z2 (R(y2, z2) and Q(z2))))) or ex w1 (C(v, w1) and Q(w1) and ex x1 (C(w1, x1) and Q(x1) and ex y1 (C(x1, y1) and Q(y1) and ex z1 (C(y1, z1) and Q(z1))))) or ex r0 (R(v, r0) and ex w0 (C(r0, w0) and Q(w0) and ex s0 (R(w0, s0) and ex x0 (C(s0, x0) and Q(x0) and ex t0 (R(x0, t0) and ex y0 (C(t0, y0) and Q(y0) and ex u0 (R(y0, u0) and ex z0 (C(u0, z0) and Q(z0))))))))) or ex r (R(v, r) and ex w (C(w, r) and Q(w) and ex s (R(w, s) and ex x (C(x, s) and Q(x) and ex t (R(x, t) and ex y (C(y, t) and Q(y) and ex u (R(y, u) and ex z (C(z, u) and Q(z)))))))))))"
 
 let formula_of_guards posi_frels nega_frels phi =
   let guards = FFTNF.ffsep posi_frels nega_frels phi in
@@ -44,24 +44,31 @@
     | _ -> Formula.Or parts
 
 
+let assert_eq_str ?(msg="") x_in y_in = 
+  let ws = Str.regexp "[ \n\t]+" in
+  let x = Str.global_replace ws " " (" " ^ x_in ^ " ") in
+  let y = Str.global_replace ws " " (" " ^ y_in ^ " ") in
+  assert_equal ~printer:(fun x -> x) ~msg ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
+
+
 let tests = "FFTNF" >::: [
   "pn_nnf: subtasks and renaming" >::
     (fun () ->
       assert_equal ~printer:(fun x->x) ~msg:"subtask, no renaming"
-        "ex x ((P(x) and (not ex x ((not Q(x))))))"
+        "ex x (P(x) and not ex x not Q(x))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "ex x P(x) and all x Q(x)")));
       assert_equal ~printer:(fun x->x)
-        "ex x, y (all x0 ((P(x) and (not R(x0, y)))))"
+        "ex x, y all x0 (P(x) and not R(x0, y))"
         (Formula.str (FFTNF.p_pn_nnf
-          (formula_of_str "ex x,y (P(x) and (not (ex x R(x,y))))")));
+          (formula_of_str "ex x,y (P(x) and not ex x R(x,y))")));
       (* "subtask": negated existential without free variables *)
       assert_equal ~printer:(fun x->x)
-        "ex x ((P(x) and (not ex x (Q(x)))))"
+        "ex x (P(x) and not ex x Q(x))"
         (Formula.str (FFTNF.p_pn_nnf
-          (formula_of_str "ex x (P(x) and (not ex x Q(x)))")));
+			(formula_of_str "ex x (P(x) and not ex x Q(x))")));
       assert_equal ~printer:(fun x->x)
-        "ex x (ex x0 ((P(x) and (not Q(x0)))))"
+        "ex x ex x0 (P(x) and not Q(x0))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "ex x (P(x) and (not (all x Q(x))))")));
     );
@@ -69,19 +76,19 @@
   "pn_nnf: subtasks and merging" >::
     (fun () ->
       assert_equal ~printer:(fun x->x)
-        "ex z (((not ex x (all y ((not R(x, y))))) and Q(z)))"
+        "ex z (not ex x all y not R(x, y) and Q(z))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "(all x ex y R(x,y)) and (ex z Q(z))")));
       assert_equal ~printer:(fun x->x) ~msg:"one subtask, merge rest"
-        "ex y (ex v (all w (all z ((((not ex x ((not P(x)))) and R(y, z)) and C(v, w))))))"
+        "ex y ex v all w all z (not ex x not P(x) and R(y, z) and C(v, w))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "all x P(x) and ex y (all z R(y,z)) and ex v (all w C(v,w))")));
       assert_equal ~printer:(fun x->x) ~msg:"subtask breaks PNF"
-        "ex y (all z (ex v (((not ex x (all y (ex v (((not Q(v)) or (not R(x, y))))))) and (P(v) and R(y, z))))))"
+        "ex y\n all z\n  ex v (not ex x all y ex v (not Q(v) or not R(x, y)) and P(v) and R(y, z))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "all x (ex y (all v (Q(v) and R(x,y)))) and ex y (all z (ex v (P(v) and R(y,z))))")));
       assert_equal ~printer:(fun x->x) ~msg:"no subtask: free dependent"
-        "ex y (all z (all x (ex y0 (ex v (all v0 ((((P(f) and Q(v0)) and R(x, y0)) and (P(v) and R(y, z)))))))))"
+        "ex y\n all z\n  all x ex y0 ex v all v0 (P(f) and Q(v0) and R(x, y0) and P(v) and R(y, z))"
         (Formula.str (FFTNF.p_pn_nnf
           (formula_of_str "all x (ex y (all v (P(f) and Q(v) and R(x,y)))) and ex y (all z (ex v (P(v) and R(y,z))))")));
     );
@@ -132,8 +139,8 @@
     (fun () ->
       (* R(x, y) comes before Q(y) etc. because x is an older
          variable in the result. *)
-      assert_equal ~printer:(fun x->x)
-        "ex x ((Q(x) and (ex y ((R(x, y) and Q(y) and ex z ((R(y, z) and Q(z))))) or ex y ((C(x, y) and Q(y) and ex z ((C(y, z) and Q(z))))) or ex v0 ((R(x, v0) and ex y ((C(v0, y) and Q(y) and ex u0 ((R(y, u0) and ex z ((C(u0, z) and Q(z))))))))) or ex v ((R(x, v) and ex y ((C(y, v) and Q(y) and ex u ((R(y, u) and ex z ((C(z, u) and Q(z))))))))))))"
+      assert_eq_str
+        "ex x (Q(x) and (ex y (R(x, y) and Q(y) and ex z (R(y, z) and Q(z))) or ex y (C(x, y) and Q(y) and ex z (C(y, z) and Q(z))) or ex v0 (R(x, v0) and ex y (C(v0, y) and Q(y) and ex u0 (R(y, u0) and ex z (C(u0, z) and Q(z))))) or ex v (R(x, v) and ex y (C(y, v) and Q(y) and ex u (R(y, u) and ex z (C(z, u) and Q(z)))))))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str winQxyz)));
@@ -141,15 +148,15 @@
 
   "ffsep: tic-tac-toe" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x) ~msg:"simple idempotence"
+      assert_eq_str ~msg:"simple idempotence"
         winQzyx
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
             (formula_of_str winQzyx)));
 
-      assert_equal ~printer:(fun x->x) ~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)))))"
+      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))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
@@ -159,7 +166,7 @@
 
   "ff_tnf: breakthrough" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x)
+      assert_eq_str
         breakW_expanded
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["W"; "B"]))
@@ -168,7 +175,7 @@
 
   "ff_tnf: idempotent breakthrough" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x)
+      assert_eq_str
         breakW_expanded
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["W"; "B"]))
@@ -177,7 +184,7 @@
 
   "ff_tnf: gomoku" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x)
+      assert_eq_str
         winQvwxyz_expanded
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
@@ -186,7 +193,7 @@
 
   "ff_tnf: idempotent gomoku" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x)
+      assert_eq_str
         winQvwxyz_idempotent
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
@@ -196,38 +203,38 @@
   "ff_tnf: deep" >::
     (fun () ->
       (* pulling out P first breaks the disjunction *)
-      assert_equal ~printer:(fun x->x) ~msg:"#1"
-        "(ex z (((not Q(z)) and ex x, y ((not R(x, y))))) or ex x ((P(x) and ex z (((not Q(z)) and ex y (C(y, z)))))))"
+      assert_eq_str ~msg:"#1"
+        "ex z (not Q(z) and ex x, y not R(x, y)) or ex x (P(x) and ex z (not Q(z) and ex y C(y, z)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#1.5"
-        "ex z (((not Q(z)) and (ex y ((C(y, z) and ex x (P(x)))) or ex x, y ((not R(x, y))))))"
+      assert_eq_str ~msg:"#1.5"
+        "ex z (not Q(z) and (ex y (C(y, z) and ex x P(x)) or ex x, y not R(x, y)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z (not Q(z) and (not R(x,y) or (P(x) and C(y,z))))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#2"
-        "(ex z (((not Q(z)) and ex x, y ((not R(x, y))))) or ex x (((not P(x)) and ex z (((not Q(z)) and ex y ((not C(y, z))))))))"
+      assert_eq_str ~msg:"#2"
+        "ex z (not Q(z) and ex x, y not R(x, y)) or ex x (not P(x) and ex z (not Q(z) and ex y not C(y, z)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#2.5"
-        "ex z (((not Q(z)) and (ex y (((not C(y, z)) and ex x ((not P(x))))) or ex x, y ((not R(x, y))))))"
+      assert_eq_str ~msg:"#2.5"
+        "ex z (not Q(z) and (ex y (not C(y, z) and ex x not P(x)) or ex x, y not R(x, y)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z not (Q(z) or (R(x,y) and (P(x) or C(y,z))))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#3"
-        "(ex x ((P(x) and ex y (R(x, y)))) or ex z ((Q(z) or ex y ((C(y, z) and ex x (R(x, y)))))))"
+      assert_eq_str ~msg:"#3"
+        "ex x (P(x) and ex y R(x, y)) or ex z (Q(z) or ex y (C(y, z) and ex x R(x, y)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#4"
-        "(ex z ((Q(z) and ex x (C(x, z)))) or ex x ((P(x) and ex y ((R(x, y) and ex z (C(x, z)))))) or ex y, z ((C(y, z) and ex x ((C(x, z) and R(x, y))))))"
+      assert_eq_str ~msg:"#4"
+        "ex z (Q(z) and ex x C(x, z)) or ex x (P(x) and ex y (R(x, y) and ex z C(x, z))) or ex y, z (C(y, z) and ex x (C(x, z) and R(x, y)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y, z (C(x, z) and ((R(x,y) and (P(x) or C(y,z))) or Q(z)))")));
@@ -236,30 +243,30 @@
   "ffsep: deep" >::
     (fun () ->
       (* only pulls out positive fluents *)
-      assert_equal ~printer:(fun x->x) ~msg:"#1"
-        "(ex y, z (((not R(x, y)) and (not Q(z)))) or ex x ((P(x) and ex y, z ((C(y, z) and (not Q(z)))))))"
+      assert_eq_str ~msg:"#1"
+        "ex y, z (not R(x, y) and not Q(z)) or ex x (P(x) and ex y, z (C(y, z) and not Q(z)))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
             (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#2"
-        "ex z ((Q(z) and ex x, y ((not (R(x, y) and (P(x) or C(y, z)))))))"
+      assert_eq_str ~msg:"#2"
+        "ex z (Q(z) and ex x, y not (R(x, y) and (P(x) or C(y, z))))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
             (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or not Q(z))")));
 
       (* TODO? simplify the result *)
-      assert_equal ~printer:(fun x->x) ~msg:"#3"
-        "(ex y ((C(y, z) and R(x, y))) or ex z ((Q(z) and ex y (true))) or ex x ((P(x) and ex y (R(x, y)))))"
+      assert_eq_str ~msg:"#3"
+        "ex y (C(y, z) and R(x, y)) or ex z (Q(z) and ex y true) or ex x (P(x) and ex y R(x, y))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
             (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#4"
-        "(ex y ((C(y, z) and R(x, y) and C(x, z))) or ex z ((Q(z) and ex y (C(x, z)))) or ex x ((P(x) and ex y ((R(x, y) and C(x, z))))))"
+      assert_eq_str ~msg:"#4"
+        "ex y (C(y, z) and R(x, y) and C(x, z)) or ex z (Q(z) and ex y C(x, z)) or ex x (P(x) and ex y (R(x, y) and C(x, z)))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"; "Q"])
             Aux.Strings.empty
@@ -267,30 +274,30 @@
 
       (* interpretation warning: in cases below, pulled-out "Q" in the
          result represents "not Q" actually (a negative literal) *)
-      assert_equal ~printer:(fun x->x) ~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)))))"
+      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))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"])
             (Aux.strings_of_list ["Q"])
             (formula_of_str "ex x, y, z ((not R(x,y) or (P(x) and C(y,z))) and not Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#6"
-        "ex x, y, z ((not ((R(x, y) and (P(x) or C(y, z))) or (not Q(z)))))"
+      assert_eq_str ~msg:"#6"
+        "ex x, y, z not ((R(x, y) and (P(x) or C(y, z))) or not Q(z))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"])
             (Aux.strings_of_list ["Q"])
             (formula_of_str "ex x, y, z not ((R(x,y) and (P(x) or C(y,z))) or not Q(z))")));
 
       (* distributes to extract P, not because of Q *)
-      assert_equal ~printer:(fun x->x) ~msg:"#7"
-        "(ex y, z ((Q(z) or (C(y, z) and R(x, y)))) or ex x ((P(x) and ex y, z (R(x, y)))))"
+      assert_eq_str ~msg:"#7"
+        "ex y, z (Q(z) or (C(y, z) and R(x, y))) or ex x (P(x) and ex y, z R(x, y))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"])
             (Aux.strings_of_list ["Q"])
             (formula_of_str "ex x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#8"
-        "(ex y ((C(y, z) and R(x, y) and C(x, z))) or ex z ((Q(z) and ex y (C(x, z)))) or ex x ((P(x) and ex y ((R(x, y) and C(x, z))))))"
+      assert_eq_str ~msg:"#8"
+        "ex y (C(y, z) and R(x, y) and C(x, z)) or ex z (Q(z) and ex y C(x, z)) or ex x (P(x) and ex y (R(x, y) and C(x, z)))"
         (Formula.str (
           formula_of_guards (Aux.strings_of_list ["P"])
             (Aux.strings_of_list ["Q"])
@@ -300,20 +307,20 @@
 
   "ff_tnf: simple subtasks" >::
     (fun () ->
-      assert_equal ~printer:(fun x->x) ~msg:"#1"
-        "(not (ex z (((not Q(z)) and ex x, y ((not R(x, y))))) or ex x (((not P(x)) and ex z (((not Q(z)) and ex y ((not C(y, z)))))))))"
+      assert_eq_str ~msg:"#1"
+        "not (ex z (not Q(z) and ex x, y not R(x, y)) or ex x (not P(x) and ex z (not Q(z) and ex y not C(y, z))))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "all x, y, z ((R(x,y) and (P(x) or C(y,z))) or Q(z))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#1.5"
-        "(not ex z (((not Q(z)) and (ex y (((not C(y, z)) and ex x ((not P(x))))) or ex x, y ((not R(x, y)))))))"
+      assert_eq_str ~msg:"#1.5"
+        "not ex z (not Q(z) and (ex y (not C(y, z) and ex x not P(x)) or ex x, y not R(x, y)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "all x, y, z (Q(z) or (R(x,y) and (P(x) or C(y,z))))")));
 
-      assert_equal ~printer:(fun x->x) ~msg:"#2"
-        "(((not ex z ((not Q(z)))) and ex y (P(y))) or ex x, y (C(x, y)))"
+      assert_eq_str ~msg:"#2"
+        "(not ex z not Q(z) and ex y P(y)) or ex x, y C(x, y)"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str "ex x, y (C(x, y) or (P(y) and all z Q(z)))")));
@@ -330,8 +337,8 @@
          ex t, u ((R(y, u) and R(x, t) and C(u, z)
          and C(t, y))) or ex t, u ((C(z, u) and
          R(y, u) and C(y, t) and R(x, t)))) and P(z) and P(y) and P(x)))))" in
-      assert_equal ~printer:(fun x->x)
-        "((not ex z ((P(z) and (ex y ((C(y, z) and P(y) and ex x ((C(x, y) and P(x))))) or ex y ((R(y, z) and P(y) and ex x ((R(x, y) and P(x))))) or ex u0 ((C(u0, z) and ex y ((R(y, u0) and P(y) and ex t0 ((C(t0, y) and ex x ((R(x, t0) and P(x))))))))) or ex u ((C(z, u) and ex y ((R(y, u) and P(y) and ex t ((C(y, t) and ex x ((R(x, t) and P(x))))))))))))) and (not P(x)) and (not P(y)) and (not P(z)) and ((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u0 ((C(z, u0) and R(y, u0) and ex t0 ((C(y, t0) and R(x, t0))))) or ex u ((R(y, u) and C(u, z) and ex t ((R(x, t) and C(t, y)))))) and (Q(z) or Q(y) or Q(x)))"
+      assert_eq_str
+        "(not ex z (P(z) and (ex y (C(y, z) and P(y) and ex x (C(x, y) and P(x))) or ex y (R(y, z) and P(y) and ex x (R(x, y) and P(x))) or ex u0 (C(u0, z) and ex y (R(y, u0) and P(y) and ex t0 (C(t0, y) and ex x (R(x, t0) and P(x))))) or ex u (C(z, u) and ex y (R(y, u) and P(y) and ex t (C(y, t) and ex x (R(x, t) and P(x))))))) and not P(x) and not P(y) and not P(z) and ((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u0 (C(z, u0) and R(y, u0) and ex t0 (C(y, t0) and R(x, t0))) or ex u (R(y, u) and C(u, z) and ex t (R(x, t) and C(t, y)))) and (Q(z) or Q(y) or Q(x)))"
         (Formula.str (FFTNF.ff_tnf
           (FFTNF.promote_rels (Aux.strings_of_list ["P"; "Q"]))
           (formula_of_str heur_phi)));

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/Formula.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -128,51 +128,28 @@
 
 (* ----------------------- PRINTING FUNCTIONS ------------------------------- *)
 
-(* Print a formula as a string. *)
-let rec str = function
-    Rel (s, vars) -> s ^ "(" ^ (var_tup_str vars) ^ ")"
-  | Eq (x, y) -> "(" ^ (var_str x) ^ " = " ^ (var_str y) ^ ")"
-  | In (x, y) -> "(" ^ (var_str x) ^ " in " ^ (var_str y) ^ ")"
-  | RealExpr (p, s) -> "(" ^ (real_str p) ^ (sign_op_str s) ^ ")"
-  | Not phi -> "(not " ^ (str phi) ^ ")"
-  | And [] -> "true"
-  | Or [] -> "false"
-  | And (flist) -> f_list_str " and " flist
-  | Or (flist) -> f_list_str " or " flist
-  | Ex (x, phi) -> "ex " ^ (var_list_str x) ^ " (" ^ (str phi) ^ ")"
-  | All (x, phi) -> "all " ^ (var_list_str x) ^ " ("^ (str phi) ^ ")"
-
-and f_list_str sep = function
-    [] -> "[]"
-  | [phi] -> str phi
-  | lst -> "(" ^ (String.concat sep (List.map str lst)) ^ ")"
-
-and real_str = function
-    RVar s -> s
-  | Const f -> string_of_float f
-  | Times (r1, r2) -> "(" ^ (real_str r1) ^ " * " ^ (real_str r2) ^ ")"
-  | Plus (r1, r2) -> "(" ^ (real_str r1) ^ " + " ^ (real_str r2) ^ ")"
-  | Fun (s, v) -> ":" ^ s ^ "(" ^ (var_str v) ^ ")"
-  | Char phi -> ":(" ^ (str phi) ^ ")"
-  | Sum (vl, f, r) -> 
-      "Sum (" ^ (var_list_str vl) ^ " | " ^ (str f) ^ " : " ^ (real_str r) ^ ")"
-
-
 let rec mona_str = function
-    Rel (s, vars) -> s ^ "(" ^ (var_tup_str vars) ^ ")"
+  | Rel (s, vars) -> s ^ "(" ^ (var_tup_str vars) ^ ")"
   | Eq (x, y) -> "(" ^ (var_str x) ^ " = " ^ (var_str y) ^ ")"
   | In (x, y) -> "(" ^ (var_str x) ^ " in " ^ (var_str y) ^ ")"
-  | RealExpr (p, s) -> "(" ^ (real_str p) ^ (sign_op_str s) ^ ")"
   | Not phi -> "(~ " ^ (mona_str phi) ^ ")"
   | And [] -> "true"
   | Or [] -> "false"
   | And (flist) -> f_list_str " & " flist
   | Or (flist) -> f_list_str " | " flist
-  | Ex (x, phi) -> (String.concat " " (List.map (fun x -> if (is_fo x) then "ex1 " ^ (var_str x) ^ ": " else "ex2 " ^ (var_str x) ^ ": ") x)) ^ (mona_str phi)
-  | All (x, phi) -> (String.concat " " (List.map (fun x -> if (is_fo x) then "all1 " ^ (var_str x) ^ ": " else "all2 " ^ (var_str x) ^ ": ") x)) ^ (mona_str phi)
+  | Ex (x, phi) ->
+    (String.concat " " (List.map (fun x -> 
+      if (is_fo x) then "ex1 " ^ (var_str x) ^ ": " else 
+	"ex2 " ^ (var_str x) ^ ": ") x)) ^ (mona_str phi)
+  | All (x, phi) -> 
+    (String.concat " " (List.map (fun x -> 
+      if (is_fo x) then "all1 " ^ (var_str x) ^ ": " else 
+	"all2 " ^ (var_str x) ^ ": ") x)) ^ (mona_str phi)
+  | _ ->
+    failwith "real-valued expressions and fixed-points not supported in MONA"
 
 and f_list_str sep = function
-    [] -> "[]"
+  | [] -> "[]"
   | [phi] -> mona_str phi
   | lst -> "(" ^ (String.concat sep (List.map mona_str lst)) ^ ")"
 
@@ -182,9 +159,9 @@
 
 (* Bracket-savvy encodings: 0 or, 1 and, 2 not ex all *)
 let rec fprint_prec prec f = function
-    Rel (s, vars) ->
-      Format.fprintf f "%s(%a)" s
-        (Aux.fprint_sep_list "," fprint_var) (Array.to_list vars)
+  | Rel (s, vars) ->
+    Format.fprintf f "%s(%a)" s
+      (Aux.fprint_sep_list "," fprint_var) (Array.to_list vars)
   | Eq (x, y) -> Format.fprintf f "%s = %s" (var_str x) (var_str y)
   | In (x, y) -> Format.fprintf f "%s in %s" (var_str x) (var_str y)
   | RealExpr (p, s) -> 
@@ -213,10 +190,18 @@
     let lb, rb = if prec > 2 then "(", ")" else "", "" in
     Format.fprintf f "@[<1>%sall@ %a@ %a%s@]" lb
       (Aux.fprint_sep_list "," fprint_var) x (fprint_prec 2) phi rb
+  | Lfp (r, vs, fpphi) ->
+    Format.fprintf f "@[<1>(lfp %a(%a) = %a)@]" fprint_var r
+      (Aux.fprint_sep_list "," fprint_var) (Array.to_list vs)
+      (fprint_prec prec) fpphi
+  | Gfp (r, vs, fpphi) ->
+    Format.fprintf f "@[<1>(gfp %a(%a) = %a)@]" fprint_var r
+      (Aux.fprint_sep_list "," fprint_var) (Array.to_list vs)
+      (fprint_prec prec) fpphi
 
 (* Bracket-savvy precedences: 0 +, 2 * *)
 and fprint_real_prec prec f = function
-    RVar s -> Format.fprintf f "%s" s
+  | RVar s -> Format.fprintf f "%s" s
   | Const fl -> Format.fprintf f "%F" fl
   | Times (r1, r2) -> 
     let lb, rb =
@@ -249,8 +234,9 @@
   Format.fprintf Format.str_formatter "@[%a@]" fprint_real r;
   Format.flush_str_formatter ()
 
+let str = sprint
+let real_str = sprint_real
 
-
 (* ------------------------ ORDER ON FORMULAS ------------------------------- *)
 
 (* Compare two variables. We assume that FO < MSO < SO < Real. *)
@@ -296,7 +282,8 @@
 
 let rec size ?(acc=0) = function
   | Rel _ | Eq _ | In _ | RealExpr _ -> acc + 1
-  | Not phi   | Ex (_, phi) | All (_, phi) -> size ~acc:(acc + 1) phi
+  | Not phi   | Ex (_, phi) | All (_, phi) | Lfp (_,_,phi) | Gfp (_,_,phi) -> 
+    size ~acc:(acc + 1) phi
   | And flist | Or flist -> 
     List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
 
@@ -336,6 +323,15 @@
       if c <> 0 then c else rec_compare psi1 psi2
     | (All _, _) -> -1
     | (_, All _) -> 1
+    | (Ex _, _) -> -1
+    | (_, Ex _) -> 1
+    | (Lfp (r1, vs1, psi1), Lfp (r2, vs2, psi2))
+    | (Gfp (r1, vs1, psi1), Gfp (r2, vs2, psi2)) ->
+      let c = compare_vars r1 r2 in if c <> 0 then c else
+	  let d = compare_var_tups vs1 vs2 in if d <> 0 then d else
+	      rec_compare psi1 psi2
+    | (Lfp _, _) -> -1
+    | (_, Lfp _) -> 1
 
 and rec_compare_re re1 re2 =
   match (re1, re2) with
@@ -351,59 +347,6 @@
 
 (* --------------- BASIC HELPER FUNCTIONS USED IN PARSER ------------------- *)
 
-(* Helper function: delete duplicates in ordered list. *)
-let rec del_dupl_ord acc = function
-    [] -> List.rev acc
-  | [x] -> List.rev (x :: acc)
-  | x :: y :: xs when x = y -> del_dupl_ord acc (y :: xs)
-  | x :: y :: xs -> del_dupl_ord (x :: acc) (y :: xs)
-
-let rec is_lit = function 
-    Rel _ | Eq _ | In _ -> true
-  | Not f -> is_lit f
-  | _ -> false
-
-let negl = function
-    Not f -> f
-  | f -> Not f
-
-let rec set_lit_in_f l nl = function
-    And flist ->
-      let sflist = List.map (set_lit_in_f l nl) flist in
-      if List.exists (fun f -> f = nl) sflist then Or[] else
-	let nflist = List.filter (fun f -> f <> l) sflist in
-	And (del_dupl_ord [] (List.sort compare nflist))
-  | Or flist -> 
-      let sflist = List.map (set_lit_in_f l nl) flist in
-      if List.exists (fun f -> f = l) sflist then And[] else
-	let nflist = List.filter (fun f -> f <> nl) sflist in
-	Or (del_dupl_ord [] (List.sort compare nflist))
-  | x -> x
-
-let rec set_lit_or l acc = function
-    [] -> (negl l) :: (List.rev acc)
-  | v :: vs ->
-      let set_v = set_lit_in_f l (negl l) v in
-      if set_v = Or[] then set_lit_or l acc vs else set_lit_or l (set_v :: acc) vs
-
-let set_first_lit_or = function
-    [] -> []
-  | v :: vs when is_lit v -> set_lit_or (negl v) [] vs
-  | x -> x
-
-
-let rec set_lit_and l acc = function
-    [] -> l :: (List.rev acc)
-  | v :: vs ->
-      let set_v = set_lit_in_f l (negl l) v in
-      if set_v = And[] then set_lit_and l acc vs else set_lit_and l (set_v :: acc) vs
-
-let set_first_lit_and = function
-    [] -> []
-  | v :: vs when is_lit v -> set_lit_and v [] vs
-  | x -> x
-
-
 (* Flatten conjunctions and disjunctions, apply f's to the respective lists. 
    This function also reduces false and true atoms and propagates them. *)
 let rec flatten_f f_or f_and phi =
@@ -426,18 +369,28 @@
     | Or [phi] -> flatten_f f_or f_and phi
     | Or fl when List.exists (fun x -> x = And []) fl -> And []
     | Or fl ->
-      Or (rev_collect_disj (List.rev_map (flatten_f f_or f_and) fl))
+      let r= f_or (rev_collect_disj (List.rev_map (flatten_f f_or f_and) fl)) in
+      if List.exists (fun x -> x = And []) r then And [] else Or r
     | And [phi] -> flatten_f f_or f_and phi
     | And fl when List.exists (fun x -> x = Or []) fl -> Or []
     | And fl ->
-      And (rev_collect_conj (List.rev_map (flatten_f f_or f_and) fl))
-    | Ex (_, Or []) | All (_, Or []) -> Or []
-    | Ex (_, And []) | All (_, And []) -> And []
+      let r=f_and (rev_collect_conj (List.rev_map (flatten_f f_or f_and) fl)) in
+      if List.exists (fun x -> x = Or []) r then Or [] else And r
     | Ex ([], phi) | All ([], phi) -> flatten_f f_or f_and phi
     | Ex (xs, Ex (ys, phi)) -> flatten_f f_or f_and (Ex (xs @ ys, phi))
-    | Ex (xs, phi) -> Ex (xs, flatten_f f_or f_and phi)
+    | Ex (xs, phi) ->
+      (match flatten_f f_or f_and phi with 
+	| Or [] -> Or [] | And [] -> And [] | f -> Ex (xs, f))
     | All (xs, All (ys, phi)) -> flatten_f f_or f_and (All (xs @ ys, phi))
-    | All (xs, phi) -> All (xs, flatten_f f_or f_and phi)
+    | All (xs, phi) -> 
+      (match flatten_f f_or f_and phi with
+	| Or [] -> Or [] | And [] -> And [] | f -> All (xs, f))
+    | Lfp (r, vs, phi) -> 
+      (match flatten_f f_or f_and phi with
+	| Or [] -> Or [] | And [] -> And [] | f -> Lfp (r, vs, f))
+    | Gfp (r, vs, phi) -> 
+      (match flatten_f f_or f_and phi with
+	| Or [] -> Or [] | And [] -> And [] | f -> Gfp (r, vs, f))
 
 and flatten_re_f f_or f_and = function
   | RVar _ | Const _ | Fun _ as re -> re
@@ -454,6 +407,71 @@
 let flatten psi = flatten_f (fun x -> x) (fun x -> x) psi
 let flatten_re psi = flatten_re_f (fun x -> x) (fun x -> x) psi
 
+
+
+(* ----- Flattening with very basic simplification and sorting. ----- *)
+
+(* Helper function: delete duplicates in ordered list. *)
+let rec del_dupl_ord acc = function
+    [] -> List.rev acc
+  | [x] -> List.rev (x :: acc)
+  | x :: y :: xs when x = y -> del_dupl_ord acc (y :: xs)
+  | x :: y :: xs -> del_dupl_ord (x :: acc) (y :: xs)
+
+let rec is_lit = function 
+  | Rel _ | Eq _ | In _ -> true
+  | Not f -> is_lit f
+  | _ -> false
+
+let negl = function
+  | Not f -> f
+  | f -> Not f
+
+let rec set_lits_in_f lits nlits = function
+  | And flist ->
+    let sflist = List.rev_map (set_lits_in_f lits nlits) flist in
+    if List.exists (fun f -> List.mem f nlits) sflist then Or [] else
+      let nflist = List.filter (fun f -> not (List.mem f lits)) sflist in
+      (match del_dupl_ord [] (List.sort compare nflist) with
+	| [x] -> x
+	| l -> And l)
+  | Or flist -> 
+    let sflist = List.rev_map (set_lits_in_f lits nlits) flist in
+    if List.exists (fun f -> List.mem f lits) sflist then And [] else
+      let nflist = List.filter (fun f -> not (List.mem f nlits)) sflist in
+      (match del_dupl_ord [] (List.sort compare nflist) with
+	| [x] -> x
+	| l -> Or l)
+  | x -> x
+
+let set_first_lit_or fl = 
+  let rec set_lits_or lits nlits acc = function
+    | [] -> List.sort compare (nlits @ acc)
+    | v :: vs ->
+      let set_v = set_lits_in_f lits nlits v in
+      if set_v = And [] then [And []] else if set_v = Or [] then
+	  set_lits_or lits nlits acc vs
+	else set_lits_or lits nlits (set_v :: acc) vs in
+  let (lits, rest) = List.partition is_lit fl in
+  if lits = [] then fl else
+    let nlits = List.rev_map negl lits in
+    if List.exists (fun l -> List.mem l nlits) lits then [And []] else
+      set_lits_or nlits lits [] rest
+
+let set_first_lit_and fl = 
+  let rec set_lits_and lits nlits acc = function
+    | [] -> List.sort compare (lits @ acc)
+    | v :: vs ->
+      let set_v = set_lits_in_f lits nlits v in
+      if set_v = Or [] then [Or []] else if set_v = And [] then
+	  set_lits_and lits nlits acc vs
+	else set_lits_and lits nlits (set_v :: acc) vs in
+  let (lits, rest) = List.partition is_lit fl in
+  if lits = [] then fl else
+    let nlits = List.rev_map negl lits in
+    if List.exists (fun l -> List.mem l nlits) lits then [Or []] else
+      set_lits_and lits nlits [] rest
+
 let flatten_sort = 
   let clean fl = del_dupl_ord [] (List.sort compare fl) in
   flatten_f (fun fl -> set_first_lit_or (clean fl))
@@ -463,72 +481,3 @@
   let clean fl = del_dupl_ord [] (List.sort compare fl) in
   flatten_re_f (fun fl -> set_first_lit_or (clean fl))
     (fun fl -> set_first_lit_and (clean fl))
-
-
-(* Helper function to flatten multiple or's and and's and sort by compare. *)
-let rec flatten_sort = function
-    Rel _ | Eq _ | In _ as phi -> phi
-  | RealExpr (re, s) -> RealExpr (flatten_sort_re re, s)
-  | Not (And []) -> Or[]
-  | Not (Or []) -> And[]
-  | Not phi -> let f = flatten_sort phi in if f = Or [] then And[] else if f = And[] then Or[] else Not f
-  | Or flist_orig ->
-      let flist = List.map flatten_sort flist_orig in
-      let is_or = function Or _ -> true | _ -> false in
-      let (ors_all, non_ors) = List.partition is_or flist in
-      let ors = List.filter (fun v -> v <> Or []) ors_all in
-      let flat_non_ors = List.rev_map flatten_sort non_ors in
-        if List.exists (fun v -> v = And []) flat_non_ors then And [] else
-          if ors = [] then 
-	    Or (set_first_lit_or (del_dupl_ord [] (List.sort compare flat_non_ors)))
-	  else
-            let fl = flatten_sort_ors [] ors in
-            Or (set_first_lit_or (del_dupl_ord [] (List.sort compare (List.rev_append fl flat_non_ors))))
-  | And flist_orig ->
-      let flist = List.map flatten_sort flist_orig in
-      let is_and = function And _ -> true | _ -> false in
-      let (ands_all, non_ands) = List.partition is_and flist in
-      let ands = List.filter (fun v -> v <> And []) ands_all in
-      let flat_non_ands = List.rev_map flatten_sort non_ands in
-        if List.exists (fun v -> v = Or []) flat_non_ands then Or [] else
-          if ands = [] then 
-	    And (set_first_lit_and (del_dupl_ord [] (List.sort compare flat_non_ands))) 
-	  else
-            let fl = flatten_sort_ands [] ands in
-            And (set_first_lit_and (del_dupl_ord [] (List.sort compare (List.rev_append fl flat_non_ands))))
-  | Ex (_, And[]) | All(_, And[]) -> And[]
-  | Ex (_, Or[]) | All(_, Or[]) -> Or[]
-  | Ex ([], phi) | All ([], phi) -> flatten_sort phi
-  | Ex (xs, Ex (ys, phi)) -> flatten_sort (Ex (xs @ ys, phi))
-  | Ex (xs, phi) -> Ex (xs, flatten_sort phi)
-  | All (xs, All (ys, phi)) -> flatten_sort (All (xs @ ys, phi))
-  | All (xs, phi) -> All (xs, flatten_sort phi)
-
-and flatten_sort_ors acc = function
-    [] -> acc
-  | (Or fl) :: ls -> 
-      let handle accu phi =
-        match flatten_sort phi with
-            Or fl -> List.rev_append fl accu
-          | _ -> phi::accu in
-      let new_acc = List.fold_left handle acc fl in
-        flatten_sort_ors new_acc ls
-  | _ -> failwith "flatten_sort_ors on a non-or"
-
-and flatten_sort_ands acc = function
-    [] -> acc
-  | (And fl) :: ls -> 
-      let handle accu phi =
-        match flatten_sort phi with
-            And fl -> List.rev_append fl accu
-          | _ -> phi::accu in
-      let new_acc = List.fold_left handle acc fl in
-        flatten_sort_ands new_acc ls
-  | _ -> failwith "flatten_sort_ands on a non-and"
-
-and flatten_sort_re = function
-    RVar _ | Const _ | Fun _ as re -> re
-  | Times (re1, re2) -> Times (flatten_sort_re re1, flatten_sort_re re2)
-  | Plus (re1, re2) -> Plus (flatten_sort_re re1, flatten_sort_re re2)
-  | Char (phi) -> Char (flatten_sort phi)
-  | Sum (vl, f, r) -> Sum (vl, flatten_sort f, flatten_sort_re r)

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -27,17 +27,17 @@
 (* Convert formula to NNF and additionally negate if [neg] is set. *)
 let rec nnf ?(neg=false) psi = 
   match psi with
-    Rel _ | Eq _ | In _ | RealExpr _ as atom -> if neg then Not atom else atom
-  | Not phi -> if neg then nnf ~neg:false phi else nnf ~neg:true phi
-  | And [f] | Or [f] -> nnf ~neg f
-  | And (flist) when neg -> Or (List.map (nnf ~neg:true) flist)
-  | And (flist) -> And (List.map (nnf ~neg:false) flist)
-  | Or (flist) when neg -> And (List.map (nnf ~neg:true) flist)
-  | Or (flist) -> Or (List.map (nnf ~neg:false) flist)
-  | Ex (x, phi) when neg -> All (x, nnf ~neg:true phi)
-  | Ex (x, phi) -> Ex (x, nnf ~neg:false phi)
-  | All (x, phi) when neg -> Ex (x, nnf ~neg:true phi)
-  | All (x, phi) -> All (x, nnf ~neg:false phi)
+    | Rel _ | Eq _ | In _ | RealExpr _ as atom -> if neg then Not atom else atom
+    | Not phi -> if neg then nnf ~neg:false phi else nnf ~neg:true phi
+    | And [f] | Or [f] -> nnf ~neg f
+    | And (flist) when neg -> Or (List.map (nnf ~neg:true) flist)
+    | And (flist) -> And (List.map (nnf ~neg:false) flist)
+    | Or (flist) when neg -> And (List.map (nnf ~neg:true) flist)
+    | Or (flist) -> Or (List.map (nnf ~neg:false) flist)
+    | Ex (x, phi) when neg -> All (x, nnf ~neg:true phi)
+    | Ex (x, phi) -> Ex (x, nnf ~neg:false phi)
+    | All (x, phi) when neg -> Ex (x, nnf ~neg:true phi)
+    | All (x, phi) -> All (x, nnf ~neg:false phi)
 
 
 (* -------------------------- FREE VARIABLES -------------------------------- *)
@@ -52,45 +52,52 @@
         | _ -> remove_dup_vars (v1::acc) (v2::vs)
 
 let rec all_vars_acc acc = function
-    Eq (x, y) -> (x :> var) :: (y :> var) :: acc
+  | Eq (x, y) -> (x :> var) :: (y :> var) :: acc
   | Rel (r, vs) -> List.rev_append ((Array.to_list vs) :> var list) acc
   | In (x, y) -> (x :> var) :: (y :> var) :: acc
   | RealExpr (p, _) -> 
       List.rev_append (List.map(fun v -> var_of_string v) (all_vars_real p)) acc
   | Not phi -> all_vars_acc acc phi
   | And (flist) | Or (flist) ->
-      List.fold_left (fun vs phi -> all_vars_acc vs phi) acc flist
+    List.fold_left (fun vs phi -> all_vars_acc vs phi) acc flist
   | Ex (vs, phi) | All (vs, phi) -> 
-      all_vars_acc (List.rev_append (vs :> var list) acc) phi
+    all_vars_acc (List.rev_append (vs :> var list) acc) phi
+  | Lfp (r, vs, phi) | Gfp (r, vs, phi) -> 
+    all_vars_acc 
+      ((r :> var):: (List.rev_append ((Array.to_list vs) :> var list) acc)) phi
 
 and all_vars_real = function
-    RVar s -> [s]
+  | RVar s -> [s]
   | Const _ -> []
   | Times (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
   | Plus (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
   | Fun (s, v) -> [var_str v]
   | Char phi -> List.rev_map var_str (all_vars_acc [] phi)
   | Sum (_, f, r) -> 
-      List.rev_append (List.rev_map var_str (all_vars_acc [] f)) (all_vars_real r)
+    List.rev_append (List.rev_map var_str (all_vars_acc [] f)) (all_vars_real r)
 
 let all_vars phi =
   remove_dup_vars [] (List.sort compare_vars (all_vars_acc [] phi))
 
 let rec free_vars_acc acc = function
-    Eq (x, y) -> (x :> var) :: (y :> var) :: acc
+  | Eq (x, y) -> (x :> var) :: (y :> var) :: acc
   | Rel (r, vs) -> List.rev_append (Array.to_list vs :> var list) acc
   | In (x, y) -> (x :> var) :: (y :> var) :: acc
   | RealExpr (p, _) -> 
-      List.rev_append (List.map (fun v->var_of_string v) (free_vars_real p)) acc
+    List.rev_append (List.map (fun v->var_of_string v) (free_vars_real p)) acc
   | Not phi -> free_vars_acc acc phi
   | And (flist) | Or (flist) ->
-      List.fold_left (fun vs phi -> free_vars_acc vs phi) acc flist
+    List.fold_left (fun vs phi -> free_vars_acc vs phi) acc flist
   | Ex (vs, phi) | All (vs, phi) -> 
-      let fv_phi = free_vars_acc [] phi in
-        List.rev_append (List.filter (fun v -> not (List.mem v vs)) fv_phi) acc
+    let fv_phi = free_vars_acc [] phi in
+    List.rev_append (List.filter (fun v -> not (List.mem v vs)) fv_phi) acc
+  | Lfp (r, xs, phi) | Gfp (r, xs, phi) ->
+    let vs = (r :> var) :: ((Array.to_list xs) :> var list) in
+    let fv_phi = free_vars_acc [] phi in
+    List.rev_append (List.filter (fun v -> not (List.mem v vs)) fv_phi) acc
 
 and free_vars_real = function
-    RVar s -> [s]
+  | RVar s -> [s]
   | Const _ -> []
   | Times (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
   | Plus (r1, r2) -> List.rev_append (all_vars_real r1) (all_vars_real r2)
@@ -103,19 +110,21 @@
 let free_vars phi =
   remove_dup_vars [] (List.sort compare_vars (free_vars_acc [] phi))
 
-(* Delete top-most quantification of [vs] in the formula. *)
+(* Delete top-most ex/all quantification of [vs] in the formula. *)
 let rec del_vars_quant vs = function
-    Eq _ | Rel _ | In _ | RealExpr _ as f -> f
+  | Eq _ | Rel _ | In _ | RealExpr _ as f -> f
   | Not phi -> Not (del_vars_quant vs phi)
   | And (flist) -> And (List.map (del_vars_quant vs) flist)
   | Or (flist) -> Or (List.map (del_vars_quant vs) flist)
   | Ex ([], phi) | All ([], phi) -> del_vars_quant vs phi
   | Ex (v :: vr, phi) when List.mem v vs ->
-      del_vars_quant (Aux.list_remove v vs) (Ex (vr, phi))
+    del_vars_quant (Aux.list_remove v vs) (Ex (vr, phi))
   | Ex (v :: vr, phi) -> Ex ([v], del_vars_quant vs (Ex (vr, phi)))
   | All (v :: vr, phi) when List.mem v vs ->
-      del_vars_quant (Aux.list_remove v vs) (All (vr, phi))
-  | All (v :: vr, phi) -> All ([v], del_vars_quant vs (Ex (vr, phi)))
+    del_vars_quant (Aux.list_remove v vs) (All (vr, phi))
+  | All (v :: vr, phi) -> All ([v], del_vars_quant vs (All (vr, phi)))
+  | Lfp (r, xs, phi) -> Lfp (r, xs, del_vars_quant vs phi)
+  | Gfp (r, xs, phi) -> Gfp (r, xs, del_vars_quant vs phi)
 
 
 (* ----------------- MAPPING TO ATOMS AND VAR SUBSTITUTION ------------------ *)

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -11,10 +11,14 @@
   FormulaParser.parse_real_expr Lexer.lex (Lexing.from_string s)
 ;;
 
-let formula_eq f1 phi1 f2 phi2 =
-  assert_equal ~printer:(fun x -> Formula.str x)
-    (Formula.flatten (f1 (formula_of_string phi1)))
-    (Formula.flatten (f2 (formula_of_string phi2)))
+let formula_eq ?(flatten=true) f1 phi1 f2 phi2 =
+  if flatten then 
+    assert_equal ~printer:(fun x -> Formula.sprint x)
+      (Formula.flatten (f1 (formula_of_string phi1)))
+      (Formula.flatten (f2 (formula_of_string phi2)))
+  else
+    assert_equal ~printer:(fun x -> Formula.sprint x)
+      (f1 (formula_of_string phi1)) (f2 (formula_of_string phi2))
 ;;
 
 let real_expr_eq f1 re1 f2 re2 =
@@ -167,13 +171,18 @@
        fts_eq "all t ((t in X) or (not Succ(t, s)) or ((t in C) and (t in X)))"
 	 "all t ((t in X)  or  (not Succ(t, s)))";
        fts_eq "(not (t in X))  and  ((t in X)  or  (not (t in C)))"
-	 "((not (t in X))  and  (not (t in C)))";
+	 "((not (t in C))  and  (not (t in X)))";
        fts_eq "all s ((((not (s in S))  and  (not (s in X2)))  or
         ((s in S)  and  (s in X2))))" "all s ((((s in S)  and  (s in X2))
         or  ((not (s in S))  and  (not (s in X2)))))";
+       fts_eq "P(x) and Q(x) and (P(x)|R(x)) and (Q(x)|R(x))" "P(x) and Q(x)";
+       fts_eq "P(x) or Q(x) or (P(x)&R(x)) or (Q(x)&R(x))" "P(x) or Q(x)";
+       fts_eq "P(x) and not P(x)" "false";
+       fts_eq "P(x) or not P(x)" "true";
+
        let double_fts_eq phi = 
-	 let fts2 phi = Formula.flatten_sort (Formula.flatten_sort phi) in
-	 formula_eq Formula.flatten_sort phi fts2 phi in
+	 let psi = Formula.str (Formula.flatten_sort (formula_of_string phi)) in
+         formula_eq id psi Formula.flatten_sort psi in
        double_fts_eq "ex X2 ((all s ((not (s in X2))) and ex zero
         ((all n (LessEq(zero, n)) and all s (((not (s = zero)) and
         (not ex x1 ((Succ(x1, s) and Succ(zero, x1)))))) and ex C
@@ -389,7 +398,7 @@
 (* ------------------------------ SL 6 formula  test ------------------------ *)
 
 (*
-let f v1 v2 = "(E (" ^ v1 ^ ", " ^ v2 ^ ") and "^ v2 ^ " in F_f) or (E(" ^
+let f v1 v2 = "(Succ (" ^ v1 ^ ", " ^ v2 ^ ") and "^ v2 ^ " in F_f) or (Succ(" ^
   v2 ^ ", " ^ v1 ^ ") and " ^ v2 ^ " in B_f) or (" ^ v1 ^ " = " ^ v2 ^ " and " ^
   v1 ^ " in L_f) or (" ^ 
   v2 ^ " = y and " ^ v1 ^ " in F_fy ) or (" ^
@@ -399,18 +408,34 @@
   v2 ^ " = x and " ^ v1 ^ " in F_fx) or (" ^
   v1 ^ " = x and " ^ v2 ^ " in B_fx)" ;;
 
-(* let closed_f h = "all v ( v in " ^ h ^ " and v != y ) -> (all u (" ^
-  (f "v" "u") ^ " -> (u in " ^ h ^ ")) and x in " ^ h ^ ")";; *)
+let partial_f = "all a,b,c (" ^ (f "a" "b") ^ " and " ^ (f "a" "c") ^ " -> b=c)"
 
-let closed_f h = "all v ( v in " ^ h ^ " ) -> (all u (" ^
+let closed_f h = "all v ( v in " ^ h ^ " and v != y ) -> (all u (" ^
   (f "v" "u") ^ " -> (u in " ^ h ^ ")) and x in " ^ h ^ ")";;
 
-let sl6_f = "all x (Z(x) -> (not x in F_f and not x in B_f)) and
+(* let closed_f h = "all v ( v in " ^ h ^ " ) -> (all u (" ^
+  (f "v" "u") ^ " -> (u in " ^ h ^ ")) and x in " ^ h ^ ")";; *)
+
+(*let sl6_f = "all x (Z(x) -> (not x in F_f and not x in B_f)) and " ^
+  partial_f ^ " and 
   (ex  H_path ((" ^ (closed_f "H_path") ^ ") and (all H_other ((" ^ 
   (closed_f "H_other") ^ ") -> all a (a in H_path -> a in H_other)))
-  and y in H_path))";;
+  and y in H_path))";; *)
 
-"TNF size" FormulaOps.tnf (fun f -> print_endline (string_of_int (Formula.size f))) sl6_f ;;
+let sl6_f = "ex x,y,z,F_f,B_f,L_f,F_fx,B_fx,F_fy,B_fy,F_fz,B_fz
+  (all u (Z(u) -> (not u in F_f and not u in B_f)) and " ^
+  partial_f ^ " and 
+  (ex  H_path ((" ^ (closed_f "H_path") ^ ") and (all H_other ((" ^ 
+  (closed_f "H_other") ^ ") -> all a (a in H_path -> a in H_other)))
+  and y in H_path)))";;
+
+let sl6_phi = Formula.flatten_sort (FormulaOps.nnf (formula_of_string sl6_f));;
+
+print_endline "SL6 = " ;;
+print_endline (Formula.str sl6_phi) ;;
+
+"TNF size" FormulaOps.tnf 
+  (fun f -> print_endline (string_of_int (Formula.size f))) sl6_f ;;
 *)
 
 (* ------- Other longer formulas -------- *)

Modified: trunk/Toss/Formula/FormulaTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Formula/FormulaTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -1,8 +1,5 @@
 open OUnit
 
-FormulaOps.set_debug_level 0;
-BoolFormula.set_debug_level 0
-
 let tests = "Formula" >::: [
   "basic flatten" >::
     (fun () ->

Modified: trunk/Toss/Play/HeuristicTest.ml
===================================================================
--- trunk/Toss/Play/HeuristicTest.ml	2011-04-29 11:37:27 UTC (rev 1426)
+++ trunk/Toss/Play/HeuristicTest.ml	2011-05-01 00:33:55 UTC (rev 1427)
@@ -25,6 +25,12 @@
       (Lexing.from_channel f) in
   res
 
+let assert_eq_str ?(msg="") x_in y_in = 
+  let ws = Str.regexp "[ \n\t]+" in
+  let x = Str.global_replace ws " " (" " ^ x_in ^ " ") in
+  let y = Str.global_replace ws " " (" " ^ y_in ^ " ") in
+  assert_equal ~printer:(fun x -> x) ~msg ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
+    
 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))))))"
 
@@ -108,8 +114,8 @@
 	W..W  W..W  W..W  W..W  
 \"" in
       (* Heuristic.debug_level := 7; *)
-      assert_equal ~printer:(fun x->x)
-        "ex y5, y4, y3, y2, y1, y0, y ((C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, y) and C(y, x)))"
+      assert_eq_str
+        "ex y5, y4, y3, y2, y1, y0, y (C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, y) and C(y, x))"
         (Formula.str (Heuristic.expanded_description 5
           (Aux.strings_of_list ["B"; "W"])
           state (formula_of_str "not ex y C(x, y)")));
@@ -141,8 +147,8 @@
 	                        
 	F  F  F  F  F  F  F  F  
 \"" in
-      assert_equal ~printer:(fun x->x)
-        "ex y7, y6, y5, y4, y3, y2, y1, y0, y ((C(y7, y6) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, x) and C(x, y)))"
+      assert_eq_str
+        "ex y7, y6, y5, y4, y3, y2, y1, y0, y (C(y7, y6) and C(y6, y5) and C(y5, y4) and C(y4, y3) and C(y3, y2) and C(y2, y1) and C(y1, y0) and C(y0, x) and C(x, y))"
         (Formula.str (Heuristic.expanded_description 5
           (Aux.strings_of_list ["B"; "W"])
           state (formula_of_str "ex y (C(x, y) and F(y))")));
@@ -174,8 +180,8 @@
 	                        
 	F  F  F  F  F  F  F  F  
 \"" in
-      assert_equ...
 
[truncated message content]