-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Queries.Abducts
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates extraction of abducts via queries.
--
-- N.B. Interpolants are only supported by CVC5 currently.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Queries.Abducts where

import Data.SBV
import Data.SBV.Control

-- | Abduct extraction example. We have the constraint @x >= 0@
-- and we want to make @x + y >= 2@. We have:
--
-- >>> example
-- Got: (define-fun abd () Bool (and (= s0 s1) (= s0 1)))
-- Got: (define-fun abd () Bool (and (= 2 s1) (= s0 1)))
-- Got: (define-fun abd () Bool (and (= s0 s1) (<= 1 s1)))
-- Got: (define-fun abd () Bool (= 2 s1))
--
-- Note that @s0@ refers to @x@ and @s1@ refers to @y@ above. You can verify
-- that adding any of these will ensure @x + y >= 2@.
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]
++)

                  -- Get and display a couple of abducts
                  Query ()
next
                  Query ()
next
                  Query ()
next