sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Queries.Interpolants

Description

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.

Synopsis

- exampleMathSAT :: Symbolic String
- evenOdd :: Symbolic String

# Documentation

    >>> -- For doctest purposes only:
    >>> import Data.SBV
    >>> import Data.SBV.Control

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:

    >>> 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!

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:

    >>> 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!