Rewrites for SMT Solvers using Syntax-Guided Enumeration

Rewrites for SMT Solvers using Syntax-Guided Enumeration” by Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, and Cesare Tinelli. In Proceedings of the 16^th International Workshop on Satisfiability Modulo Theories (SMT '18), July 2018. Oxford, United Kingdom.

Abstract

In this paper, we explore a development paradigm for SMT solver developers where rewrite rules are suggested to the developer using syntax-guided enumeration. We capitalize on the recent advances in enumerative syntax-guided synthesis (SyGuS) techniques for efficiently enumerating terms in a grammar of interest, and novel sampling techniques for testing equivalence between terms. We present our preliminary experience with this feature in the SMT solver cvc4, showing its impact on its rewriting capabilities using several internal metrics, and its subsequent impact on solving bit-vector and string constraints.

BibTeX entry:

@inproceedings{RBN+18,
   author = {Andrew Reynolds and Haniel Barbosa and Aina Niemetz and
	Andres N{\"o}tzli and Mathias Preiner and Clark Barrett and Cesare
	Tinelli},
   title = {Rewrites for {SMT} Solvers using Syntax-Guided Enumeration},
   booktitle = {Proceedings of the {\it 16^{th}} International Workshop on
	Satisfiability Modulo Theories (SMT '18)},
   month = jul,
   year = {2018},
   note = {Oxford, United Kingdom},
   url = {http://theory.stanford.edu/~barrett/pubs/RBN+18.pdf}
}

(This webpage was created with bibtex2web.)