ersatz-0.4: 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 #

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 # 

Methods

showsPrec :: Int -> Bit -> ShowS #

show :: Bit -> String #

showList :: [Bit] -> ShowS #

Variable Bit # 

Methods

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

Codec Bit # 

Associated Types

type Decoded Bit :: * #

Methods

decode :: MonadPlus f => Solution -> Bit -> f (Decoded Bit) #

encode :: Decoded Bit -> Bit #

Boolean 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 # 

Methods

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

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

Orderable Bit # 

Methods

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

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

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

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

HasBits Bit # 

Methods

bits :: Bit -> Bits #

type Decoded Bit # 

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 #

false :: b #

(&&) :: 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 :: b -> b -> b -> 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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 #