-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.Insertion
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Minimal Unsatifiable Subset (MUS) Finder
--
-- References:
--
-- * <http://logos.ucd.ie/~jpms/talks/talksite/jpms-ismvl10.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.SAT.MUS.Insertion
  ( module ToySolver.SAT.MUS.Base
  , findMUSAssumptions
  ) where

import Control.Monad
import Data.Default.Class
import Data.List
import qualified Data.IntSet as IntSet
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 insertion 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
IntSet.null MUS
core then
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
core
  else do
    MUS
mus <- do
      Bool
b <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
b then
        MUS -> MUS -> IO MUS
loop MUS
IntSet.empty MUS
core
      else
        MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
IntSet.empty
    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
mus
    MUS -> IO ()
update MUS
mus
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
mus
  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 :: IntSet.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]
IntSet.toList MUS
ls)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

    loop :: IntSet.IntSet -> IntSet.IntSet -> IO MUS
    loop :: MUS -> MUS -> IO MUS
loop MUS
m MUS
f = do
      -- pre: (m∩f = ∅), (m⊎f is unsatisfiable), (f=∅ → m is unsatisfiable)
      case MUS -> Maybe (Lit, MUS)
IntSet.minView MUS
f of
        Maybe (Lit, MUS)
Nothing -> MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
m
        Just (Lit
c, MUS
f') -> do
          -- m is satisfiable
          let loop2 :: MUS -> Lit -> IO (MUS, Lit)
loop2 MUS
s Lit
c = do
                -- pre: (m⊎s⊎{c} ⊆ f), (m⊎s is satisfiable)
                Bool
b <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (Lit
c Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: MUS -> [Lit]
IntSet.toList (MUS
m MUS -> MUS -> MUS
`IntSet.union` MUS
s))
                if Bool -> Bool
not Bool
b then do
                  -- c is a transition clause
                  String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"found a transition constraint: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
showLit Lit
c
                  (MUS, Lit) -> IO (MUS, Lit)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MUS
s,Lit
c)
                else do
                  Model
model <- Solver -> IO Model
SAT.getModel Solver
solver
                  let s' :: MUS
s' = (Lit -> Bool) -> MUS -> MUS
IntSet.filter (Options -> Model -> Lit -> Bool
optEvalConstr Options
opt Model
model) MUS
f
                  case MUS -> Maybe (Lit, MUS)
IntSet.minView (MUS
f MUS -> MUS -> MUS
`IntSet.difference` MUS
s') of
                    Maybe (Lit, MUS)
Nothing -> String -> IO (MUS, Lit)
forall a. HasCallStack => String -> a
error String
"shuld not happen"
                    Just (Lit
c', MUS
_) -> MUS -> Lit -> IO (MUS, Lit)
loop2 MUS
s' Lit
c'
          (MUS
s,Lit
c') <- MUS -> Lit -> IO (MUS, Lit)
loop2 MUS
IntSet.empty Lit
c
          MUS -> MUS -> IO MUS
loop (Lit -> MUS -> MUS
IntSet.insert Lit
c' MUS
m) MUS
s