module Jukebox.Sat
( Solver
, newSolver
, deleteSolver
, Lit, neg
, false, true
, SatSolver(..)
, newLit
, addClause
, solve
, conflict
, modelValue
, value
)
where
import MiniSat
( Solver
, deleteSolver
, Lit(..)
, neg
)
import qualified MiniSat as M
false, true :: Lit
true :: Lit
true = CInt -> Lit
MkLit CInt
0
false :: Lit
false = Lit -> Lit
neg Lit
true
newSolver :: IO Solver
newSolver :: IO Solver
newSolver =
do Solver
s <- IO Solver
M.newSolver
Lit
x <- Solver -> IO Lit
M.newLit Solver
s
if Lit
x Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
false Bool -> Bool -> Bool
|| Lit
x Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
true
then do Solver -> [Lit] -> IO Bool
M.addClause Solver
s [Lit
true]
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
s
else do [Char] -> IO Solver
forall a. HasCallStack => [Char] -> a
error [Char]
"failed to initialize false and true!"
class SatSolver s where
getSolver :: s -> Solver
instance SatSolver Solver where
getSolver :: Solver -> Solver
getSolver Solver
s = Solver
s
newLit :: SatSolver s => s -> IO Lit
newLit :: s -> IO Lit
newLit s
s = Solver -> IO Lit
M.newLit (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s)
addClause :: SatSolver s => s -> [Lit] -> IO ()
addClause :: s -> [Lit] -> IO ()
addClause s
s [Lit]
xs = Solver -> [Lit] -> IO Bool
M.addClause (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s) [Lit]
xs IO Bool -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
solve :: SatSolver s => s -> [Lit] -> IO Bool
solve :: s -> [Lit] -> IO Bool
solve s
s [Lit]
xs = Solver -> [Lit] -> IO Bool
M.solve (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s) [Lit]
xs
conflict :: SatSolver s => s -> IO [Lit]
conflict :: s -> IO [Lit]
conflict s
s = Solver -> IO [Lit]
M.conflict (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s)
modelValue :: SatSolver s => s -> Lit -> IO (Maybe Bool)
modelValue :: s -> Lit -> IO (Maybe Bool)
modelValue s
s Lit
x = Solver -> Lit -> IO (Maybe Bool)
M.modelValue (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s) Lit
x
value :: SatSolver s => s -> Lit -> IO (Maybe Bool)
value :: s -> Lit -> IO (Maybe Bool)
value s
s Lit
x = Solver -> Lit -> IO (Maybe Bool)
M.value (s -> Solver
forall s. SatSolver s => s -> Solver
getSolver s
s) Lit
x