module Jukebox.Sat.Minimise where

import Jukebox.Sat

solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
solveLocalMin :: forall s. SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
solveLocalMin s
s [Lit]
as [Lit]
ms =
  do Bool
b <- s -> [Lit] -> IO Bool
forall s. SatSolver s => s -> [Lit] -> IO Bool
solve s
s [Lit]
as
     if Bool
b then do Lit
l <- s -> IO Lit
forall s. SatSolver s => s -> IO Lit
newLit s
s -- used as a local assumption for this minimization
                  s -> [Lit] -> Lit -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms
                  s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s [Lit -> Lit
neg Lit
l]
                  Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          else do Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

localMin :: SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin :: forall s. SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms =
  do -- find out the current values of the m's
     [Maybe Bool]
bs <- [IO (Maybe Bool)] -> IO [Maybe Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ s -> Lit -> IO (Maybe Bool)
forall s. SatSolver s => s -> Lit -> IO (Maybe Bool)
modelValue s
s Lit
m | Lit
m <- [Lit]
ms ]
  
     -- assert that all false m's should stay false
     [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s [Lit -> Lit
neg Lit
l, Lit -> Lit
neg Lit
m] | (Lit
m,Maybe Bool
b) <- [Lit]
ms [Lit] -> [Maybe Bool] -> [(Lit, Maybe Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Maybe Bool]
bs, Maybe Bool
b Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True ]
     
     -- assert that at least one true m should become false also
     let ms1 :: [Lit]
ms1 = [ Lit
m | (Lit
m,Just Bool
True)  <- [Lit]
ms [Lit] -> [Maybe Bool] -> [(Lit, Maybe Bool)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Maybe Bool]
bs ]
     s -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> IO ()
addClause s
s (Lit -> Lit
neg Lit
l Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: [ Lit -> Lit
neg Lit
m | Lit
m <- [Lit]
ms1 ])
     
     -- is there still a solution?
     Bool
b <- s -> [Lit] -> IO Bool
forall s. SatSolver s => s -> [Lit] -> IO Bool
solve s
s (Lit
lLit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
:[Lit]
as)
     if Bool
b then s -> [Lit] -> Lit -> [Lit] -> IO ()
forall s. SatSolver s => s -> [Lit] -> Lit -> [Lit] -> IO ()
localMin s
s [Lit]
as Lit
l [Lit]
ms1
          else () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()