ersatz-0.6: A monad for expressing SAT or QSAT problems using observable sharing.
Copyright© Edward Kmett 2010-2014 Johan Kiviniemi 2013
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellTrustworthy
LanguageHaskell2010

Ersatz.Bit

Description

 
Synopsis

Documentation

data Bit Source #

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 :: Type -> Type) s. MonadSAT s m => m Bit) 

Instances

Instances details
Show Bit Source # 
Instance details

Defined in Ersatz.Bit

Methods

showsPrec :: Int -> Bit -> ShowS #

show :: Bit -> String #

showList :: [Bit] -> ShowS #

Boolean Bit Source # 
Instance details

Defined in Ersatz.Bit

Methods

bool :: Bool -> Bit Source #

true :: Bit Source #

false :: Bit Source #

(&&) :: Bit -> Bit -> Bit Source #

(||) :: Bit -> Bit -> Bit Source #

(==>) :: Bit -> Bit -> Bit Source #

not :: Bit -> Bit Source #

and :: Foldable t => t Bit -> Bit Source #

or :: Foldable t => t Bit -> Bit Source #

nand :: Foldable t => t Bit -> Bit Source #

nor :: Foldable t => t Bit -> Bit Source #

all :: Foldable t => (a -> Bit) -> t a -> Bit Source #

any :: Foldable t => (a -> Bit) -> t a -> Bit Source #

xor :: Bit -> Bit -> Bit Source #

choose :: Bit -> Bit -> Bit -> Bit Source #

HasBits Bit Source # 
Instance details

Defined in Ersatz.Bits

Methods

bits :: Bit -> Bits Source #

Codec Bit Source # 
Instance details

Defined in Ersatz.Bit

Associated Types

type Decoded Bit 
Instance details

Defined in Ersatz.Bit

Equatable Bit Source # 
Instance details

Defined in Ersatz.Equatable

Methods

(===) :: Bit -> Bit -> Bit Source #

(/==) :: Bit -> Bit -> Bit Source #

Orderable Bit Source # 
Instance details

Defined in Ersatz.Orderable

Methods

(<?) :: Bit -> Bit -> Bit Source #

(<=?) :: Bit -> Bit -> Bit Source #

(>=?) :: Bit -> Bit -> Bit Source #

(>?) :: Bit -> Bit -> Bit Source #

Variable Bit Source # 
Instance details

Defined in Ersatz.Bit

Methods

literally :: MonadSAT s m => m Literal -> m Bit Source #

type Decoded Bit Source # 
Instance details

Defined in Ersatz.Bit

assert :: MonadSAT s m => Bit -> m () Source #

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

class Boolean b where Source #

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

Minimal complete definition

Nothing

Methods

bool :: Bool -> b Source #

Lift a Bool

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

true :: b Source #

false :: b Source #

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

Logical conjunction.

default (&&) :: (Generic b, GBoolean (Rep b)) => b -> b -> b Source #

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

Logical disjunction (inclusive or).

default (||) :: (Generic b, GBoolean (Rep b)) => b -> b -> b Source #

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

Logical implication.

not :: b -> b Source #

Logical negation

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

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

The logical conjunction of several values.

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

The logical disjunction of several values.

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

The negated logical conjunction of several values.

nand = not . and

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

The negated logical disjunction of several values.

nor = not . or

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

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

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

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

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

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

xor :: b -> b -> b Source #

Exclusive-or

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

choose Source #

Arguments

:: b

False branch

-> b

True branch

-> b

Predicate/selector branch

-> b 

Choose between two alternatives based on a selector bit.

Instances

Instances details
Boolean Bit Source # 
Instance details

Defined in Ersatz.Bit

Methods

bool :: Bool -> Bit Source #

true :: Bit Source #

false :: Bit Source #

(&&) :: Bit -> Bit -> Bit Source #

(||) :: Bit -> Bit -> Bit Source #

(==>) :: Bit -> Bit -> Bit Source #

not :: Bit -> Bit Source #

and :: Foldable t => t Bit -> Bit Source #

or :: Foldable t => t Bit -> Bit Source #

nand :: Foldable t => t Bit -> Bit Source #

nor :: Foldable t => t Bit -> Bit Source #

all :: Foldable t => (a -> Bit) -> t a -> Bit Source #

any :: Foldable t => (a -> Bit) -> t a -> Bit Source #

