{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module ToySolver.SAT.MUS.Enum
( module ToySolver.SAT.MUS.Types
, Method (..)
, showMethod
, parseMethod
, Options (..)
, allMUSAssumptions
) where
import Data.Char
import Data.Default.Class
import qualified Data.IntSet as IntSet
import Data.List (intercalate)
import qualified Data.Set as Set
import qualified ToySolver.Combinatorial.HittingSet.InterestingSets as I
import qualified ToySolver.Combinatorial.HittingSet.DAA as DAA
import qualified ToySolver.Combinatorial.HittingSet.MARCO as MARCO
import qualified ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 as GurvichKhachiyan1999
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Types
import ToySolver.SAT.MUS.Enum.Base
import qualified ToySolver.SAT.MUS.Enum.CAMUS as CAMUS
showMethod :: Method -> String
showMethod m = map toLower (show m)
parseMethod :: String -> Maybe Method
parseMethod s =
case filter (/='-') $ map toLower s of
"camus" -> Just CAMUS
"daa" -> Just DAA
"marco" -> Just MARCO
"gurvichkhachiyan1999" -> Just GurvichKhachiyan1999
_ -> Nothing
allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
allMUSAssumptions solver sels opt =
case optMethod opt of
CAMUS -> CAMUS.allMUSAssumptions solver sels opt
DAA -> do
(msses, muses) <- DAA.run prob opt2
return (Set.toList muses, map mss2mcs (Set.toList msses))
MARCO -> do
(msses, muses) <- MARCO.run prob opt2
return (Set.toList muses, map mss2mcs (Set.toList msses))
GurvichKhachiyan1999 -> do
(msses, muses) <- GurvichKhachiyan1999.run prob opt2
return (Set.toList muses, map mss2mcs (Set.toList msses))
where
prob = Problem solver selsSet opt
opt2 :: I.Options IO
opt2 =
(def :: I.Options IO)
{ I.optOnMaximalInterestingSetFound = \xs ->
optOnMCSFound opt (mss2mcs xs)
, I.optOnMinimalUninterestingSetFound = \xs ->
optOnMUSFound opt xs
}
selsSet :: LitSet
selsSet = IntSet.fromList sels
mss2mcs :: LitSet -> LitSet
mss2mcs = (selsSet `IntSet.difference`)
data Problem = Problem SAT.Solver LitSet Options
instance I.IsProblem Problem IO where
universe (Problem _ univ _) = univ
isInteresting' (Problem solver univ opt) xs = do
b <- SAT.solveWith solver (IntSet.toList xs)
if b then do
m <- SAT.getModel solver
return $ I.InterestingSet $ IntSet.fromList [l | l <- IntSet.toList univ, optEvalConstr opt m l]
else do
zs <- SAT.getFailedAssumptions solver
return $ I.UninterestingSet $ IntSet.fromList zs
grow prob@(Problem _ _ opt) xs = do
optLogger opt $ show (optMethod opt) ++ ": grow " ++ showLits prob xs
ys <- I.defaultGrow prob xs
optLogger opt $ show (optMethod opt) ++ ": grow added " ++ showLits prob (ys `IntSet.difference` xs)
return ys
shrink prob@(Problem _ _ opt) xs = do
optLogger opt $ show (optMethod opt) ++ ": shrink " ++ showLits prob xs
ys <- I.defaultShrink prob xs
optLogger opt $ show (optMethod opt) ++ ": shrink deleted " ++ showLits prob (xs `IntSet.difference` ys)
return ys
showLits :: Problem -> IntSet.IntSet -> String
showLits (Problem _ _ opt) ls =
"{" ++ intercalate ", " (map (optShowLit opt) (IntSet.toList ls)) ++ "}"