Home « Service « Software
metaSMT - An Embedded Domain Specific Language for SMT
, metaSMT's web-interface interface!
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
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 us in case of questions and/or problems at metaSMT@informatik.uni-bremen.de
Users of metaSMT
- [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.
- [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.