{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Queries.Interpolants where
import Data.SBV
import Data.SBV.Control
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"
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
[(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
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!"
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]