Issue Viewing Larger Interpolants

[cvick32]

I'm encountering some pretty large interpolants for a problem. I've included the problem below, if you want to take a look at the output. I'm wondering if there is anyway to simplify these interpolants from within smtinterpol, or if there is a setting that I can enable that will eliminate let statements in the output.

I'm mainly interested in seeing how the array functions select and store are being used in the interpolants and the let statements just confuse that.

Thanks in advance.

(set-option :produce-proofs true)
(set-option :interpolant-check-mode true)
(set-logic QF_ALIA)
(declare-fun a-0 () (Array Int Int))
(declare-fun a-1 () (Array Int Int))
(declare-fun i-0 () Int)
(declare-fun i-1 () Int)
(declare-fun x-0 () Int)
(declare-fun x-1 () Int)
(declare-fun y-0 () Int)
(declare-fun y-1 () Int)
(declare-fun n-0 () Int)
(declare-fun n-1 () Int)
(declare-fun pc-0 () Int)
(declare-fun pc-1 () Int)
(declare-fun Z-0 () Int)
(declare-fun Z-1 () Int)
(declare-fun a-2 () (Array Int Int))
(declare-fun i-2 () Int)
(declare-fun x-2 () Int)
(declare-fun y-2 () Int)
(declare-fun n-2 () Int)
(declare-fun pc-2 () Int)
(declare-fun Z-2 () Int)
(declare-fun a-3 () (Array Int Int))
(declare-fun i-3 () Int)
(declare-fun x-3 () Int)
(declare-fun y-3 () Int)
(declare-fun n-3 () Int)
(declare-fun pc-3 () Int)
(declare-fun Z-3 () Int)
(declare-fun a-4 () (Array Int Int))
(declare-fun i-4 () Int)
(declare-fun x-4 () Int)
(declare-fun y-4 () Int)
(declare-fun n-4 () Int)
(declare-fun pc-4 () Int)
(declare-fun Z-4 () Int)
(declare-fun a-5 () (Array Int Int))
(declare-fun i-5 () Int)
(declare-fun x-5 () Int)
(declare-fun y-5 () Int)
(declare-fun n-5 () Int)
(declare-fun pc-5 () Int)
(declare-fun Z-5 () Int)
(declare-fun a-6 () (Array Int Int))
(declare-fun i-6 () Int)
(declare-fun x-6 () Int)
(declare-fun y-6 () Int)
(declare-fun n-6 () Int)
(declare-fun pc-6 () Int)
(declare-fun Z-6 () Int)
(declare-fun a-7 () (Array Int Int))
(declare-fun i-7 () Int)
(declare-fun x-7 () Int)
(declare-fun y-7 () Int)
(declare-fun n-7 () Int)
(declare-fun pc-7 () Int)
(declare-fun Z-7 () Int)
(declare-fun a-8 () (Array Int Int))
(declare-fun i-8 () Int)
(declare-fun x-8 () Int)
(declare-fun y-8 () Int)
(declare-fun n-8 () Int)
(declare-fun pc-8 () Int)
(declare-fun Z-8 () Int)
(assert (! (and (and (not (<= n-0 2)) (and (= i-0 0) (= pc-0 0))) (and (or (= pc-0 0) (= pc-0 1)) (and (and (= n-0 n-1) (and (or (not (and (<= n-0 i-0) (= pc-0 1))) (= pc-0 pc-1)) (and (or (not (and (not (<= n-0 i-0)) (= pc-0 1))) (= pc-1 1)) (and (or (= pc-1 1) (not (and (<= n-0 i-0) (= pc-0 0)))) (and (or (not (and (not (<= n-0 i-0)) (= pc-0 0))) (= pc-1 0)) (and (not (<= n-0 y-0)) (and (<= 0 y-0) (and (not (<= n-0 x-0)) (and (<= 0 x-0) (and (or (= i-0 i-1) (not (and (<= n-0 i-0) (= pc-0 1)))) (and (or (= (+ i-0 (- i-1))(- 1)) (not (and (not (<= n-0 i-0)) (= pc-0 1)))) (and (or (= i-1 0) (not (and (<= n-0 i-0) (= pc-0 0)))) (and (or (= (+ i-0 (- i-1))(- 1)) (not (and (not (<= n-0 i-0)) (= pc-0 0)))) (and (or (= a-0 a-1) (not (and (<= n-0 i-0) (= pc-0 1)))) (and (and (or (= a-1 (store a-0 i-0 0)) (not (and (not (<= n-0 i-0)) (= pc-0 0)))) (or (= a-0 a-1) (not (and (<= n-0 i-0) (= pc-0 0))))) (or (= a-1 (store a-0 x-0 (+ (select a-0 y-0) 1))) (not (and (not (<= n-0 i-0)) (= pc-0 1))))))))))))))))))) (= Z-0 Z-1)))) :named A))
(assert (! (and (or (= pc-1 1) (= pc-1 0)) (and (and (= n-1 n-2) (and (or (not (and (= pc-1 1) (<= n-1 i-1))) (= pc-1 pc-2)) (and (or (not (and (= pc-1 1) (not (<= n-1 i-1)))) (= pc-2 1)) (and (or (= pc-2 1) (not (and (= pc-1 0) (<= n-1 i-1)))) (and (or (not (and (= pc-1 0) (not (<= n-1 i-1)))) (= pc-2 0)) (and (not (<= n-1 y-1)) (and (<= 0 y-1) (and (not (<= n-1 x-1)) (and (<= 0 x-1) (and (or (= i-1 i-2) (not (and (= pc-1 1) (<= n-1 i-1)))) (and (or (= (+ i-1 (- i-2))(- 1)) (not (and (= pc-1 1) (not (<= n-1 i-1))))) (and (or (= i-2 0) (not (and (= pc-1 0) (<= n-1 i-1)))) (and (or (= (+ i-1 (- i-2))(- 1)) (not (and (= pc-1 0) (not (<= n-1 i-1))))) (and (or (= a-1 a-2) (not (and (= pc-1 1) (<= n-1 i-1)))) (and (and (or (= a-2 (store a-1 i-1 0)) (not (and (= pc-1 0) (not (<= n-1 i-1))))) (or (= a-1 a-2) (not (and (= pc-1 0) (<= n-1 i-1))))) (or (= a-2 (store a-1 x-1 (+ (select a-1 y-1) 1))) (not (and (= pc-1 1) (not (<= n-1 i-1)))))))))))))))))))) (= Z-1 Z-2))) :named B))
(assert (! (and (or (= pc-2 1) (= pc-2 0)) (and (and (= n-2 n-3) (and (or (not (and (= pc-2 1) (<= n-2 i-2))) (= pc-2 pc-3)) (and (or (not (and (= pc-2 1) (not (<= n-2 i-2)))) (= pc-3 1)) (and (or (= pc-3 1) (not (and (= pc-2 0) (<= n-2 i-2)))) (and (or (not (and (= pc-2 0) (not (<= n-2 i-2)))) (= pc-3 0)) (and (not (<= n-2 y-2)) (and (<= 0 y-2) (and (not (<= n-2 x-2)) (and (<= 0 x-2) (and (or (= i-2 i-3) (not (and (= pc-2 1) (<= n-2 i-2)))) (and (or (= (+ i-2 (- i-3))(- 1)) (not (and (= pc-2 1) (not (<= n-2 i-2))))) (and (or (= i-3 0) (not (and (= pc-2 0) (<= n-2 i-2)))) (and (or (= (+ i-2 (- i-3))(- 1)) (not (and (= pc-2 0) (not (<= n-2 i-2))))) (and (or (= a-2 a-3) (not (and (= pc-2 1) (<= n-2 i-2)))) (and (and (or (= a-3 (store a-2 i-2 0)) (not (and (= pc-2 0) (not (<= n-2 i-2))))) (or (= a-2 a-3) (not (and (= pc-2 0) (<= n-2 i-2))))) (or (= a-3 (store a-2 x-2 (+ (select a-2 y-2) 1))) (not (and (= pc-2 1) (not (<= n-2 i-2)))))))))))))))))))) (= Z-2 Z-3))) :named C))
(assert (! (and (or (= pc-3 1) (= pc-3 0)) (and (and (= n-3 n-4) (and (or (not (and (= pc-3 1) (<= n-3 i-3))) (= pc-3 pc-4)) (and (or (not (and (= pc-3 1) (not (<= n-3 i-3)))) (= pc-4 1)) (and (or (= pc-4 1) (not (and (= pc-3 0) (<= n-3 i-3)))) (and (or (not (and (= pc-3 0) (not (<= n-3 i-3)))) (= pc-4 0)) (and (not (<= n-3 y-3)) (and (<= 0 y-3) (and (not (<= n-3 x-3)) (and (<= 0 x-3) (and (or (= i-3 i-4) (not (and (= pc-3 1) (<= n-3 i-3)))) (and (or (= (+ i-3 (- i-4))(- 1)) (not (and (= pc-3 1) (not (<= n-3 i-3))))) (and (or (= i-4 0) (not (and (= pc-3 0) (<= n-3 i-3)))) (and (or (= (+ i-3 (- i-4))(- 1)) (not (and (= pc-3 0) (not (<= n-3 i-3))))) (and (or (= a-3 a-4) (not (and (= pc-3 1) (<= n-3 i-3)))) (and (and (or (= a-4 (store a-3 i-3 0)) (not (and (= pc-3 0) (not (<= n-3 i-3))))) (or (= a-3 a-4) (not (and (= pc-3 0) (<= n-3 i-3))))) (or (= a-4 (store a-3 x-3 (+ (select a-3 y-3) 1))) (not (and (= pc-3 1) (not (<= n-3 i-3)))))))))))))))))))) (= Z-3 Z-4))) :named D))
(assert (! (and (or (= pc-4 1) (= pc-4 0)) (and (and (= n-4 n-5) (and (or (not (and (= pc-4 1) (<= n-4 i-4))) (= pc-4 pc-5)) (and (or (not (and (= pc-4 1) (not (<= n-4 i-4)))) (= pc-5 1)) (and (or (= pc-5 1) (not (and (= pc-4 0) (<= n-4 i-4)))) (and (or (not (and (= pc-4 0) (not (<= n-4 i-4)))) (= pc-5 0)) (and (not (<= n-4 y-4)) (and (<= 0 y-4) (and (not (<= n-4 x-4)) (and (<= 0 x-4) (and (or (= i-4 i-5) (not (and (= pc-4 1) (<= n-4 i-4)))) (and (or (= (+ i-4 (- i-5))(- 1)) (not (and (= pc-4 1) (not (<= n-4 i-4))))) (and (or (= i-5 0) (not (and (= pc-4 0) (<= n-4 i-4)))) (and (or (= (+ i-4 (- i-5))(- 1)) (not (and (= pc-4 0) (not (<= n-4 i-4))))) (and (or (= a-4 a-5) (not (and (= pc-4 1) (<= n-4 i-4)))) (and (and (or (= a-5 (store a-4 i-4 0)) (not (and (= pc-4 0) (not (<= n-4 i-4))))) (or (= a-4 a-5) (not (and (= pc-4 0) (<= n-4 i-4))))) (or (= a-5 (store a-4 x-4 (+ (select a-4 y-4) 1))) (not (and (= pc-4 1) (not (<= n-4 i-4)))))))))))))))))))) (= Z-4 Z-5))) :named E))
(assert (! (and (or (= pc-5 1) (= pc-5 0)) (and (and (= n-5 n-6) (and (or (not (and (= pc-5 1) (<= n-5 i-5))) (= pc-5 pc-6)) (and (or (not (and (= pc-5 1) (not (<= n-5 i-5)))) (= pc-6 1)) (and (or (= pc-6 1) (not (and (= pc-5 0) (<= n-5 i-5)))) (and (or (not (and (= pc-5 0) (not (<= n-5 i-5)))) (= pc-6 0)) (and (not (<= n-5 y-5)) (and (<= 0 y-5) (and (not (<= n-5 x-5)) (and (<= 0 x-5) (and (or (= i-5 i-6) (not (and (= pc-5 1) (<= n-5 i-5)))) (and (or (= (+ i-5 (- i-6))(- 1)) (not (and (= pc-5 1) (not (<= n-5 i-5))))) (and (or (= i-6 0) (not (and (= pc-5 0) (<= n-5 i-5)))) (and (or (= (+ i-5 (- i-6))(- 1)) (not (and (= pc-5 0) (not (<= n-5 i-5))))) (and (or (= a-5 a-6) (not (and (= pc-5 1) (<= n-5 i-5)))) (and (and (or (= a-6 (store a-5 i-5 0)) (not (and (= pc-5 0) (not (<= n-5 i-5))))) (or (= a-5 a-6) (not (and (= pc-5 0) (<= n-5 i-5))))) (or (= a-6 (store a-5 x-5 (+ (select a-5 y-5) 1))) (not (and (= pc-5 1) (not (<= n-5 i-5)))))))))))))))))))) (= Z-5 Z-6))) :named F))
(assert (! (and (or (= pc-6 1) (= pc-6 0)) (and (and (= n-6 n-7) (and (or (not (and (= pc-6 1) (<= n-6 i-6))) (= pc-6 pc-7)) (and (or (not (and (= pc-6 1) (not (<= n-6 i-6)))) (= pc-7 1)) (and (or (= pc-7 1) (not (and (= pc-6 0) (<= n-6 i-6)))) (and (or (not (and (= pc-6 0) (not (<= n-6 i-6)))) (= pc-7 0)) (and (not (<= n-6 y-6)) (and (<= 0 y-6) (and (not (<= n-6 x-6)) (and (<= 0 x-6) (and (or (= i-6 i-7) (not (and (= pc-6 1) (<= n-6 i-6)))) (and (or (= (+ i-6 (- i-7))(- 1)) (not (and (= pc-6 1) (not (<= n-6 i-6))))) (and (or (= i-7 0) (not (and (= pc-6 0) (<= n-6 i-6)))) (and (or (= (+ i-6 (- i-7))(- 1)) (not (and (= pc-6 0) (not (<= n-6 i-6))))) (and (or (= a-6 a-7) (not (and (= pc-6 1) (<= n-6 i-6)))) (and (and (or (= a-7 (store a-6 i-6 0)) (not (and (= pc-6 0) (not (<= n-6 i-6))))) (or (= a-6 a-7) (not (and (= pc-6 0) (<= n-6 i-6))))) (or (= a-7 (store a-6 x-6 (+ (select a-6 y-6) 1))) (not (and (= pc-6 1) (not (<= n-6 i-6)))))))))))))))))))) (= Z-6 Z-7))) :named G))
(assert (! (not (or (not (and (and (and (= pc-7 1) (<= n-7 i-7)) (<= 0 Z-7)) (not (<= n-7 Z-7)))) (<= 0 (select a-7 Z-7)))) :named H))
(check-sat)
(get-interpolants A B C D E F G H)

