From 36449d16458fee2adadb6613886c5d1c9dc15908 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 10 Jun 2019 15:05:20 -0500
Subject: [PATCH] feat(cc): expose a way to access bitfields

---
 src/cc/Sidekick_cc.ml     | 33 +++++++++++++++++++++++++++++++--
 src/core/Sidekick_core.ml | 11 +++++++++++
 src/util/Stat.ml          |  2 +-
 src/util/Stat.mli         |  3 ++-
 4 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 3cd61915..66ec066a 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -26,8 +26,32 @@ module Make(CC_A: ARG) = struct
   module Fun = A.Fun
   module Lit = CC_A.Lit
 
-  module Bits = CCBitField.Make()
-  (* TODO: give theories the possibility to allocate new bits in nodes *)
+  module Bits : sig
+    type t = private int
+    type field
+    val empty : t
+    val equal : t -> t -> bool
+    val mk_field : unit -> field
+    val get : field -> t -> bool
+    val set : field -> bool -> t -> t
+    val merge : t -> t -> t
+  end = struct
+    let max_width = Sys.word_size - 2
+    let width = ref 0
+    type t = int
+    type field = int
+    let empty : t = 0
+    let mk_field () : field =
+      let n = !width in
+      if n > max_width then Error.errorf "maximum number of CC bitfields reached";
+      incr width;
+      n
+    let[@inline] get field x = (x land field) <> 0
+    let[@inline] set field b x =
+      if b then x lor field else x land (lnot field)
+    let merge = (lor)
+    let equal : t -> t -> bool = Pervasives.(=)
+  end
 
   let field_is_pending = Bits.mk_field()
   (** true iff the node is in the [cc.pending] queue *)
@@ -112,6 +136,8 @@ module Make(CC_A: ARG) = struct
       assert (is_root n);
       Bag.to_seq n.n_parents
 
+    type bitfield = Bits.field
+    let allocate_bitfield = Bits.mk_field
     let[@inline] get_field f t = Bits.get f t.n_bits
     let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits
   end
@@ -636,17 +662,20 @@ module Make(CC_A: ARG) = struct
         let r_into_old_next = r_into.n_next in
         let r_from_old_next = r_from.n_next in
         let r_into_old_parents = r_into.n_parents in
+        let r_into_old_bits = r_into.n_bits in
         (* swap [into.next] and [from.next], merging the classes *)
         r_into.n_next <- r_from_old_next;
         r_from.n_next <- r_into_old_next;
         r_into.n_parents <- Bag.append r_into.n_parents r_from.n_parents;
         r_into.n_size <- r_into.n_size + r_from.n_size;
+        r_into.n_bits <- Bits.merge r_into.n_bits r_from.n_bits;
         (* on backtrack, unmerge classes and restore the pointers to [r_from] *)
         on_backtrack cc
           (fun () ->
              Log.debugf 15
                (fun k->k "(@[cc.undo_merge@ :from %a :into %a@])"
                    N.pp r_from N.pp r_into);
+             r_into.n_bits <- r_into_old_bits;
              r_into.n_next <- r_into_old_next;
              r_from.n_next <- r_from_old_next;
              r_into.n_parents <- r_into_old_parents;
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 042981ce..37c1c453 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -170,6 +170,17 @@ module type CC_S = sig
     val iter_parents : t -> t Iter.t
     (** Traverse the parents of the class.
         Precondition: [is_root n] (see {!find} below) *)
+
+    type bitfield
+    (** A field in the bitfield of this node. This should only be
+        allocated when a theory is initialized.
+
+        All fields are initially 0, are backtracked automatically,
+        and are merged automatically when classes are merged. *)
+
+    val allocate_bitfield : unit -> bitfield
+    val get_field : bitfield -> t -> bool
+    val set_field : bitfield -> bool -> t -> unit
   end
 
   module Expl : sig
diff --git a/src/util/Stat.ml b/src/util/Stat.ml
index b6d69d72..795cf019 100644
--- a/src/util/Stat.ml
+++ b/src/util/Stat.ml
@@ -1,4 +1,3 @@
-
 (** {1 Statistics} *)
 
 module Fmt = CCFormat
@@ -39,6 +38,7 @@ let mk_float self name =
 
 let[@inline] incr x = x.count <- 1 + x.count
 let[@inline] incr_f x by = x.count <- by +. x.count
+let[@inline] set c x : unit = c.count <- x
 
 let pp_all out l =
   let pp_w out = function
diff --git a/src/util/Stat.mli b/src/util/Stat.mli
index 6ea3846b..3db55042 100644
--- a/src/util/Stat.mli
+++ b/src/util/Stat.mli
@@ -1,4 +1,3 @@
-
 (** {1 Statistics} *)
 
 module Fmt = CCFormat
@@ -15,6 +14,8 @@ val mk_float : t -> string -> float counter
 val incr : int counter -> unit
 val incr_f : float counter -> float -> unit
 
+val set : 'a counter -> 'a -> unit
+
 (** Existential counter *)
 type ex_counter