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

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