{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.MUS.Enum
-- Copyright   :  (c) Masahiro Sakai 2012-2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- In this module, we assume each soft constraint /C_i/ is represented as a literal.
-- If a constraint /C_i/ is not a literal, we can represent it as a fresh variable /v/
-- together with a hard constraint /v ⇒ C_i/.
--
-- References:
--
-- * [CAMUS] M. Liffiton and K. Sakallah, Algorithms for computing minimal
--   unsatisfiable subsets of constraints, Journal of Automated Reasoning,
--   vol. 40, no. 1, pp. 1-33, Jan. 2008.
--   <http://sun.iwu.edu/~mliffito/publications/jar_liffiton_CAMUS.pdf>
--
-- * [HYCAM] A. Gregoire, B. Mazure, and C. Piette, Boosting a complete
--   technique to find MSS and MUS: thanks to a local search oracle, in
--   Proceedings of the 20th international joint conference on Artifical
--   intelligence, ser. IJCAI'07. San Francisco, CA, USA: Morgan Kaufmann
--   Publishers Inc., 2007, pp. 2300-2305.
--   <http://ijcai.org/papers07/Papers/IJCAI07-370.pdf>
--
-- * [DAA] J. Bailey and P. Stuckey, Discovery of minimal unsatisfiable
--   subsets of constraints using hitting set dualization," in Practical
--   Aspects of Declarative Languages, pp. 174-186, 2005.
--   <http://ww2.cs.mu.oz.au/~pjs/papers/padl05.pdf>
--
-----------------------------------------------------------------------------
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 :: 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 -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
'-') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"camus" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
CAMUS
    String
"daa" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
DAA
    String
"marco" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
MARCO
    String
"gurvichkhachiyan1999" -> Method -> Maybe Method
forall a. a -> Maybe a
Just Method
GurvichKhachiyan1999
    String
_ -> Maybe Method
forall a. Maybe a
Nothing

allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
allMUSAssumptions :: Solver -> [Lit] -> Options -> IO ([MUS], [MUS])
allMUSAssumptions Solver
solver [Lit]
sels Options
opt =
  case Options -> Method
optMethod Options
opt of
    Method
CAMUS -> Solver -> [Lit] -> Options -> IO ([MUS], [MUS])
CAMUS.allMUSAssumptions Solver
solver [Lit]
sels Options
opt
    Method
DAA -> do
      (Set MUS
msses, Set MUS
muses) <- Problem -> Options IO -> IO (Set MUS, Set MUS)
forall prob (m :: * -> *).
IsProblem prob m =>
prob -> Options m -> m (Set MUS, Set MUS)
DAA.run Problem
prob Options IO
opt2
      ([MUS], [MUS]) -> IO ([MUS], [MUS])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
muses, (MUS -> MUS) -> [MUS] -> [MUS]
forall a b. (a -> b) -> [a] -> [b]
map MUS -> MUS
mss2mcs (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
msses))
    Method
MARCO -> do
      (Set MUS
msses, Set MUS
muses) <- Problem -> Options IO -> IO (Set MUS, Set MUS)
forall prob.
IsProblem prob IO =>
prob -> Options IO -> IO (Set MUS, Set MUS)
MARCO.run Problem
prob Options IO
opt2
      ([MUS], [MUS]) -> IO ([MUS], [MUS])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
muses, (MUS -> MUS) -> [MUS] -> [MUS]
forall a b. (a -> b) -> [a] -> [b]
map MUS -> MUS
mss2mcs (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
msses))
    Method
GurvichKhachiyan1999 -> do
      (Set MUS
msses, Set MUS
muses) <- Problem -> Options IO -> IO (Set MUS, Set MUS)
forall (m :: * -> *) prob.
IsProblem prob m =>
prob -> Options m -> m (Set MUS, Set MUS)
GurvichKhachiyan1999.run Problem
prob Options IO
opt2
      ([MUS], [MUS]) -> IO ([MUS], [MUS])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
muses, (MUS -> MUS) -> [MUS] -> [MUS]
forall a b. (a -> b) -> [a] -> [b]
map MUS -> MUS
mss2mcs (Set MUS -> [MUS]
forall a. Set a -> [a]
Set.toList Set MUS
msses))
  where
    prob :: Problem
prob = Solver -> MUS -> Options -> Problem
Problem Solver
solver MUS
selsSet Options
opt

    opt2 :: I.Options IO
    opt2 :: Options IO
