Ersatz.Bit

Documentation

newtype Bit

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

Constructors

Bit (Circuit Bit)

Instances

Show Bit

Typeable Bit

Variable Bit

Encoding Bit

Decoding Bit

Boolean Bit

Equatable Bit

assert :: MonadSAT m => Bit -> m ()

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

class Boolean t 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 -> t

Lift a Bool

true :: t

true = bool True

false :: t

false = bool False

(&&) :: t -> t -> t

Logical conjunction.

(||) :: t -> t -> t

Logical disjunction (inclusive or).

(==>) :: t -> t -> t

Logical implication.

not :: t -> t

Logical negation

and :: [t] -> t

The logical conjunction of several values.

or :: [t] -> t

The logical disjunction of several values.

nand :: [t] -> t

The negated logical conjunction of several values.

nand = not . and

nor :: [t] -> t

The negated logical disjunction of several values.

nor = not . or

xor :: t -> t -> t

Exclusive-or

choose

Arguments

:: t

False branch

-> t

True branch

-> t

Predicate/selector branch

-> t

Choose between two alternatives based on a selector bit.

Instances

Boolean Bool

Boolean Bit

Boolean Bit8

Boolean Bit7

Boolean Bit6

Boolean Bit5

Boolean Bit4

Boolean Bit3

Boolean Bit2

Boolean Bit1