EUF interpolation

This page provides information on our EUF interpolation system and implementation.  The work is summarized in the conference paper  "Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions" [1].

We give here a 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 yields a new EUF interpolation algorithm. The three EUF interpolation algorithms from [1] and [3] (Itps is 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 - Itps [1] [2] [3]
  • 2 - Itpw [1] [3]
  • 3 - Itpr [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))))


Reference