{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Minimal Unsatifiable Subset (MUS) Finder
--
-- References:
--
-- * Ulrich Junker. QuickXplain: Preferred explanations and relaxations for
--   over-constrained problems. In Proc. of AAAI’04, pages 167-172, 2004.
--   <http://www.aaai.org/Papers/AAAI/2004/AAAI04-027.pdf>
--
-----------------------------------------------------------------------------
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

-- | Find a minimal set of assumptions that causes a conflict.
-- Initial set of assumptions is taken from 'SAT.getFailedAssumptions'.
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