Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. metaSMT: focus on your application and not on solver integration
 
research article

metaSMT: focus on your application and not on solver integration

Riener, Heinz  
•
Haedicke, Finn
•
Frehse, Stefan
Show more
2017
International Journal on Software Tools For Technology Transfer

Many applications from artificial intelligence and formal methods use decision procedures as their core solving engines. In this context, automated reasoning based on Satisfiability (SAT) or Satisfiability Modulo Theories (SMT) is very effective. For a given application, however, selecting the best reasoning engine is a daunting task requiring first-hand experience and insight into engine-specific implementation details. Developers have to decide which concrete engine to use and how to integrate the engine into an application. Although file formats, e.g., DIMACS CNF or SMT-LIB, standardize the input of SAT and SMT solvers, not all engines provide input interfaces compliant with these standards. When following the standard, advanced (and not standardized) features of the solvers remain unused and their integration is left to the users. This work presents 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.

  • Details
  • Metrics
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés