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
AuthorsSylvain Conchon, Alain Mebsout, Stephane Lecuyer, Simon Cruanes and Guillaume Bury
LicenseApache
Published
Homepagehttps://github.com/Gbury/mSAT
Issue Trackerhttps://github.com/Gbury/mSAT/issues/
Maintainersguillaume.bury@gmail.com and simon.cruanes@inria.fr
Dependencies
Source [http] https://github.com/Gbury/mSAT/archive/v0.7.tar.gz
md5=c921093f88fcf2cfe2e9a4787ffb24f3
sha512=3b8fb33996840dfbe56943a57c4c8cb5ad4684af89a0e67c3e9f10fdde9a4a508069e082f9489d058b30d3d345718bab190f9d55fe2d06d91eafa9296a0b1e30
StatisticsInstalled 14 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/msat/msat.0.7/opam
Required by
Optionally used by