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 (Method -> Method -> Bool
(Method -> Method -> Bool)
-> (Method -> Method -> Bool) -> Eq Method
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Method -> Method -> Bool
$c/= :: Method -> Method -> Bool
== :: Method -> Method -> Bool
$c== :: Method -> Method -> Bool
Eq, Eq Method
Eq Method
-> (Method -> Method -> Ordering)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Bool)
-> (Method -> Method -> Method)
-> (Method -> Method -> Method)
-> Ord Method
Method -> Method -> Bool
Method -> Method -> Ordering
Method -> Method -> Method
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Method -> Method -> Method
$cmin :: Method -> Method -> Method
max :: Method -> Method -> Method
$cmax :: Method -> Method -> Method
>= :: Method -> Method -> Bool
$c>= :: Method -> Method -> Bool
> :: Method -> Method -> Bool
$c> :: Method -> Method -> Bool
<= :: Method -> Method -> Bool
$c<= :: Method -> Method -> Bool
< :: Method -> Method -> Bool
$c< :: Method -> Method -> Bool
compare :: Method -> Method -> Ordering
$ccompare :: Method -> Method -> Ordering
$cp1Ord :: Eq Method
Ord, Int -> Method
Method -> Int
Method -> [Method]
Method -> Method
Method -> Method -> [Method]
Method -> Method -> Method -> [Method]
(Method -> Method)
-> (Method -> Method)
-> (Int -> Method)
-> (Method -> Int)
-> (Method -> [Method])
-> (Method -> Method -> [Method])
-> (Method -> Method -> [Method])
-> (Method -> Method -> Method -> [Method])
-> Enum Method
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Method -> Method -> Method -> [Method]
$cenumFromThenTo :: Method -> Method -> Method -> [Method]
enumFromTo :: Method -> Method -> [Method]
$cenumFromTo :: Method -> Method -> [Method]
enumFromThen :: Method -> Method -> [Method]
$cenumFromThen :: Method -> Method -> [Method]
enumFrom :: Method -> [Method]
$cenumFrom :: Method -> [Method]
fromEnum :: Method -> Int
$cfromEnum :: Method -> Int
toEnum :: Int -> Method
$ctoEnum :: Int -> Method
pred :: Method -> Method
$cpred :: Method -> Method
succ :: Method -> Method
$csucc :: Method -> Method
Enum, Method
Method -> Method -> Bounded Method
forall a. a -> a -> Bounded a
maxBound :: Method
$cmaxBound :: Method
minBound :: Method
$cminBound :: Method
Bounded, Int -> Method -> ShowS
[Method] -> ShowS
Method -> String
(Int -> Method -> ShowS)
-> (Method -> String) -> ([Method] -> ShowS) -> Show Method
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Method] -> ShowS
$cshowList :: [Method] -> ShowS
show :: Method -> String
$cshow :: Method -> String
showsPrec :: Int -> Method -> ShowS
$cshowsPrec :: Int -> Method -> ShowS
Show)
data Options
= Options
{ Options -> Method
optMethod :: Method
, Options -> String -> IO ()
optLogger :: String -> IO ()
, Options -> Int -> String
optShowLit :: Lit -> String
, Options -> Model -> Int -> Bool
optEvalConstr :: SAT.Model -> Lit -> Bool
, Options -> MCS -> IO ()
optOnMCSFound :: MCS -> IO ()
, Options -> MCS -> IO ()
optOnMUSFound :: MUS -> IO ()
, Options -> [MCS]
optKnownMCSes :: [MCS]
, Options -> [MCS]
optKnownMUSes :: [MUS]
, Options -> [MCS]
optKnownCSes :: [CS]
}
instance Default Options where
def :: Options
def =
Options :: Method
-> (String -> IO ())
-> (Int -> String)
-> (Model -> Int -> Bool)
-> (MCS -> IO ())
-> (MCS -> IO ())
-> [MCS]
-> [MCS]
-> [MCS]
-> Options
Options
{ optMethod :: Method
optMethod = Method
CAMUS
, optLogger :: String -> IO ()
optLogger = \String
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, optShowLit :: Int -> String
optShowLit = Int -> String
forall a. Show a => a -> String
show
, optEvalConstr :: Model -> Int -> Bool
optEvalConstr = Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit
, optOnMCSFound :: MCS -> IO ()
optOnMCSFound = \MCS
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, optOnMUSFound :: MCS -> IO ()
optOnMUSFound = \MCS
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, optKnownMCSes :: [MCS]
optKnownMCSes = []
, optKnownMUSes :: [MCS]
optKnownMUSes = []
, optKnownCSes :: [MCS]
optKnownCSes = []
}