Faster iterating over subterms

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;

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
 

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

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