feat(core/cc): expose more from the congruence closure

src/cc/Sidekick_cc.ml

@@ -558,6 +558,8 @@ module Make (A: CC_ARG)
 
   let[@inline] add_term cc t : node = add_term_rec_ cc t
 
+  let mem_term = mem
+
   let set_as_lit cc (n:node) (lit:lit) : unit =
     match n.n_as_lit with
     | Some _ -> ()

src/core/Sidekick_core.ml

@@ -216,6 +216,9 @@ module type CC_S = sig
   (** Add the term to the congruence closure, if not present already.
       Will be backtracked. *)
 
+  val mem_term : t -> term -> bool
+  (** Returns [true] if the term is explicitly present in the congruence closure *)
+
   type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit
   type ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
   type ev_on_new_term = t -> N.t -> term -> unit
@@ -458,6 +461,10 @@ module type SOLVER_INTERNAL = sig
   (** Add/retrieve congruence closure node for this term.
       To be used in theories *)
 
+  val cc_mem_term : t -> term -> bool
+  (** Return [true] if the term is explicitly in the congruence closure.
+      To be used in theories *)
+
   val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
   (** Callback for when two classes containing data for this key are merged (called before) *)
 

src/msat-solver/Sidekick_msat_solver.ml

@@ -282,6 +282,7 @@ module Make(A : ARG)
     let on_cc_propagate self f = CC.on_propagate (cc self) f
 
     let cc_add_term self t = CC.add_term (cc self) t
+    let cc_mem_term self t = CC.mem_term (cc self) t
     let cc_find self n = CC.find (cc self) n
     let cc_are_equal self t1 t2 =
       let n1 = cc_add_term self t1 in