Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)

“Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)” by Gereon Kremer, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 11^th International Joint Conference on Automated Reasoning (IJCAR '22), (Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, eds.), Aug. 2022, pp. 95-105.

Abstract

The cvc5 SMT solver solves quantifier-free nonlinear real arithmetic problems by combining the cylindrical algebraic coverings method with incremental linearization in an abstraction-refinement loop. The result is a complete algebraic decision procedure that leverages efficient heuristics for refining candidate models. Furthermore, it can be used with quantifiers, integer variables, and in combination with other theories. We describe the overall framework, individual solving techniques, and a number of implementation details. We demonstrate its effectiveness with an evaluation on the SMT-LIB benchmarks.

BibTeX entry:

@inproceedings{KRB+22,
   author = {Gereon Kremer and Andrew Reynolds and Clark Barrett and
	Cesare Tinelli},
   editor = {Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson},
   title = {Cooperating Techniques for Solving Nonlinear Real Arithmetic
	in the cvc5 SMT Solver (System Description)},
   booktitle = {Proceedings of the {\it 11^{th}} International Joint
	Conference on Automated Reasoning (IJCAR '22)},
   series = {Lecture Notes in Computer Science},
   volume = {13385},
   pages = {95--105},
   publisher = {Springer Nature},
   month = aug,
   year = {2022},
   doi = {10.1007/978-3-031-10769-6_7},
   url = {http://theory.stanford.edu/~barrett/pubs/KRB+22.pdf}
}

(This webpage was created with bibtex2web.)