Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2021 | OriginalPaper | Chapter

Quantifier Simplification by Unification in SMT

Authors: Pascal Fontaine, Hans-Jörg Schurr

Published in: Frontiers of Combining Systems

Publisher: Springer International Publishing

share
SHARE

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.
Footnotes
1
The raw data is available on Zenodo [1].
 
2
Benchmarks known to be satisfiable can identify soundness problems. Hence, we included them in the experiments, but removed them from the data.
 
4
Using: -L smt2.6 --no-incremental --no-type-checking --no-interactive
--full-saturate-quant.
 
5
Using: -t 180s -m 6000 --mode portfolio --schedule smtcomp --input_syntax smtlib2 -om smtcomp -p off.
 
6
This has been confirmed to us by the Vampire team in conversations.
 
Literature
5.
go back to reference Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.​SMT-LIB.​org Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.​SMT-LIB.​org
Metadata
Title
Quantifier Simplification by Unification in SMT
Authors
Pascal Fontaine
Hans-Jörg Schurr
Copyright Year
2021
DOI
https://doi.org/10.1007/978-3-030-86205-3_13

Premium Partner