    -----------------------------------------------------------------------------
    -- |
    -- 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 (= s1 2))
    -- Got: (define-fun abd () Bool (<= 2 s1))
    -- Got: (define-fun abd () Bool (= (+ s1 s0) 2))
    -- Got: (define-fun abd () Bool (= (+ s0 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