HOME | CONTACT | Switch DE

Logo Universtity of Bremen
LOGO AGRA | AG Rechnerarchitektur



Group of Computer Architecture / AGRA | Computer Science | Faculty 03 | University of Bremen

metaSMT


metaSMT - An Embedded Domain Specific Language for SMT

Logo metaSMT
Abstract
metaSMT provides an easy to use Embedded Domain Specific Language (EDSL) 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 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: Boolector, Z3, STP SWORD
  • Supported SAT solvers: MiniSAT (API), PicoSAT (API), Glucose (CNF files), PrecoSAT (CNF files), Plingeling (CNF files)
  • Other: CUDD, Aiger
Download  [Changes]
Development
Since June 2012 the metaSMT project is developed on GitHub: metaSMT GitHub project. Dependency scripts are available on GitHub (dependencies GitHub), too.

License
metaSMT is published under MIT license as contained in the source archive.

Contact
Please contact Rolf Drechsler in case of questions and/or problems at drechsler@uni-bremen.de.

References
Users of metaSMT
  • 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 www.systemc-verification.org
  • metaSMT is used by the Software Reliability Group at Imperial College London for symbolic execution supporting multiple SMT solvers.


©2023 | Group of Computer Architecture | Contact | Legal & Data Privacy