[jhoenicke]

We have an undocumented option (set-option :proof-transformation LURPI) that does some proof optimization before computing interpolants. It seems to already help for your example. The values are LU, RPI, RPILU, and LURPI, where LU (lower units) stands for one optimization, RPI (Recycle Pivots with Intersection) for the other, and RPILU and LURPI are the combination in two different orders. With LURPI, I already get much smaller interpolants.

We also have a formula simplifier that can be enabled with (set-option :simplify-interpolants true). You can also call it manually as (simplify (some-big-formula)), which returns a simplified formula. This uses some fast solving to check if parts of the formula are redundant, which can help a lot for the interpolants we produce. Combining these techniques, I get the following much simpler interpolants:

((and (= 1 i-1) (= 0 pc-1) (<= 0 (+ n-1 (- 3))) (= 0 (select (store a-1 i-1 0) 0))) (and (= 0 pc-2) (and (<= 0 (+ n-2 (- 3))) (let ((.cse0 (store a-2 i-2 0))) (and (= 0 (select .cse0 1)) (and (<= i-2 2) (= (select .cse0 0) 0))))) (<= 0 (+ i-2 (- 2)))) (and (= 0 pc-3) (and (and (and (= 0 (select a-3 1)) (= 0 (select a-3 0))) (and (<= (+ i-3 (- 1)) 2) (= (select a-3 2) 0))) (<= 0 (+ i-3 (- 3)))) (<= 0 (+ n-3 (- 3)))) (or (and (= 1 pc-4) (<= i-4 0) (<= 0 (+ n-4 (- 3))) (and (and (= 0 (select a-4 1)) (= 0 (select a-4 0))) (and (<= (+ n-4 (- 1)) 2) (= (select a-4 2) 0)))) (and (= 0 pc-4) (<= 0 (+ n-4 (- 4))))) (let ((.cse0 (= 1 pc-5))) (or (and .cse0 (and (<= (+ i-5 (- 1)) 0) (<= 0 (+ n-5 (- 3)))) (let ((.cse6 (+ n-5 (- 1)))) (let ((.cse3 (<= .cse6 2)) (.cse4 (select a-5 2))) (let ((.cse1 (select a-5 1)) (.cse2 (select a-5 0)) (.cse5 (and .cse3 (or (< .cse6 2) (= .cse4 0))))) (or (and (and (= 0 .cse1) (= 0 .cse2)) (and .cse3 (= .cse4 1))) (and (= .cse2 1) (= .cse1 0) .cse5) (and (= .cse1 1) (= .cse2 0) .cse5)))))) (let ((.cse7 (+ n-5 (- 4)))) (and (=> .cse0 (<= i-5 .cse7)) (<= 0 .cse7))))) (let ((.cse0 (= 0 pc-6)) (.cse1 (+ n-6 (- 1)))) (and (or .cse0 (<= i-6 .cse1)) (or .cse0 (let ((.cse12 (select a-6 2))) (let ((.cse13 (select a-6 1)) (.cse8 (= .cse12 1)) (.cse6 (select a-6 0))) (let ((.cse10 (or (<= 0 (+ .cse6 (- 2))) (= .cse6 1))) (.cse5 (<= .cse1 2)) (.cse2 (or (<= 0 (+ .cse12 (- 2))) .cse8)) (.cse7 (= .cse13 0)) (.cse11 (or (<= 0 (+ .cse13 (- 2))) (= .cse13 1)))) (let ((.cse4 (or .cse7 .cse11)) (.cse9 (and .cse5 (or (= .cse12 0) .cse2))) (.cse3 (or (= .cse6 0) .cse10))) (or (and .cse2 .cse3 .cse4 .cse5 (<= (+ .cse6 (- 1)) 0) (or .cse7 .cse8)) (and .cse9 .cse10 .cse4) (and .cse9 .cse11 .cse3) (<= i-6 (+ n-6 (- 2))))))))) (<= 0 (+ n-6 (- 3))))) (or (or (and (not (= Z-7 0)) (and (not (= (+ Z-7 (- 1)) 0)) (<= Z-7 1))) (<= 0 (select a-7 Z-7))) (<= n-7 Z-7) (not (= 1 pc-7)) (<= i-7 (+ n-7 (- 1)))))

