Portal de Periódicos da CAPES

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers

2019; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-24258-9_20

1611-3349

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, Cesare Tinelli,

Formal Methods in Verification

The performance of modern Satisfiability Modulo Theories (SMT) solvers relies crucially on efficient decision procedures as well as static simplification techniques, which include large sets of rewrite rules. Manually discovering and implementing rewrite rules is challenging. In this work, we propose a framework that uses enumerative syntax-guided synthesis (SyGuS) to propose rewrite rules that are not implemented in a given SMT solver. We implement this framework in cvc4, a state-of-the-art SMT and SyGuS solver, and evaluate several use cases. We show that some SMT solvers miss rewriting opportunities, or worse, have bugs in their rewriters. We also show that a variation of our approach can be used to test the correctness of a rewriter. Finally, we show that rewrites discovered with this technique lead to significant improvements in cvc4 on both SMT and SyGuS problems over bit-vectors and strings.