Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories.
Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice.
However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences.
Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions.
Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT.
To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories.
The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space.
By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs.
For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior.
We implement this methodology in Iris, a practical framework for validating OMT solvers.
When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers.
Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability.