-----------------------------------------------------------------------------
-- |
-- 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
(Method -> Method -> Bool)
-> (Method -> Method -> Bool) -> Eq Method
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Method -> Method -> Bool
== :: Method -> Method -> Bool
$c/= :: Method -> Method -> Bool
/= :: 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
$ccompare :: Method -> Method -> Ordering
compare :: Method -> Method -> Ordering
$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
>= :: Method -> Method -> Bool
$cmax :: Method -> Method -> Method
max :: Method -> Method -> Method
$cmin :: Method -> Method -> Method
min :: Method -> Method -> 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
$csucc :: Method -> Method
succ :: Method -> Method
$cpred :: Method -> Method
pred :: Method -> Method
$ctoEnum :: Int -> Method
toEnum :: Int -> Method
$cfromEnum :: Method -> Int
fromEnum :: Method -> Int
$cenumFrom :: Method -> [Method]
enumFrom :: Method -> [Method]
$cenumFromThen :: Method -> Method -> [Method]
enumFromThen :: Method -> Method -> [Method]
$cenumFromTo :: Method -> Method -> [Method]
enumFromTo :: Method -> Method -> [Method]
$cenumFromThenTo :: Method -> Method -> Method -> [Method]
enumFromThenTo :: Method -> Method -> Method -> [Method]
Enum, Method
Method -> Method -> Bounded Method
forall a. a -> a -> Bounded a
$cminBound :: Method
minBound :: Method
$cmaxBound :: Method
maxBound :: 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
$cshowsPrec :: Int -> Method -> ShowS
showsPrec :: Int -> Method -> ShowS
$cshow :: Method -> String
show :: Method -> String
$cshowList :: [Method] -> ShowS
showList :: [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
_ -> () -> IO ()
forall a. a -> IO a
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    , optOnMUSFound :: MCS -> IO ()
optOnMUSFound = \MCS
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    , optKnownMCSes :: [MCS]
optKnownMCSes = []
    , optKnownMUSes :: [MCS]
optKnownMUSes = []
    , optKnownCSes :: [MCS]
optKnownCSes = []
    }