mReason
A solver-agnostic API for incremental machine reasoning
mReason is a generic C++ API that provides an abstraction layer for SMT (Satisfiability Modulo Theories) solving. It enables developers to work with multiple SMT solvers through a unified interface using three primary abstract base classes: AbsSolver, AbsSort, and AbsTerm.
The library supports multiple backends including Boolector, CVC4, MathSAT, and Yices2. It follows the SMT-LIB naming standard and includes a logging solver wrapper for term DAG tracking, Python bindings via Cython, and a term translator for moving terms between solver instances.
This project was developed as a final thesis at Eindhoven University of Technology in cooperation with Siemens. You can read the full thesis here.