Satchmo.SAT

Documentation

data SAT a

Instances

Monad SAT

Functor SAT

MonadIO SAT

MonadSAT SAT

MonadReader Handle SAT

MonadState Accu SAT

data Header

Constructors

Header

Fields

numClauses :: Int

numVars :: Int

universals :: [Int]

fresh :: MonadSAT m => m Literal

fresh_forall :: MonadSAT m => m Literal

emit :: MonadSAT m => Clause -> m ()

type Weight = Int

sat :: SAT a -> IO (ByteString, Header, a)