Is solver guidance redundant for strong SMT implementations?
An exploration of domain-specific vs general improvements applied to Z3's string theories
O. Machairas (TU Delft - Electrical Engineering, Mathematics and Computer Science)
D.G. Sprokholt – Graduation committee member (TU Delft - Programming Languages)
S.S. Chakraborty – Graduation committee member (TU Delft - Programming Languages)
A.E. Zaidman – Graduation committee member (TU Delft - Software Technology)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
The Z3 SMT solver, a type of satisfiability solver used both in research and in industry, can give better performance by either improving the underlying
implementation or using domain-specific guidance. We present a way to simulate domain-specific help automatically by reducing the search space based on the model solution, and we use it to compare two implementations of Z3′s string solver – Z3str3 (weaker) and Z3-Noodler (stronger) – with and without domain-specific help. We find that Z3-Noodler sees significantly less improvement than Z3str3 because 1) the additional “helping” constraints are in fact occasionally counterproductive and 2) Z3-Noodler solves equivalent problems much faster than Z3str3, so the relative overhead of the additional constraints is more noticed.