From 2ed541d528b6b48b3211125c69266f9ebdee9202 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 18 Dec 2014 15:34:01 +0100
Subject: [PATCH] Faster iterating over subterms

---
 solver/mcsolver.ml            |  4 ++--
 solver/mcsolver_types.ml      | 13 +++++++++++++
 solver/mcsolver_types_intf.ml |  4 ++++
 tests/run                     |  2 +-
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 8707c4d8..08b3748a 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -182,7 +182,7 @@ module Make (E : Expr_intf.S)
       (fun v -> Iheap.insert f_weight env.order v.vid)
       (fun v ->
           Iheap.insert f_weight env.order v.vid;
-          Th.iter_assignable (fun t -> Iheap.insert f_weight env.order (St.add_term t).vid) v.tag.pa.lit
+          iter_sub (fun t -> Iheap.insert f_weight env.order t.vid) v
       )
 
   let var_decay_activity () =
@@ -204,7 +204,7 @@ module Make (E : Expr_intf.S)
 
   let var_bump_activity v =
       var_bump_activity_aux v;
-      Th.iter_assignable (fun t -> var_bump_activity_aux (St.add_term t)) v.tag.pa.lit
+      iter_sub (fun t -> var_bump_activity_aux t) v
 
   let clause_bump_activity c =
     c.activity <- c.activity +. env.clause_inc;
diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml
index 092ed047..3b116c1f 100644
--- a/solver/mcsolver_types.ml
+++ b/solver/mcsolver_types.ml
@@ -199,6 +199,19 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
     let cpt = ref 0 in
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
+  (* Iteration over subterms *)
+  module Mi = Map.Make(struct type t = int let compare= Pervasives.compare end)
+  let iter_map = ref Mi.empty
+
+  let iter_sub f v =
+      try
+          List.iter f (Mi.find v.vid !iter_map)
+      with Not_found ->
+          let l = ref [] in
+          Th.iter_assignable (fun t -> l := add_term t :: !l) v.tag.pa.lit;
+          iter_map := Mi.add v.vid !l !iter_map;
+          List.iter f !l
+
   (* Pretty printing for atoms and clauses *)
   let print_semantic_var fmt v = E.Term.print fmt v.tag.term
 
diff --git a/solver/mcsolver_types_intf.ml b/solver/mcsolver_types_intf.ml
index ae7213ee..a0a313cc 100644
--- a/solver/mcsolver_types_intf.ml
+++ b/solver/mcsolver_types_intf.ml
@@ -82,6 +82,10 @@ module type S = sig
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
 
+  val iter_sub : (semantic var -> unit) -> boolean var -> unit
+  (** Iterates over the semantic var corresponding to subterms of the fiven literal, according
+      to Th.iter_assignable *)
+
   val empty_clause : clause
   (** The empty clause *)
   val make_clause : string -> atom list -> int -> bool -> premise -> clause
diff --git a/tests/run b/tests/run
index a95a345b..7ad8e67a 100755
--- a/tests/run
+++ b/tests/run
@@ -15,7 +15,7 @@ solvertest () {
             exit 2
         fi
     done
-    echo -e "\r\033[K\e[32m[OK]\e[0m $2-$3"
+    echo -e "\r\033[K\e[32m[OK]\e[0m $3/$2"
 }
 
 solvertest "$CURDIR/sat/" "Sat" $1