simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
sidekick/index.md
Simon Cruanes 744f8d60b8
update index
2021-08-27 09:49:42 -04:00

1.3 KiB
Raw Permalink 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-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.

API Documentation