Conference proceeding
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.95-105
Lecture Notes in Artificial Intelligence
01/01/2022
DOI: 10.1007/978-3-031-10769-6_7
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.
Details
- Title: Subtitle
- Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
- Creators
- Gereon Kremer - Stanford UniversityAndrew Reynolds - University of IowaClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Contributors
- J Blanchette (Editor)L Kovacs (Editor)D Pattinson (Editor)
- Resource Type
- Conference proceeding
- Publication Details
- AUTOMATED REASONING, IJCAR 2022, Vol.13385, pp.95-105
- Series
- Lecture Notes in Artificial Intelligence
- DOI
- 10.1007/978-3-031-10769-6_7
- ISSN
- 0302-9743
- eISSN
- 1611-3349
- Publisher
- Springer Nature
- Number of pages
- 11
- Language
- English
- Date published
- 01/01/2022
- Academic Unit
- Computer Science
- Record Identifier
- 9984410849302771
Metrics
25 Record Views