From 3b671aa7a44d4cf71465a51c5ead147c25a33055 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 16 Feb 2019 15:08:49 -0600
Subject: [PATCH] refactor(term): use hashconsing with a weak table

---
 src/smt/Hashcons.ml   | 35 +++++++++++++++++++++++++++++++++++
 src/smt/Term.ml       | 33 ++++++++++++++++-----------------
 src/smt/Term.mli      |  2 +-
 src/smt/Term_cell.ml  |  2 +-
 src/smt/Term_cell.mli |  2 --
 5 files changed, 53 insertions(+), 21 deletions(-)
 create mode 100644 src/smt/Hashcons.ml

diff --git a/src/smt/Hashcons.ml b/src/smt/Hashcons.ml
new file mode 100644
index 00000000..44a9fa66
--- /dev/null
+++ b/src/smt/Hashcons.ml
@@ -0,0 +1,35 @@
+
+module type ARG = sig
+  type t
+  val equal : t -> t -> bool
+  val hash : t -> int
+  val set_id : t -> int -> unit
+end
+
+module Make(A : ARG): sig
+  type t
+  val create : ?size:int -> unit -> t
+  val hashcons : t -> A.t -> A.t
+  val to_seq : t -> A.t Sequence.t
+end = struct
+  module W = Weak.Make(A)
+
+  type t = {
+    tbl: W.t;
+    mutable n: int;
+  }
+
+  let create ?(size=1024) () : t = {tbl=W.create size; n=0}
+
+  (* hashcons terms *)
+  let hashcons st t =
+    let t' = W.merge st.tbl t in
+    if t == t' then (
+      st.n <- 1 + st.n;
+      A.set_id t' st.n;
+    );
+    t'
+
+  let to_seq st yield =
+    W.iter yield st.tbl
+end
diff --git a/src/smt/Term.ml b/src/smt/Term.ml
index b61b608b..7f9007c8 100644
--- a/src/smt/Term.ml
+++ b/src/smt/Term.ml
@@ -21,30 +21,29 @@ let equal = term_equal_
 let hash = term_hash_
 let compare a b = CCInt.compare a.term_id b.term_id
 
-(* TODO: when GC is implemented, add a field for recycling IDs
-   that have been free'd, so we can keep the ID space dense. *)
+module H = Hashcons.Make(struct
+    type t = term
+    let equal t1 t2 = Term_cell.equal t1.term_view t2.term_view
+    let hash t = Term_cell.hash t.term_view
+    let set_id t id =
+      assert (t.term_id < 0);
+      t.term_id <- id
+  end)
 
 type state = {
-  tbl : term Term_cell.Tbl.t;
+  tbl : H.t;
   mutable n: int;
   true_ : t lazy_t;
   false_ : t lazy_t;
 }
 
-let mk_real_ st c : t =
-  let term_ty = Term_cell.ty c in
-  let t = {
-    term_id= st.n;
-    term_ty;
-    term_view=c;
-  } in
-  st.n <- 1 + st.n;
-  Term_cell.Tbl.add st.tbl c t;
-  t
-
 let[@inline] make st (c:t term_view) : t =
-  try Term_cell.Tbl.find st.tbl c
-  with Not_found -> mk_real_ st c
+  let t = {term_id= -1; term_ty=Ty.prop; term_view=c} in
+  let t' = H.hashcons st.tbl t in
+  if t == t' then (
+    t'.term_ty <- Term_cell.ty c;
+  );
+  t'
 
 let[@inline] true_ st = Lazy.force st.true_
 let[@inline] false_ st = Lazy.force st.false_
@@ -53,7 +52,7 @@ let bool st b = if b then true_ st else false_ st
 let create ?(size=1024) () : state =
   let rec st ={
     n=2;
-    tbl=Term_cell.Tbl.create size;
+    tbl=H.create ~size ();
     true_ = lazy (make st Term_cell.true_);
     false_ = lazy (make st Term_cell.false_);
   } in
diff --git a/src/smt/Term.mli b/src/smt/Term.mli
index 2a7da645..e329beb4 100644
--- a/src/smt/Term.mli
+++ b/src/smt/Term.mli
@@ -34,7 +34,7 @@ val eq : state -> t -> t -> t
 val if_: state -> t -> t -> t -> t
 val and_eager : state -> t -> t -> t (* evaluate left argument first *)
 
-(* TODO: remove *)
+(** Obtain unsigned version of [t], + the sign as a boolean *)
 val abs : t -> t * bool
 
 val to_seq : t -> t Sequence.t
diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml
index 6f9e248d..85cd04b8 100644
--- a/src/smt/Term_cell.ml
+++ b/src/smt/Term_cell.ml
@@ -46,7 +46,7 @@ end[@@inline]
 include Make_eq(struct
     type t = term
     let equal (t1:t) t2 = t1==t2
-    let hash (t:term): int = t.term_id
+    let hash (t:term): int = CCHash.int t.term_id
     let pp = pp_term
   end)
 
diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli
index a7689c99..c31e4c9e 100644
--- a/src/smt/Term_cell.mli
+++ b/src/smt/Term_cell.mli
@@ -24,8 +24,6 @@ val ty : t -> Ty.t
 
 val pp : t Fmt.printer
 
-module Tbl : CCHashtbl.S with type key = t
-
 module type ARG = sig
   type t
   val hash : t -> int