module ToySolver.SAT.MUS.Enum.CAMUS
( module ToySolver.SAT.MUS.Enum.Base
, allMUSAssumptions
, allMCSAssumptions
, enumMCSAssumptions
) where
import Control.Monad
import Data.Array.IArray
import Data.Default.Class
import qualified Data.IntSet as IS
import Data.List
import Data.IORef
import Data.Set (Set)
import qualified Data.Set as Set
import qualified ToySolver.Combinatorial.HittingSet.Simple as HittingSet
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types
import ToySolver.SAT.MUS.Enum.Base
enumMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ()
enumMCSAssumptions :: Solver -> [Lit] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Lit]
sels Options
opt = do
IORef [(Lit, CS)]
candRef <- [(Lit, CS)] -> IO (IORef [(Lit, CS)])
forall a. a -> IO (IORef a)
newIORef [(CS -> Lit
IS.size CS
cs, CS
cs) | CS
cs <- Options -> [CS]
optKnownCSes Options
opt]
IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef Lit
1
where
log :: String -> IO ()
log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt
mcsFound :: MCS -> IO ()
mcsFound :: CS -> IO ()
mcsFound CS
mcs = do
Options -> CS -> IO ()
optOnMCSFound Options
opt CS
mcs
Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver (CS -> [Lit]
IS.toList CS
mcs)
loop :: IORef [(Int, LitSet)] -> Int -> IO ()
loop :: IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef Lit
k = do
String -> IO ()
log (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"CAMUS: k = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
k
[(Lit, CS)]
cand <- IORef [(Lit, CS)] -> IO [(Lit, CS)]
forall a. IORef a -> IO a
readIORef IORef [(Lit, CS)]
candRef
Bool
ret <- if Bool -> Bool
not ([(Lit, CS)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Lit, CS)]
cand) then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Solver -> IO Bool
SAT.solve Solver
solver
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[(Lit, CS)] -> ((Lit, CS) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Lit, CS)]
cand (((Lit, CS) -> IO ()) -> IO ()) -> ((Lit, CS) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Lit
size,CS
cs) -> do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Lit
size Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
k) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
CS -> IO ()
mcsFound CS
cs
IORef [(Lit, CS)] -> [(Lit, CS)] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef [(Lit, CS)]
candRef [(Lit
size,CS
cs) | (Lit
size,CS
cs) <- [(Lit, CS)]
cand, Lit
size Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
/= Lit
k]
Lit
vk <- Solver -> IO Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar Solver
solver
Solver -> Lit -> PBLinSum -> Integer -> IO ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> Lit -> PBLinSum -> Integer -> m ()
SAT.addPBAtMostSoft Solver
solver Lit
vk [(Integer
1,-Lit
sel) | Lit
sel <- [Lit]
sels] (Lit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
k)
let loop2 :: IO ()
loop2 = do
Bool
ret2 <- Solver -> [Lit] -> IO Bool
SAT.solveWith Solver
solver [Lit
vk]
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret2 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
let mcs :: CS
mcs = [Lit] -> CS
IS.fromList [Lit
sel | Lit
sel <- [Lit]
sels, Bool -> Bool
not (Model -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
evalLit Model
m Lit
sel)]
CS -> IO ()
mcsFound CS
mcs
IORef [(Lit, CS)] -> ([(Lit, CS)] -> [(Lit, CS)]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(Lit, CS)]
candRef (((Lit, CS) -> Bool) -> [(Lit, CS)] -> [(Lit, CS)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Lit
_,CS
cs) -> Bool -> Bool
not (CS
mcs CS -> CS -> Bool
`IS.isSubsetOf` CS
cs)))
IO ()
loop2
IO ()
loop2
Solver -> [Lit] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Solver
solver [-Lit
vk]
IORef [(Lit, CS)] -> Lit -> IO ()
loop IORef [(Lit, CS)]
candRef (Lit
kLit -> Lit -> Lit
forall a. Num a => a -> a -> a
+Lit
1)
allMCSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO [MCS]
allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Lit]
sels Options
opt = do
IORef [CS]
ref <- [CS] -> IO (IORef [CS])
forall a. a -> IO (IORef a)
newIORef []
let opt2 :: Options
opt2 =
Options
opt
{ optOnMCSFound :: CS -> IO ()
optOnMCSFound = \CS
mcs -> do
IORef [CS] -> ([CS] -> [CS]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [CS]
ref (CS
mcsCS -> [CS] -> [CS]
forall a. a -> [a] -> [a]
:)
Options -> CS -> IO ()
optOnMCSFound Options
opt CS
mcs
}
Solver -> [Lit] -> Options -> IO ()
enumMCSAssumptions Solver
solver [Lit]
sels Options
opt2
IORef [CS] -> IO [CS]
forall a. IORef a -> IO a
readIORef IORef [CS]
ref
allMUSAssumptions :: SAT.Solver -> [Lit] -> Options -> IO ([MUS], [MCS])
allMUSAssumptions :: Solver -> [Lit] -> Options -> IO ([CS], [CS])
allMUSAssumptions Solver
solver [Lit]
sels Options
opt = do
String -> IO ()
log String
"CAMUS: MCS enumeration begins"
[CS]
mcses <- Solver -> [Lit] -> Options -> IO [CS]
allMCSAssumptions Solver
solver [Lit]
sels Options
opt
String -> IO ()
log String
"CAMUS: MCS enumeration done"
let muses :: [CS]
muses = Set CS -> [CS]
HittingSet.enumMinimalHittingSets (Set CS -> [CS]) -> Set CS -> [CS]
forall a b. (a -> b) -> a -> b
$ [CS] -> Set CS
forall a. Ord a => [a] -> Set a
Set.fromList [CS]
mcses
(CS -> IO ()) -> [CS] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Options -> CS -> IO ()
optOnMUSFound Options
opt) [CS]
muses
([CS], [CS]) -> IO ([CS], [CS])
forall (m :: * -> *) a. Monad m => a -> m a
return ([CS]
muses, [CS]
mcses)
where
log :: String -> IO ()
log :: String -> IO ()
log = Options -> String -> IO ()
optLogger Options
opt