mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00

A modular library for CDCL(T) SMT solvers, with [wip] proof generation.

Find a file

Guillaume Bury 6a21dafb22 Added some tests.		2014-11-04 15:54:33 +01:00
common	remove Bitv and Heap from common, they are unused	2014-11-04 00:25:57 +01:00
docs	added minisat paper	2014-11-03 23:28:27 +01:00
sat	Merge branch 'master' of github.com:Gbury/mSAT	2014-11-04 00:18:45 +01:00
smt	Updated .merlin	2014-10-31 16:56:31 +01:00
tests	Added some tests.	2014-11-04 15:54:33 +01:00
util	New lexer/parser for dimacs format.	2014-11-04 15:41:25 +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
.ocp-indent	Everything has now been properly indented with ocp-indent.	2014-10-31 16:40:59 +01:00
_tags	in _tags, add more warnings and stronger inlining	2014-11-03 15:23:55 +01:00
LICENSE	update of license	2014-10-29 13:42:53 +01:00
Makefile	New lexer/parser for dimacs format.	2014-11-04 15:41:25 +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	updated opam file	2014-11-03 16:17:31 +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

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:

COPYRIGHT

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

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

make install