Interpolation and Model Checking for Nonlinear Arithmetic

TL;DR

This paper introduces a novel model-based interpolation method for SMT that enhances nonlinear arithmetic solving by integrating model construction and explanation generation, improving model checking capabilities.

Contribution

It develops a new interaction mode with SMT solvers called solving modulo a model, enabling effective interpolation for nonlinear real arithmetic within the MCSAT framework.

Findings

Improved interpolation procedure for nonlinear real arithmetic

Enhanced model checking performance with the new method

Effective integration into existing model checkers

Abstract

We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic.