Data.Diagram.Simple

Reduced Ordered Binary Decision Diagrams

Diagram

data Diagram l s a

A binary decision diagram

Instances

Monad (Diagram l s)

Defined in Data.Diagram.Simple

Methods

(>>=) :: Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b

(>>) :: Diagram l s a -> Diagram l s b -> Diagram l s b

return :: a -> Diagram l s a

Functor (Diagram l s)

Defined in Data.Diagram.Simple

Methods

fmap :: (a -> b) -> Diagram l s a -> Diagram l s b

(<$) :: a -> Diagram l s b -> Diagram l s a

Applicative (Diagram l s)

Defined in Data.Diagram.Simple

Methods

pure :: a -> Diagram l s a

(<*>) :: Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b

liftA2 :: (a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c

(*>) :: Diagram l s a -> Diagram l s b -> Diagram l s b

(<*) :: Diagram l s a -> Diagram l s b -> Diagram l s a

runDiagram :: (forall s. Diagram l s a) -> a

Extract non-diagrammatic information

Propositions

data Prop l s

A diagramatic proposition build on atomic propositions of type l

Instances

Eq (Prop l s)

Defined in Data.Diagram.Simple

Methods

(==) :: Prop l s -> Prop l s -> Bool

(/=) :: Prop l s -> Prop l s -> Bool

Ord (Prop l s)

Defined in Data.Diagram.Simple

Methods

compare :: Prop l s -> Prop l s -> Ordering

(<) :: Prop l s -> Prop l s -> Bool

(<=) :: Prop l s -> Prop l s -> Bool

(>) :: Prop l s -> Prop l s -> Bool

(>=) :: Prop l s -> Prop l s -> Bool

max :: Prop l s -> Prop l s -> Prop l s

min :: Prop l s -> Prop l s -> Prop l s

true :: Prop l s

Simple propositions

false :: Prop l s

Simple propositions

atom :: (Hashable l, Eq l) => l -> Diagram l s (Prop l s)

Construct a diagramatic proposition from an atom

notAtom :: (Hashable l, Eq l) => l -> Diagram l s (Prop l s)

Construct a diagramatic proposition from an atom

mapAtom :: (Eq l, Hashable l) => (l -> l) -> Prop l s -> Diagram l s (Prop l s)

Map atoms in proposition

bindAtom :: (Ord l, Hashable l) => Prop l s -> (l -> Diagram l s (Prop l s)) -> Diagram l s (Prop l s)

Replace an atom with a non-terminal in a Prop sub-diagram

Combinations

and :: (Ord l, Hashable l) => Prop l s -> Prop l s -> Diagram l s (Prop l s)

Lift boolean and to diagramatic proposition

or :: (Ord l, Hashable l) => Prop l s -> Prop l s -> Diagram l s (Prop l s)

Lift boolean or to diagramatic proposition

not :: (Ord l, Hashable l) => Prop l s -> Diagram l s (Prop l s)

Lift boolean not to diagramatic proposition

restrict :: (Hashable l, Ord l) => l -> Bool -> Prop l s -> Diagram l s (Prop l s)

Assign an atomic proposition a boolean value

Summary

fold :: (Hashable l, Eq l) => (l -> b -> b -> b) -> (Bool -> b) -> Prop l s -> Diagram l s b

Create a summary value of a proposition

anySat :: (Hashable l, Eq l) => Prop l s -> Diagram l s Bool

Determine if a proposition is satisfiable

 anySat = fold (\_ p q -> p || q) id