Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
From MaRDI portal
Publication:2104500
DOI10.1007/978-3-031-10769-6_7OpenAlexW4289104052MaRDI QIDQ2104500
Andrew Reynolds, Clark Barrett, Cesare Tinelli, Gereon Kremer
Publication date: 7 December 2022
Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_7
abstraction refinementsatisfiability modulo theoriesnonlinear real arithmeticcylindrical algebraic coverings
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Solving systems of polynomial inequalities in subexponential time
- Real quantifier elimination is doubly exponential
- Designing theory solvers with extensions
- Subtropical satisfiability
- Validity proof of Lazard's method for CAD construction
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Fully incremental cylindrical algebraic decomposition
- raSAT: An SMT Solver for Polynomial Constraints
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Virtual Substitution for SMT-Solving
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Solving SAT and SAT Modulo Theories
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- On the combinatorial and algebraic complexity of quantifier elimination
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Planning for Hybrid Systems via Satisfiability Modulo Theories
- The MathSAT5 SMT Solver
