simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: mli for the SAT solver

Browse source
This commit is contained in:
Simon Cruanes 2021-07-18 22:27:54 -04:00
parent cab541e712
commit 923033f9bf
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/sat/Solver.mli Normal file
View file

@ -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