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

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

Revision: 1195
          http://toss.svn.sourceforge.net/toss/?rev=1195&view=rev
Author:   lukaszkaiser
Date:     2010-11-24 00:34:10 +0000 (Wed, 24 Nov 2010)

Log Message:
-----------
Correcting solver cache gives significant speed improvement. Added profiling targets.

Modified Paths:
--------------
    trunk/Toss/.cvsignore
    trunk/Toss/Arena/.cvsignore
    trunk/Toss/Formula/.cvsignore
    trunk/Toss/Makefile
    trunk/Toss/Play/.cvsignore
    trunk/Toss/Solver/.cvsignore
    trunk/Toss/Solver/Solver.ml

Property Changed:
----------------
    trunk/Toss/
    trunk/Toss/Arena/
    trunk/Toss/Formula/
    trunk/Toss/Play/
    trunk/Toss/Solver/


Property changes on: trunk/Toss
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

Toss.docdir
_build
Server
*.native
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

Toss.docdir
_build
Server
*.native
*Profile.log
gmon.out
*~
*.annot
*.cmx
*.cmi
*.o
*.cmo
*.a
*.cmxa
log.*


Modified: trunk/Toss/.cvsignore
===================================================================
--- trunk/Toss/.cvsignore	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/.cvsignore	2010-11-24 00:34:10 UTC (rev 1195)
@@ -6,6 +6,8 @@
 _build
 Server
 *.native
+*Profile.log
+gmon.out
 *~
 *.annot
 *.cmx


Property changes on: trunk/Toss/Arena
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*~

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*Profile.log
*~


Modified: trunk/Toss/Arena/.cvsignore
===================================================================
--- trunk/Toss/Arena/.cvsignore	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Arena/.cvsignore	2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
 # than svn properties. Therefore if you change .cvsignore do the following.
 #     svn propset svn:ignore -F .cvsignore .
 
+*Profile.log
 *~


Property changes on: trunk/Toss/Formula
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*~

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*Profile.log
*~


Modified: trunk/Toss/Formula/.cvsignore
===================================================================
--- trunk/Toss/Formula/.cvsignore	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Formula/.cvsignore	2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
 # than svn properties. Therefore if you change .cvsignore do the following.
 #     svn propset svn:ignore -F .cvsignore .
 
+*Profile.log
 *~

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Makefile	2010-11-24 00:34:10 UTC (rev 1195)
@@ -71,6 +71,11 @@
 %TestDebug: %Test.d.byte
 	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; _build/$<
 
+%TestProfile: %Test.p.native
+	_build/$<
+	gprof _build/$< > $@.log
+	
+
 # Formula tests
 Formula_tests: \
 	Formula/AuxTest \


Property changes on: trunk/Toss/Play
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*~

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*~
*Profile.log


Modified: trunk/Toss/Play/.cvsignore
===================================================================
--- trunk/Toss/Play/.cvsignore	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Play/.cvsignore	2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
 # than svn properties. Therefore if you change .cvsignore do the following.
 #     svn propset svn:ignore -F .cvsignore .
 
+*Profile.log
 *~


Property changes on: trunk/Toss/Solver
___________________________________________________________________
Modified: svn:ignore
   - # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*~

   + # We are still using .cvsignore files as we find them easier to manage
# than svn properties. Therefore if you change .cvsignore do the following.
#     svn propset svn:ignore -F .cvsignore .

*Profile.log
*~


Modified: trunk/Toss/Solver/.cvsignore
===================================================================
--- trunk/Toss/Solver/.cvsignore	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Solver/.cvsignore	2010-11-24 00:34:10 UTC (rev 1195)
@@ -2,4 +2,5 @@
 # than svn properties. Therefore if you change .cvsignore do the following.
 #     svn propset svn:ignore -F .cvsignore .
 
