Satchmo.Boolean

Documentation

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

Associated Types

type Decoder m :: * -> *

Methods

fresh, fresh_forall :: m Literal

emit :: Clause -> m ()

note :: String -> m ()

emit some note (could be printed by the backend)

decode_variable :: Variable -> Decoder m Bool

Instances

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)

data Boolean

Constructors

Boolean

Fields

encode :: !Literal

Constant

Fields

value :: !Bool

Instances

Eq Boolean

Ord Boolean

Show Boolean

Generic Boolean

Hashable Boolean

Memoizable Boolean

Decode SAT Boolean Bool

type Rep Boolean

type Booleans = [Boolean]

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

implement the function by giving a full CNF that determines the outcome

fun3 :: MonadSAT m => (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> m Boolean

implement the function by giving a full CNF that determines the outcome

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