xor :: Bit -> Bit -> Bit Source #

choose :: Bit -> Bit -> Bit -> Bit Source #

Boolean Bit1 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit1 Source #

true :: Bit1 Source #

false :: Bit1 Source #

(&&) :: Bit1 -> Bit1 -> Bit1 Source #

(||) :: Bit1 -> Bit1 -> Bit1 Source #

(==>) :: Bit1 -> Bit1 -> Bit1 Source #

not :: Bit1 -> Bit1 Source #

and :: Foldable t => t Bit1 -> Bit1 Source #

or :: Foldable t => t Bit1 -> Bit1 Source #

nand :: Foldable t => t Bit1 -> Bit1 Source #

nor :: Foldable t => t Bit1 -> Bit1 Source #

all :: Foldable t => (a -> Bit1) -> t a -> Bit1 Source #

any :: Foldable t => (a -> Bit1) -> t a -> Bit1 Source #

xor :: Bit1 -> Bit1 -> Bit1 Source #

choose :: Bit1 -> Bit1 -> Bit1 -> Bit1 Source #

Boolean Bit2 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit2 Source #

true :: Bit2 Source #

false :: Bit2 Source #

(&&) :: Bit2 -> Bit2 -> Bit2 Source #

(||) :: Bit2 -> Bit2 -> Bit2 Source #

(==>) :: Bit2 -> Bit2 -> Bit2 Source #

not :: Bit2 -> Bit2 Source #

and :: Foldable t => t Bit2 -> Bit2 Source #

or :: Foldable t => t Bit2 -> Bit2 Source #

nand :: Foldable t => t Bit2 -> Bit2 Source #

nor :: Foldable t => t Bit2 -> Bit2 Source #

all :: Foldable t => (a -> Bit2) -> t a -> Bit2 Source #

any :: Foldable t => (a -> Bit2) -> t a -> Bit2 Source #

xor :: Bit2 -> Bit2 -> Bit2 Source #

choose :: Bit2 -> Bit2 -> Bit2 -> Bit2 Source #

Boolean Bit3 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit3 Source #

true :: Bit3 Source #

false :: Bit3 Source #

(&&) :: Bit3 -> Bit3 -> Bit3 Source #

(||) :: Bit3 -> Bit3 -> Bit3 Source #

(==>) :: Bit3 -> Bit3 -> Bit3 Source #

not :: Bit3 -> Bit3 Source #

and :: Foldable t => t Bit3 -> Bit3 Source #

or :: Foldable t => t Bit3 -> Bit3 Source #

nand :: Foldable t => t Bit3 -> Bit3 Source #

nor :: Foldable t => t Bit3 -> Bit3 Source #

all :: Foldable t => (a -> Bit3) -> t a -> Bit3 Source #

any :: Foldable t => (a -> Bit3) -> t a -> Bit3 Source #

xor :: Bit3 -> Bit3 -> Bit3 Source #

choose :: Bit3 -> Bit3 -> Bit3 -> Bit3 Source #

Boolean Bit4 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit4 Source #

true :: Bit4 Source #

false :: Bit4 Source #

(&&) :: Bit4 -> Bit4 -> Bit4 Source #

(||) :: Bit4 -> Bit4 -> Bit4 Source #

(==>) :: Bit4 -> Bit4 -> Bit4 Source #

not :: Bit4 -> Bit4 Source #

and :: Foldable t => t Bit4 -> Bit4 Source #

or :: Foldable t => t Bit4 -> Bit4 Source #

nand :: Foldable t => t Bit4 -> Bit4 Source #

nor :: Foldable t => t Bit4 -> Bit4 Source #

all :: Foldable t => (a -> Bit4) -> t a -> Bit4 Source #

any :: Foldable t => (a -> Bit4) -> t a -> Bit4 Source #

xor :: Bit4 -> Bit4 -> Bit4 Source #

choose :: Bit4 -> Bit4 -> Bit4 -> Bit4 Source #

Boolean Bit5 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit5 Source #

true :: Bit5 Source #

false :: Bit5 Source #

(&&) :: Bit5 -> Bit5 -> Bit5 Source #

(||) :: Bit5 -> Bit5 -> Bit5 Source #

(==>) :: Bit5 -> Bit5 -> Bit5 Source #

not :: Bit5 -> Bit5 Source #

and :: Foldable t => t Bit5 -> Bit5 Source #

