From 0902777527b9bc59e03207456b27ce6d64aaad99 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 19 Sep 2021 13:03:44 -0400
Subject: [PATCH] feat(core): provide `mk_eqn` in CC

---
 src/base-solver/sidekick_base_solver.ml | 1 +
 src/core/Sidekick_core.ml               | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 5d6fe2e8..c0e567bf 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/src/base-solver/sidekick_base_solver.ml
@@ -13,6 +13,7 @@ module Solver_arg = struct
   module Lit = Sidekick_base.Lit
 
   let cc_view = Term.cc_view
+  let mk_eqn = Term.eq
   let is_valid_literal _ = true
   module P = Proof_stub
   type proof = P.t
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 4bd1e85c..0e8e73e1 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -336,6 +336,8 @@ module type CC_ARG = sig
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
   (** View the term through the lens of the congruence closure *)
+
+  val mk_eqn : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t
 end
 
 (** Main congruence closure signature.