Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

DOI10.1007/978-3-031-10769-6_7MaRDI QIDQ2104500zbMATH OpenOpenAlexFDO

Authors Gereon Kremer, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-10769-6_7

zbMATH Keywords

abstraction refinementsatisfiability modulo theoriesnonlinear real arithmeticcylindrical algebraic coverings

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 589124 (Why is no real title available?)
• A model-constructing satisfiability calculus
• A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Designing theory solvers with extensions
• Fully incremental cylindrical algebraic decomposition
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• On the combinatorial and algebraic complexity of quantifier elimination
• Planning for hybrid systems via satisfiability modulo theories
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Real quantifier elimination is doubly exponential
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving non-linear arithmetic
• Solving systems of polynomial inequalities in subexponential time
• Subtropical satisfiability
• The MathSAT5 SMT solver
• Validity proof of Lazard's method for CAD construction
• Virtual substitution for SMT-solving
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• dReal: an SMT solver for nonlinear theories over the reals
• raSAT: An SMT Solver for Polynomial Constraints

Cited in

(1)

• CVC4

Describes a project that uses

Uses Software

• CoCoA
• CoCoALib
• REDLOG
• Yices
• z3
• libpoly
• dReal
• veriT
• MathSAT5
• SMT-RAT
• raSAT
• Zephyrus2

This page was built for publication: Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104500)