satchmo-2.9.9.4: SAT encoding monad
Safe HaskellSafe-Inferred
LanguageHaskell2010

Satchmo.MonadSAT

Documentation

class (Applicative m, Monad m) => MonadSAT m where Source #

Associated Types

type Decoder m :: * -> * Source #

Methods

fresh :: m Literal Source #

fresh_forall :: m Literal Source #

emit :: Clause -> m () Source #

note :: String -> m () Source #

emit some note (could be printed by the backend)

decode_variable :: Variable -> Decoder m Bool Source #

Instances

Instances details
MonadSAT SAT Source # 
Instance details

Defined in Satchmo.SAT.External

Associated Types

type Decoder SAT :: Type -> Type Source #

Methods

fresh :: SAT Literal Source #

fresh_forall :: SAT Literal Source #

emit :: Clause -> SAT () Source #

note :: String -> SAT () Source #

decode_variable :: Variable -> Decoder SAT Bool Source #

MonadSAT SAT Source # 
Instance details

Defined in Satchmo.SAT.Mini

Associated Types

type Decoder SAT :: Type -> Type Source #

Methods

fresh :: SAT Literal Source #

fresh_forall :: SAT Literal Source #

emit :: Clause -> SAT () Source #

note :: String -> SAT () Source #

decode_variable :: Variable -> Decoder SAT Bool Source #

MonadSAT SAT Source # 
Instance details

Defined in Satchmo.SAT.Tmpfile

Associated Types

type Decoder SAT :: Type -> Type Source #

Methods

fresh :: SAT Literal Source #

fresh_forall :: SAT Literal Source #

emit :: Clause -> SAT () Source #

note :: String -> SAT () Source #

decode_variable :: Variable -> Decoder SAT Bool Source #

(Monad m, MonadSAT m) => MonadSAT (ListT m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (ListT m) :: Type -> Type Source #

Methods

fresh :: ListT m Literal Source #

fresh_forall :: ListT m Literal Source #

emit :: Clause -> ListT m () Source #

note :: String -> ListT m () Source #

decode_variable :: Variable -> Decoder (ListT m) Bool Source #

(Monad m, MonadSAT m) => MonadSAT (ReaderT r m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (ReaderT r m) :: Type -> Type Source #

Methods

fresh :: ReaderT r m Literal Source #

fresh_forall :: ReaderT r m Literal Source #

emit :: Clause -> ReaderT r m () Source #

note :: String -> ReaderT r m () Source #

decode_variable :: Variable -> Decoder (ReaderT r m) Bool Source #

(Monad m, MonadSAT m) => MonadSAT (StateT s m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (StateT s m) :: Type -> Type Source #

Methods

fresh :: StateT s m Literal Source #

fresh_forall :: StateT s m Literal Source #

emit :: Clause -> StateT s m () Source #

note :: String -> StateT s m () Source #

decode_variable :: Variable -> Decoder (StateT s m) Bool Source #

(Monad m, MonadSAT m) => MonadSAT (StateT s m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (StateT s m) :: Type -> Type Source #

Methods

fresh :: StateT s m Literal Source #

fresh_forall :: StateT s m Literal Source #

emit :: Clause -> StateT s m () Source #

note :: String -> StateT s m () Source #

decode_variable :: Variable -> Decoder (StateT s m) Bool Source #

(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (WriterT w m) :: Type -> Type Source #

Methods

fresh :: WriterT w m Literal Source #

fresh_forall :: WriterT w m Literal Source #

emit :: Clause -> WriterT w m () Source #

note :: String -> WriterT w m () Source #

decode_variable :: Variable -> Decoder (WriterT w m) Bool Source #

(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (WriterT w m) :: Type -> Type Source #

Methods

fresh :: WriterT w m Literal Source #

fresh_forall :: WriterT w m Literal Source #

emit :: Clause -> WriterT w m () Source #

note :: String -> WriterT w m () Source #

decode_variable :: Variable -> Decoder (WriterT w m) Bool Source #

(Monad m, MonadSAT m) => MonadSAT (ContT s m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (ContT s m) :: Type -> Type Source #

Methods

fresh :: ContT s m Literal Source #

fresh_forall :: ContT s m Literal Source #

emit :: Clause -> ContT s m () Source #

note :: String -> ContT s m () Source #

decode_variable :: Variable -> Decoder (ContT s m) Bool Source #

(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (RWST r w s m) :: Type -> Type Source #

Methods

fresh :: RWST r w s m Literal Source #

fresh_forall :: RWST r w s m Literal Source #

emit :: Clause -> RWST r w s m () Source #

note :: String -> RWST r w s m () Source #

decode_variable :: Variable -> Decoder (RWST r w s m) Bool Source #

(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m) Source # 
Instance details

Defined in Satchmo.MonadSAT

Associated Types

type Decoder (RWST r w s m) :: Type -> Type Source #

Methods

fresh :: RWST r w s m Literal Source #

fresh_forall :: RWST r w s m Literal Source #

emit :: Clause -> RWST r w s m () Source #

note :: String -> RWST r w s m () Source #

decode_variable :: Variable -> Decoder (RWST r w s m) Bool Source #

type Weight = Int Source #

data Header Source #

Constructors

Header 

Fields

Instances

Instances details
Show Header Source # 
Instance details

Defined in Satchmo.MonadSAT

Methods

showsPrec :: Int -> Header -> ShowS #

show :: Header -> String #

showList :: [Header] -> ShowS #