+*Profile.log
 *~

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2010-11-23 11:20:21 UTC (rev 1194)
+++ trunk/Toss/Solver/Solver.ml	2010-11-24 00:34:10 UTC (rev 1195)
@@ -11,14 +11,13 @@
 (* CACHE *)
 
 let cache_struc = ref (empty_structure ())
-let cache_results = ref []
-let cCACHESIZE = ref 50
+let cache_results = Hashtbl.create 15;
 
 
 (* ----------------------- BASIC TYPE DEFINITION -------------------------- *)
 
 type solver = {
-  reg_formulas        : (Formula.formula * int) list ref ;
+  reg_formulas        : (Formula.formula, int) Hashtbl.t ;
   formulas_eval       : (int, Formula.formula) Hashtbl.t ;
   formulas_check      : (int, Formula.formula) Hashtbl.t ;
 }
@@ -27,7 +26,7 @@
 (* ----------------------- CONSTRUCTOR FUNCTIONS -------------------------- *)
 
 let new_solver () = {
-  reg_formulas    = ref [] ;
+  reg_formulas    = Hashtbl.create 3 ;
   formulas_eval   = Hashtbl.create 3 ;
   formulas_check  = Hashtbl.create 3 ;
 }
@@ -36,16 +35,16 @@
   let rec check_form = function
       Ex (vs, phi) -> check_form phi
     | phi -> phi in
-  let psi = FormulaOps.tnf_fv phi in
   try
-    let res = List.assoc psi !(solver.reg_formulas) in
+    let res = Hashtbl.find solver.reg_formulas phi in
     if !debug_level > 0 then print_endline ("Found " ^ (str phi));
     res
   with Not_found ->
+    let psi = FormulaOps.tnf_fv phi in
     if !debug_level > 0 then print_endline ("Entered " ^ (str phi));
     if !debug_level > 0 then print_endline ("Registering " ^ (str psi));
     let id = Hashtbl.length solver.formulas_eval + 1 in
-    solver.reg_formulas := (psi, id) :: !(solver.reg_formulas);
+    Hashtbl.add solver.reg_formulas phi id;
     Hashtbl.add solver.formulas_eval id psi;
     Hashtbl.add solver.formulas_check id (check_form psi);
     id
@@ -193,23 +192,21 @@
     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)];
+    Hashtbl.clear cache_results;
+    Hashtbl.add cache_results phi asg;
     asg
   ) else 
     try
-      let (res, new_cache) = assoc_del phi !cache_results in
-      cache_results := (phi, res) :: new_cache;
+      let res = Hashtbl.find cache_results phi in
       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;
+      Hashtbl.add cache_results phi asg;
       asg
 
 (* Helper function, assignment of tuple. *)
@@ -234,7 +231,7 @@
 let eval_cache_sentences solver struc in_phi =
   let reg_tnf phi = 
     try
-      let phi_id = List.assoc phi !(solver.reg_formulas) in
+      let phi_id = Hashtbl.find solver.reg_formulas phi in
       Hashtbl.find solver.formulas_eval phi_id
     with Not_found ->
       Hashtbl.find solver.formulas_eval (register_formula solver phi) in
@@ -257,7 +254,7 @@
     | 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 (
+  if !debug_level > 1 then (
     print_endline ("in phi: " ^ (Formula.str in_phi));
     print_endline ("phi: " ^ (Formula.str phi));
     print_endline ("proc phi: " ^ (Formula.str proc_phi));
@@ -283,9 +280,9 @@
 	print_endline ("sum vars " ^ (Formula.var_list_str vl));
 	print_endline ("all vars " ^ (Formula.var_list_str all_vs));
       );
-      let gd = FFTNF.ff_tnf (FFSolver.promote_for struc) guard in
-      let asg_gd = join asg (FFSolver.evaluate struc gd) in
-      (* let asg_gd = join asg (eval_cache_sentences solver struc guard) in *)
+      (* let gd = FFTNF.ff_tnf (FFSolver.promote_for struc) guard in
+      let asg_gd = join asg (FFSolver.evaluate 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


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