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

DOI10.1007/978-3-031-10769-6_7OpenAlexW4289104052MaRDI QIDQ2104500FDOQ2104500

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

Publication date: 7 December 2022

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

• dReal: an SMT solver for nonlinear theories over the reals
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• The MathSAT5 SMT solver
• Solving SAT and SAT Modulo Theories
• Solving non-linear arithmetic
• A Model-Constructing Satisfiability Calculus
• Title not available (Why is that?)
• Solving systems of polynomial inequalities in subexponential time
• On the combinatorial and algebraic complexity of quantifier elimination
• Real quantifier elimination is doubly exponential
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Validity proof of Lazard's method for CAD construction
• Title not available (Why is that?)
• A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
• Designing theory solvers with extensions
• Subtropical satisfiability
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Fully incremental cylindrical algebraic decomposition
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• raSAT: An SMT Solver for Polynomial Constraints
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Virtual substitution for SMT-solving
• Planning for Hybrid Systems via Satisfiability Modulo Theories

Cited In (1)

• CVC4

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)