EUF interpolation

The experiments set for the TACAS 2017 submission [1] can be found hereA tutorial on how to generate different interpolants using OpenSMT with an example is given below.

The EUF-interpolation system is a framework that allows the generation of multiple interpolants from the same congruence graph (created by the congruence closure algorithm) by using a labeling function. Each labeling function yelds a new EUF interpolation algorithm. The three EUF interpolation algorithms from [1] and [3] (Itpis equivalent to the algorithm from [2]) are implemented in OpenSMT2 and this page gives a tutorial on how to use them.

 

Requirements: OpenSMT compiled from the trunk with support to proof generation.

For instructions check here.

Also, please check how to construct interpolants for propositional logic here before going ahead with EUF interpolation.

 

For this example we will use this smt formula.

OpenSMT requires at least two assertions in order to generate interpolants. OpenSMT will then generate an interpolant such that the first assertion belongs to A, and the remaining assertions belong to B. The feature of custom partitioning is under development.

When we run

$ opensmt euf_example.smt2

we can see that the formula is UNSAT.

 

In order to generate an interpolant, there are two commands that have to be added to the .smt2 file.

In the header, add

(set-option :produce-interpolants true)

This option will enable proof production and prepare interpolation data

After

(check-sat)

, add

(get-interpolants)

This command will call the interpolation procedures and print the interpolants.

 

Now we can specify which EUF interpolation algorithm from [1] and [2] we want to use via

(set-option :interpolation-euf-algorithm <algo>)

<algo>

  • 0 - Itp[1] [2] [3]
  • 2 - Itp[1] [3]
  • 3 - Itp[1] [3]

 

After introducing these commands to the smt2 file and running OpenSMT on it we have

; Interpolant: (and (and (= u1 u2) (or (not (= s1 s2)) (= t1 t2))) (not (= v1 v2)))
 
Since both propositional and EUF interpolation are used, we can choose specific algorithms for each theory as shown in this file. The generated interpolant is
; Interpolant: (not (and (and (= u1 u2) (or (not (= s1 s2)) (= t1 t2))) (not (= v1 v2))))

 


  1. Duality-based Interpolation for Equalities and Uninterpreted Functions. Alt, L., Hyvärinen, A. E. J., Asadi, S., and Sharygina, N.
  2. Ground Interpolation for the Theory of Equality. Fuchs, A., Goel, A., Grundy, J., Krstić, S., and Tinelli, C.
  3. Controlled and Effective Interpolation. Alt, L.