{-# OPTIONS_GHC -Wall #-}
module ToySolver.SAT.MUS
( module ToySolver.SAT.MUS.Types
, Method (..)
, showMethod
, parseMethod
, Options (..)
, findMUSAssumptions
) where
import Data.Char
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.MUS.Base
import ToySolver.SAT.MUS.Types
import qualified ToySolver.SAT.MUS.Deletion as Deletion
import qualified ToySolver.SAT.MUS.Insertion as Insertion
import qualified ToySolver.SAT.MUS.QuickXplain as QuickXplain
showMethod :: Method -> String
showMethod m = map toLower (show m)
parseMethod :: String -> Maybe Method
parseMethod s =
case map toLower s of
"linear" -> Just Deletion
"deletion" -> Just Deletion
"insertion" -> Just Insertion
"quickxplain" -> Just QuickXplain
_ -> Nothing
findMUSAssumptions
:: SAT.Solver
-> Options
-> IO MUS
findMUSAssumptions solver opt =
case optMethod opt of
Deletion -> Deletion.findMUSAssumptions solver opt
Insertion -> Insertion.findMUSAssumptions solver opt
QuickXplain -> QuickXplain.findMUSAssumptions solver opt