“Syntax-Guided Quantifier Instantiation” by Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 27^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), (Jan Friso Groote and Kim Guldstrand Larsen, eds.), Mar. 2021, pp. 145-163. Nominated for the EATCS Best ETAPS Theory Paper Award.
This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.
BibTeX entry:
@inproceedings{NPR+21,
author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and
Clark Barrett and Cesare Tinelli},
editor = {Jan Friso Groote and Kim Guldstrand Larsen},
title = {Syntax-Guided Quantifier Instantiation},
booktitle = {Proceedings of the {\it 27^{th}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '21)},
series = {Lecture Notes in Computer Science},
volume = {12652},
pages = {145--163},
publisher = {Springer},
month = mar,
year = {2021},
doi = {10.1007/978-3-030-72013-1},
note = {{\em Nominated for the EATCS Best ETAPS Theory Paper Award}},
url = {http://theory.stanford.edu/~barrett/pubs/NPR+21.pdf}
}
(This webpage was created with bibtex2web.)