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. As of Z3 version 4.8.0; Z3 no longer supports interpolants. You need to use the MathSAT backend for this example to work.

# Documentation

example :: Symbolic String Source #

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 example`

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!