×

SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. (English) Zbl 1471.68241

Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 360-368 (2015).
Summary: During the last decade, popular SMT solvers have been extended step-by-step with a wide range of decision procedures for different theories. Some SMT solvers also support the user-defined tuning and combination of such procedures, typically via command-line options. However, configuring solvers this way is a tedious task with restricted options.
In this paper we present our modular and extensible C++ library SMT-RAT, which offers numerous parameterized procedure modules for different logics. These modules can be configured and combined into an SMT solver using a comprehensible whilst powerful strategy, which can be specified via a graphical user interface. This makes it easier to construct a solver which is tuned for a specific set of problem instances. Compared to a previous version, we have extended our library with a number of new modules and support for parallelization in strategies. An additional contribution is our thread-safe and generic C++ library CArL, offering efficient data structures and basic operations for real arithmetic, which can be used for the fast implementation of new theory-solving procedures.
For the entire collection see [Zbl 1323.68009].

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abbott, J., Bigatti, A.M.: CoCoALib: a C++ library for computations in commutative algebra.. and beyond. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 73–76. Springer, Heidelberg (2010) · Zbl 1267.13048 · doi:10.1007/978-3-642-15582-6_15
[2] Akbarpour, B., Paulson, L.C.: Metitarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning 44(3), 175–205 (2010) · Zbl 1215.68206 · doi:10.1007/s10817-009-9149-2
[3] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011) · Zbl 05940712 · doi:10.1007/978-3-642-22110-1_14
[4] Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer (2010) · Zbl 1031.14028
[5] Bauer, C., Frink, A., Kreckel, R.: Introduction to the GiNaC framework for symbolic computation within the C++ programming language. Journal of Symbolic Computation 33(1), 1–12 (2002) · Zbl 1017.68163 · doi:10.1006/jsco.2001.0494
[6] Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010) · Zbl 05702237 · doi:10.1007/978-3-642-12002-2_12
[7] Chauhan, P., Goyal, D., Hasteer, G., Mathur, A., Sharma, N.: Non-cycle-accurate sequential equivalence checking. In: Proc. of DAC 2009, pp. 460–465. ACM Press (2009) · doi:10.1145/1629911.1630033
[8] Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013) · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[9] Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. In: Proc. of SMT 2012. EPiC Series, vol. 20, pp. 88–97. EasyChair (2013)
[10] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975) · doi:10.1007/3-540-07407-4_17
[11] Corzilius, F., Ábrahám, E.: Virtual substitution for SMT-solving. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 360–371. Springer, Heidelberg (2011) · Zbl 1342.68282 · doi:10.1007/978-3-642-22953-4_31
[12] Corzilius, F., Loup, U., Junges, S., Ábrahám, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442–448. Springer, Heidelberg (2012) · Zbl 06197774 · doi:10.1007/978-3-642-31612-8_35
[13] Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., Ábrahám, E.: PROPhESY: a PRObabilistic ParamEter SYthesis tool. In: Proc. of CAV 2015. LNCS, vol. 9207. Springer (2015) · Zbl 06845660 · doi:10.1007/978-3-319-21690-4_13
[14] Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulas over ordered fields. Journal of Symbolic Computation 24, 209–231 (1995) · Zbl 0882.03030 · doi:10.1006/jsco.1997.0123
[15] Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006) · Zbl 05187406 · doi:10.1007/11817963_11
[16] Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37
[17] Fränzle, M., et al.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3–4), 209–236 (2007) · Zbl 1144.68371
[18] Gao, S., Ganai, M.K., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: Proc. of FMCAD 2010, pp. 81–89. IEEE (2010)
[19] Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with \[ \mathsf AProVE \]
. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184–191. Springer, Heidelberg (2014) · Zbl 1409.68256 · doi:10.1007/978-3-319-08587-6_13
[20] Granlund, T.: the GMP development team: GNU MP: The GNU Multiple Precision Arithmetic Library. http://gmplib.org
[21] Haible, B., Kreckel, R.B.: CLN: Class Library for Numbers. http://www.ginac.de/CLN
[22] Heintz, J., Roy, M.F., Solerno, P.: On the theoretical and practical complexity of the existential theory of reals. The Computer Journal 36(5), 427–431 (1993) · Zbl 0780.68058 · doi:10.1093/comjnl/36.5.427
[23] Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Tech. Rep. 91–41, Research Institute for Symbolic Computation, Johannes Kepler University Linz (1991)
[24] Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27
[25] Junges, S., Loup, U., Corzilius, F., Ábrahám, E.: On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers. In: Muntean, T., Poulakis, D., Rolland, R. (eds.) CAI 2013. LNCS, vol. 8080, pp. 186–198. Springer, Heidelberg (2013) · Zbl 1398.68696 · doi:10.1007/978-3-642-40663-8_18
[26] Kremer, G., Corzilius, F., Junges, S., Schupp, S., Ábrahám, E.: CArL: Computer ARithmetic and Logic Library. https://github.com/smtrat/carl · Zbl 1471.68241
[27] Loup, U., Scheibler, K., Corzilius, F., Ábrahám, E., Becker, B.: A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 193–207. Springer, Heidelberg (2013) · Zbl 1381.68274 · doi:10.1007/978-3-642-38574-2_13
[28] de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[29] de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15–44. Springer, Heidelberg (2013) · Zbl 1383.68084 · doi:10.1007/978-3-642-36675-8_2
[30] Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 485–501. Springer, Heidelberg (2009) · Zbl 1250.68197 · doi:10.1007/978-3-642-02959-2_35
[31] Ravanbakhsh, H., Sankaranarayanan, S.: Counterexample guided synthesis of switched controllers for reach-while-stay properties. CoRR abs/1505.01180 (2015). http://arxiv.org/abs/1505.01180
[32] Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. In: Proc. of MBMV 2013, pp. 231–241. Institut für Angewandte Mikroelektronik und Datentechnik, Fakultät für Informatik und Elektrotechnik, Universität Rostock (2013)
[33] Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation 3, 141–224 (2007) · Zbl 1145.68501
[34] https://github.com/smtrat/smtrat/wiki
[35] Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376–392. Springer (1998) · Zbl 0900.03046 · doi:10.1007/978-3-7091-9459-1_20
[36] Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1–2), 3–27 (1988) · Zbl 0646.03005 · doi:10.1016/S0747-7171(88)80003-8
[37] Weispfenning, V.: Quantifier elimination for real algebra - the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997) · Zbl 0867.03003 · doi:10.1007/s002000050055
[38] Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481–500. Springer, Heidelberg (2010) · Zbl 1310.68126 · doi:10.1007/978-3-642-17511-4_27
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.