Homepage Sitemap Contact

Group
Reasearch
Studies
Publications
Software
Service
Contact




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

References
Users of metaSMT


Add to Favorites
Deutsch


Team





Sitemap Kontakt

ISMVL2014 DUHDE