opt2 =
      (Options IO
forall a. Default a => a
def :: I.Options IO)
      { I.optOnMaximalInterestingSetFound = \MUS
xs ->
          Options -> MUS -> IO ()
optOnMCSFound Options
opt (MUS -> MUS
mss2mcs MUS
xs)
      , I.optOnMinimalUninterestingSetFound = \MUS
xs ->
          Options -> MUS -> IO ()
optOnMUSFound Options
opt MUS
xs
      }

    selsSet :: LitSet
    selsSet :: MUS
selsSet = [Lit] -> MUS
IntSet.fromList [Lit]
sels

    mss2mcs :: LitSet -> LitSet
    mss2mcs :: MUS -> MUS
mss2mcs = (MUS
selsSet MUS -> MUS -> MUS
`IntSet.difference`)

-- -----------------------------------------------------------------

data Problem = Problem SAT.Solver LitSet Options

instance I.IsProblem Problem IO where
  universe :: Problem -> MUS
universe (Problem Solver
_ MUS
univ Options
_) = MUS
univ

  isInteresting' :: Problem -> MUS -> IO InterestingOrUninterestingSet
isInteresting' (Problem Solver
solver MUS
univ Options
opt) MUS
xs = do
    Bool
b <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver (MUS -> [Lit]
IntSet.toList MUS
xs)
    if Bool
b then do
      Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
      InterestingOrUninterestingSet -> IO InterestingOrUninterestingSet
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InterestingOrUninterestingSet -> IO InterestingOrUninterestingSet)
-> InterestingOrUninterestingSet
-> IO InterestingOrUninterestingSet
forall a b. (a -> b) -> a -> b
$ MUS -> InterestingOrUninterestingSet
I.InterestingSet (MUS -> InterestingOrUninterestingSet)
-> MUS -> InterestingOrUninterestingSet
forall a b. (a -> b) -> a -> b
$ [Lit] -> MUS
IntSet.fromList [Lit
l | Lit
l <- MUS -> [Lit]
IntSet.toList MUS
univ, Options -> Model -> Lit -> Bool
optEvalConstr Options
opt Model
m Lit
l]
    else do
      MUS
zs <- Solver -> IO MUS
SAT.getFailedAssumptions Solver
solver
      InterestingOrUninterestingSet -> IO InterestingOrUninterestingSet
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InterestingOrUninterestingSet -> IO InterestingOrUninterestingSet)
-> InterestingOrUninterestingSet
-> IO InterestingOrUninterestingSet
forall a b. (a -> b) -> a -> b
$ MUS -> InterestingOrUninterestingSet
I.UninterestingSet MUS
zs

  grow :: Problem -> MUS -> IO MUS
grow prob :: Problem
prob@(Problem Solver
_ MUS
_ Options
opt) MUS
xs = do
    Options -> String -> IO ()
optLogger Options
opt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Method -> String
forall a. Show a => a -> String
show (Options -> Method
optMethod Options
opt) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": grow " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Problem -> MUS -> String
showLits Problem
prob MUS
xs
    MUS
ys <- Problem -> MUS -> IO MUS
forall prob (m :: * -> *). IsProblem prob m => prob -> MUS -> m MUS
I.defaultGrow Problem
prob MUS
xs
    Options -> String -> IO ()
optLogger Options
opt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Method -> String
forall a. Show a => a -> String
show (Options -> Method
optMethod Options
opt) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": grow added " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Problem -> MUS -> String
showLits Problem
prob (MUS
ys MUS -> MUS -> MUS
`IntSet.difference` MUS
xs)
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
ys

  shrink :: Problem -> MUS -> IO MUS
shrink prob :: Problem
prob@(Problem Solver
_ MUS
_ Options
opt) MUS
xs = do
    Options -> String -> IO ()
optLogger Options
opt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Method -> String
forall a. Show a => a -> String
show (Options -> Method
optMethod Options
opt) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": shrink " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Problem -> MUS -> String
showLits Problem
prob MUS
xs
    MUS
ys <- Problem -> MUS -> IO MUS
forall prob (m :: * -> *). IsProblem prob m => prob -> MUS -> m MUS
I.defaultShrink Problem
prob MUS
xs
    Options -> String -> IO ()
optLogger Options
opt (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Method -> String
forall a. Show a => a -> String
show (Options -> Method
optMethod Options
opt) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": shrink deleted " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Problem -> MUS -> String
showLits Problem
prob (MUS
xs MUS -> MUS -> MUS
`IntSet.difference` MUS
ys)
    MUS -> IO MUS
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MUS
ys

showLits :: Problem -> IntSet.IntSet -> String
showLits :: Problem -> MUS -> String
showLits (Problem Solver
_ MUS
_ Options
opt) 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 (Options -> Lit -> String
optShowLit Options
opt) (MUS -> [Lit]
IntSet.toList MUS
ls)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

-- -----------------------------------------------------------------