package msat

  1. Overview
  2. Docs

Description

This library provides functor to easily build a SAT, SMT and/or McSAT solver given an implementation of terms. Current features of the solver are:

  • proof output
  • push/pop operations
  • CNF transformation tools

This project derives from Alt-Ergo Zero, but does not provide any built-in theories, it is designed to let the users use their own implementation of terms and theories.

Tags

sat smt

Published: 29 Feb 2016

Dependencies (4)

  1. base-unix
  2. ocamlbuild build
  3. ocamlfind build
  4. ocaml >= "4.02.1" & < "5.0.0"

Dev Dependencies

None

Used by

None

Conflicts

None