Scaling up DPLL(T) string solvers using context-dependent simplification

DOI10.1007/978-3-319-63390-9_24zbMath1494.68255OpenAlexW2736027423MaRDI QIDQ2164248

Andrew Reynolds, Tianyi Liang, Cesare Tinelli, Clark Barrett, David Brumley, Maverick Woo

Publication date: 12 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-319-63390-9_24

Mathematics Subject Classification ID

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

Related Items (8)

Reasoning about vectors: satisfiability modulo a theory of sequences ⋮ Word equations in synergy with regular constraints ⋮ Chain-Free String Constraints ⋮ Unnamed Item ⋮ A decision procedure for string to code point conversion ⋮ Subsumption demodulation in first-order theorem proving ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Reasoning about vectors using an SMT theory of sequences

This page was built for publication: Scaling up DPLL(T) string solvers using context-dependent simplification