feat(cc): expose more functions for N.t->literals

src/cc/Sidekick_cc.ml

@@ -306,7 +306,8 @@ module Make (A: CC_ARG)
 
   (* check if [t] is in the congruence closure.
      Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
-  let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
+  let[@inline] mem_term (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
+  let[@inline] find_n_of_term cc t : N.t option = T_tbl.get cc.tbl t
 
   (* print full state *)
   let pp_full out (cc:t) : unit =
@@ -501,7 +502,7 @@ module Make (A: CC_ARG)
 
   (* add [t] to [cc] when not present already *)
   and add_new_term_ cc (t:term) : node =
-    assert (not @@ mem cc t);
+    assert (not @@ mem_term cc t);
     Log.debugf 15 (fun k->k "(@[cc.add-term@ %a@])" Term.pp t);
     let n = N.make t in
     (* register sub-terms, add [t] to their parent list, and return the
@@ -564,7 +565,7 @@ module Make (A: CC_ARG)
 
   let[@inline] add_term cc t : node = add_term_rec_ cc t
 
-  let mem_term = mem
+  let mem_term = mem_term
 
   let set_as_lit cc (n:node) (lit:lit) : unit =
     match n.n_as_lit with
@@ -574,6 +575,14 @@ module Make (A: CC_ARG)
       on_backtrack cc (fun () -> n.n_as_lit <- None);
       n.n_as_lit <- Some lit
 
+  let[@inline] find_lit _self (n:node) : _ option = n.n_as_lit
+  let[@inline] has_lit self n = CCOpt.is_some (find_lit self n)
+
+  let has_lit_for_eqn self t u =
+    match find_n_of_term self (A.mk_eqn self.tst t u) with
+    | None -> false
+    | Some n -> has_lit self n
+
   (* is [n] true or false? *)
   let n_is_bool_value (self:t) n : bool =
     N.equal n (n_true self) || N.equal n (n_false self)

src/core/Sidekick_core.ml

@@ -578,6 +578,13 @@ module type CC_S = sig
   val set_as_lit : t -> N.t -> lit -> unit
   (** map the given node to a literal. *)
 
+  val find_lit : t -> N.t -> lit option
+
+  val has_lit : t -> N.t -> bool
+
+  val has_lit_for_eqn : t -> term -> term -> bool
+  (** Is there a literal for [t = u]? *)
+
   val find_t : t -> term -> repr
   (** Current representative of the term.
       @raise Not_found if the term is not already {!add}-ed. *)

src/smt-solver/Sidekick_smt_solver.ml

@@ -20,6 +20,8 @@ module type ARG = sig
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
 
+  val mk_eqn : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t
+
   val is_valid_literal : T.Term.t -> bool
   (** Is this a valid boolean literal? (e.g. is it a closed term, not inside
       a quantifier) *)
@@ -56,6 +58,7 @@ module Make(A : ARG)
     module Lit = Lit
     type nonrec proof = proof
     let cc_view = A.cc_view
+    let mk_eqn = A.mk_eqn
 
     module Actions = struct
       module T = T