Both techniques should be relatively fast even for larger proofs/formulas.

[jhoenicke]

You can also disable let outputs with (set-option :print-terms-cse false). However, for larger formulas this will just explode. For the unsimplified interpolants it produces 11 MB of output.

[cvick32]

Thanks so much for your response! I'm able to recreate everything except for calling simplify.

I tried calling it like (simplify (get-interpolants A B C..)) but that throws an error.

Is there another way to call it?

[jhoenicke]

For simplify you need to give the formula directly as argument:

(simplify (let ((.cse4 (+ i-1 (- 1)))) (let ((.cse3 (<= 0 .cse4)) (.cse0 (<= i-1 1))) (ite (= 1 i-1) (and (= 0 pc-1) (<= i-1 (+ n-1 (- 2))) (<= 0 (+ n-1 (- 3))) (or (let ((.cse2 (= 0 0)) (.cse1 (select (store a-1 i-1 0) 0))) (and .cse0 (= .cse1 0) .cse2 (and .cse2 .cse2) .cse2 (= 0 .cse1))) (= 1 0)) .cse3 (not (= 0 1))) (and (not (= .cse4 0)) (ite (<= .cse4 0) (=> (<= i-1 0) .cse3) .cse0))))))

outputs

(and (= 1 i-1) (= 0 pc-1) (<= 0 (+ n-1 (- 3))) (= 0 (select (store a-1 i-1 0) 0)))

So you would first need to parse the output and then send it back to the solver. You can also do it in a different smt script, but then you need to declare all the variables and functions again.

But (set-option :simplify-interpolants true) is the way you want to use it.

[cvick32]

Cool, thanks so much!