| ||||
| ||||
![]() Title:Rewrites for SMT Solvers using Syntax-Guided Enumeration Authors:Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Noetzli, Mathias Preiner, Clark Barrett and Cesare Tinelli Conference:SMT 2018 Tags:Rewrite Rules, SMT and Syntax-Guided Synthesis Abstract: In this paper, we explore a development paradigm where rewrite rules are suggested to the SMT solver 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 in applications. Rewrites for SMT Solvers using Syntax-Guided Enumeration ![]() Rewrites for SMT Solvers using Syntax-Guided Enumeration | ||||
Copyright © 2002 – 2025 EasyChair |