module ToySolver.SAT.MUS.Enum.Base
( module ToySolver.SAT.MUS.Types
, Method (..)
, Options (..)
) where
import Data.Default.Class
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Types
data Method
= CAMUS
| DAA
| MARCO
| GurvichKhachiyan1999
deriving (Eq, Ord, Enum, Bounded, Show)
data Options
= Options
{ optMethod :: Method
, optLogger :: String -> IO ()
, optShowLit :: Lit -> String
, optEvalConstr :: SAT.Model -> Lit -> Bool
, optOnMCSFound :: MCS -> IO ()
, optOnMUSFound :: MUS -> IO ()
, optKnownMCSes :: [MCS]
, optKnownMUSes :: [MUS]
, optKnownCSes :: [CS]
}
instance Default Options where
def =
Options
{ optMethod = CAMUS
, optLogger = \_ -> return ()
, optShowLit = show
, optEvalConstr = SAT.evalLit
, optOnMCSFound = \_ -> return ()
, optOnMUSFound = \_ -> return ()
, optKnownMCSes = []
, optKnownMUSes = []
, optKnownCSes = []
}