msatversion
A library to create SAT/SMT/McSat solvers
mSAT is a library intended to make creating new SMT/McSat solvers easier.
mSAT implements a SAT solver core functorized over a theory. It thus provides functors that take an arbitrary theory (either for SMT or McSat), and returns a functionning SMT or McSat solver.
mSAT solvers support arbitrarily nested local assumptions. Solvers created using mSAT functors can additionally provide formal proofs whenever the solver answers UNSAT on a problem.
| Tags | sat smt |
|---|---|
| Authors | Sylvain Conchon, Alain Mebsout, Stephane Lecuyer, Simon Cruanes and Guillaume Bury |
| License | Apache-1.0+ |
| Published | |
| Homepage | https://github.com/Gbury/mSAT |
| Issue Tracker | https://github.com/Gbury/mSAT/issues/ |
| Maintainers | guillaume.bury@gmail.com and simon.cruanes@inria.fr |
| Dependencies |
|
| Source [http] | https://github.com/ocaml/opam-source-archives/raw/main/msat-0.7.tar.gz md5=c921093f88fcf2cfe2e9a4787ffb24f3 sha512=3b8fb33996840dfbe56943a57c4c8cb5ad4684af89a0e67c3e9f10fdde9a4a508069e082f9489d058b30d3d345718bab190f9d55fe2d06d91eafa9296a0b1e30 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/msat/msat.0.7/opam |
Required by
- archsat
- hardcaml-lua
- smbc>=0.4 & <0.6
- zipperposition>=1.1 & <1.5.1
Optionally used by
