LRA Interpolation

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

 


  1. An Interpolating Theorem Prover. McMillan, K. 
  2. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Pudlák, P.
  3. Controlled and Effective Interpolation. Alt, L.