module Satchmo.SAT.BS
( SAT, Header(..)
, fresh, fresh_forall
, emit, Weight
, sat
)
where
import Satchmo.Data
import Satchmo.MonadSAT
import Control.Exception
import Control.Monad.RWS.Strict
import qualified Data.ByteString.Char8 as BS
import Data.Foldable
import Data.String
newtype SAT a
= SAT { unSAT ::
RWS () BS.ByteString Header
a
}
deriving ( Functor, Monad
, MonadState Header
, MonadWriter BS.ByteString
)
instance MonadSAT SAT where
fresh = do
a <- get
let v = numVars a
put $ a { numVars = succ v }
return $ literal True $ succ v
emit cl = do
a <- get
put $ a { numClauses = succ $ numClauses a }
tell $ fromString $ show cl ++ "\n"
note msg = do
return ()
start :: Header
start = Header { numClauses = 0, numVars = 0
, universals = []
}
sat :: SAT a -> IO (BS.ByteString, Header, a )
sat (SAT m) = do
let
(res, accu, bs) = runRWS m () start
return ( bs , accu, res )