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.
17 commits 53 branches 1 tag 17 MiB
SMT 89.4%
OCaml 10.4%
Find a file
Simon Cruanes a1f46f4870 documentation
2014-10-29 14:25:29 +01:00
common initial commit 2014-03-06 10:45:04 +01:00
doc initial commit 2014-03-06 10:45:04 +01:00
smt modify build system 2014-10-29 14:18:00 +01:00
tests fix Tseitin CNF conversion; 2014-03-06 10:53:56 +01:00
.depend initial commit 2014-03-06 10:45:04 +01:00
.gitignore documentation 2014-10-29 14:25:29 +01:00
_tags modify build system 2014-10-29 14:18:00 +01:00
LICENSE update of license 2014-10-29 13:42:53 +01:00
Makefile documentation 2014-10-29 14:25:29 +01:00
META missing files now installed 2014-10-29 14:21:49 +01:00
msat.mlpack update build system 2014-10-29 13:56:13 +01:00
msat.odocl documentation 2014-10-29 14:25:29 +01:00
README.md updated README 2014-10-29 13:45:19 +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 COPYING.

INSTALLATION

============

You will need ocamlfind.