content: -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.MUS.Base
  -- Copyright   :  (c) Masahiro Sakai 2012
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  portable
  --
  -----------------------------------------------------------------------------
  module ToySolver.SAT.MUS.Base
    ( module ToySolver.SAT.MUS.Types
    , Method (..)
    , Options (..)
    ) where
  
  import Control.Monad
  import Data.Default.Class
  import qualified Data.IntSet as IS
  import qualified ToySolver.SAT as SAT
  import ToySolver.SAT.Types
  import ToySolver.SAT.MUS.Types
  
  data Method
    = Deletion
    | Insertion
    | QuickXplain
    deriving (Eq, Ord, Enum, Bounded, Show)
  
  -- | Options for MUS finding.
  --
  -- The default value can be obtained by 'def'.
  data Options
    = Options
    { optMethod     :: Method
    , optLogger     :: String -> IO ()
    , optShowLit    :: Lit -> String
    , 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/.
    , optUpdateBest :: US -> IO ()
    }
  
  instance Default Options where
    def =
      Options
      { optMethod     = Deletion
      , optLogger     = \_ -> return ()
      , optShowLit    = show
      , optEvalConstr = SAT.evalLit
      , optUpdateBest = \_ -> return ()
      }
  