    -----------------------------------------------------------------------------
    -- |
    -- 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.
    -----------------------------------------------------------------------------

    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 = do a <- sInteger "a"
           b <- sInteger "b"

           -- tell the solver we want unsat-cores
           setOption $ ProduceUnsatCores True

           -- create named constraints, which will allow
           -- unsat-core extraction with the given names
           namedConstraint "less than 5"  $ a .< 5
           namedConstraint "more than 10" $ a .> 10
           namedConstraint "irrelevant"   $ a .> b

           -- To obtain the unsat-core, we run a query
           query $ do cs <- checkSat
                      case cs of
                        Unsat -> Just <$> getUnsatCore
                        _     -> return 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 = do mbCore <- runSMT p
                case mbCore of
                  Nothing   -> putStrLn "Problem is satisfiable."
                  Just core -> putStrLn $ "Unsat core is: " ++ show core