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]

• metaSMT Version 3, from November 2011
  metaSMT-3.tar.gz (source)
• metaSMT Version 2, from June 2011
  metaSMT-2.tar.gz (source)
• metaSMT Version 1, from June 2011
  metaSMT-1.tar.gz (source)

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

• [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

Users of metaSMT

• metaSMT is used for constraint random verification of SystemC models. For more details see www.systemc-verification.org
• metaSMT is used by the Software Reliability Group at Imperial College London for symbolic execution supporting multiple SMT solvers. For more details see KLEE-MultiSolver.