“Smt-Switch: A Solver-Agnostic C++ API for SMT Solving” by Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, and Clark Barrett. In Proceedings of the 24^th International Conference on Theory and Applications of Satisfiability Testing (SAT '21), (Chu-Min Li and Felip Manyà, eds.), July 2021, pp. 377-386. Barcelona, Spain.
This paper presents Smt-Switch, an open-source, solver-agnostic API for SMT solving. Smt-Switch provides simple, uniform, and high-performance access to SMT solving for applications in areas such as automated reasoning, planning, and formal verification. It defines an abstract interface, which can be implemented by different SMT solvers. The interface allows the user to create, traverse, and manipulate terms, as well as dynamically dispatch queries to various underlying SMT solvers.
BibTeX entry:
@inproceedings{MWZ+21,
author = {Makai Mann and Amalee Wilson and Yoni Zohar and Lindsey
Stuntz and Ahmed Irfan and Kristopher Brown and Caleb Donovick and
Allison Guman and Cesare Tinelli and Clark Barrett},
editor = {Chu-Min Li and Felip Many{\`a}},
title = {Smt-Switch: A Solver-Agnostic {C}++ {API} for {SMT} Solving},
booktitle = {Proceedings of the {\it 24^{th}} International Conference
on Theory and Applications of Satisfiability Testing (SAT '21)},
series = {Lecture Notes in Computer Science},
volume = {12831},
pages = {377--386},
publisher = {Springer},
month = jul,
year = {2021},
doi = {10.1007/978-3-030-80223-3_26},
note = {Barcelona, Spain},
url = {http://theory.stanford.edu/~barrett/pubs/MWZ+21.pdf}
}
(This webpage was created with bibtex2web.)