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

       x <- String -> Symbolic SInteger
sInteger String
"x"
       y <- sInteger "y"

       constrain $ x .>= 0

       query $ do abd <- getAbduct Nothing "abd" $ x + y .>= 2
                  io $ putStrLn $ "Got: " ++ abd

                  let 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
                  next
                  next
                  next