-----------------------------------------------------------------------------
-- |
-- 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 String
"a"
       SInteger
b <- String -> Symbolic SInteger
sInteger String
"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 String
"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
.< SInteger
5
       String -> SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> SBool -> m ()
namedConstraint String
"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
.> SInteger
10
       String -> SBool -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> SBool -> m ()
namedConstraint String
"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
                    CheckSatResult
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
                    CheckSatResult
_     -> 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
              Maybe [String]
Nothing   -> String -> IO ()
putStrLn String
"Problem is satisfiable."
              Just [String]
core -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Unsat core is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
core