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.

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

baseLength :: Base k m a v -> Int

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)

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

Defined in Data.Mapping.Decision

Methods

mempty :: Decision k m a v

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

mconcat :: [Decision k m a v] -> Decision k m a v

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

Defined in Data.Mapping.Decision

Methods

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

sconcat :: NonEmpty (Decision k m a v) -> Decision k m a v

stimes :: Integral b => b -> Decision k m a v -> Decision k m a v

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

Defined in Data.Mapping.Decision

Methods

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

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

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

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

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

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

fromInteger :: Integer -> Decision k m a v

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

Defined in Data.Mapping.Decision

Methods

true :: Decision k m a v

false :: Decision k m a v

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

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

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

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

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

(<-->) :: Decision k m a v -> Decision k m a v -> Decision k m a 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

decisionLength :: Decision k m a v -> Int

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

generalCounts

Arguments

:: (Ord a, Ord n, Mapping k m)

=> (a -> a -> Int)

In the list of decisions, how far apart are these?

-> a

The first possible decision

-> a

The last possible decision

-> (v -> n)

The count of a value

-> (m n -> n)

How to combine counts at a node

-> Decision k m a v

The input decision diagram

-> n

The count

A general counting function

numberTrueGeneral :: Mapping k m => (m Integer -> Integer) -> Int -> Int -> Decision k m Int Bool -> Integer

How many values are true in a decision diagram with integer leaves?

numberTrue :: Int -> Int -> Decision Bool OnBool Int Bool -> Integer

How many values are True in a binary decision diagram with integer leaves?

chunksTrue :: (Mapping k m, FoldableWithIndex k m, Ord k, Ord a) => Decision k m a Bool -> [Map a k]

Assignments of variables that result in True

listTrue :: forall k m a. (Mapping k m, FoldableWithIndex k m, Ord k, Ord a) => Set a -> Decision k m a Bool -> [Map a k]

All true values (may be a very long list even for reasonable Decisions)

bestSuchThat :: (Mapping k m, Ord k, Ord a, Ord v) => (v -> Bool) -> (forall w. a -> m w -> Maybe (k, w)) -> Decision k m a v -> Maybe ([(a, k)], v)

What is the best assignment of keys to values resulting in a value on which p is True?

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 :: (Mapping k m, Ord (m Int), Ord a, Ord v) => a -> m v -> Decision k m a v

A decision tree based on a single decision

genTest :: Boolean b => a -> Decision Bool OnBool a b

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

test :: a -> 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