Interpolation

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)
in the header of the smt2 file, and
(get-interpolants)
after satisfiability is checked.
If the problem is not 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>)
 
<bool_algo>
0 - Ms [1]
1 - P [2]
2 - Mw [3]
3 - PS [4]
4 - PSw [4]
5 - PSs [4]
6 - Dmin [3]
 
<euf_algo>
0 - Itps [5] [6]
2 - Itpw [5]
3 - Itpr [5]
 
<lra_algo>
0 - Itps [1]
3 - Custom normalized strength factor, requires option (d) [7]
 
<lra_factor>
Any rational number N such that 0 <= N < 1, in the form of a fraction.
 
Interpolant Soundness
The soundness of the generated interpolants can be checked by an external SAT/SMT solver with the option
(set-option :certify-interpolants <certification_level>)

<certification_level>

1 - Soundness check for the final interpolant only
2 - Soundness check for every partial interpolant annotated to the nodes of the proof of unsatisfiability
 
This option uses the script 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

The following option controls the amount of information that is printed:
(set-option :verbosity <verbosity_level>)
<verbosity_level>:
1 - Basic information is given, such as statistics on the proof of unsatisfiability, the interpolation algorithm used, and the size of the interpolants.
2 - All the information was given by (1) plus the interpolant.
 
 
Examples
For concrete examples for each theory, visit the following pages:
 
 

References

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