-----------------------------------------------------------------------------
-- |
-- 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 String
"x"
       SInteger
y <- String -> Symbolic SInteger
sInteger String
"y"
       SInteger
z <- String -> Symbolic SInteger
sInteger String
"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 [(String
":interpolation-group", String
"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
3SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
y SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= -SInteger
1
       [(String, String)] -> SBool -> SymbolicT IO ()
forall (m :: * -> *).
SolverContext m =>
[(String, String)] -> SBool -> m ()
constrainWithAttribute [(String
":interpolation-group", String
"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
.>=  SInteger
0
       [(String, String)] -> SBool -> SymbolicT IO ()
forall (m :: * -> *).
SolverContext m =>
[(String, String)] -> SBool -> m ()
constrainWithAttribute [(String
":interpolation-group", String
"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
- SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>=  SInteger
3
       [(String, String)] -> SBool -> SymbolicT IO ()
forall (m :: * -> *).
SolverContext m =>
[(String, String)] -> SBool -> m ()
constrainWithAttribute [(String
":interpolation-group", String
"B")] (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
z     SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<=  SInteger
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
                    CheckSatResult
Unsat  -> [String] -> Query String
getInterpolantMathSAT [String
"A"]
                    DSat{} -> String -> Query String
forall a. HasCallStack => String -> a
error String
"Unexpected delta-sat result!"
                    CheckSatResult
Sat    -> String -> Query String
forall a. HasCallStack => String -> a
error String
"Unexpected sat result!"
                    CheckSatResult
Unk    -> String -> Query String
forall a. HasCallStack => String -> a
error String
"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 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 String
"x"
       SInteger
y <- String -> Symbolic SInteger
sInteger String
"y"
       SInteger
z <- String -> Symbolic SInteger
sInteger String
"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
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
x, SInteger
y SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
zSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1]