From af55371eb4c8fc89e52be92f670352851362dfb6 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 29 Jul 2016 22:50:37 +0200
Subject: [PATCH] change the caching mechanism for var's assignable subterms

---
 src/core/internal.ml          | 22 ++++++++++++----------
 src/core/solver_types.ml      |  3 +++
 src/core/solver_types_intf.ml |  1 +
 3 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 75d0ef3f..f20e6402 100644
--- a/src/core/internal.ml
+++ b/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
-     list of subterms. *)
-  let iter_map = Hashtbl.create 1003
-
-  let iter_sub f v =
-    List.iter f (Hashtbl.find iter_map v.vid)
+     of subterms of each formula, so we have a field [v_assignable]
+     directly in variables to do so.  *)
+  let iter_sub f v = match v.v_assignable with
+    | None -> assert false
+    | Some [] -> ()
+    | 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
-      let l = ref [] in
-      Plugin.iter_assignable (fun t -> l := add_term t :: !l) res.var.pa.lit;
-      Hashtbl.add iter_map res.var.vid !l
+    begin match res.var.v_assignable with
+      | Some _ -> ()
+      | None ->
+        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
 
diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index 642d4724..8a1dc92c 100644
--- a/src/core/solver_types.ml
+++ b/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 =
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index cad58fd9..955f60dd 100644
--- a/src/core/solver_types_intf.ml
+++ b/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;
   }