Syntax-guided rewrite rule enumeration for SMT solvers

DOI10.1007/978-3-030-24258-9_20zbMath1441.68233OpenAlexW2953973768MaRDI QIDQ2181939

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

Publication date: 20 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-24258-9_20

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (5)

Approximate bit dependency analysis to identify program synthesis problems as infeasible ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ CVC4SY ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Scalable algorithms for abduction via enumerative syntax-guided synthesis

Uses Software

• Boolector
• SMT-LIB
• z3
• KLEE
• CVC4
• TRANSIT
• Z3str3
• StringFuzz
• OPTGEN

This page was built for publication: Syntax-guided rewrite rule enumeration for SMT solvers