refactor: core and CC

src/cc/CC.ml

@@ -969,3 +969,6 @@ module Default = struct
         | _ -> View.Opaque t)
   end)
 end
+
+let create (module A : ARG) ?stat ?size tst proof : t =
+  create_ ?stat ?size tst proof ~view_as_cc:A.view_as_cc

src/cc/CC.mli

@@ -1,3 +1,5 @@
+(** Main congruence closure type. *)
+
 open Sidekick_core
 
 type e_node = E_node.t
@@ -275,6 +277,20 @@ end
 module Make (_ : ARG) : BUILD
 module Default : BUILD
 
+val create :
+  (module ARG) ->
+  ?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

src/cc/dune

@@ -2,6 +2,6 @@
  (name Sidekick_cc)
  (public_name sidekick.cc)
  (synopsis "main congruence closure implementation")
- (private_modules types_ signature)
+ (private_modules signature)
  (libraries containers iter sidekick.sigs sidekick.core sidekick.util)
  (flags :standard -open Sidekick_util))

src/core-logic/t_builtins.ml

@@ -39,6 +39,12 @@ let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store)
 let true_ store = const store @@ Const.make C_true ops ~ty:(bool store)
 let false_ store = const store @@ Const.make C_false ops ~ty:(bool store)
 
+let bool_val store b =
+  if b then
+    true_ store
+  else
+    false_ store
+
 let c_eq store =
   let type_ = type_ store in
   let v = bvar_i store 0 ~ty:type_ in

src/core-logic/t_builtins.mli

@@ -11,6 +11,7 @@ val c_eq : store -> t
 val c_ite : store -> t
 val true_ : store -> t
 val false_ : store -> t
+val bool_val : store -> bool -> t
 
 val eq : store -> t -> t -> t
 (** [eq a b] is [a = b] *)

src/core/Sidekick_core.ml

@@ -32,3 +32,5 @@ module Proof_trace = Proof_trace
 module Proof_term = Proof_term
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
+
+exception Resource_exhausted