17.06.2016 | Regular Paper
metaSMT
: focus on your application and not on solver integration
Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2017
EinloggenAktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
metaSMT
, a framework that eases the integration of existing reasoning engines into applications. Inspired by SMT-LIB, metaSMT
provides a domain-specific language that allows for engine-independent programming and offers a generic interface to advanced features as an extra abstraction layer. State-of-the-art solvers for satisfiability and other theories are available via metaSMT
with little programming effort. Language bindings for C++ and Python are provided. We show how metaSMT
can be used as a portfolio consistency checker for SMT-LIB2 instances. The benchmark set of the category quantifier-free bit-vector theory from SMT-LIB (1.6 GB) is used for these experiments.