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 yelds a new EUF interpolation algorithm. The framwork 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 - Itp
_{s }[1] [2] [3] - 3 - Custom strength factor

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)))))))

**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.