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.