    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Queries.UnsatCore
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates extraction of unsat-cores via queries.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Queries.UnsatCore where

    import Data.SBV
    import Data.SBV.Control

    -- | A simple goal with three constraints, two of which are
    -- conflicting with each other. The third is irrelevant, in the sense
    -- that it does not contribute to the fact that the goal is unsatisfiable.
    p :: Symbolic (Maybe [String])
    p :: Symbolic (Maybe [String])
    p = do SInteger
    a <- String -> Symbolic SInteger
    sInteger "a"
           SInteger
    b <- String -> Symbolic SInteger
    sInteger "b"

           -- tell the solver we want unsat-cores
           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
    ProduceUnsatCores Bool
    True

           -- create named constraints, which will allow
           -- unsat-core extraction with the given names
           String -> SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> SBool -> m ()
    namedConstraint "less than 5"  (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    a SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< 5
           String -> SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> SBool -> m ()
    namedConstraint "more than 10" (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    a SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> 10
           String -> SBool -> SymbolicT IO ()
    forall (m :: * -> *). SolverContext m => String -> SBool -> m ()
    namedConstraint "irrelevant"   (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SInteger
    a SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .> SInteger
    b

           -- To obtain the unsat-core, we run a query
           Query (Maybe [String]) -> Symbolic (Maybe [String])
    forall a. Query a -> Symbolic a
    query (Query (Maybe [String]) -> Symbolic (Maybe [String]))
    -> Query (Maybe [String]) -> Symbolic (Maybe [String])
    forall a b. (a -> b) -> a -> b
    $ do CheckSatResult
    cs <- Query CheckSatResult
    checkSat
                      case CheckSatResult
    cs of
                        Unsat -> [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ([String] -> Maybe [String])
    -> QueryT IO [String] -> Query (Maybe [String])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QueryT IO [String]
    getUnsatCore
                        _     -> Maybe [String] -> Query (Maybe [String])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [String]
    forall a. Maybe a
    Nothing

    -- | Extract the unsat-core of 'p'. We have:
    --
    -- >>> ucCore
    -- Unsat core is: ["less than 5","more than 10"]
    --
    -- Demonstrating that the constraint @a .> b@ is /not/ needed for unsatisfiablity in this case.
    ucCore :: IO ()
    ucCore :: IO ()
    ucCore = do Maybe [String]
    mbCore <- Symbolic (Maybe [String]) -> IO (Maybe [String])
    forall a. Symbolic a -> IO a
    runSMT Symbolic (Maybe [String])
    p
                case Maybe [String]
    mbCore of
                  Nothing   -> String -> IO ()
    putStrLn "Problem is satisfiable."
                  Just core :: [String]
    core -> String -> IO ()
    putStrLn (String -> IO ()) -> String -> IO ()
    forall a b. (a -> b) -> a -> b
    $ "Unsat core is: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    forall a. Show a => a -> String
    show [String]
    core