|
Home « Service « Software
metaSMT - A Domain Specific Embedded Language for SMT programming
Abstract
metaSMT provides an easy to use Domain Specific Embedded
Language (DSEL) for C++ similar to SMT-LIB. Various
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
Features
- Theories and Logics:
- Simple Boolean expressions over Boolean predicates
- Closed quantifier-free formulas over the theory of fixed-size bitvectors (QF_BV)
- Closed quantifier-free formulas over the theory of bitvectors and bitvector 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:
Boolector,
Z3,
STP
SWORD
- Supported SAT solvers:
MiniSAT (API),
PicoSAT (API),
Glucoser (CNF files),
PrecoSAT (CNF files),
Plingeling (CNF files)
- Other: CUDD, Aiger
Download [Changes]
Development
Since June 2012 the metaSMT project is developed at GitHub: metaSMT GitHub project.
License
metaSMT is published under MIT license as contained in the source archive.
Contact
Please contact us in case of questions and/or problems at metaSMT@informatik.uni-bremen.de.
References
Users of metaSMT
|
|
|
metaSMT-3.tar.gz (source)
Download Paper
