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

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

Revision: 1190
          http://toss.svn.sourceforge.net/toss/?rev=1190&view=rev
Author:   lukaszkaiser
Date:     2010-11-22 02:05:26 +0000 (Mon, 22 Nov 2010)

Log Message:
-----------
Solver optimization and small corrections.

Modified Paths:
--------------
    trunk/Toss/Formula/Makefile
    trunk/Toss/Makefile
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/TossTest.ml

Modified: trunk/Toss/Formula/Makefile
===================================================================
--- trunk/Toss/Formula/Makefile	2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Formula/Makefile	2010-11-22 02:05:26 UTC (rev 1190)
@@ -3,6 +3,7 @@
 %Test:
 	make -C .. Formula/$@
 
+AuxTest:
 FormulaTest:
 BoolFormulaTest:
 FormulaOpsTest:

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Makefile	2010-11-22 02:05:26 UTC (rev 1190)
@@ -32,9 +32,9 @@
 OCB_CFLAG=-cflags -I,+oUnit,-g
 OCB_LIB=-libs str,nums,unix,oUnit 
 OCB_PP=-pp "camlp4o ../caml_extensions/pa_let_try.cmo ../caml_extensions/pa_backtrace.cmo"
-OCAMLBUILD=ocamlbuild -j 4 -menhir ../menhir_conf $(OCB_PP) \
+OCAMLBUILD=ocamlbuild -j 8 -menhir ../menhir_conf $(OCB_PP) \
 	$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
-OCAMLBUILDBT=ocamlbuild -j 4 menhir ../menhir_conf $(OCB_PP) \
+OCAMLBUILDBT=ocamlbuild -j 8 menhir ../menhir_conf $(OCB_PP) \
 	$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAGBT)
 
 FormulaINC=Formula/Sat
@@ -68,6 +68,7 @@
 
 # Formula tests
 Formula_tests: \
+	Formula/AuxTest \
 	Formula/FormulaTest \
 	Formula/BoolFormulaTest \
 	Formula/FormulaOpsTest \

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/Solver/Solver.ml	2010-11-22 02:05:26 UTC (rev 1190)
@@ -177,23 +177,39 @@
     process_vars [] (List.sort Formula.compare_vars (fo_vars_real p))
 
 
+(* Helper: find assoc and remove. *)
+let rec assoc_del (x : Formula.formula) = function
+  | [] -> raise Not_found
+  | (a, b as pair) :: l ->
+      if x = a then (b, l) else 
+	let (b, nl) = assoc_del x l in
+	(b, pair :: nl)
+
 (* Eval with very basic caching. *)
 let eval_m struc phi = 
+  if phi = And [] then Any else
   if !cache_struc != struc then (
     let els = Set (Elems.cardinal struc.elements, struc.elements) in
     let asg = eval struc (ref els) Any phi in
     cache_struc := struc;
     cache_results := [(phi, asg)];
     asg
-  ) else try
-    List.assoc phi !cache_results
-  with Not_found ->
-    if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));    
-    if List.length !cache_results > !cCACHESIZE then cache_results := [];
-    let els = Set (Elems.cardinal struc.elements, struc.elements) in
-    let asg = eval struc (ref els) Any phi in
-    cache_results := (phi, asg) :: !cache_results;
-    asg
+  ) else 
+    try
+      let (res, new_cache) = assoc_del phi !cache_results in
+      cache_results := (phi, res) :: new_cache;
+      if !debug_level > 1 then (
+	print_endline ("found in cache: " ^ (Formula.str phi));
+	print_endline ("size: "^ (string_of_int (List.length !cache_results)));
+      );
+      res
+    with Not_found ->
+      if !debug_level > 0 then print_endline ("Eval_m " ^ (str phi));    
+      if List.length !cache_results > !cCACHESIZE then cache_results := [];
+      let els = Set (Elems.cardinal struc.elements, struc.elements) in
+      let asg = eval struc (ref els) Any phi in
+      cache_results := (phi, asg) :: !cache_results;
+      asg
 
 (* Helper function, assignment of tuple. *)
 let asg_of_tuple struc vars tuple =
@@ -207,37 +223,66 @@
   eval_m struc
     (RealExpr (Plus (expr, Times (Const (-1.), RVar rvar)), Formula.EQZero))
 
