{-# 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 :: Method -> String
showMethod Method
m = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (Method -> String
forall a. Show a => a -> String
show Method
m)
parseMethod :: String -> Maybe Method
parseMethod :: String -> Maybe Method
parseMethod String
s =
case (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
String
"linear" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
Deletion
String
"deletion" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
Deletion
String
"insertion" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
Insertion
String
"quickxplain" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
QuickXplain
String
_ -> Maybe Method
forall a. Maybe a
Nothing
findMUSAssumptions
:: SAT.Solver
-> Options
-> IO MUS
findMUSAssumptions :: Solver -> Options -> IO MUS
findMUSAssumptions Solver
solver Options
opt =
case Options -> Method
optMethod Options
opt of
Method
Deletion -> Solver -> Options -> IO MUS
Deletion.findMUSAssumptions Solver
solver Options
opt
Method
Insertion -> Solver -> Options -> IO MUS
Insertion.findMUSAssumptions Solver
solver Options
opt
Method
QuickXplain -> Solver -> Options -> IO MUS
QuickXplain.findMUSAssumptions Solver
solver Options
opt