Documentation

MathSAT example. Compute the interpolant for the following sets of formulas:

{x - 3y >= -1, x + y >= 0}

AND

{z - 2x >= 3, 2z <= 1}

where the variables are integers. Note that these sets of formulas are themselves satisfiable, but not taken all together. The pair (x, y) = (0, 0) satisfies the first set. The pair (x, z) = (-2, 0) satisfies the second. However, there's no triple (x, y, z) that satisfies all these four formulas together. We can use SBV to check this fact:

>>> sat $ \x y z -> sAnd [x - 3*y .>= -1, x + y .>= 0, z - 2*x .>= 3, 2 * z .<= (1::SInteger)]
Unsatisfiable

An interpolant for these sets would only talk about the variable x that is common to both. We have:

>>> runSMTWith mathSAT exampleMathSAT
"(<= 0 s0)"

Notice that we get a string back, not a term; so there's some back-translation we need to do. We know that s0 is x through our translation mechanism, so the interpolant is saying that x >= 0 is entailed by the first set of formulas, and is inconsistent with the second. Let's use SBV to indeed show that this is the case:

>>> prove $ \x y -> (x - 3*y .>= -1 .&& x + y .>= 0) .=> (x .>= (0::SInteger))
Q.E.D.

And:

>>> prove $ \x z -> (z - 2*x .>= 3 .&& 2 * z .<= 1) .=> sNot (x .>= (0::SInteger))
Q.E.D.

This establishes that we indeed have an interpolant!

Z3 example. 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
"(or (= s1 0) (= s1 (* 2 (div 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:

(y == 0) || (y == 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 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) .=> ((y .== 0) .|| (y .== 2 * (y `sDiv` (2::SInteger))))
Q.E.D.

And:

>>> prove $ \y -> (y `sMod` 2 .== 1) .=> sNot ((y .== 0) .|| (y .== 2 * (y `sDiv` (2::SInteger))))
Q.E.D.

This establishes that we indeed have an interpolant!