Skip to Main content Skip to Navigation
Conference papers

Quantifier Simplification by Unification in SMT

Pascal Fontaine 1, 2, 3 Hans-Jörg Schurr 1, 2 
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Quantifier reasoning in SMT solvers relies on instantiation: ground instances are generated heuristically from the quantified formulas until a contradiction is reached at the ground level. Current instantiation heuristics, however, often fail in presence of nested quantifiers. To address this issue we introduce a unification-based method that augments the problem with shallow quantified formulas obtained from assertions with nested quantifiers. These new formulas help unlocking the regular instantiation techniques, but parsimony is necessary since they might also be misguiding. To mitigate this, we identify some effective restricting conditions. The method is implemented in the veriT solver, and tested on benchmarks from the SMT-LIB. It allows the solver to prove more formulas, faster.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03341368
Contributor : Hans-Jörg Schurr Connect in order to contact the contributor
Submitted on : Friday, September 10, 2021 - 4:54:09 PM
Last modification on : Thursday, May 5, 2022 - 10:19:16 AM

File

frocos2021.pdf
Files produced by the author(s)

Identifiers

Citation

Pascal Fontaine, Hans-Jörg Schurr. Quantifier Simplification by Unification in SMT. FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.232-249, ⟨10.1007/978-3-030-86205-3_13⟩. ⟨hal-03341368⟩

Share

Metrics

Record views

48

Files downloads

98