OpenSMT2 supports interpolation for propositional logic, QF_UF, QF_LRA, QF_LIA, and QF_IDL.

For instructions on how to compile OpenSMT2 with interpolation please check here.

This page provides a short tutorial on how to compute interpolants for the three theories.

**General Instructions**

In order to generate interpolants, OpenSMT2 requires at least two commands:

(set-option :produce-interpolants true)

(get-interpolants)

*UNSAT*, an interpolation error is shown.

This will create an interpolant assuming that the first assertion belongs to partition *A* and the rest of the assertions belong to partition *B*.

**Interpolation Algorithms**

Different interpolation algorithms may be chosen for the different theories.

The header commands to specify the interpolation algorithms are:

`(a) `**(set-option :interpolation-bool-algorithm ***<bool_algo>*)

`(b) `**(set-option :interpolation-euf-algorithm ***<euf_algo>*)

`(c) `**(set-option :interpolation-lra-algorithm ***<lra_algo>*)

`(d) `**(set-option :interpolation-lra-factor ***<lra_factor>*)

_{s}[1]

_{w}[3]

_{w}[4]

_{s}[4]

_{min}[3]

_{s}[5] [6]

_{w}[5]

_{r}[5]

_{s}[1]

*N*such that

*0 <= N < 1*, in the form of a fraction.

**Interpolant Soundness**

(set-option :certify-interpolants<certification_level>)

<certification_level>

*tool_wrapper.sh*, distributed with OpenSMT2. By default, this script uses the opensmt binary, but it can be changed to use any SAT/SMT solver.

Your PATH should know about these two binaries. That can be done via:

$ cd opensmt2

$ export PATH=$PATH:`pwd`

**Verbosity**

(set-option :verbosity<verbosity_level>)

**Examples**

**References**

**An Interpolating Theorem Prover**. McMillan, K.**Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations**. Pudlák, P.**Interpolant Strength**. D'Silva, V., Kroening, D,. Purandare, M., and Weissenbacher, G.**A Proof-Sensitive Approach for Small Propositional Interpolants**. Alt, L., Fedyukovich, G., Hyvärinen, A. E. J., and Sharygina, N.**Duality-based Interpolation for Equalities and Uninterpreted Functions**. Alt, L., Hyvärinen, A. E. J., Asadi, S., and Sharygina, N.**Ground Interpolation for the Theory of Equality**. Fuchs, A., Goel, A., Grundy, J., Krstić, S., and Tinelli, C.**Controlled and Effective Interpolation.**Alt, L.