or :: Foldable t => t Bit5 -> Bit5 Source #

nand :: Foldable t => t Bit5 -> Bit5 Source #

nor :: Foldable t => t Bit5 -> Bit5 Source #

all :: Foldable t => (a -> Bit5) -> t a -> Bit5 Source #

any :: Foldable t => (a -> Bit5) -> t a -> Bit5 Source #

xor :: Bit5 -> Bit5 -> Bit5 Source #

choose :: Bit5 -> Bit5 -> Bit5 -> Bit5 Source #

Boolean Bit6 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit6 Source #

true :: Bit6 Source #

false :: Bit6 Source #

(&&) :: Bit6 -> Bit6 -> Bit6 Source #

(||) :: Bit6 -> Bit6 -> Bit6 Source #

(==>) :: Bit6 -> Bit6 -> Bit6 Source #

not :: Bit6 -> Bit6 Source #

and :: Foldable t => t Bit6 -> Bit6 Source #

or :: Foldable t => t Bit6 -> Bit6 Source #

nand :: Foldable t => t Bit6 -> Bit6 Source #

nor :: Foldable t => t Bit6 -> Bit6 Source #

all :: Foldable t => (a -> Bit6) -> t a -> Bit6 Source #

any :: Foldable t => (a -> Bit6) -> t a -> Bit6 Source #

xor :: Bit6 -> Bit6 -> Bit6 Source #

choose :: Bit6 -> Bit6 -> Bit6 -> Bit6 Source #

Boolean Bit7 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit7 Source #

true :: Bit7 Source #

false :: Bit7 Source #

(&&) :: Bit7 -> Bit7 -> Bit7 Source #

(||) :: Bit7 -> Bit7 -> Bit7 Source #

(==>) :: Bit7 -> Bit7 -> Bit7 Source #

not :: Bit7 -> Bit7 Source #

and :: Foldable t => t Bit7 -> Bit7 Source #

or :: Foldable t => t Bit7 -> Bit7 Source #

nand :: Foldable t => t Bit7 -> Bit7 Source #

nor :: Foldable t => t Bit7 -> Bit7 Source #

all :: Foldable t => (a -> Bit7) -> t a -> Bit7 Source #

any :: Foldable t => (a -> Bit7) -> t a -> Bit7 Source #

xor :: Bit7 -> Bit7 -> Bit7 Source #

choose :: Bit7 -> Bit7 -> Bit7 -> Bit7 Source #

Boolean Bit8 Source # 
Instance details

Defined in Ersatz.Bits

Methods

bool :: Bool -> Bit8 Source #

true :: Bit8 Source #

false :: Bit8 Source #

(&&) :: Bit8 -> Bit8 -> Bit8 Source #

(||) :: Bit8 -> Bit8 -> Bit8 Source #

(==>) :: Bit8 -> Bit8 -> Bit8 Source #

not :: Bit8 -> Bit8 Source #

and :: Foldable t => t Bit8 -> Bit8 Source #

or :: Foldable t => t Bit8 -> Bit8 Source #

nand :: Foldable t => t Bit8 -> Bit8 Source #

nor :: Foldable t => t Bit8 -> Bit8 Source #

all :: Foldable t => (a -> Bit8) -> t a -> Bit8 Source #

any :: Foldable t => (a -> Bit8) -> t a -> Bit8 Source #

xor :: Bit8 -> Bit8 -> Bit8 Source #

choose :: Bit8 -> Bit8 -> Bit8 -> Bit8 Source #

Boolean Bool Source # 
Instance details

Defined in Ersatz.Bit

Methods

bool :: Bool -> Bool Source #

true :: Bool Source #

false :: Bool Source #

(&&) :: Bool -> Bool -> Bool Source #

(||) :: Bool -> Bool -> Bool Source #

(==>) :: Bool -> Bool -> Bool Source #

not :: Bool -> Bool Source #

and :: Foldable t => t Bool -> Bool Source #

or :: Foldable t => t Bool -> Bool Source #

nand :: Foldable t => t Bool -> Bool Source #

nor :: Foldable t => t Bool -> Bool Source #

all :: Foldable t => (a -> Bool) -> t a -> Bool Source #

any :: Foldable t => (a -> Bool) -> t a -> Bool Source #

xor :: Bool -> Bool -> Bool Source #

choose :: Bool -> Bool -> Bool -> Bool Source #