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

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

Revision: 1206
          http://toss.svn.sourceforge.net/toss/?rev=1206&view=rev
Author:   lukaszkaiser
Date:     2010-11-28 17:05:43 +0000 (Sun, 28 Nov 2010)

Log Message:
-----------
Corrections to mso solving and variable ordering.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Solver/Assignments.ml
    trunk/Toss/Solver/SolverTest.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2010-11-28 16:10:41 UTC (rev 1205)
+++ trunk/Toss/Formula/FormulaOps.ml	2010-11-28 17:05:43 UTC (rev 1206)
@@ -840,40 +840,46 @@
     let (somefo, nofo) = List.partition has_fo msos in
     Or (fos @ somefo @ nofo)
 
+let free_vars_fo f =
+  let is_fo = function `FO _ -> true | _ -> false in
+  List.filter is_fo (free_vars f)
+
+let rec order_by_fv acc_fv = function
+  | [] -> [] 
+  | [f] -> [order_by_fv_phi acc_fv f]
+  | l ->
+    let cross x = List.exists (fun v -> List.mem v acc_fv) (free_vars x) in
+    let (cf, o) = List.partition cross l in
+    if cf = [] then 
+      let new_fv = free_vars (List.hd l) in
+      order_by_fv new_fv l
+    else
+      let new_fv = acc_fv @ (free_vars_fo (And cf)) in
+      (List.map (order_by_fv_phi acc_fv) cf) @ (order_by_fv new_fv o)
+
+and order_by_fv_phi acc_fv = function
+  | And fl ->
+    let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
+    let (p, np) = List.partition is_pred fl in 
+    let res = And (order_by_fv acc_fv (p @ np)) in
+    if !debug_level > 0 then print_endline ("fvordered and: " ^ (str res));
+    res
+  | Or fl ->
+    let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
+    let (p, np) = List.partition is_pred fl in 
+    let res = Or (order_by_fv acc_fv (p @ np)) in
+    if !debug_level > 0 then print_endline ("fvordered or: " ^ (str res));
+    res
+  | Ex (vs, phi) -> Ex (vs, order_by_fv_phi acc_fv phi)
+  | All (vs, phi) -> All (vs, order_by_fv_phi acc_fv phi)
+  | f -> f
+    
 let tnf_fv phi =
   let fv = free_vars phi in
   let psi = rename_quant_avoiding [] (Ex (fv, phi)) in
-  let rec order_by_fv acc_fv = function
-    | [] -> []    
-    | [f] -> [f]
-    | l ->
-      let cross x = List.exists (fun v -> List.mem v acc_fv) (free_vars x) in
-      let (cf, o) = List.partition cross l in
-      if cf = [] then 
-	let new_fv = free_vars (List.hd l) in
-	order_by_fv new_fv (List.map (order_by_fv_phi new_fv) l)
-      else
-	let new_fv = acc_fv @ (free_vars (And cf)) in
-	cf @ (order_by_fv new_fv (List.map (order_by_fv_phi new_fv) o)) 
-  and order_by_fv_phi acc_fv = function
-    | And fl ->
-      let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
-      let (p, np) = List.partition is_pred fl in 
-      let res = And (order_by_fv acc_fv (p @ np)) in
-      if !debug_level > 1 then print_endline ("fvordered and: " ^ (str res));
-      res
-    | Or fl ->
-      let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
-      let (p, np) = List.partition is_pred fl in 
-      let res = Or (order_by_fv acc_fv (p @ np)) in
-      if !debug_level > 1 then print_endline ("fvordered or: " ^ (str res));
-      res
-    | Ex (vs, phi) -> Ex (vs, order_by_fv_phi acc_fv phi)
-    | All (vs, phi) -> All (vs, order_by_fv_phi acc_fv phi)
-    | f -> f in
   match mso_last (flatten (del_vars_quant fv (tnf psi))) with
     | Or fl -> Or (List.map (order_by_fv_phi []) fl)
-    | f -> f
+    | f -> order_by_fv_phi [] f
 
 (* Assign emptyset to the MSO-variable v by replacing "x in X" with "false".  *)
 let assign_emptyset v phi =

Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml	2010-11-28 16:10:41 UTC (rev 1205)
+++ trunk/Toss/Solver/Assignments.ml	2010-11-28 17:05:43 UTC (rev 1206)
@@ -297,6 +297,13 @@
   let ndisj = List.rev_map (fun l -> List.rev_map neg_sign l) poly_disj in
     List.filter RealQuantElim.sat (Aux.product ndisj)
 
+let convert dnf = (* Sat.convert cnf *)
+  let bv v = BoolFormula.BVar v in
+  let bool_dnf = BoolFormula.BOr 
+    (List.map (fun lits -> BoolFormula.BAnd (List.map bv lits)) dnf) in
+  let conv = BoolFormula.convert bool_dnf in
+  conv
+
 (* Project assignments on a given universal variable. We assume that [elems]
    are all elements and are sorted. Corresponds to the for-all v quantifier. *)
 let rec universal elems v = function
@@ -324,7 +331,7 @@
         let (assgs, _) = List.partition (fun x-> x > max_elem) conj in
         List.fold_left (fun s i -> sum elems s disj_arr.(i - max_elem - 1))
           Empty assgs in
-      let dnf = Sat.convert cnf in
+      let dnf = convert cnf in
       List.fold_left (fun s c -> join s (assgn_of_conj c)) Any dnf
   | Real poly_disj -> 
       let neg_disj = negate_real_disj poly_disj in
@@ -395,7 +402,7 @@
     let assgn = List.fold_left appd Any con_assgs in
     if assgn = Empty then cur_list else
       ((pos, neg), assgn) :: cur_list in
-  let dnf = Sat.convert cnf in
+  let dnf = convert cnf in
   List.fold_left add_assgn_of_conj [] dnf
 
 

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2010-11-28 16:10:41 UTC (rev 1205)
+++ trunk/Toss/Solver/SolverTest.ml	2010-11-28 17:05:43 UTC (rev 1206)
@@ -135,6 +135,16 @@
 
   "eval: bigger tc tests" >::
     (fun () ->
+      let diag_phi = 
+        "set d1(x, y) = ex z ((R(x, z) and C(z, y)) or (R(y, z) and C(z, x))) in
+         set d2(x, y) = ex z ((R(x, z) and C(y, z)) or (R(y, z) and C(x, z))) in
+         set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
+         set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
+         set fd1(x, y) = tc x,y (d1(x, y) and not w(y) and not b(y)) in
+         set fd2(x, y) = tc x,y (d2(x, y) and not w(y) and not b(y)) in
+         set Diag1 (x, y) = ex z (fd1 (x, z) and (z = y or d1 (z, y))) in
+         set Diag2 (x, y) = ex z (fd2 (x, z) and (z = y or d2 (z, y))) in
+         wB(x) and (Diag1 (x, y) or Diag2 (x, y))" in
       eval_eq "[  |  |  ] \"
 	   ...   ...
 	   ...   ...
@@ -144,16 +154,24 @@
 	   ...   ...
 	...   ...   
 	...   wB.   
-\"" "set d1(x, y) = ex z ((R(x, z) and C(z, y)) or (R(y, z) and C(z, x))) in
-     set d2(x, y) = ex z ((R(x, z) and C(y, z)) or (R(y, z) and C(x, z))) in
-     set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
-     set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
-     set fd1(x, y) = tc x,y (d1(x, y) and not w(y) and not b(y)) in
-     set fd2(x, y) = tc x,y (d2(x, y) and not w(y) and not b(y)) in
-     set Diag1 (x, y) = ex z (fd1 (x, z) and (z = y or d1 (z, y))) in
-     set Diag2 (x, y) = ex z (fd2 (x, z) and (z = y or d2 (z, y))) in
-     wB(x) and (Diag1 (x, y) or Diag2 (x, y))" 
+\"" diag_phi
 	"{ y->3{ x->3 } , y->6{ x->3 } , y->8{ x->3 } , y->9{ x->3 }  }";
+      eval_eq "[  |  |  ] \"
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   ...   ...   
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   ...   ...   
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   wB.   ...   
+\"" diag_phi
+	("{ y->3{ x->3 } , y->8{ x->3 } , y->10{ x->3 } ," ^
+	    " y->13{ x->3 } , y->17{ x->3 } , y->24{ x->3 }  }");
     );
 
   "eval: with real values" >::


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