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
A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
82 commits 53 branches 1 tag 17 MiB
SMT 89.4%
OCaml 10.4%
Find a file
Exact
Simon Cruanes fad14a7e4f use Neperien for logging
2014-11-05 21:15:06 +01:00
bench Makefile for benchs. 2014-11-05 15:59:04 +01:00
docs added minisat paper 2014-11-03 23:28:27 +01:00
sat use Neperien for logging 2014-11-05 21:15:06 +01:00
smt Updated .merlin 2014-10-31 16:56:31 +01:00
tests main test program: move test.ml to sat_solve.ml 2014-11-04 20:40:08 +01:00
util use Neperien for logging 2014-11-05 21:15:06 +01:00
.depend initial commit 2014-03-06 10:45:04 +01:00
.gitignore Sat Solver is broken. 2014-11-01 02:12:17 +01:00
.header copyright header in .header; authors in opam file 2014-11-04 17:59:58 +01:00
.merlin use Neperien for logging 2014-11-05 21:15:06 +01:00
.ocp-indent Everything has now been properly indented with ocp-indent. 2014-10-31 16:40:59 +01:00
_tags use Neperien for logging 2014-11-05 21:15:06 +01:00
LICENSE update of license 2014-10-29 13:42:53 +01:00
Makefile main test program: move test.ml to sat_solve.ml 2014-11-04 20:40:08 +01:00
META missing files now installed 2014-10-29 14:21:49 +01:00
msat.mlpack Added a module to represent resolution proof (not tested yet) 2014-11-03 00:49:07 +01:00
msat.odocl Added a module to represent resolution proof (not tested yet) 2014-11-03 00:49:07 +01:00
opam copyright header in .header; authors in opam file 2014-11-04 17:59:58 +01:00
README.md small fix in README 2014-11-03 15:56:41 +01:00
TODO.md TODO update. 2014-11-01 20:20:53 +01:00

README.md

MSAT

MSAT is an OCaml library that features a modular SAT-solver and some extensions (including SMT). This is work in progress.

It derives from Alt-Ergo Zero.

The following theories should be supported:

  • Equality and uninterpreted functions
  • Arithmetic (linear, non-linear, integer, real)
  • Enumerated data-types

COPYRIGHT

This program is distributed under the Apache Software License version 2.0. See the enclosed file LICENSE.

INSTALLATION

Via opam

Once the package is on opam, just opam install msat. For the development version, use:

opam pin add msat https://github.com/Gbury/mSAT.git

Manual installation You will need ocamlfind. The command is:

make install