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

  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.
  4. LRA Interpolants from No Man's Land. Alt et. al 
  5. Decomposing Farkas Interpolants. Blicha et. al,