funsat-0.5.2: A modern DPLL-style SAT solver



The main SAT solver monad. Embeds ST. See type SSTErrMonad, which stands for ''State ST Error Monad''.



liftST :: MonadST s m => ST s a -> m aSource

runSSTErrMonad :: Error e => SSTErrMonad e st s a -> st -> ST s (Either e a, st)Source

runSSTErrMonad m s executes a SSTErrMonad action with initial state s until an error occurs or a result is returned.

evalSSTErrMonad :: Error e => SSTErrMonad e st s a -> st -> ST s (Either e a)Source

data SSTErrMonad e st s a Source

SSTErrMonad e st s a: the error type e, state type st, ST thread s and result type a.

This is a monad embedding ST and supporting error handling and state threading. It uses CPS to avoid checking Left and Right for every >>=; instead only checks on catchError. Idea adapted from


MonadState st (SSTErrMonad e st s) 
Error e => MonadError e (SSTErrMonad e st s) 
MonadST s (SSTErrMonad e st s) 
Monad (SSTErrMonad e st s) 
Error e => MonadPlus (SSTErrMonad e st s)