Constraint Solvers for the Working PL Researcher
summary
Demonstrates using Z3 Python bindings to build a small toolchain that does constraint-based declarative execution, verification, and synthesis. Encodes array partitioning into SMT: integer size variables, pairwise |si−sj| ≤ 1 and sum(si)=n, then verifies universally by making n symbolic and finding counterexamples (n=0, n=12 for wrong candidates). Uses CEGIS loop where a synthesizer picks a control C and verifier yields counterexamples, converging to k = n mod p, which verifies for all n.
AI-written summary · about