A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
Sidekick is an OCaml framework to implement and use SMT solvers based on CDCL.
It is heavily functorized (parametrized) so it can use user-provided data structures, term representation, etc. and each part is potentially swappable, even the SAT solver.
Sidekick is composed of a few libraries:
sidekick contains the core type definitions, a congruence closure,
some theories (boolean formuals, algebraic datatypes),
and a solver implementation based on mSAT.
Sidekick_core is the most important module to read there.
sidekick-base provides a concrete implementation of terms, types,
literals, etc. as well as an instantiation the SMT solver.
It also depends on Zarith
for arbitrary-precision computations.sidekick-bin is an executable that uses the previous building blocks
to implement a concrete SMT solver executable. It is useful for testing, but
can also be used as a normal SMT solver on the command line.
It contains examples of how to instantiate the functors of sidekick
and sidekick-base.