Copyright	© Edward Kmett 2010-2014 Johan Kiviniemi 2013
License	BSD3
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	Trustworthy
Language	Haskell2010

Ersatz.Bit

Description

Synopsis

data Bit
- = And !(Seq Bit)
- | Xor !Bit !Bit
- | Mux !Bit !Bit !Bit
- | Not !Bit
- | Var !Literal
- | Run (forall m s. (MonadState s m, HasSAT s) => m Bit)
assert :: (MonadState s m, HasSAT s) => Bit -> m ()
class Boolean b where

Documentation

data Bit #

A Bit provides a reference to a possibly indeterminate boolean value that can be determined by an external SAT solver.

Constructors

And !(Seq Bit)
Xor !Bit !Bit
Mux !Bit !Bit !Bit
Not !Bit
Var !Literal
Run (forall m s. (MonadState s m, HasSAT s) => m Bit)

Instances

Show Bit #
Instance details Defined in Ersatz.Bit Methods showsPrec :: Int -> Bit -> ShowS # show :: Bit -> String # showList :: [Bit] -> ShowS #
Codec Bit #
Instance details Defined in Ersatz.Bit Associated Types type Decoded Bit :: * # Methods decode :: MonadPlus f => Solution -> Bit -> f (Decoded Bit) # encode :: Decoded Bit -> Bit #
Variable Bit #
Instance details Defined in Ersatz.Bit Methods literally :: (HasSAT s, MonadState s m) => m Literal -> m Bit #
Boolean Bit #
Instance details Defined in Ersatz.Bit Methods bool :: Bool -> Bit # true :: Bit # false :: Bit # (&&) :: Bit -> Bit -> Bit # (\|\|) :: Bit -> Bit -> Bit # (==>) :: Bit -> Bit -> Bit # not :: Bit -> Bit # and :: Foldable t => t Bit -> Bit # or :: Foldable t => t Bit -> Bit # nand :: Foldable t => t Bit -> Bit # nor :: Foldable t => t Bit -> Bit # all :: Foldable t => (a -> Bit) -> t a -> Bit # any :: Foldable t => (a -> Bit) -> t a -> Bit # xor :: Bit -> Bit -> Bit # choose :: Bit -> Bit -> Bit -> Bit #
Equatable Bit #
Instance details Defined in Ersatz.Equatable Methods (===) :: Bit -> Bit -> Bit # (/==) :: Bit -> Bit -> Bit #
Orderable Bit #
Instance details Defined in Ersatz.Orderable Methods (<?) :: Bit -> Bit -> Bit # (<=?) :: Bit -> Bit -> Bit # (>=?) :: Bit -> Bit -> Bit # (>?) :: Bit -> Bit -> Bit #
HasBits Bit #
Instance details Defined in Ersatz.Bits Methods bits :: Bit -> Bits #
type Decoded Bit #
Instance details Defined in Ersatz.Bit type Decoded Bit = Bool

assert :: (MonadState s m, HasSAT s) => Bit -> m () #

Assert claims that Bit must be true in any satisfying interpretation of the current problem.

class Boolean b where #

The normal Bool operators in Haskell are not overloaded. This provides a richer set that are.

Instances for this class for product-like types can be automatically derived for any type that is an instance of Generic

Methods

bool :: Bool -> b #

Lift a Bool

true :: b #

true = bool True

false :: b #

false = bool False

(&&) :: b -> b -> b infixr 3 #

Logical conjunction.

(||) :: b -> b -> b infixr 2 #

Logical disjunction (inclusive or).

(==>) :: b -> b -> b infixr 0 #

Logical implication.

not :: b -> b #

Logical negation

and :: Foldable t => t b -> b #

The logical conjunction of several values.

or :: Foldable t => t b -> b #

The logical disjunction of several values.

nand :: Foldable t => t b -> b #

The negated logical conjunction of several values.

nand = not . and

nor :: Foldable t => t b -> b #

The negated logical disjunction of several values.

nor = not . or

all :: Foldable t => (a -> b) -> t a -> b #

The logical conjunction of the mapping of a function over several values.

any :: Foldable t => (a -> b) -> t a -> b #

The logical disjunction of the mapping of a function over several values.

xor :: b -> b -> b #

Exclusive-or

choose #

Arguments

:: b	False branch
-> b	True branch
-> b	Predicate/selector branch
-> b

Choose between two alternatives based on a selector bit.

bool :: (Generic b, GBoolean (Rep b)) => Bool -> b #

Lift a Bool

