msat

A library to create SAT/SMT/McSat solvers
Description

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.

Install
Published
15 Jan 2019
Sources
msat-0.7.tar.gz
md5=c921093f88fcf2cfe2e9a4787ffb24f3
sha512=3b8fb33996840dfbe56943a57c4c8cb5ad4684af89a0e67c3e9f10fdde9a4a508069e082f9489d058b30d3d345718bab190f9d55fe2d06d91eafa9296a0b1e30
Dependencies
dolmen
with-test & >= "0.4" & < "0.5"
ocaml
>= "4.00.1"
Reverse Dependencies
smbc
>= "0.4" & < "0.6"
zipperposition
>= "1.1" & < "1.5.1"