Satchmo.MonadSAT

Documentation

class (Functor m, Monad m) => MonadSAT m where

Methods

fresh :: m Literal

fresh_forall :: m Literal

emit :: Clause -> m ()

emitW :: Weight -> Clause -> m ()

note :: String -> m ()

emit some note (could be printed by the backend)

Instances

MonadSAT SAT

MonadSAT SAT

MonadSAT SAT

MonadSAT SAT

MonadSAT SAT

(Monad m, MonadSAT m) => MonadSAT (ListT m)

(Monad m, MonadSAT m) => MonadSAT (ContT s m)

(Monad m, MonadSAT m) => MonadSAT (ReaderT r m)

(Monad m, MonadSAT m) => MonadSAT (StateT s m)

(Monad m, MonadSAT m) => MonadSAT (StateT s m)

(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m)

(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m)

(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m)

(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m)

type Weight = Int

data Header

Constructors

Header

Fields

numClauses :: !Int

numVars :: !Int

universals :: ![Int]

Instances

Show Header

MonadState Header SAT

MonadState Header SAT