    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.Queries.Interpolants
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- 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.
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.Queries.Interpolants where

    import Data.SBV
    import Data.SBV.Control

    -- | 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 -> bAnd [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 example
    -- "(<= 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) ==> bnot (x .>= (0::SInteger))
    -- Q.E.D.
    --
    -- This establishes that we indeed have an interpolant!
    example :: Symbolic String
    example = do
           x <- sInteger "x"
           y <- sInteger "y"
           z <- sInteger "z"

           -- tell the solver we want interpolants
           setOption $ ProduceInterpolants True

           -- create interpolation constraints. MathSAT requires the relevant formulas
           -- to be marked with the attribute :interpolation-group
           constrainWithAttribute [(":interpolation-group", "A")] $ x - 3*y .>= -1
           constrainWithAttribute [(":interpolation-group", "A")] $ x + y   .>=  0
           constrainWithAttribute [(":interpolation-group", "B")] $ z - 2*x .>=  3
           constrainWithAttribute [(":interpolation-group", "B")] $ 2*z     .<=  1

           -- To obtain the interpolant, we run a query
           query $ do cs <- checkSat
                      case cs of
                        Unsat -> getInterpolant ["A"]
                        Sat   -> error "Unexpected sat result!"
                        Unk   -> error "Unexpected unknown result!"