wip: refactor(cc): remove layers of functorization

src/cc/Sidekick_cc.mli

@@ -1,15 +1,15 @@
 (** Congruence Closure Implementation *)
 
-module View = Sidekick_sigs_cc.View
-open Sidekick_sigs_cc
+open Sidekick_core
+module View = View
 
-module type ARG = ARG
+module type ARG = Sigs.ARG
 
 module type S = sig
-  include S
+  include Sigs.S
 
   val create :
-    ?stat:Stat.t -> ?size:[ `Small | `Big ] -> term_store -> proof_trace -> t
+    ?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
   (** Create a new congruence closure.
 
       @param term_store used to be able to create new terms. All terms
@@ -26,8 +26,4 @@ module type S = sig
   (**/**)
 end
 
-module Make (A : ARG) :
-  S
-    with module T = A.T
-     and module Lit = A.Lit
-     and module Proof_trace = A.Proof_trace
+module Make (_ : ARG) : S

src/cc/bits.ml

@@ -0,0 +1,26 @@
+type bitfield_gen = int ref
+
+let max_width = Sys.word_size - 2
+let mk_gen () = ref 0
+
+type t = int
+type field = int
+
+let empty : t = 0
+
+let mk_field (gen : bitfield_gen) : field =
+  let n = !gen in
+  if n > max_width then Error.errorf "maximum number of CC bitfields reached";
+  incr gen;
+  1 lsl 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 = CCEqual.poly

src/cc/bits.mli

@@ -0,0 +1,13 @@
+(** Basic bitfield *)
+
+type t = private int
+type field
+type bitfield_gen
+
+val empty : t
+val equal : t -> t -> bool
+val mk_field : bitfield_gen -> field
+val mk_gen : unit -> bitfield_gen
+val get : field -> t -> bool
+val set : field -> bool -> t -> t
+val merge : t -> t -> t

src/cc/dune

@@ -1,5 +1,7 @@
 (library
  (name Sidekick_cc)
  (public_name sidekick.cc)
- (libraries containers iter sidekick.sigs sidekick.sigs.cc sidekick.util)
- (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))
+ (synopsis "main congruence closure implementation")
+ (private_modules core_cc)
+ (libraries containers iter sidekick.sigs sidekick.core sidekick.util)
+ (flags :standard -open Sidekick_util))

src/cc/mini/Sidekick_mini_cc.ml

@@ -1,46 +1,34 @@
-module CC_view = Sidekick_sigs_cc.View
-
-module type TERM = Sidekick_sigs_term.S
+open Sidekick_core
+module CC_view = Sidekick_cc.View
 
 module type ARG = sig
-  module T : TERM
-
-  val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
+  val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
 end
 
 module type S = sig
-  type term
-  type fun_
-  type term_store
   type t
 
-  val create : term_store -> t
+  val create : Term.store -> t
   val clear : t -> unit
-  val add_lit : t -> term -> bool -> unit
+  val add_lit : t -> Term.t -> bool -> unit
   val check_sat : t -> bool
-  val classes : t -> term Iter.t Iter.t
+  val classes : t -> Term.t Iter.t Iter.t
 end
 
 module Make (A : ARG) = struct
   open CC_view
-  module Fun = A.T.Fun
-  module T = A.T.Term
-
-  type fun_ = A.T.Fun.t
-  type term = T.t
-  type term_store = T.store
-
-  module T_tbl = CCHashtbl.Make (T)
+  module T = Term
+  module T_tbl = Term.Tbl
 
   type node = {
-    n_t: term;
+    n_t: Term.t;
     mutable n_next: node; (* next in class *)
     mutable n_size: int; (* size of class *)
     mutable n_parents: node list;
     mutable n_root: node; (* root of the class *)
   }
 
-  type signature = (fun_, node, node list) CC_view.t
+  type signature = (Const.t, node, node list) CC_view.t
 
   module Node = struct
     type t = node
@@ -51,7 +39,7 @@ module Make (A : ARG) = struct
     let[@inline] is_root n = n == n.n_root
     let[@inline] root n = n.n_root
     let[@inline] term n = n.n_t
-    let pp out n = T.pp out n.n_t
+    let pp out n = T.pp_debug out n.n_t
     let add_parent (self : t) ~p : unit = self.n_parents <- p :: self.n_parents
 
     let make (t : T.t) : t =
@@ -79,9 +67,9 @@ module Make (A : ARG) = struct
     let equal (s1 : t) s2 : bool =
       match s1, s2 with
       | Bool b1, Bool b2 -> b1 = b2
-      | App_fun (f1, []), App_fun (f2, []) -> Fun.equal f1 f2
+      | App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2
       | App_fun (f1, l1), App_fun (f2, l2) ->
-        Fun.equal f1 f2 && CCList.equal Node.equal l1 l2
+        Const.equal f1 f2 && CCList.equal Node.equal l1 l2
       | App_ho (f1, a1), App_ho (f2, a2) -> Node.equal f1 f2 && Node.equal a1 a2
       | Not n1, Not n2 -> Node.equal n1 n2
       | If (a1, b1, c1), If (a2, b2, c2) ->
@@ -101,7 +89,7 @@ module Make (A : ARG) = struct
       let module H = CCHash in
       match s with
       | Bool b -> H.combine2 10 (H.bool b)
-      | App_fun (f, l) -> H.combine3 20 (Fun.hash f) (H.list Node.hash l)
+      | App_fun (f, l) -> H.combine3 20 (Const.hash f) (H.list Node.hash l)
       | App_ho (f, a) -> H.combine3 30 (Node.hash f) (Node.hash a)
       | Eq (a, b) -> H.combine3 40 (Node.hash a) (Node.hash b)
       | Opaque u -> H.combine2 50 (Node.hash u)
@@ -110,9 +98,9 @@ module Make (A : ARG) = struct
 
     let pp out = function
       | Bool b -> Fmt.bool out b
-      | App_fun (f, []) -> Fun.pp out f
+      | App_fun (f, []) -> Const.pp out f
       | App_fun (f, l) ->
-        Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_list Node.pp) l
+        Fmt.fprintf out "(@[%a@ %a@])" Const.pp f (Util.pp_list Node.pp) l
       | App_ho (f, a) -> Fmt.fprintf out "(@[%a@ %a@])" Node.pp f Node.pp a
       | Opaque t -> Node.pp out t
       | Not u -> Fmt.fprintf out "(@[not@ %a@])" Node.pp u
@@ -134,8 +122,8 @@ module Make (A : ARG) = struct
   }
 
   let create tst : t =
-    let true_ = T.bool tst true in
-    let false_ = T.bool tst false in
+    let true_ = Term.true_ tst in
+    let false_ = Term.false_ tst in
     let self =
       {
         ok = true;
@@ -180,7 +168,7 @@ module Make (A : ARG) = struct
       k b;
       k c
 
-  let rec add_t (self : t) (t : term) : node =
+  let rec add_t (self : t) (t : Term.t) : node =
     match T_tbl.find self.tbl t with
     | n -> n
     | exception Not_found ->
@@ -194,9 +182,10 @@ module Make (A : ARG) = struct
       self.pending <- node :: self.pending;
       node
 
-  let find_t_ (self : t) (t : term) : node =
+  let find_t_ (self : t) (t : Term.t) : node =
     try T_tbl.find self.tbl t |> Node.root
-    with Not_found -> Error.errorf "mini-cc.find_t: no node for %a" T.pp t
+    with Not_found ->
+      Error.errorf "mini-cc.find_t: no node for %a" T.pp_debug t
 
   exception E_unsat
 

src/cc/mini/Sidekick_mini_cc.mli

@@ -5,35 +5,28 @@
     It just decides the satisfiability of a set of (dis)equations.
 *)
 
-module CC_view = Sidekick_sigs_cc.View
-
-module type TERM = Sidekick_sigs_term.S
+open Sidekick_core
+module CC_view = Sidekick_cc.View
 
 (** Argument for the functor {!Make}
 
-    It only requires a term structure, and a congruence-oriented view. *)
+    It only requires a Term.t structure, and a congruence-oriented view. *)
 module type ARG = sig
-  module T : TERM
-
-  val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
+  val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) CC_view.t
 end
 
 (** Main signature for an instance of the mini congruence closure *)
 module type S = sig
-  type term
-  type fun_
-  type term_store
-
   type t
   (** An instance of the congruence closure. Mutable *)
 
-  val create : term_store -> t
+  val create : Term.store -> t
   (** New instance *)
 
   val clear : t -> unit
   (** Fully reset the congruence closure's state *)
 
-  val add_lit : t -> term -> bool -> unit
+  val add_lit : t -> Term.t -> bool -> unit
   (** [add_lit cc p sign] asserts that [p] is true if [sign],
       or [p] is false if [not sign]. If [p] is an equation and [sign]
       is [true], this adds a new equation to the congruence relation. *)
@@ -42,14 +35,10 @@ module type S = sig
   (** [check_sat cc] returns [true] if the current state is satisfiable, [false]
       if it's unsatisfiable. *)
 
-  val classes : t -> term Iter.t Iter.t
+  val classes : t -> Term.t Iter.t Iter.t
   (** Traverse the set of classes in the congruence closure.
       This should be called only if {!check} returned [Sat]. *)
 end
 
-(** Instantiate the congruence closure for the given term structure. *)
-module Make (A : ARG) :
-  S
-    with type term = A.T.Term.t
-     and type fun_ = A.T.Fun.t
-     and type term_store = A.T.Term.store
+(** Instantiate the congruence closure for the given Term.t structure. *)
+module Make (_ : ARG) : S

src/cc/mini/dune

@@ -1,5 +1,5 @@
 (library
  (name Sidekick_mini_cc)
  (public_name sidekick.mini-cc)
- (libraries containers iter sidekick.sigs.cc sidekick.sigs.term sidekick.util)
+ (libraries containers iter sidekick.cc sidekick.core sidekick.util)
  (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))

src/cc/plugin/dune

@@ -1,5 +1,5 @@
 (library
  (name Sidekick_cc_plugin)
  (public_name sidekick.cc.plugin)
- (libraries containers iter sidekick.sigs sidekick.sigs.cc sidekick.util)
- (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util))
+ (libraries containers iter sidekick.sigs sidekick.cc sidekick.util)
+ (flags :standard -w +32 -open Sidekick_util))

src/cc/plugin/sidekick_cc_plugin.ml

@@ -1,4 +1,4 @@
-open Sidekick_sigs_cc
+open Sidekick_cc
 
 module type EXTENDED_PLUGIN_BUILDER = sig
   include MONOID_PLUGIN_BUILDER

src/cc/plugin/sidekick_cc_plugin.mli

@@ -1,6 +1,6 @@
-(** Congruence Closure Implementation *)
+(** Congruence Closure Plugin *)
 
-open Sidekick_sigs_cc
+open Sidekick_cc
 
 module type EXTENDED_PLUGIN_BUILDER = sig
   include MONOID_PLUGIN_BUILDER

src/cc/sigs.ml

@@ -0,0 +1,506 @@
+(** Main types for congruence closure *)
+
+open Sidekick_core
+module View = View
+
+(** Arguments to a congruence closure's implementation *)
+module type ARG = sig
+  val view_as_cc : Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
+  (** View the Term.t through the lens of the congruence closure *)
+end
+
+(** Collection of input types, and types defined by the congruence closure *)
+module type ARGS_CLASSES_EXPL_EVENT = sig
+  (** E-node.
+
+      An e-node is a node in the congruence closure that is contained
+      in some equivalence classe).
+      An equivalence class is a set of terms that are currently equal
+      in the partial model built by the solver.
+      The class is represented by a collection of nodes, one of which is
+      distinguished and is called the "representative".
+
+      All information pertaining to the whole equivalence class is stored
+      in its representative's {!E_node.t}.
+
+      When two classes become equal (are "merged"), one of the two
+      representatives is picked as the representative of the new class.
+      The new class contains the union of the two old classes' nodes.
+
+      We also allow theories to store additional information in the
+      representative. This information can be used when two classes are
+      merged, to detect conflicts and solve equations à la Shostak.
+  *)
+  module E_node : sig
+    type t
+    (** An E-node.
+
+        A value of type [t] points to a particular Term.t, but see
+        {!find} to get the representative of the class. *)
+
+    include Sidekick_sigs.PRINT with type t := t
+
+    val term : t -> Term.t
+    (** Term contained in this equivalence class.
+        If [is_root n], then [Term.t n] is the class' representative Term.t. *)
+
+    val equal : t -> t -> bool
+    (** Are two classes {b physically} equal? To check for
+        logical equality, use [CC.E_node.equal (CC.find cc n1) (CC.find cc n2)]
+        which checks for equality of representatives. *)
+
+    val hash : t -> int
+    (** An opaque hash of this E_node.t. *)
+
+    val is_root : t -> bool
+    (** Is the E_node.t a root (ie the representative of its class)?
+        See {!find} to get the root. *)
+
+    val iter_class : t -> t Iter.t
+    (** Traverse the congruence class.
+        Precondition: [is_root n] (see {!find} below) *)
+
+    val iter_parents : t -> t Iter.t
+    (** Traverse the parents of the class.
+        Precondition: [is_root n] (see {!find} below) *)
+
+    (* FIXME:
+       [@@alert refactor "this should be replaced with a Per_class concept"]
+    *)
+
+    type bitfield
+    (** A field in the bitfield of this node. This should only be
+        allocated when a theory is initialized.
+
+        Bitfields are accessed using preallocated keys.
+        See {!CC_S.allocate_bitfield}.
+
+        All fields are initially 0, are backtracked automatically,
+        and are merged automatically when classes are merged. *)
+  end
+
+  (** Explanations
+
+      Explanations are specialized proofs, created by the congruence closure
+      when asked to justify why two terms are equal. *)
+  module Expl : sig
+    type t
+
+    include Sidekick_sigs.PRINT with type t := t
+
+    val mk_merge : E_node.t -> E_node.t -> t
+    (** Explanation: the nodes were explicitly merged *)
+
+    val mk_merge_t : Term.t -> Term.t -> t
+    (** Explanation: the terms were explicitly merged *)
+
+    val mk_lit : Lit.t -> t
+    (** Explanation: we merged [t] and [u] because of literal [t=u],
+        or we merged [t] and [true] because of literal [t],
+        or [t] and [false] because of literal [¬t] *)
+
+    val mk_list : t list -> t
+    (** Conjunction of explanations *)
+
+    val mk_theory :
+      Term.t ->
+      Term.t ->
+      (Term.t * Term.t * t list) list ->
+      Proof_term.step_id ->
+      t
+    (** [mk_theory t u expl_sets pr] builds a theory explanation for
+        why [|- t=u]. It depends on sub-explanations [expl_sets] which
+        are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
+        explanations that justify [t_i = u_i] in the current congruence closure.
+
+        The proof [pr] is the theory lemma, of the form
+        [ (t_i = u_i)_i |- t=u ].
+        It is resolved against each [expls_i |- t_i=u_i] obtained from
+        [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
+        where [Gamma] is a subset of the literals asserted into the congruence
+        closure.
+
+        For example for the lemma [a=b] deduced by injectivity
+        from [Some a=Some b] in the theory of datatypes,
+        the arguments would be
+        [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
+        where [pr] is the injectivity lemma [Some a=Some b |- a=b].
+    *)
+  end
+
+  (** Resolved explanations.
+
+      The congruence closure keeps explanations for why terms are in the same
+      class. However these are represented in a compact, cheap form.
+      To use these explanations we need to {b resolve} them into a
+      resolved explanation, typically a list of
+      literals that are true in the current trail and are responsible for
+      merges.
+
+      However, we can also have merged classes because they have the same value
+      in the current model. *)
+  module Resolved_expl : sig
+    type t = { lits: Lit.t list; pr: Proof_trace.t -> Proof_term.step_id }
+
+    include Sidekick_sigs.PRINT with type t := t
+  end
+
+  (** Per-node data *)
+
+  type e_node = E_node.t
+  (** A node of the congruence closure *)
+
+  type repr = E_node.t
+  (** Node that is currently a representative. *)
+
+  type explanation = Expl.t
+end
+
+(** Main congruence closure signature.
+
+    The congruence closure handles the theory QF_UF (uninterpreted
+    function symbols).
+    It is also responsible for {i theory combination}, and provides
+    a general framework for equality reasoning that other
+    theories piggyback on.
+
+    For example, the theory of datatypes relies on the congruence closure
+    to do most of the work, and "only" adds injectivity/disjointness/acyclicity
+    lemmas when needed.
+
+    Similarly, a theory of arrays would hook into the congruence closure and
+    assert (dis)equalities as needed.
+*)
+module type S = sig
+  include ARGS_CLASSES_EXPL_EVENT
+
+  type t
+  (** The congruence closure object.
+      It contains a fair amount of state and is mutable
+      and backtrackable. *)
+
+  (** {3 Accessors} *)
+
+  val term_store : t -> Term.store
+  val proof : t -> Proof_trace.t
+
+  val find : t -> e_node -> repr
+  (** Current representative *)
+
+  val add_term : t -> Term.t -> e_node
+  (** Add the Term.t to the congruence closure, if not present already.
+      Will be backtracked. *)
+
+  val mem_term : t -> Term.t -> bool
+  (** Returns [true] if the Term.t is explicitly present in the congruence closure *)
+
+  val allocate_bitfield : t -> descr:string -> E_node.bitfield
+  (** Allocate a new e_node field (see {!E_node.bitfield}).
+
+      This field descriptor is henceforth reserved for all nodes
+      in this congruence closure, and can be set using {!set_bitfield}
+      for each class_ individually.
+      This can be used to efficiently store some metadata on nodes
+      (e.g. "is there a numeric value in the class"
+      or "is there a constructor Term.t in the class").
+
+      There may be restrictions on how many distinct fields are allocated
+      for a given congruence closure (e.g. at most {!Sys.int_size} fields).
+  *)
+
+  val get_bitfield : t -> E_node.bitfield -> E_node.t -> bool
+  (** Access the bit field of the given e_node *)
+
+  val set_bitfield : t -> E_node.bitfield -> bool -> E_node.t -> unit
+  (** Set the bitfield for the e_node. This will be backtracked.
+      See {!E_node.bitfield}. *)
+
+  type propagation_reason = unit -> Lit.t list * Proof_term.step_id
+
+  (** Handler Actions
+
+      Actions that can be scheduled by event handlers. *)
+  module Handler_action : sig
+    type t =
+      | Act_merge of E_node.t * E_node.t * Expl.t
+      | Act_propagate of Lit.t * propagation_reason
+
+    (* TODO:
+       - an action to modify data associated with a class
+    *)
+
+    type conflict = Conflict of Expl.t [@@unboxed]
+
+    type or_conflict = (t list, conflict) result
+    (** Actions or conflict scheduled by an event handler.
+
+      - [Ok acts] is a list of merges and propagations
+      - [Error confl] is a conflict to resolve.
+    *)
+  end
+
+  (** Result Actions.
+
+
+    Actions returned by the congruence closure after calling {!check}. *)
+  module Result_action : sig
+    type t =
+      | Act_propagate of { lit: Lit.t; reason: propagation_reason }
+          (** [propagate (Lit.t, reason)] declares that [reason() => Lit.t]
+          is a tautology.
+
+          - [reason()] should return a list of literals that are currently true,
+            as well as a proof.
+          - [Lit.t] should be a literal of interest (see {!S.set_as_lit}).
+
+          This function might never be called, a congruence closure has the right
+          to not propagate and only trigger conflicts. *)
+
+    type conflict =
+      | Conflict of Lit.t list * Proof_term.step_id
+          (** [raise_conflict (c,pr)] declares that [c] is a tautology of
+          the theory of congruence.
+          @param pr the proof of [c] being a tautology *)
+
+    type or_conflict = (t list, conflict) result
+  end
+
+  (** {3 Events}
+
+      Events triggered by the congruence closure, to which
+      other plugins can subscribe. *)
+
+  (** Events emitted by the congruence closure when something changes. *)
+  val on_pre_merge :
+    t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
+  (** [Ev_on_pre_merge acts n1 n2 expl] is emitted right before [n1]
+      and [n2] are merged with explanation [expl].  *)
+
+  val on_pre_merge2 :
+    t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
+  (** Second phase of "on pre merge". This runs after {!on_pre_merge}
+      and is used by Plugins. {b NOTE}: Plugin state might be observed as already
+      changed in these handlers. *)
+
+  val on_post_merge :
+    t -> (t * E_node.t * E_node.t, Handler_action.t list) Event.t
+  (** [ev_on_post_merge acts n1 n2] is emitted right after [n1]
+      and [n2] were merged. [find cc n1] and [find cc n2] will return
+      the same E_node.t. *)
+
+  val on_new_term : t -> (t * E_node.t * Term.t, Handler_action.t list) Event.t
+  (** [ev_on_new_term n t] is emitted whenever a new Term.t [t]
+      is added to the congruence closure. Its E_node.t is [n]. *)
+
+  type ev_on_conflict = { cc: t; th: bool; c: Lit.t list }
+  (** Event emitted when a conflict occurs in the CC.
+
+      [th] is true if the explanation for this conflict involves
+      at least one "theory" explanation; i.e. some of the equations
+      participating in the conflict are purely syntactic theories
+      like injectivity of constructors. *)
+
+  val on_conflict : t -> (ev_on_conflict, unit) Event.t
+  (** [ev_on_conflict {th; c}] is emitted when the congruence
+      closure triggers a conflict by asserting the tautology [c]. *)
+
+  val on_propagate :
+    t ->
+    ( t * Lit.t * (unit -> Lit.t list * Proof_term.step_id),
+      Handler_action.t list )
+    Event.t
+  (** [ev_on_propagate Lit.t reason] is emitted whenever [reason() => Lit.t]
+      is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
+
+  val on_is_subterm :
+    t -> (t * E_node.t * Term.t, Handler_action.t list) Event.t
+  (** [ev_on_is_subterm n t] is emitted when [n] is a subterm of
+      another E_node.t for the first time. [t] is the Term.t corresponding to
+      the E_node.t [n]. This can be useful for theory combination. *)
+
+  (** {3 Misc} *)
+
+  val n_true : t -> E_node.t
+  (** Node for [true] *)
+
+  val n_false : t -> E_node.t
+  (** Node for [false] *)
+
+  val n_bool : t -> bool -> E_node.t
+  (** Node for either true or false *)
+
+  val set_as_lit : t -> E_node.t -> Lit.t -> unit
+  (** map the given e_node to a literal. *)
+
+  val find_t : t -> Term.t -> repr
+  (** Current representative of the Term.t.
+      @raise E_node.t_found if the Term.t is not already {!add}-ed. *)
+
+  val add_iter : t -> Term.t Iter.t -> unit
+  (** Add a sequence of terms to the congruence closure *)
+
+  val all_classes : t -> repr Iter.t
+  (** All current classes. This is costly, only use if there is no other solution *)
+
+  val explain_eq : t -> E_node.t -> E_node.t -> Resolved_expl.t
+  (** Explain why the two nodes are equal.
+      Fails if they are not, in an unspecified way. *)
+
+  val explain_expl : t -> Expl.t -> Resolved_expl.t
+  (** Transform explanation into an actionable conflict clause *)
+
+  (* FIXME: remove
+        val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
+        (** Raise a conflict with the given explanation.
+            It must be a theory tautology that [expl ==> absurd].
+            To be used in theories.
+
+            This fails in an unspecified way if the explanation, once resolved,
+            satisfies {!Resolved_expl.is_semantic}. *)
+  *)
+
+  val merge : t -> E_node.t -> E_node.t -> Expl.t -> unit
+  (** Merge these two nodes given this explanation.
+         It must be a theory tautology that [expl ==> n1 = n2].
+         To be used in theories. *)
+
+  val merge_t : t -> Term.t -> Term.t -> Expl.t -> unit
+  (** Shortcut for adding + merging *)
+
+  (** {3 Main API *)
+
+  val assert_eq : t -> Term.t -> Term.t -> Expl.t -> unit
+  (** Assert that two terms are equal, using the given explanation. *)
+
+  val assert_lit : t -> Lit.t -> unit
+  (** Given a literal, assume it in the congruence closure and propagate
+      its consequences. Will be backtracked.
+
+      Useful for the theory combination or the SAT solver's functor *)
+
+  val assert_lits : t -> Lit.t Iter.t -> unit
+  (** Addition of many literals *)
+
+  val check : t -> Result_action.or_conflict
+  (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
+      Will use the {!actions} to propagate literals, declare conflicts, etc. *)
+
+  val push_level : t -> unit
+  (** Push backtracking level *)
+
+  val pop_levels : t -> int -> unit
+  (** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
+
+  val get_model : t -> E_node.t Iter.t Iter.t
+  (** get all the equivalence classes so they can be merged in the model *)
+
+  val create :
+    ?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
+  (** Create a new congruence closure.
+
+      @param term_store used to be able to create new terms. All terms
+      interacting with this congruence closure must belong in this term state
+      as well.
+  *)
+
+  (**/**)
+
+  module Debug_ : sig
+    val pp : t Fmt.printer
+    (** Print the whole CC *)
+  end
+
+  (**/**)
+end
+
+(* TODO: full EGG, also have a function to update the value when
+   the subterms (produced in [of_term]) are updated *)
+
+(** Data attached to the congruence closure classes.
+
+    This helps theories keeping track of some state for each class.
+    The state of a class is the monoidal combination of the state for each
+    Term.t in the class (for example, the set of terms in the
+    class whose head symbol is a datatype constructor). *)
+module type MONOID_PLUGIN_ARG = sig
+  module CC : S
+
+  type t
+  (** Some type with a monoid structure *)
+
+  include Sidekick_sigs.PRINT with type t := t
+
+  val name : string
+  (** name of the monoid structure (short) *)
+
+  (* FIXME: for subs, return list of e_nodes, and assume of_term already
+     returned data for them. *)
+  val of_term :
+    CC.t -> CC.E_node.t -> Term.t -> t option * (CC.E_node.t * t) list
+  (** [of_term n t], where [t] is the Term.t annotating node [n],
+      must return [maybe_m, l], where:
+
+      - [maybe_m = Some m] if [t] has monoid value [m];
+        otherwise [maybe_m=None]
+      - [l] is a list of [(u, m_u)] where each [u]'s Term.t
+        is a direct subterm of [t]
+        and [m_u] is the monoid value attached to [u].
+
+      *)
+
+  val merge :
+    CC.t ->
+    CC.E_node.t ->
+    t ->
+    CC.E_node.t ->
+    t ->
+    CC.Expl.t ->
+    (t * CC.Handler_action.t list, CC.Handler_action.conflict) result
+  (** Monoidal combination of two values.
+
+      [merge cc n1 mon1 n2 mon2 expl] returns the result of merging
+      monoid values [mon1] (for class [n1]) and [mon2] (for class [n2])
+      when [n1] and [n2] are merged with explanation [expl].
+
+      @return [Ok mon] if the merge is acceptable, annotating the class of [n1 ∪ n2];
+      or [Error expl'] if the merge is unsatisfiable. [expl'] can then be
+      used to trigger a conflict and undo the merge.
+    *)
+end
+
+(** Stateful plugin holding a per-equivalence-class monoid.
+
+    Helps keep track of monoid state per equivalence class.
+    A theory might use one or more instance(s) of this to
+    aggregate some theory-specific state over all terms, with
+    the information of what terms are already known to be equal
+    potentially saving work for the theory. *)
+module type DYN_MONOID_PLUGIN = sig
+  module M : MONOID_PLUGIN_ARG
+  include Sidekick_sigs.DYN_BACKTRACKABLE
+
+  val pp : unit Fmt.printer
+
+  val mem : M.CC.E_node.t -> bool
+  (** Does the CC E_node.t have a monoid value? *)
+
+  val get : M.CC.E_node.t -> M.t option
+  (** Get monoid value for this CC E_node.t, if any *)
+
+  val iter_all : (M.CC.repr * M.t) Iter.t
+end
+
+(** Builder for a plugin.
+
+    The builder takes a congruence closure, and instantiate the
+    plugin on it. *)
+module type MONOID_PLUGIN_BUILDER = sig
+  module M : MONOID_PLUGIN_ARG
+
+  module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M
+
+  type t = (module DYN_PL_FOR_M)
+
+  val create_and_setup : ?size:int -> M.CC.t -> t
+  (** Create a new monoid state *)
+end

src/cc/view.ml

@@ -0,0 +1,38 @@
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't
+(* do not enter *)
+
+let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
+  match v with
+  | Bool b -> Bool b
+  | App_fun (f, args) -> App_fun (f_f f, f_ts args)
+  | App_ho (f, a) -> App_ho (f_t f, f_t a)
+  | Not t -> Not (f_t t)
+  | If (a, b, c) -> If (f_t a, f_t b, f_t c)
+  | Eq (a, b) -> Eq (f_t a, f_t b)
+  | Opaque t -> Opaque (f_t t)
+
+let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
+  match v with
+  | Bool _ -> ()
+  | App_fun (f, args) ->
+    f_f f;
+    f_ts args
+  | App_ho (f, a) ->
+    f_t f;
+    f_t a
+  | Not t -> f_t t
+  | If (a, b, c) ->
+    f_t a;
+    f_t b;
+    f_t c
+  | Eq (a, b) ->
+    f_t a;
+    f_t b
+  | Opaque t -> f_t t

src/cc/view.mli

@@ -0,0 +1,33 @@
+(** View terms through the lens of the Congruence Closure *)
+
+(** A view of a term fron the point of view of the congruence closure.
+
+      - ['f] is the type of function symbols
+      - ['t] is the type of terms
+      - ['ts] is the type of sequences of terms (arguments of function application)
+  *)
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't  (** do not enter *)
+
+val map_view :
+  f_f:('a -> 'b) ->
+  f_t:('c -> 'd) ->
+  f_ts:('e -> 'f) ->
+  ('a, 'c, 'e) t ->
+  ('b, 'd, 'f) t
+(** Map function over a view, one level deep.
+    Each function maps over a different type, e.g. [f_t] maps over terms *)
+
+val iter_view :
+  f_f:('a -> unit) ->
+  f_t:('b -> unit) ->
+  f_ts:('c -> unit) ->
+  ('a, 'b, 'c) t ->
+  unit
+(** Iterate over a view, one level deep. *)