simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 04:35:35 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
sidekick/index.md
Simon Cruanes fad57a7ee0 update index
2021-06-11 22:25:09 -04:00

1.3 KiB
Raw Blame History

Sidekick

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-arith depends on Zarith for arbitrary-precision computations, and provides a LRA theory based on an implementation of the Simplex algorithm.

  • sidekick-bin is an executable that uses the previous building blocks to implement a concrete SMT solver. 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-arith.

API Documentation