change the caching mechanism for var's assignable subterms

src/core/internal.ml

@@ -183,21 +183,23 @@ module Make
      all subterms of a formula. However, the function provided by the theory
      may be costly (if it walks a tree-like structure, and does some processing
      to ignore some subterms for instance), so we want to 'cache' to list
-     of subterms of each formula. To do so we use a hashtable from variable id to
+     of subterms of each formula, so we have a field [v_assignable]
-     list of subterms. *)
+     directly in variables to do so.  *)
-  let iter_map = Hashtbl.create 1003
+  let iter_sub f v = match v.v_assignable with
-
+    | None -> assert false
-  let iter_sub f v =
+    | Some [] -> ()
-    List.iter f (Hashtbl.find iter_map v.vid)
+    | Some l -> List.iter f l
 
   (* When we have a new literal,
      we need to first create the list of its subterms. *)
   let atom (f:St.formula) : atom =
     let res = add_atom f in
-    if not (Hashtbl.mem iter_map res.var.vid) then begin
+    begin match res.var.v_assignable with
-      let l = ref [] in
+      | Some _ -> ()
-      Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
+      | None ->
-      Hashtbl.add iter_map res.var.vid !l
+        let l = ref [] in
+        Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
+        res.var.v_assignable <- Some !l;
     end;
     res
 

src/core/solver_types.ml

@@ -42,6 +42,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     mutable seen : bool;
     mutable v_level : int;
     mutable v_weight : float;
+    mutable v_assignable: lit list option;
     mutable reason : reason option;
   }
 
@@ -88,6 +89,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       seen = false;
       v_level = -1;
       v_weight = -1.;
+      v_assignable = None;
       reason = None;
     }
   and dummy_atom =
@@ -154,6 +156,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
             seen = false;
             v_level = -1;
             v_weight = 0.;
+            v_assignable = None;
             reason = None;
           }
         and pa =

src/core/solver_types_intf.ml

@@ -37,6 +37,7 @@ module type S = sig
     mutable seen : bool;
     mutable v_level : int;
     mutable v_weight : float;
+    mutable v_assignable: lit list option;
     mutable reason : reason option;
   }