-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.
-- | A monadic interface to the functions of
-- "SAT.MiniSat.LowLevel". This layer:
--
-- * hooks into garbage collection;
--
-- * converts low-level types to Haskell types;
--
-- * replaces the 'IO' monad by a state monad;
--
-- * converts low-level errors to I/O exceptions.
--
-- All of the exported functions may potentially raise an exception.
module SAT.MiniSat.Monadic where
import SAT.MiniSat.LowLevel
import SAT.MiniSat.Literals
import Foreign
import Foreign.C.Error
import Control.Monad.Trans.State
import System.IO.Unsafe
-- ----------------------------------------------------------------------
-- * Error handling
-- | Check an assertion, and raise an 'IO' exception (using the current
-- errno and the supplied location string) if the assertion fails.
ensure :: String -> Bool -> IO ()
ensure s True = return ()
ensure s False = throwErrno s
-- ----------------------------------------------------------------------
-- * Conversions
-- | Marshall a C boolean to a Haskell boolean.
bool_of_cbool :: C_Bool -> Bool
bool_of_cbool 0 = False
bool_of_cbool n = True
-- | Marshall a Haskell boolean to a C boolean.
cbool_of_bool :: Bool -> C_Bool
cbool_of_bool True = 1
cbool_of_bool False = 0
-- | Marshall a Haskell literal to a MiniSat literal.
clit_of_lit :: Lit Int -> C_Lit
clit_of_lit (Pos n) = c_lit_new (fromIntegral n) (cbool_of_bool False)
clit_of_lit (Neg n) = c_lit_new (fromIntegral n) (cbool_of_bool True)
-- | Marshall an \"lbool\" to a 'Maybe' 'Bool'.
maybebool_of_lbool :: C_LBool -> Maybe Bool
maybebool_of_lbool 0 = Nothing
maybebool_of_lbool 1 = Just True
maybebool_of_lbool (-1) = Just False
maybebool_of_lbool _ = error "maybebool_of_lbool"
-- ----------------------------------------------------------------------
-- * High-level Solver type
-- | The type of solvers.
newtype Solver = Solver (ForeignPtr C_Solver)
-- | Convert a low-level pointer to a garbage-collected 'Solver'.
make_Solver :: Ptr C_Solver -> IO Solver
make_Solver p = do
fptr <- newForeignPtr c_solver_delete_ptr p
return (Solver fptr)
-- | Marshall a 'Solver' to a 'Ptr' 'C_Solver'.
with_Solver :: Solver -> (Ptr C_Solver -> IO a) -> IO a
with_Solver (Solver fptr) = withForeignPtr fptr
-- | Create a new solver.
solver_new :: IO Solver
solver_new = do
p <- c_solver_new
ensure "solver_new" (p /= nullPtr)
make_Solver p
-- ----------------------------------------------------------------------
-- * State monad
-- $ The low-level C functions live in the 'IO' monad. However, the only
-- actual side effect of these functions is to update the 'Solver'
-- object. Therefore, it is safe to lift these functions to a state
-- monad. Moreover, in doing so, we are able to exploit laziness in a
-- way that is not possible in the 'IO' monad.
-- | The 'SolverState' monad is for functions whose only side effect
-- is to update the 'Solver' object.
type SolverState a = State Solver a
-- | Marshall a function from the 'IO' monad to the state monad. The
-- call to 'unsafePerformIO' is safe, provided that the 'IO'
-- computation's only side effect is to update the 'Solver' object.
stateful :: (Solver -> IO a) -> SolverState a
stateful body = state $ \s -> unsafePerformIO $ do
r <- body s
return (r, s)
-- | Run a 'SolverState' computation in the context of a newly created
-- solver. The use of 'unsafePerformIO' is safe because the only side
-- effect of 'solver_new' is to create a new solver state.
m_run :: SolverState a -> a
m_run body = unsafePerformIO $ do
s <- solver_new
let (a, s') = runState body s
return a
-- ----------------------------------------------------------------------
-- * Marshalled API functions
-- | Add a clause to the solver. May return 'False' if the clause is
-- unsatisfiable, in which case the Solver should not be searched.
-- The clause is represented as a list of literals.
m_solver_addclause :: [Lit Int] -> SolverState Bool
m_solver_addclause lits = stateful $ \s -> do
with_Solver s $ \s_ptr -> do
withArrayLen clits $ \n clits_ptr -> do
r <- c_solver_addclause s_ptr clits_ptr (fromIntegral n)
return (bool_of_cbool r)
where
clits = map clit_of_lit lits
-- | Initialize the solver for searching.
m_solver_solve_start :: SolverState ()
m_solver_solve_start = stateful $ \s -> do
with_Solver s $ \s_ptr -> do
c_solver_solve_start s_ptr
-- | Search the next solution.
m_solver_solve_next :: SolverState Bool
m_solver_solve_next = stateful $ \s -> do
with_Solver s $ \s_ptr -> do
r <- c_solver_solve_next s_ptr
return (bool_of_cbool r)
-- | Finalizer to run after search.
m_solver_solve_finish :: SolverState ()
m_solver_solve_finish = stateful $ \s -> do
with_Solver s $ \s_ptr -> do
c_solver_solve_finish s_ptr
-- | Retrieve the most recent solution (only valid if
-- 'm_solver_solve_next' returned 'True', and no other API functions
-- have been called since then). The solution is represented as a
-- list, where the /n/th element of the list represents the assignment
-- ('True', 'False', or 'Nothing') of variable /n/.
m_solver_solution :: SolverState [Maybe Bool]
m_solver_solution = stateful $ \s -> do
with_Solver s $ \s_ptr -> do
lbools_ptr <- c_solver_solution s_ptr
n <- c_solver_nvars s_ptr
lbools <- peekArray (fromIntegral n) lbools_ptr
let mbools = map maybebool_of_lbool lbools
return mbools
-- ----------------------------------------------------------------------
-- * Derived API functions
-- | Add a list of clauses to the solver. May return 'False' if the
-- clauses are unsatisfiable, in which case the Solver should not be
-- searched.
m_solver_addclauses :: [[Lit Int]] -> SolverState Bool
m_solver_addclauses [] = return True
m_solver_addclauses (h:t) = do
r <- m_solver_addclause h
if r == False then do
return False
else do
m_solver_addclauses t
-- | Search and return the next solution.
m_solver_next_solution :: SolverState (Maybe [Maybe Bool])
m_solver_next_solution = do
r <- m_solver_solve_next
if r == False then do
return Nothing
else do
sol <- m_solver_solution
return (Just sol)
-- | Return all remaining solutions.
m_solver_next_solutions :: SolverState [[Maybe Bool]]
m_solver_next_solutions = do
r <- m_solver_next_solution
case r of
Nothing -> do
return []
Just h -> do
t <- m_solver_next_solutions
return (h:t)