-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.Enum.Base
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
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
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
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
Ord, Int -> Method
Method -> Int
Method -> [Method]
Method -> Method
Method -> Method -> [Method]
Method -> Method -> Method -> [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
forall a. a -> a -> Bounded a
maxBound :: Method
$cmaxBound :: Method
minBound :: Method
$cminBound :: Method
Bounded, Int -> Method -> ShowS
[Method] -> ShowS
Method -> String
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)

-- The default value can be obtained by 'def'.
data Options
  = Options
  { Options -> Method
optMethod     :: Method
  , Options -> String -> IO ()
optLogger     :: String -> IO ()
  , Options -> Int -> String
optShowLit    :: Lit -> String
    -- ^ MCS candidates (see HYCAM paper for details).
    -- A MCS candidate must be a superset of a real MCS.
  , Options -> Model -> Int -> Bool
optEvalConstr :: SAT.Model -> Lit -> Bool
    -- ^ Because each soft constraint /C_i/ is represented as a selector
    -- literal /l_i/ together with a hard constraint /l_i ⇒ C_i/, there
    -- are cases that a model assigns false to /l_i/ even though /C_i/
    -- itself is true. This function is used to inform the truth value
    -- of the original constraint /C_i/ that corresponds to the selector
    -- literal /l_i/.
  , 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
    { optMethod :: Method
optMethod     = Method
CAMUS
    , optLogger :: String -> IO ()
optLogger     = \String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    , optShowLit :: Int -> String
optShowLit    = forall a. Show a => a -> String
show
    , optEvalConstr :: Model -> Int -> Bool
optEvalConstr = forall m. IModel m => m -> Int -> Bool
SAT.evalLit
    , optOnMCSFound :: MCS -> IO ()
optOnMCSFound = \MCS
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    , optOnMUSFound :: MCS -> IO ()
optOnMUSFound = \MCS
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    , optKnownMCSes :: [MCS]
optKnownMCSes = []
    , optKnownMUSes :: [MCS]
optKnownMUSes = []
    , optKnownCSes :: [MCS]
optKnownCSes = []
    }