(&&) :: (Generic b, GBoolean (Rep b)) => b -> b -> b infixr 3 #

Logical conjunction.

(||) :: (Generic b, GBoolean (Rep b)) => b -> b -> b infixr 2 #

Logical disjunction (inclusive or).

not :: (Generic b, GBoolean (Rep b)) => b -> b #

Logical negation

all :: (Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b #

The logical conjunction of the mapping of a function over several values.

any :: (Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b #

The logical disjunction of the mapping of a function over several values.

xor :: (Generic b, GBoolean (Rep b)) => b -> b -> b #

Exclusive-or

Instances

Boolean Bool #
Instance details Defined in Ersatz.Bit Methods bool :: Bool -> Bool # true :: Bool # false :: Bool # (&&) :: Bool -> Bool -> Bool # (\|\|) :: Bool -> Bool -> Bool # (==>) :: Bool -> Bool -> Bool # not :: Bool -> Bool # and :: Foldable t => t Bool -> Bool # or :: Foldable t => t Bool -> Bool # nand :: Foldable t => t Bool -> Bool # nor :: Foldable t => t Bool -> Bool # all :: Foldable t => (a -> Bool) -> t a -> Bool # any :: Foldable t => (a -> Bool) -> t a -> Bool # xor :: Bool -> Bool -> Bool # choose :: Bool -> Bool -> Bool -> Bool #
Boolean Bit #
Instance details Defined in Ersatz.Bit Methods bool :: Bool -> Bit # true :: Bit # false :: Bit # (&&) :: Bit -> Bit -> Bit # (\|\|) :: Bit -> Bit -> Bit # (==>) :: Bit -> Bit -> Bit # not :: Bit -> Bit # and :: Foldable t => t Bit -> Bit # or :: Foldable t => t Bit -> Bit # nand :: Foldable t => t Bit -> Bit # nor :: Foldable t => t Bit -> Bit # all :: Foldable t => (a -> Bit) -> t a -> Bit # any :: Foldable t => (a -> Bit) -> t a -> Bit # xor :: Bit -> Bit -> Bit # choose :: Bit -> Bit -> Bit -> Bit #
Boolean Bit8 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit8 # true :: Bit8 # false :: Bit8 # (&&) :: Bit8 -> Bit8 -> Bit8 # (\|\|) :: Bit8 -> Bit8 -> Bit8 # (==>) :: Bit8 -> Bit8 -> Bit8 # not :: Bit8 -> Bit8 # and :: Foldable t => t Bit8 -> Bit8 # or :: Foldable t => t Bit8 -> Bit8 # nand :: Foldable t => t Bit8 -> Bit8 # nor :: Foldable t => t Bit8 -> Bit8 # all :: Foldable t => (a -> Bit8) -> t a -> Bit8 # any :: Foldable t => (a -> Bit8) -> t a -> Bit8 # xor :: Bit8 -> Bit8 -> Bit8 # choose :: Bit8 -> Bit8 -> Bit8 -> Bit8 #
Boolean Bit7 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit7 # true :: Bit7 # false :: Bit7 # (&&) :: Bit7 -> Bit7 -> Bit7 # (\|\|) :: Bit7 -> Bit7 -> Bit7 # (==>) :: Bit7 -> Bit7 -> Bit7 # not :: Bit7 -> Bit7 # and :: Foldable t => t Bit7 -> Bit7 # or :: Foldable t => t Bit7 -> Bit7 # nand :: Foldable t => t Bit7 -> Bit7 # nor :: Foldable t => t Bit7 -> Bit7 # all :: Foldable t => (a -> Bit7) -> t a -> Bit7 # any :: Foldable t => (a -> Bit7) -> t a -> Bit7 # xor :: Bit7 -> Bit7 -> Bit7 # choose :: Bit7 -> Bit7 -> Bit7 -> Bit7 #
Boolean Bit6 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit6 # true :: Bit6 # false :: Bit6 # (&&) :: Bit6 -> Bit6 -> Bit6 # (\|\|) :: Bit6 -> Bit6 -> Bit6 # (==>) :: Bit6 -> Bit6 -> Bit6 # not :: Bit6 -> Bit6 # and :: Foldable t => t Bit6 -> Bit6 # or :: Foldable t => t Bit6 -> Bit6 # nand :: Foldable t => t Bit6 -> Bit6 # nor :: Foldable t => t Bit6 -> Bit6 # all :: Foldable t => (a -> Bit6) -> t a -> Bit6 # any :: Foldable t => (a -> Bit6) -> t a -> Bit6 # xor :: Bit6 -> Bit6 -> Bit6 # choose :: Bit6 -> Bit6 -> Bit6 -> Bit6 #
Boolean Bit5 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit5 # true :: Bit5 # false :: Bit5 # (&&) :: Bit5 -> Bit5 -> Bit5 # (\|\|) :: Bit5 -> Bit5 -> Bit5 # (==>) :: Bit5 -> Bit5 -> Bit5 # not :: Bit5 -> Bit5 # and :: Foldable t => t Bit5 -> Bit5 # or :: Foldable t => t Bit5 -> Bit5 # nand :: Foldable t => t Bit5 -> Bit5 # nor :: Foldable t => t Bit5 -> Bit5 # all :: Foldable t => (a -> Bit5) -> t a -> Bit5 # any :: Foldable t => (a -> Bit5) -> t a -> Bit5 # xor :: Bit5 -> Bit5 -> Bit5 # choose :: Bit5 -> Bit5 -> Bit5 -> Bit5 #
Boolean Bit4 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit4 # true :: Bit4 # false :: Bit4 # (&&) :: Bit4 -> Bit4 -> Bit4 # (\|\|) :: Bit4 -> Bit4 -> Bit4 # (==>) :: Bit4 -> Bit4 -> Bit4 # not :: Bit4 -> Bit4 # and :: Foldable t => t Bit4 -> Bit4 # or :: Foldable t => t Bit4 -> Bit4 # nand :: Foldable t => t Bit4 -> Bit4 # nor :: Foldable t => t Bit4 -> Bit4 # all :: Foldable t => (a -> Bit4) -> t a -> Bit4 # any :: Foldable t => (a -> Bit4) -> t a -> Bit4 # xor :: Bit4 -> Bit4 -> Bit4 # choose :: Bit4 -> Bit4 -> Bit4 -> Bit4 #
Boolean Bit3 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit3 # true :: Bit3 # false :: Bit3 # (&&) :: Bit3 -> Bit3 -> Bit3 # (\|\|) :: Bit3 -> Bit3 -> Bit3 # (==>) :: Bit3 -> Bit3 -> Bit3 # not :: Bit3 -> Bit3 # and :: Foldable t => t Bit3 -> Bit3 # or :: Foldable t => t Bit3 -> Bit3 # nand :: Foldable t => t Bit3 -> Bit3 # nor :: Foldable t => t Bit3 -> Bit3 # all :: Foldable t => (a -> Bit3) -> t a -> Bit3 # any :: Foldable t => (a -> Bit3) -> t a -> Bit3 # xor :: Bit3 -> Bit3 -> Bit3 # choose :: Bit3 -> Bit3 -> Bit3 -> Bit3 #
Boolean Bit2 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit2 # true :: Bit2 # false :: Bit2 # (&&) :: Bit2 -> Bit2 -> Bit2 # (\|\|) :: Bit2 -> Bit2 -> Bit2 # (==>) :: Bit2 -> Bit2 -> Bit2 # not :: Bit2 -> Bit2 # and :: Foldable t => t Bit2 -> Bit2 # or :: Foldable t => t Bit2 -> Bit2 # nand :: Foldable t => t Bit2 -> Bit2 # nor :: Foldable t => t Bit2 -> Bit2 # all :: Foldable t => (a -> Bit2) -> t a -> Bit2 # any :: Foldable t => (a -> Bit2) -> t a -> Bit2 # xor :: Bit2 -> Bit2 -> Bit2 # choose :: Bit2 -> Bit2 -> Bit2 -> Bit2 #
Boolean Bit1 #
Instance details Defined in Ersatz.Bits Methods bool :: Bool -> Bit1 # true :: Bit1 # false :: Bit1 # (&&) :: Bit1 -> Bit1 -> Bit1 # (\|\|) :: Bit1 -> Bit1 -> Bit1 # (==>) :: Bit1 -> Bit1 -> Bit1 # not :: Bit1 -> Bit1 # and :: Foldable t => t Bit1 -> Bit1 # or :: Foldable t => t Bit1 -> Bit1 # nand :: Foldable t => t Bit1 -> Bit1 # nor :: Foldable t => t Bit1 -> Bit1 # all :: Foldable t => (a -> Bit1) -> t a -> Bit1 # any :: Foldable t => (a -> Bit1) -> t a -> Bit1 # xor :: Bit1 -> Bit1 -> Bit1 # choose :: Bit1 -> Bit1 -> Bit1 -> Bit1 #