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

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

Revision: 1203
          http://toss.svn.sourceforge.net/toss/?rev=1203&view=rev
Author:   lukaszkaiser
Date:     2010-11-28 13:27:59 +0000 (Sun, 28 Nov 2010)

Log Message:
-----------
First small step in mso solver optimizations.

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

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2010-11-28 01:40:56 UTC (rev 1202)
+++ trunk/Toss/Formula/FormulaOps.ml	2010-11-28 13:27:59 UTC (rev 1203)
@@ -813,6 +813,33 @@
   if !debug_level_tnf > 0 then print_endline ("TNF re of " ^ (real_str re));
   tnf_re_fun re
 
+
+let rec has_mso = function
+  | In _ -> true
+  | Rel _ | Eq _ | RealExpr _ -> false
+  | Not phi | Ex (_, phi) | All (_, phi) -> has_mso phi
+  | And flist | Or flist -> List.exists has_mso flist
+
+let rec has_fo = function
+  | In _ -> false
+  | Rel _ | Eq _ | RealExpr _ -> true
+  | Not phi | Ex (_, phi) | All (_, phi) -> has_fo phi
+  | And flist | Or flist -> List.exists has_fo flist
+
+let rec mso_last = function
+  | Rel _ | Eq _ | In _ | RealExpr _ as phi -> phi
+  | Not phi -> Not (mso_last phi)
+  | Ex (vs, phi) -> Ex (vs, mso_last phi)
+  | All (vs, phi) -> All (vs, mso_last phi)
+  | And flist ->
+    let (msos, fos) = List.partition has_mso (List.map mso_last flist) in
+    let (somefo, nofo) = List.partition has_fo msos in
+    And (fos @ somefo @ nofo)
+  | Or flist -> 
+    let (msos, fos) = List.partition has_mso (List.map mso_last flist) in
+    let (somefo, nofo) = List.partition has_fo msos in
+    Or (fos @ somefo @ nofo)
+
 let tnf_fv phi =
   let fv = free_vars phi in
   let psi = rename_quant_avoiding [] (Ex (fv, phi)) in
@@ -833,11 +860,18 @@
       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: " ^ (str res));
+      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 flatten (del_vars_quant fv (tnf psi)) with
+  match mso_last (flatten (del_vars_quant fv (tnf psi))) with
     | Or fl -> Or (List.map (order_by_fv_phi []) fl)
     | f -> f
 

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2010-11-28 01:40:56 UTC (rev 1202)
+++ trunk/Toss/Solver/Solver.ml	2010-11-28 13:27:59 UTC (rev 1203)
@@ -85,6 +85,11 @@
             MSO (y, [((Elems.add e Elems.empty, Elems.empty), Any)]) in
           report (join aset (FO (x, List.map (fun e -> (e, sing_mso e)) 
                                    (slist elems))))
+      | Not (In (x, y)) ->
+          let sing_non_mso e = 
+            MSO (y, [((Elems.empty, Elems.add e Elems.empty), Any)]) in
+          report (join aset (FO (x, List.map (fun e -> (e, sing_non_mso e))
+                                   (slist elems))))
       | RealExpr (p, s) -> (* TODO: use aset directly as context for speed *)
           report (join aset (assignment_of_real_expr model elems (p, s)))
       | Not phi -> 
@@ -95,9 +100,16 @@
       | And fl -> report (List.fold_left (eval model elems) aset fl)
       | Or [phi] -> report (eval model elems aset phi)
       | Or fl -> 
-          let asets = List.rev_map (fun f -> eval model elems aset f) fl in
-            report 
-              (List.fold_left (sum elems) Empty asets)
+	let step_or (ast, asets) = function
+	  (* | Not psi -> 
+	    let nast = eval model elems ast psi in
+	    (nast, report (complement_join elems ast nast) :: asets) 
+	  | (In (x, y)) as psi -> 
+	    let nast = eval model elems ast (Not psi) in 
+	    (nast, report (eval model elems ast psi) :: asets) *)
+	  | psi -> (ast, report (eval model elems ast psi) :: asets) in
+        let (_, asets) = List.fold_left step_or (aset, []) fl in
+        report (List.fold_left (sum elems) Empty asets)
       | Ex ([], phi) | All ([], phi) -> failwith "evaluating empty quantifier"
       | Ex (vl, phi) ->
 	let aset_vars = AssignmentSet.assigned_vars [] aset in


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