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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Queries.Interpolants where

    import Data.SBV
    import Data.SBV.Control

    -- | 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!
    exampleMathSAT :: Symbolic String
    exampleMathSAT :: Symbolic String
    exampleMathSAT = do
           SInteger
    x <- String -> Symbolic SInteger
    sInteger "x"
           SInteger
    y <- String -> Symbolic SInteger
    sInteger "y"
           SInteger
    z <- String -> Symbolic SInteger
    sInteger "z"

           -- tell the solver we want interpolants
           -- NB. Only MathSAT needs this. Z3 doesn't need or like this setting!
           SMTOption -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => SMTOption -> m ()
    setOption (SMTOption -> SymbolicT IO ()) -> SMTOption -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> SMTOption
    ProduceInterpolants Bool
    True

           -- create interpolation constraints. MathSAT requires the relevant formulas
           -- to be marked with the attribute :interpolation-group
           [(String, String)] -> SBool -> SymbolicT IO ()
    forall (m :: * -> *).
    SolverContext m =>
    [(String, String)] -> SBool -> m ()
    constrainWithAttribute [(":interpolation-group", "A")] (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 3SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    *SInteger
    y SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= -1
           [(String, String)] -> SBool -> SymbolicT IO ()
    forall (m :: * -> *).
    SolverContext m =>
    [(String, String)] -> SBool -> m ()
    constrainWithAttribute [(":interpolation-group", "A")] (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + SInteger
    y   SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>=  0
           [(String, String)] -> SBool -> SymbolicT IO ()
    forall (m :: * -> *).
    SolverContext m =>
    [(String, String)] -> SBool -> m ()
    constrainWithAttribute [(":interpolation-group", "B")] (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    z SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 2SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    *SInteger
    x SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>=  3
           [(String, String)] -> SBool -> SymbolicT IO ()
    forall (m :: * -> *).
    SolverContext m =>
    [(String, String)] -> SBool -> m ()
    constrainWithAttribute [(":interpolation-group", "B")] (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ 2SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    *SInteger
    z     SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<=  1

           -- To obtain the interpolant, we run a query
           Query String -> Symbolic String
    forall a. Query a -> Symbolic a
    query (Query String -> Symbolic String)
    -> Query String -> Symbolic String
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                      case CheckSatResult
    cs of
                        Unsat -> [String] -> Query String
    getInterpolantMathSAT ["A"]
                        Sat   -> String -> Query String
    forall a. HasCallStack => String -> a
    error "Unexpected sat result!"
                        Unk   -> String -> Query String
    forall a. HasCallStack => String -> a
    error "Unexpected unknown result!"

    -- | 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 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!
    evenOdd :: Symbolic String
    evenOdd :: Symbolic String
    evenOdd = do
           SInteger
    x <- String -> Symbolic SInteger
    sInteger "x"
           SInteger
    y <- String -> Symbolic SInteger
    sInteger "y"
           SInteger
    z <- String -> Symbolic SInteger
    sInteger "z"

           Query String -> Symbolic String
    forall a. Query a -> Symbolic a
    query (Query String -> Symbolic String)
    -> Query String -> Symbolic String
    forall a b. (a -> b) -> a -> b
    $ [SBool] -> Query String
    getInterpolantZ3 [SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 2SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    *SInteger
    x, SInteger
    y SInteger -> SInteger -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== 2SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    *SInteger
    zSInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    +1]