Data.SBV.Examples.Queries.Interpolants

Demonstrates extraction of interpolants via queries.

Documentation

evenOdd :: Symbolic [String]

Compute the interpolant for formulas y = 2x and y = 2z+1. These formulas are not satisfiable together since it would mean y is both even and odd at the same time. An interpolant for this pair of formulas is a formula that's expressed only in terms of y, which is the only common symbol among them. We have:

>>> runSMT evenOdd
["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"]

This is a bit hard to read unfortunately, due to translation artifacts and use of strings. To analyze, we need to know that s1 is y through SBV's translation. Let's express it in regular infix notation with y for s1:

 0 <= (y div 2) + ((-y) div 2)

Notice that the only symbol is y, as required. To establish that this is indeed an interpolant, we should establish that when y is even, this formula is True; and if y is odd, then then it should be False. You can argue mathematically that this indeed the case, but let's just use SBV to prove these:

>>> prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
Q.E.D.

And:

>>> prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
Q.E.D.

This establishes that we indeed have an interpolant!