Satchmo.Boolean

Documentation

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

Associated Types

type Decoder m :: * -> *

Methods

fresh :: m Literal

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

Defined in Satchmo.SAT.External

Associated Types

type Decoder SAT :: Type -> Type

Methods

fresh :: SAT Literal

fresh_forall :: SAT Literal

emit :: Clause -> SAT ()

note :: String -> SAT ()

decode_variable :: Variable -> Decoder SAT Bool

MonadSAT SAT

Defined in Satchmo.SAT.Mini

Associated Types

type Decoder SAT :: Type -> Type

Methods

fresh :: SAT Literal

fresh_forall :: SAT Literal

emit :: Clause -> SAT ()

note :: String -> SAT ()

decode_variable :: Variable -> Decoder SAT Bool

MonadSAT SAT

Defined in Satchmo.SAT.Tmpfile

Associated Types

type Decoder SAT :: Type -> Type

Methods

fresh :: SAT Literal

fresh_forall :: SAT Literal

emit :: Clause -> SAT ()

note :: String -> SAT ()

decode_variable :: Variable -> Decoder SAT Bool

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: ListT m Literal

fresh_forall :: ListT m Literal

emit :: Clause -> ListT m ()

note :: String -> ListT m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: ReaderT r m Literal

fresh_forall :: ReaderT r m Literal

emit :: Clause -> ReaderT r m ()

note :: String -> ReaderT r m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: StateT s m Literal

fresh_forall :: StateT s m Literal

emit :: Clause -> StateT s m ()

note :: String -> StateT s m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: StateT s m Literal

fresh_forall :: StateT s m Literal

emit :: Clause -> StateT s m ()

note :: String -> StateT s m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: WriterT w m Literal

fresh_forall :: WriterT w m Literal

emit :: Clause -> WriterT w m ()

note :: String -> WriterT w m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: WriterT w m Literal

fresh_forall :: WriterT w m Literal

emit :: Clause -> WriterT w m ()

note :: String -> WriterT w m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: ContT s m Literal

fresh_forall :: ContT s m Literal

emit :: Clause -> ContT s m ()

note :: String -> ContT s m ()

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: RWST r w s m Literal

fresh_forall :: RWST r w s m Literal

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

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

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

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

Defined in Satchmo.MonadSAT

Associated Types

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

Methods

fresh :: RWST r w s m Literal

fresh_forall :: RWST r w s m Literal

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

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

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

data Boolean

Constructors

Boolean

Fields

• encode :: !Literal

Constant

Fields

• value :: !Bool

Instances

Generic Boolean

Defined in Satchmo.Boolean.Data

Associated Types

type Rep Boolean :: Type -> Type

Methods

from :: Boolean -> Rep Boolean x

to :: Rep Boolean x -> Boolean

Show Boolean

Defined in Satchmo.Boolean.Data

Methods

showsPrec :: Int -> Boolean -> ShowS

show :: Boolean -> String

showList :: [Boolean] -> ShowS

Eq Boolean

Defined in Satchmo.Boolean.Data

Methods

(==) :: Boolean -> Boolean -> Bool

(/=) :: Boolean -> Boolean -> Bool

Ord Boolean

Defined in Satchmo.Boolean.Data

Methods

compare :: Boolean -> Boolean -> Ordering

(<) :: Boolean -> Boolean -> Bool

(<=) :: Boolean -> Boolean -> Bool

(>) :: Boolean -> Boolean -> Bool

(>=) :: Boolean -> Boolean -> Bool

max :: Boolean -> Boolean -> Boolean

min :: Boolean -> Boolean -> Boolean

Hashable Boolean

Defined in Satchmo.Boolean.Data

Methods

hashWithSalt :: Int -> Boolean -> Int

hash :: Boolean -> Int

Decode SAT Boolean Bool

Defined in Satchmo.SAT.Mini

Methods

decode :: Boolean -> SAT Bool

Decode (Reader (Array Variable Bool)) Boolean Bool

Defined in Satchmo.SAT.Tmpfile

Methods

decode :: Boolean -> Reader (Array Variable Bool) Bool

type Rep Boolean

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)))

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

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