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
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


Files produced by the author(s)



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⟩



Record views


Files downloads