The LRA-interpolation system [3] is a framework that allows the generation of an infinite amount of interpolants from the same simplex explanation by using a strength factor. Each labeling function yields a new EUF interpolation algorithm. The framework is implemented in OpenSMT2 and this page gives a tutorial on how to use it. The benchmarks used in [3] can be found here.

This file gives an example of how the LRA interpolation algorithm can be changed with the option

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

<algo>

- 0 - Farkas
_{s }[1] [2] [3] - 2 - Dual Farkas
- 3 - Flexible Farkas (custom strength factor)[4]
- 4 - Decomposing Farkas [5]
- 5 - Dual Decomposing Farkas [5]

Ordering the LRA interpolants by their logical strengths, we get:

Decomposing Farkas → Farkas → Flexible Farkas → Dual Farkas → Dual decomposing Farkas

(see the papers [3,5] for the proof.)

Running OpenSMT2 with the given file we obtain the interpolant

; Interpolant: (and (or (<= 4 y) (and (<= 4 x) (and (<= 4 x) (or (<= 4 y) (<= 4 x))))) (and (or (<= 4 y) (<= 4 x)) (or (<= 3 x) (and (<= 4 x) (and (<= 4 x) (or (<= 4 y) (<= 4 x)))))))

The strength factor [3] is a normalized value in the interval [0, 1) that given be given to control the strength of interpolants. The strength factor 0 leads to the strongest interpolants, and is equivalent to the algorithm from [1][2]. The closer to 1, the weaker the interpolant is. Notice that this allows for an infinite amount of interpolants. In OpenSMT2, the strength factor is given as a fraction. This file gives an example of how to generate the following weaker interpolant

; Interpolant: (and (or (<= (/ 100003 100000) y) (and (<= (/ 100001 50000) x) (and (<= (/ 300001 100000) x) (or (<= (/ 100003 100000) x) (<= (/ 300001 100000) y))))) (and (or (<= (/ 100003 100000) x) (<= (/ 300001 100000) y)) (or (<= (/ 200001 100000) x) (and (<= (/ 100001 50000) x) (and (<= (/ 300001 100000) x) (or (<= (/ 100003 100000) x) (<= (/ 300001 100000) y)))))))

### Reference

**An Interpolating Theorem Prover**. McMillan, K.**Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations**. Pudlák, P.**Controlled and Effective Interpolation.**Alt, L.**LRA Interpolants from No Man's Land**. Alt et. al**Decomposing Farkas Interpolants**. Blicha et. al,