ersatz-0.3: 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) 
Or (Seq Bit) 
Xor Bit Bit 
Mux Bit Bit Bit 
Not Bit 
Var !Literal 

assert :: (MonadState s m, HasSAT s) => 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

true :: b Source

false :: b Source

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

Logical conjunction.

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

Logical disjunction (inclusive or).

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

Logical implication.

not :: b -> b Source

Logical negation

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, Boolean b) => (a -> b) -> t a -> b Source

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

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

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

xor :: b -> b -> b Source

Exclusive-or

choose Source

Arguments

:: b

False branch

-> b

True branch

-> b

Predicate/selector branch

-> b 

Choose between two alternatives based on a selector bit.