module Satchmo.Internal
( SAT
, fresh, emit
, sat
)
where
import Satchmo.Data
import Control.Monad.State.Strict
import Control.Monad.Writer.Strict
data Accu = Accu
{ next :: ! Int
, size :: ! Int
}
start :: Accu
start = Accu
{ next = 1
, size = 0
}
type SAT a = WriterT [ Clause ] (State Accu) a
sat :: SAT a -> ( String, a )
sat m =
let ~( ~(a,w), accu) = runState ( runWriterT m ) start
in ( unlines $ unwords [ "p", "cnf", show ( next accu 1), show ( size accu ) ]
: map show w
, a
)
fresh :: SAT Literal
fresh = do
a <- get
put $ a { next = next a + 1 }
return $ literal $ next a
emit :: Clause -> SAT ()
emit clause = do
a <- get
tell [ clause ]
put $ a
{ size = size a + 1
}