Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Demonstrates extraction of interpolants via queries.

N.B. Interpolants are supported by MathSAT and Z3. Unfortunately the extraction of interpolants is not standardized, and are slightly different for these two solvers. So, we have two separate examples to demonstrate the usage.

# Documentation

exampleMathSAT :: Symbolic String Source #

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:

`>>>`

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

An interpolant for these sets would only talk about the variable `x`

that is common
to both. We have:

`>>>`

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

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:

`>>>`

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

And:

`>>>`

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

This establishes that we indeed have an interpolant!

evenOdd :: Symbolic String Source #

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:

`>>>`

"(or (= s1 0) (= s1 (* 2 (div s1 2))))"`runSMT evenOdd`

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 then it should be `False`

. You can argue
mathematically that this indeed the case, but let's just use SBV to prove these:

`>>>`

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

And:

`>>>`

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

This establishes that we indeed have an interpolant!