From 1ecb189fd5cdbe0854955a9c525c29bc55289cb7 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 30 Jul 2022 21:17:20 -0400
Subject: [PATCH] refactor: core and CC

---
 src/cc/CC.ml                  |  3 +++
 src/cc/CC.mli                 | 16 ++++++++++++++++
 src/cc/dune                   |  2 +-
 src/core-logic/t_builtins.ml  |  6 ++++++
 src/core-logic/t_builtins.mli |  1 +
 src/core/Sidekick_core.ml     |  2 ++
 6 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/src/cc/CC.ml b/src/cc/CC.ml
index ba2214be..a9192ccf 100644
--- a/src/cc/CC.ml
+++ b/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
diff --git a/src/cc/CC.mli b/src/cc/CC.mli
index 117a56e2..9107db9e 100644
--- a/src/cc/CC.mli
+++ b/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
diff --git a/src/cc/dune b/src/cc/dune
index 5994f7ba..cd929144 100644
--- a/src/cc/dune
+++ b/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))
diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml
index 3b83a4f7..3bc09bd0 100644
--- a/src/core-logic/t_builtins.ml
+++ b/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
diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli
index 9f090b58..8ae490ee 100644
--- a/src/core-logic/t_builtins.mli
+++ b/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] *)
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 8e78ae4c..204c1174 100644
--- a/src/core/Sidekick_core.ml
+++ 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