From 923033f9bfd17a8620890d746ec96fddcade7d00 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 18 Jul 2021 22:27:54 -0400
Subject: [PATCH] feat: mli for the SAT solver

---
 src/sat/Solver.mli | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 src/sat/Solver.mli

diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli
new file mode 100644
index 00000000..c6b8e28d
--- /dev/null
+++ b/src/sat/Solver.mli
@@ -0,0 +1,13 @@
+
+module type S = Solver_intf.S
+(** Safe external interface of solvers. *)
+
+module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
+  : S with module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = unit
+
+module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
+  : S with module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = Th.t