{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Queries.Abducts where
import Data.SBV
import Data.SBV.Control
example :: IO ()
example :: IO ()
example = SMTConfig -> Symbolic () -> IO ()
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith SMTConfig
cvc5 (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
SMTOption -> Symbolic ()
forall (m :: * -> *). SolverContext m => SMTOption -> m ()
setOption (SMTOption -> Symbolic ()) -> SMTOption -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Bool -> SMTOption
ProduceAbducts Bool
True
SInteger
x <- String -> Symbolic SInteger
sInteger String
"x"
SInteger
y <- String -> Symbolic SInteger
sInteger String
"y"
SBool -> Symbolic ()
forall a. QuantifiedBool a => a -> Symbolic ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
0
Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do String
abd <- Maybe String -> String -> SBool -> Query String
getAbduct Maybe String
forall a. Maybe a
Nothing String
"abd" (SBool -> Query String) -> SBool -> Query String
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
2
IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> IO () -> Query ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
abd
let next :: Query ()
next = Query String
getAbductNext Query String -> (String -> Query ()) -> Query ()
forall a b. QueryT IO a -> (a -> QueryT IO b) -> QueryT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> IO ()) -> (String -> String) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"Got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++)
Query ()
next
Query ()
next
Query ()
next