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
sat smt
Documentation github.com Edit opam file
Published
15 Jan 2019
Authors
Maintainers
Sources
msat-0.7.tar.gz
md5=c921093f88fcf2cfe2e9a4787ffb24f3 sha512=3b8fb33996840dfbe56943a57c4c8cb5ad4684af89a0e67c3e9f10fdde9a4a508069e082f9489d058b30d3d345718bab190f9d55fe2d06d91eafa9296a0b1e30
Dependencies
dolmen with-test & >= "0.4" & < "0.5"
ocamlbuild build
ocamlfind build
ocaml >= "4.00.1" & < "5.0.0"
Reverse Dependencies
archsat
smbc >= "0.4" & < "0.6"
zipperposition >= "1.1" & < "1.5.1"