SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving

DOI10.1007/978-3-319-24318-4_26zbMath1471.68241OpenAlexW2277676404MaRDI QIDQ3453240

Gereon Kremer, Florian Corzilius, Erika Ábrahám, Sebastian Junges, Stefan Schupp

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_26

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Satisfiability Checking: Theory and Applications ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Experiments with automated reasoning in the class ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ \textsf{PFL}: a probabilistic logic for fault trees ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Fully incremental cylindrical algebraic decomposition ⋮ SMT-RAT ⋮ Efficient Simplification Techniques for Special Real Quantifier Elimination with Applications to the Synthesis of Optimal Numerical Algorithms ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}

Uses Software

• CoCoALib
• gmp
• MetiTarski
• MiniSat
• GiNaC
• z3
• Orbital library
• CLN
• AProVE
• OpenSMT
• CVC4
• MathSAT5
• CArL
• GitHub
• iSAT
• PROPhESY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quantifier elimination for real algebra -- the quadratic case and beyond
• MetiTarski: An automatic theorem prover for real-valued special functions
• The complexity of linear problems in fields
• Simplification of quantifier-free formulae over ordered fields
• Introduction to the GiNaC framework for symbolic computation within the \(\text{C}^{++}\) programming language
• On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers
• Solving Non-linear Arithmetic
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Virtual Substitution for SMT-Solving
• On the Theoretical and Practical Complexity of the Existential Theory of Reals
• Proving Termination of Programs Automatically with AProVE
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• The Strategy Challenge in SMT Solving
• A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
• Real World Verification
• Theory and Applications of Satisfiability Testing
• The MathSAT5 SMT Solver
• CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
• Algorithms in real algebraic geometry