metaSMT - An Embedded Domain Specific Language for SMT
metaSMT provides an easy to use Embedded Domain Specific
Language (EDSL) for C++ similar to SMT-LIB
Satisfiability (SAT) and SAT Modulo Theories (SMT) solvers can
be used directly over their API through the language. The main
advantages of metaSMT are:
- Engine independence through efficient abstraction layers
- Simplified development of algorithms based on formal methods
- Extensibility in terms of input language and reasoning engines
- Customizability in terms of optimization and infrastructure
- Translation of the input language into native engine calls at compile time
- Theories and logics:
- Simple Boolean expressions over Boolean predicates
- Closed quantifier-free formulas over the theory of fixed-size bit-vectors (QF_BV)
- Closed quantifier-free formulas over the theory of bit-vectors and bit-vector arrays (QF_ABV)
- Assertion management:
- Stack with push and pop (as in SMT-LIB 2.0)
- Groups of assertions (creation, deletion)
- Assumptions (valid during one SAT call)
- Supported SMT solvers:
- Supported SAT solvers:
Glucose (CNF files),
PrecoSAT (CNF files),
Plingeling (CNF files)
- Other: CUDD, Aiger
- metaSMT Version 3, from November 2011
- metaSMT Version 2, from June 2011
- metaSMT Version 1, from June 2011
Since June 2012 the metaSMT project is developed on GitHub: metaSMT GitHub project
Dependency scripts are available on GitHub (dependencies GitHub
metaSMT is published under MIT license as contained in the source archive.
Please contact Rolf Drechsler in case of questions and/or problems at firstname.lastname@example.org
Users of metaSMT
- [RHF+:2016] Heinz Riener, Finn Haedicke, Stefan Frehse, Mathias Soeken, Daniel Große, Rolf Drechsler, Görschwin Fey: "metaSMT: Focus On Your
Application And Not On Solver Integration", International Journal of
Software Tools for Technology Transfer (STTT), 2016. DOI10.1007/s10009-016-0426-1.
- [RSW+:2014] Heinz Riener, Mathias Soeken, Clemens Werther, Görschwin Fey, and Rolf Drechsler: "metaSMT: A Unified Interface to SMT-LIB2",
Forum on specification & Design Languages (FDL), 2014.
Download Paper | Download Slides |
- [RKD+:2014] Heinz Riener, Oliver Keszöcze, Rolf Drechsler, Görschwin Fey, "A Logic for Cardinality Constraints", 17. ITG/GMM/GI-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'14), Böblingen, Germany, 2014.
- [HFF+:2011] Finn Haedicke, Stefan Frehse, Görschwin Fey, Daniel Große, and Rolf Drechsler: "metaSMT: Focus On Your Application Not On Solver Integration",
First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS), 2011.
Download Paper | Download Slides
metaSMT is used in metaSMT-webifc,
a portfolio solver with a web-based input interface. A variety of
different decision procedures are provided which solve a given SMT
instance, optionally in parallel.
metaSMT is used for constraint random verification of SystemC
models. For more details see
metaSMT is used by the Software Reliability Group
at Imperial College London for symbolic execution
supporting multiple SMT solvers.