package msat

  1. Overview
  2. Docs
A library to create SAT/SMT/McSat solvers

Install

Dune Dependency

github.com Edit opam file Versions (16)

Authors

  1. S
    Sylvain Conchon
  2. A
    Alain Mebsout
  3. S
    Stephane Lecuyer
  4. S
    Simon Cruanes
  5. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com
  2. S
    simon.cruanes@inria.fr

Sources

msat-0.7.tar.gz
md5=c921093f88fcf2cfe2e9a4787ffb24f3
sha512=3b8fb33996840dfbe56943a57c4c8cb5ad4684af89a0e67c3e9f10fdde9a4a508069e082f9489d058b30d3d345718bab190f9d55fe2d06d91eafa9296a0b1e30

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.

Tags

sat smt

Published: 15 Jan 2019

Dependencies (3)

  1. ocamlbuild build
  2. ocamlfind build
  3. ocaml >= "4.00.1" & < "5.0.0"

Dev Dependencies (1)

  1. dolmen with-test & >= "0.4" & < "0.5"

Used by (3)

  1. archsat
  2. smbc >= "0.4" & < "0.6"
  3. zipperposition >= "1.1" & < "1.5.1"

Conflicts

None