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.
- 15 Jan 2019
with-test & >= "0.4" & < "0.5"
>= "4.00.1" & < "5.0.0"