Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class (Applicative m, Monad m) => MonadSAT m where
- data Boolean
- type Booleans = [Boolean]
- encode :: Boolean -> Literal
- boolean :: MonadSAT m => m Boolean
- exists :: MonadSAT m => m Boolean
- forall :: MonadSAT m => m Boolean
- constant :: MonadSAT m => Bool -> m Boolean
- not :: Boolean -> Boolean
- monadic :: Monad m => ([a] -> m b) -> [m a] -> m b
- assertOr :: MonadSAT m => [Boolean] -> m ()
- assertAnd :: (Foldable t, MonadSAT m) => t Boolean -> m ()
- assert :: MonadSAT m => [Boolean] -> m ()
- constant :: MonadSAT m => Bool -> m Boolean
- and :: MonadSAT m => [Boolean] -> m Boolean
- or :: MonadSAT m => [Boolean] -> m Boolean
- xor :: MonadSAT m => [Boolean] -> m Boolean
- xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
- equals2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
- equals :: MonadSAT m => [Boolean] -> m Boolean
- implies :: MonadSAT m => Boolean -> Boolean -> m Boolean
- (||) :: MonadSAT m => Boolean -> Boolean -> m Boolean
- (&&) :: MonadSAT m => Boolean -> Boolean -> m Boolean
- fun2 :: MonadSAT m => (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
- fun3 :: MonadSAT m => (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> m Boolean
- ifThenElse :: MonadSAT m => Boolean -> m Boolean -> m Boolean -> m Boolean
- ifThenElseM :: MonadSAT m => m Boolean -> m Boolean -> m Boolean -> m Boolean
- assert_fun2 :: MonadSAT m => (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m ()
- assert_fun3 :: MonadSAT m => (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> m ()
- monadic :: Monad m => ([a] -> m b) -> [m a] -> m b
Documentation
class (Applicative m, Monad m) => MonadSAT m where Source #
fresh_forall :: m Literal Source #
emit :: Clause -> m () Source #
note :: String -> m () Source #
emit some note (could be printed by the backend)
Instances
MonadSAT SAT Source # | |
MonadSAT SAT Source # | |
MonadSAT SAT Source # | |
(Monad m, MonadSAT m) => MonadSAT (ListT m) Source # | |
(Monad m, MonadSAT m) => MonadSAT (ReaderT r m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m) => MonadSAT (StateT s m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m) => MonadSAT (StateT s m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m, Monoid w) => MonadSAT (WriterT w m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m) => MonadSAT (ContT s m) Source # | |
(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m) Source # | |
Defined in Satchmo.MonadSAT | |
(Monad m, MonadSAT m, Monoid w) => MonadSAT (RWST r w s m) Source # | |
Defined in Satchmo.MonadSAT |
Instances
Generic Boolean Source # | |
Show Boolean Source # | |
Eq Boolean Source # | |
Ord Boolean Source # | |
Hashable Boolean Source # | |
Defined in Satchmo.Boolean.Data | |
Decode SAT Boolean Bool Source # | |
Decode (Reader (Array Variable Bool)) Boolean Bool Source # | |
type Rep Boolean Source # | |
Defined in Satchmo.Boolean.Data type Rep Boolean = D1 ('MetaData "Boolean" "Satchmo.Boolean.Data" "satchmo-2.9.9.4-Aqsq65NcGJ9IL95KAH1ZK1" 'False) (C1 ('MetaCons "Boolean" 'PrefixI 'True) (S1 ('MetaSel ('Just "encode") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Literal)) :+: C1 ('MetaCons "Constant" 'PrefixI 'True) (S1 ('MetaSel ('Just "value") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))) |
fun2 :: MonadSAT m => (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean Source #
implement the function by giving a full CNF that determines the outcome
fun3 :: MonadSAT m => (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> m Boolean Source #
implement the function by giving a full CNF that determines the outcome