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

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

Revision: 1748
          http://toss.svn.sourceforge.net/toss/?rev=1748&view=rev
Author:   lukaszkaiser
Date:     2012-07-18 15:33:21 +0000 (Wed, 18 Jul 2012)
Log Message:
-----------
Testing TC - bug found and removed.

Modified Paths:
--------------
    trunk/Toss/Formula/BoolFormula.ml
    trunk/Toss/Formula/BoolFormula.mli
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/SolverTest.ml

Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml	2012-07-18 13:38:17 UTC (rev 1747)
+++ trunk/Toss/Formula/BoolFormula.ml	2012-07-18 15:33:21 UTC (rev 1748)
@@ -40,20 +40,23 @@
 let var_str = string_of_int
 
 (** Print a Boolean formula as a string. *)
-let rec str = function
-  | BVar v -> var_str v
-  | BNot phi -> "(not " ^ (str phi) ^ ")"
-  | BAnd [] -> "true"
-  | BOr [] -> "false"
-  | BAnd (bflist) -> bf_list_str " and " bflist
-  | BOr (bflist) -> bf_list_str " or " bflist
+let rec str ?names bf = 
+  let name s = match names with None -> var_str s | Some tbl ->
+    try Hashtbl.find tbl s with Not_found -> var_str s in
+  let rec str_rec = function
+    | BVar v -> if v < 0 then "-" ^ (name (-v)) else name v
+    | BNot phi -> "(not " ^ (str_rec phi) ^ ")"
+    | BAnd [] -> "true"
+    | BOr [] -> "false"
+    | BAnd (bflist) -> bf_list_str " and " bflist
+    | BOr (bflist) -> bf_list_str " or " bflist
+  and bf_list_str sep = function
+    | [] -> "[]"
+    | [phi] -> str_rec phi
+    | lst -> "(" ^ (String.concat sep (List.map str_rec lst)) ^ ")" in
+  str_rec bf
 
-and bf_list_str sep = function
-  | [] -> "[]"
-  | [phi] -> str phi
-  | lst -> "(" ^ (String.concat sep (List.map str lst)) ^ ")"
 
-
 (* ------------------------ ORDER ON FORMULAS ------------------------------- *)
 
 (** Compare two variables. We assume that FO < MSO < Real. *)
@@ -961,7 +964,7 @@
   let name s = match names with None -> var_str s | Some tbl ->
     try Hashtbl.find tbl s with Not_found -> var_str s in
   let rec qbf_str_rec = function
-    | QVar v -> name v
+    | QVar v -> if v < 0 then "-" ^ (name (-v)) else name v
     | QNot phi -> "(not " ^ (qbf_str_rec phi) ^ ")"
     | QAnd [] -> "true"
     | QOr [] -> "false"

Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli	2012-07-18 13:38:17 UTC (rev 1747)
+++ trunk/Toss/Formula/BoolFormula.mli	2012-07-18 15:33:21 UTC (rev 1748)
@@ -17,7 +17,7 @@
 val var_str : int -> string
 
 (** Print a formula as a string. *)
-val str : bool_formula -> string
+val str : ?names: (int, string) Hashtbl.t -> bool_formula -> string
 
 (** Helper function to flatten multiple or's and and's. *)
 val flatten_sort : bool_formula -> bool_formula

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-07-18 13:38:17 UTC (rev 1747)
+++ trunk/Toss/Solver/Solver.ml	2012-07-18 15:33:21 UTC (rev 1748)
@@ -554,7 +554,7 @@
     let qbf, rev_ids = so_to_qbf struc psi in
     (match logtime with None -> () | Some t ->
       LOG 0 "%sQBF constructed at %.3fs" logprefix (AuxIO.gettimeofday ()-.t));
-    let bf = BoolFormula.sat_of_qbf (*elim_quant*) qbf in
+    let bf = BoolFormula.elim_quant qbf in
     (match logtime with None -> () | Some t ->
       LOG 0 "%sBF constructed at %.3fs" logprefix (AuxIO.gettimeofday () -. t));
     match BoolFormula.find_model ?logtime ~logprefix bf with

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2012-07-18 13:38:17 UTC (rev 1747)
+++ trunk/Toss/Solver/SolverTest.ml	2012-07-18 15:33:21 UTC (rev 1748)
@@ -198,8 +198,11 @@
           (String.concat "." (Array.to_list (Array.map string_of_int arr))) in
         let names_tbl = Hashtbl.create (Hashtbl.length rev_ids) in
         Hashtbl.iter (fun k v -> Hashtbl.add names_tbl k (name v)) rev_ids;
-        assert_equal ~printer:(fun x -> x) qbf_s 
-          (BoolFormula.qbf_str ~names:names_tbl qbf_res) in
+        let qbf_res_s = BoolFormula.qbf_str ~names:names_tbl qbf_res in
+        LOG 1 "QBF %s BF %s" qbf_res_s (
+          let bf = BoolFormula.simplify (BoolFormula.sat_of_qbf qbf_res) in
+          (BoolFormula.str ~names:names_tbl bf) );
+        assert_equal ~printer:(fun x -> x) qbf_s qbf_res_s in
 
       qbf_str_eq "[ a, b | T { a } | ]" "ex |R all x, y (T(x) or |R (x, y))"
 	"(ex R.2.2, R.2.1, R.1.2, R.1.1 (R.2.1 and R.2.2))";            
@@ -229,8 +232,8 @@
                      "(|A(x) | (|A(y) & E(x,y))) & (|B(x) | (|B(u)&E(x,u))) &" ^
                      " (|C(x)|(|C(v) & E(x,v))))") in
       let yd = "(&x2=&x1+1 | &x2=&x1+2 | &x1=&x2+1 | &x1=&x2+2)" in ();
-(*      find_so_test dnp3 ("[ 0 - 4 | | - ] with E(x1, x2) = " ^ yd) 
-        "|C {e1; e3}; |B {e0; e4}; |A (e2)"; *)
+      find_so_test dnp3 ("[ 0 - 4 | | - ] with E(x1, x2) = " ^ yd) 
+        "|C {e1; e3}; |B {e0; e4}; |A (e2)";
 
       let nd = yd ^ "& ((~(&x1=1) & ~(&x2=1)) | (&x1=1 & &x2=3))" in
       find_so_test dnp3 ("[ 0 - 4 | | - ] with E(x1, x2) = " ^ nd) "UNSAT";
@@ -246,8 +249,10 @@
           "( (|Tc(x, y) ∧ |Tc(y, z)) -> |Tc(x, z) ) ) ) ∧ " ^
           "( ∀ |T ( (∀ x,y,z ( ( E(x, y) → |T(x, y) ) ∧ " ^
           "( (|T(x, y) ∧ |T(y, z)) -> |T(x, z) ) ) ) → " ^
-          "(∀ x, y (|T(x, y) → |Tc(x, y) )) ))" in
-      find_so_test tc2phi "[ c | E { (a, b) } | ]" "|Tc?";
+          "(∀ x, y (|Tc(x, y) → |T(x, y) )) ))" in
+      find_so_test tc2phi "[ | E { (a, b); (c, d) } | ]" "|Tc {(a, b); (c, d)}";
+      find_so_test tc2phi "[ | E { (a, b); (b, c) } | ]" 
+        "|Tc {(a, b); (a, c); (b, c)}";
     );
 
   "eval: second-order" >::

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