Data.Mapping.Decision

Decision diagrams, parametric in the mapping type for the decisions.

This is inspired by binary decision diagrams (as described in detail in Knuth's The Art of Computer Programming, volume 4A); these are the specific case where m is BoolMapping and v is Bool. Our algorithms are mostly straightforward generalisations of those considered there.

TODO * Decisions go upwards in order currently, I believe; should they go downwards, to coincide with lexicographical orderings on maps and hence maybe make smaller decision diagrams? We can use Down if necessary to amend this * Increase test coverage * Examples: - finding optima - finding random elements (as examples of the more general functions, already coded, I hope) * Separate out various stuff into other modules? * Reformat types * Refactor by changing order of arguments of addLeaf and addNode and simplifying Might even want a more general Node, for even greater simplicity Could use a pair instead of node. * Documentation * Tidy out any commented-out code

MAYBE TO DO * Implement the two monadic algorithms? * Comment on a more efficient mapping algorithm * Composition algorithm? composite :: (a -> Decision k m v w) -> Decision k m a v -> Decision k m a w ??? * Optimisation by reordering

Documentation

data Node k m a

A node of a decision diagram: which value do we scrutinise, and what do we do with it?

Constructors

Node

Fields

• nodeDecision :: !a
• nodeBranch :: !(m Int)

Instances

(Eq a, Eq (m Int)) => Eq (Node k2 m a)

Defined in Data.Mapping.Decision

Methods

(==) :: Node k2 m a -> Node k2 m a -> Bool

(/=) :: Node k2 m a -> Node k2 m a -> Bool

(Ord a, Ord (m Int)) => Ord (Node k2 m a)

Defined in Data.Mapping.Decision

Methods

compare :: Node k2 m a -> Node k2 m a -> Ordering

(<) :: Node k2 m a -> Node k2 m a -> Bool

(<=) :: Node k2 m a -> Node k2 m a -> Bool

(>) :: Node k2 m a -> Node k2 m a -> Bool

(>=) :: Node k2 m a -> Node k2 m a -> Bool

max :: Node k2 m a -> Node k2 m a -> Node k2 m a

min :: Node k2 m a -> Node k2 m a -> Node k2 m a

data Base k m a v

A decision diagram (with no preferred starting point), containing leaves (representing final values of the decision process) indexed from -1 downwards, and nodes (representing the need to scrutinise a value) indexed from 0 upwards

Constructors

Base

Fields

• leaves :: Seq v
• nodes :: Seq (Node k m a)

Instances

Foldable (Base k2 m a)

Folds over *all* the leaves; not something you want to do to an arbitrary base

Defined in Data.Mapping.Decision

Methods

fold :: Monoid m0 => Base k2 m a m0 -> m0

foldMap :: Monoid m0 => (a0 -> m0) -> Base k2 m a a0 -> m0

foldMap' :: Monoid m0 => (a0 -> m0) -> Base k2 m a a0 -> m0

foldr :: (a0 -> b -> b) -> b -> Base k2 m a a0 -> b

foldr' :: (a0 -> b -> b) -> b -> Base k2 m a a0 -> b

foldl :: (b -> a0 -> b) -> b -> Base k2 m a a0 -> b

foldl' :: (b -> a0 -> b) -> b -> Base k2 m a a0 -> b

foldr1 :: (a0 -> a0 -> a0) -> Base k2 m a a0 -> a0

foldl1 :: (a0 -> a0 -> a0) -> Base k2 m a a0 -> a0

toList :: Base k2 m a a0 -> [a0]

null :: Base k2 m a a0 -> Bool

length :: Base k2 m a a0 -> Int

elem :: Eq a0 => a0 -> Base k2 m a a0 -> Bool

maximum :: Ord a0 => Base k2 m a a0 -> a0

minimum :: Ord a0 => Base k2 m a a0 -> a0

sum :: Num a0 => Base k2 m a a0 -> a0

product :: Num a0 => Base k2 m a a0 -> a0

data Decision k m a v

A decision diagram with a starting point

Constructors

Decision

Fields

• base :: !(Base k m a v)
• start :: !Int

Instances

(Ord a, Ord (m Int), Mapping k m) => Mapping (a -> k) (Decision k m a)

Defined in Data.Mapping.Decision

Methods

cst :: v -> Decision k m a v

act :: Decision k m a v -> (a -> k) -> v

isConst :: Ord v => Decision k m a v -> Maybe v

mtraverse :: (Applicative f, Ord v) => (u -> f v) -> Decision k m a u -> f (Decision k m a v)

mmap :: Ord v => (u -> v) -> Decision k m a u -> Decision k m a v

mergeA :: (Applicative f, Ord w) => (u -> v -> f w) -> Decision k m a u -> Decision k m a v -> f (Decision k m a w)

merge :: Ord w => (u -> v -> w) -> Decision k m a u -> Decision k m a v -> Decision k m a w

Foldable m => Foldable (Decision k2 m a)

Defined in Data.Mapping.Decision

Methods

fold :: Monoid m0 => Decision k2 m a m0 -> m0

foldMap :: Monoid m0 => (a0 -> m0) -> Decision k2 m a a0 -> m0

foldMap' :: Monoid m0 => (a0 -> m0) -> Decision k2 m a a0 -> m0

foldr :: (a0 -> b -> b) -> b -> Decision k2 m a a0 -> b

foldr' :: (a0 -> b -> b) -> b -> Decision k2 m a a0 -> b

foldl :: (b -> a0 -> b) -> b -> Decision k2 m a a0 -> b

foldl' :: (b -> a0 -> b) -> b -> Decision k2 m a a0 -> b

foldr1 :: (a0 -> a0 -> a0) -> Decision k2 m a a0 -> a0

foldl1 :: (a0 -> a0 -> a0) -> Decision k2 m a a0 -> a0

toList :: Decision k2 m a a0 -> [a0]

null :: Decision k2 m a a0 -> Bool

length :: Decision k2 m a a0 -> Int

elem :: Eq a0 => a0 -> Decision k2 m a a0 -> Bool

maximum :: Ord a0 => Decision k2 m a a0 -> a0

minimum :: Ord a0 => Decision k2 m a a0 -> a0

sum :: Num a0 => Decision k2 m a a0 -> a0

product :: Num a0 => Decision k2 m a a0 -> a0

(Mapping k m, Neighbourly m, Ord a, Ord (m Int)) => Neighbourly (Decision k m a)

Defined in Data.Mapping.Decision

Methods

neighbours :: Ord v => Decision k m a v -> Set (v, v)

(Eq a, Eq v, Mapping k m) => Eq (Decision k m a v)

Defined in Data.Mapping.Decision

Methods

(==) :: Decision k m a v -> Decision k m a v -> Bool

(/=) :: Decision k m a v -> Decision k m a v -> Bool

(Ord a, Ord v, Ord (m Int), Mapping k m) => Ord (Decision k m a v)

A ludicrously short definition!

Defined in Data.Mapping.Decision

Methods

compare :: Decision k m a v -> Decision k m a v -> Ordering

(<) :: Decision k m a v -> Decision k m a v -> Bool

(<=) :: Decision k m a v -> Decision k m a v -> Bool

(>) :: Decision k m a v -> Decision k m a v -> Bool

(>=) :: Decision k m a v -> Decision k m a v -> Bool

max :: Decision k m a v -> Decision k m a v -> Decision k m a v

min :: Decision k m a v -> Decision k m a v -> Decision k m a v

data BaseMap v

A value for every node of a base

Constructors

BaseMap

Fields

• onLeaves :: Seq v
• onNodes :: Seq v

bindex :: BaseMap v -> Int -> v

Index a BaseMap

closure :: (Int -> IntSet) -> IntSet -> IntSet

Close a set under an operation

baseRecurse

Arguments

:: (Ord c, Mapping k m)

=> (v -> c)

What to do on a value

-> (a -> m c -> c)

What do do on a node

-> Base k m a v

Input base

-> BaseMap c

A general kind of recursive function on a Base

decisionRecurse

Arguments

:: (Ord c, Mapping k m)

=> (v -> c)

What to do on a value

-> (a -> m c -> c)

What do do on a node

-> Decision k m a v

Input decision

-> c

A general kind of recursive function on a Decision

genCounts :: (Ord a, Ord n, Mapping k m) => (v -> n) -> (a -> a -> n -> n) -> (m n -> n) -> a -> a -> Decision k m a v -> n

A general counting function

Not sure if this is the best way of laying this out

numberTrue :: Integral a => a -> a -> Decision Bool OnBool a Bool -> Integer

How many values are True in a binary decision diagram?

fromKeyVals :: Foldable f => f (Int, a) -> Seq a

Build a sequence from key-value pairs; we take on trust that all values are represented once.

data Builder o k m a v

A data structure for work-in-progress decision diagrams

Constructors

Builder

Fields

• leavesMap :: Map v Int
• nodesMap :: Map (Node k m a) Int
• fromOld :: Map o Int

emptyBuilder :: Builder o k m a v

addLeaf :: (Ord o, Ord v) => v -> o -> Builder o k m a v -> Builder o k m a v

addNode :: (Ord o, Ord (m Int), Ord a, Mapping k m) => a -> m o -> o -> Builder o k m a v -> Builder o k m a v

makeBuilder :: (Mapping k m, Ord o, Ord (m Int), Ord a, Ord v) => Map o v -> Map o (a, m o) -> Builder o k m a v

buildBase :: Builder o k m a v -> Base k m a v

buildDecision :: Ord o => o -> Builder o k m a v -> Decision k m a v

singleNode :: (Ord v, Mapping k m) => a -> m v -> Decision k m a v

genTest :: Boolean b => a -> AlgebraWrapper (a -> Bool) (Decision Bool OnBool a) b

A building block for BDD's - tests if a variable is true

Again, would be nice to remove the AlgebraWrapper

test :: a -> AlgebraWrapper (a -> Bool) (Decision Bool OnBool a) Bool

Test if a variable is true (specialised to Bool)

buildAll :: Mapping k m => Map a (m Bool) -> Decision k m a Bool

Rapidly take the conjunction of the inputs

buildAny :: Mapping k m => Map a (m Bool) -> Decision k m a Bool

Rapidly take the disjunction of the inputs

baseTraverse :: (Applicative f, Ord a, Ord (m Int), Ord w, Mapping k m) => (v -> f w) -> Base k m a v -> f (Builder Int k m a w)

Traverse bases

baseMap :: (Ord a, Ord (m Int), Ord w, Mapping k m) => (v -> w) -> Base k m a v -> Builder Int k m a w

Map bases

baseTransform :: (Ord a, Ord (n Int), Mapping l n, Ord w) => (v -> w) -> (forall x. a -> m x -> n x) -> Base k m a v -> IntSet -> Builder Int l n a w

A more general map for Base, where the shape of nodes can change

decisionTransform :: (Mapping l n, Ord (n Int), Ord a, Ord w) => (v -> w) -> (forall x. a -> m x -> n x) -> Decision k m a v -> Decision l n a w

A more general map for Decision, where the shape of nodes can change

restrict :: (Ord (m Int), Ord v, Ord a, Mapping k m) => (a -> Maybe k) -> Decision k m a v -> Decision k m a v

Fill in some values of a map > act (restrict h d) f = let > f' x = case h x of > Just y -> y > Nothing -> f x > in act d f'

baseGenMerge :: (Ord a, Ord w, Ord (o Int), Mapping l o) => (u -> v -> w) -> (forall x. Ord x => a -> m x -> o x) -> (forall y. Ord y => a -> n y -> o y) -> (forall x y. (Ord x, Ord y) => a -> m x -> n y -> o (x, y)) -> Base h m a u -> Base k n a v -> Set (Int, Int) -> Builder (Int, Int) l o a w

A general function for merging bases

baseMergeA :: (Applicative f, Ord a, Ord w, Ord (m Int), Mapping k m) => (u -> v -> f w) -> Base k m a u -> Base k m a v -> Set (Int, Int) -> f (Builder (Int, Int) k m a w)

Merge two bases in an applicative functor

baseMerge :: (Ord a, Ord w, Ord (m Int), Mapping k m) => (u -> v -> w) -> Base k m a u -> Base k m a v -> Set (Int, Int) -> Builder (Int, Int) k m a w

Merge two bases

checkBijection :: (Eq a, Eq v, Mapping k m) => Base k m a v -> Base k m a v -> Bij -> Maybe Bij

Attempt to extend to a bijection

findBijection :: (Eq a, Eq v, Mapping k m) => Decision k m a v -> Decision k m a v -> Maybe Bij

Are these Decisions isomorphic?

debugShow :: (Show a, Show v, Show (m Int)) => Decision k m a v -> String

Output the structure of a Decision