+(* Helper checking function. *)
+let rec check_f struc asg = function
+  | Ex (vs, phi) -> check_f struc asg phi
+  | Or (fl) -> List.exists (check_f struc asg) fl
+  | phi -> join asg (eval_m struc phi) <> Empty
 
+(* Almost as eval_m but cache sub-formulas in boolean form without free vars. *)
+let eval_cache_sentences solver struc in_phi =
+  let reg_tnf phi = 
+    try
+      let phi_id = List.assoc phi !(solver.reg_formulas) in
+      Hashtbl.find solver.formulas_eval phi_id
+    with Not_found ->
+      Hashtbl.find solver.formulas_eval (register_formula solver phi) in
+  let eval_no_fv phi = 
+    if FormulaOps.free_vars phi = [] then (
+      if !debug_level > 1 then
+	print_endline ("sentence check: " ^ (Formula.str phi));
+      if check_f struc Any (reg_tnf phi) then And [] else Or []
+    )
+    else phi in
+  let not_true f = f <> And [] in
+  let not_false f = f <> Or [] in
+  let rec subst_no_fv = function
+    | And fl ->
+      let nfl = List.filter not_true (List.map subst_no_fv fl) in
+      if List.exists (fun f -> f = Or []) nfl then Or [] else And nfl
+    | Or fl ->
+      let nfl = List.filter not_false (List.map subst_no_fv fl) in
+      if List.exists (fun f -> f = And []) nfl then And [] else Or nfl
+    | f -> eval_no_fv f in
+  let phi = subst_no_fv in_phi in
+  let proc_phi = reg_tnf phi in
+  if !debug_level > 0 then (
+    print_endline ("in phi: " ^ (Formula.str in_phi));
+    print_endline ("phi: " ^ (Formula.str phi));
+    print_endline ("proc phi: " ^ (Formula.str proc_phi));
+  );
+  eval_m struc proc_phi
+
+
 (* Fast function to get a value of a real expression without free variables
    other than those assigned in [asg] explicitely. *)
 let rec get_real_val solver asg expr struc =
-  let rec check_f = function
-      Ex (vs, phi) -> check_f phi
-    | Or (fl) -> List.exists check_f fl
-    | phi -> join asg (eval_m struc phi) <> Empty in
+  let check_fa = check_f struc asg in
   match expr with
-      Char phi -> if check_f phi then 1. else 0.
+      Char phi -> if check_fa phi then 1. else 0.
     | Const v -> v
     | Times (e1, e2) -> 
       (get_real_val solver asg e1 struc) *. (get_real_val solver asg e2 struc)
     | Plus (e1, e2) -> 
       (get_real_val solver asg e1 struc) +. (get_real_val solver asg e2 struc)
     | Sum (vl, guard, r) ->
-      let gd = (
-	try
-	  let gd_id = List.assoc guard !(solver.reg_formulas) in
-	  Hashtbl.find solver.formulas_eval gd_id
-	with Not_found ->
-	  Hashtbl.find solver.formulas_eval (register_formula solver guard)
-      ) in
       let all_vs = (List.map to_fo (AssignmentSet.assigned_vars [] asg)) @ vl in
       if !debug_level > 0 then (
-	print_endline ("guard " ^ (Formula.str guard));
 	print_endline ("asg " ^ (AssignmentSet.str asg));
 	print_endline ("sum vars " ^ (Formula.var_list_str vl));
 	print_endline ("all vars " ^ (Formula.var_list_str all_vs));
       );
-      let asg_gd = join asg (eval_m struc gd) in
+      let asg_gd = join asg (eval_cache_sentences solver struc guard) in
       let tps = tuples struc.elements (List.map var_str all_vs) asg_gd in
       let add_val acc tp = 
 	let tp_asg = asg_of_tuple struc all_vs tp in

Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml	2010-11-21 21:44:23 UTC (rev 1189)
+++ trunk/Toss/TossTest.ml	2010-11-22 02:05:26 UTC (rev 1190)
@@ -1,7 +1,7 @@
 open OUnit
 
 let formula_tests = "Formula" >::: [
-  (* AuxTest.tests; *)
+  AuxTest.tests;
   FormulaTest.tests;
   FormulaOpsTest.tests;
   FFTNFTest.tests;


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