Rewrites for SMT Solvers using Syntax-Guided Enumeration


We explore a paradigm for SMT solver development where rewrite rules are suggested to solver developers using syntax-guided enumeration. We capitalize on recent advances in enumerative syntax-guided synthesis (SyGuS) techniques for efficiently enumerating terms in a grammar of interest, and on novel sampling techniques for testing equivalence between terms. We present our preliminary experience with this paradigm in the SMT solver CVC4. We show its impact on CVC4’s rewriting capabilities, and on solving constraints and SyGuS problems over bit-vectors and strings.

Proceedings of the 16th International Workshop on Satisfiability Modulo Theories, SMT 2018), affiliated with the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK, July 12-13, 2018