Smt-Switch: a solver-agnostic C++ API for SMT solving. (English) Zbl 07495586

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 377-386 (2021).
Summary: 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.
For the entire collection see [Zbl 1482.68030].


68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI


[1] Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical Report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org
[2] Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2021). www.SMT-LIB.org
[3] Barrett, C.; Gopalakrishnan, G.; Qadeer, S., CVC4, Computer Aided Verification, 171-177 (2011), Heidelberg: Springer, Heidelberg
[4] Behnel, S.; Bradshaw, R.; Citro, C.; Dalcin, L.; Seljebotn, DS; Smith, K., Cython: The best of both worlds, Comput. Sci. Eng., 13, 2, 31-39 (2011)
[5] Cimatti, A.; Griggio, A.; Schaafsma, BJ; Sebastiani, R.; Piterman, N.; Smolka, SA, The MathSAT5 SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 93-107 (2013), Heidelberg: Springer, Heidelberg · Zbl 1381.68153
[6] Dutertre, B.; Biere, A.; Bloem, R., Yices 2.2, Computer Aided Verification, 737-744 (2014), Cham: Springer, Cham
[7] Erkok, L.: SBV: SMT Based Verification in Haskell (2019). http://leventerkok.github.io/sbv/
[8] Free Software Foundation: bison (2021). https://www.gnu.org/software/bison/
[9] Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: Proceedings of the 13th International Workshop on Satisfiability Modulo Theories (SMT), pp. 373-384 (2015)
[10] Google: GoogleTest. https://github.com/google/googletest
[11] Horn, A.: Smt-kit: C++11 library for many sorted logics. http://ahorn.github.io/smt-kit/
[12] Ignatiev, A.; Morgado, A.; Marques-Silva, J.; Beyersdorff, O.; Wintersteiger, CM, PySAT: a python toolkit for prototyping with sat oracles, Theory and Applications of Satisfiability Testing - SAT 2018, 428-437 (2018), Cham: Springer, Cham · Zbl 1484.68215
[13] KitWare: CMake. https://cmake.org
[14] Krekel, H., Oliveira, B., Pfannschmidt, R., Bruynooghe, F., Laugher, B., Bruhin, F.: pytest 5.4.2 (2004). https://github.com/pytest-dev/pytest
[15] Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: CAV. Lecture Notes in Computer Science, Springer (2021)
[16] de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg
[17] Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621 (2020). https://arxiv.org/abs/2006.01621
[18] Niemetz, A.; Preiner, M.; Wolf, C.; Biere, A.; Chockler, H.; Weissenbacher, G., Btor2, BtorMC and Boolector 3.0, Computer Aided Verification, 587-595 (2018), Cham: Springer, Cham
[19] Riener, H., metaSMT: focus on your application and not on solver integration, Int. J. Softw. Tools Technol. Transf., 19, 5, 605-621 (2017)
[20] Vern Paxson: flex (2021). https://github.com/westes/flex
[21] Zohar, Y., Irfan, A., Mann, M., Nötzli, A., Reynolds, A., Barrett, C.: lazybv2int at the SMT Competition 2020. https://github.com/yoni206/lazybv2int (2020)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.