-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.Deletion
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Minimal Unsatifiable Subset (MUS) Finder
--
-----------------------------------------------------------------------------
module ToySolver.SAT.MUS.Deletion
  ( module ToySolver.SAT.MUS.Base
  , findMUSAssumptions
  ) where

import Control.Monad
import Data.Default.Class
import Data.List
import qualified Data.IntSet as IS
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Base

-- | 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 = do
  String -> IO ()
log String
"computing a minimal unsatisfiable core by deletion method"
  MUS
core <- Solver -> IO MUS
SAT.getFailedAssumptions Solver
solver
  String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"initial core = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
core
  MUS -> IO ()
update MUS
core
  if MUS -> Bool
IS.null MUS
core then
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
core
  else
    MUS -> MUS -> IO MUS
loop MUS
core MUS
IS.empty

  where
    log :: String -> IO ()
    log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt

    update :: US -> IO ()
    update :: MUS -> IO ()
update = Options -> MUS -> IO ()
optUpdateBest Options
opt

    showLit :: Lit -> String
    showLit :: Lit -> String
showLit = Options -> Lit -> String
optShowLit Options
opt

    showLits :: IS.IntSet -> String
    showLits :: MUS -> String
showLits MUS
ls = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Lit -> String) -> [Lit] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> String
showLit (MUS -> [Lit]
IS.toList MUS
ls)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

    loop :: IS.IntSet -> IS.IntSet -> IO MUS
    loop :: MUS -> MUS -> IO MUS
loop MUS
ls1 MUS
fixed = do
      case MUS -> Maybe (Lit, MUS)
IS.minView MUS
ls1 of
        Maybe (Lit, MUS)
Nothing -> do
          String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"found a minimal unsatisfiable core"
          MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
fixed
        Just (Lit
l,MUS
ls) -> do
          String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"trying to remove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
showLit Lit
l
          Bool
ret <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (MUS -> [Lit]
IS.toList MUS
ls)
          if Bool -> Bool
not Bool
ret then do
            MUS
ls2 <- Solver -> IO MUS
SAT.getFailedAssumptions Solver
solver
            let removed :: MUS
removed = MUS
ls1 MUS -> MUS -> MUS
`IS.difference` MUS
ls2
            String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"successed to remove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits MUS
removed
            String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"new core = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ MUS -> String
showLits (MUS
ls2 MUS -> MUS -> MUS
`IS.union` MUS
fixed)
            MUS -> IO ()
update MUS
ls2
            [Lit] -> (Lit -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (MUS -> [Lit]
IS.toList MUS
removed) ((Lit -> IO ()) -> IO ()) -> (Lit -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Lit
l ->
              Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
l]
            MUS -> MUS -> IO MUS
loop MUS
ls2 MUS
fixed
          else do
            String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"failed to remove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
showLit Lit
l
            Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [Lit
l]
            MUS -> MUS -> IO MUS
loop MUS
ls (Lit -> MUS -> MUS
IS.insert Lit
l MUS
fixed)