Inter-theory Dependency Analysis for SMT String Solvers
summary
Introduces a concrete analysis called solved form distance that measures how many case splits are needed to break string/integer coupling, plus decision witness traces to replay local solves globally; implements the technique inside Z3 and prioritizes equations via a variable priority map. Evaluation on JavaScript and Python symbolic‑execution benchmarks shows real gains: about 8× faster on SAT JS sets, >3× on UNSAT, and over 10× speedups on Python SATs while also solving more UNSAT instances.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:22Inter-theory Dependency
- 2:17Main Challenges
- 5:15Solved Form Distance
- 7:03Partial Order for String Equations
- 8:23Decision Witness
- 9:21Implementing the Partial Order
- 10:34Implementing a Branching Decision
- 11:14Experiment (with JavaScript benchmarks)
- 12:24Experiment (with Python benchmarks)
- 13:35Concluding Remarks
related talks
35mA Peek Inside SAT Solvers
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
30mAnalyzing Programs with SMT Solvers
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
35mThe Mastermind behind Refinement Types
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
13mProgram Analysis via Efficient Symbolic Abstraction