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.