Copyright	(c) Eddie Jones 2020
License	BSD-3
Maintainer	eddiejones2108@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.ZSDD

Contents

Diagrams
Propositions

Description

Zero suppressed decision diagrams provide an efficient representation of boolean formulas build from atomic propositions or atoms.

Warning

The space used by a diagram can grows with each operation due to the cache.

Implementation

Internally it is a directed acyclic graph, thereby allowing for sharing of subterms. Operations have a monotonic effect on the diagram and their results are cached. The implementations was outlined by this paper:

Shin-ichi Minato, "Zero-suppressed BDDs for set manipulation in combinatorial problems", DAC '93: Proceedings of the 30th international Design Automation Conference https://dl.acm.org/doi/10.1145/157485.164890

Synopsis

data Diagram d a m r
runDiagram :: Monad m => (forall d. Diagram d a m r) -> m r
data Prop d a
- = Top
- | Bot
class Invertible a
atomic :: (Ord a, Hashable a, Monad m) => a -> Diagram d a m (Prop d a)
negate :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Diagram d a m (Prop d a)
assign :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
union :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
intersect :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
difference :: (Ord a, Invertible a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
isEmpty :: Monad m => Prop d a -> Diagram d a m Bool
isNotEmpty :: Monad m => Prop d a -> Diagram d a m Bool
count :: Monad m => Prop d a -> Diagram d a m Int
mapAtom :: (Eq a, Hashable a, Monad m) => (a -> a) -> Prop d a -> Diagram d a m (Prop d a)
bindAtom :: (Eq a, Hashable a, Monad m) => (a -> Diagram d a m (Prop d a)) -> Prop d a -> Diagram d a m (Prop d a)

Diagrams

data Diagram d a m r Source #

The ambient decision diagram of propositions.

The type parameter d is the diagrams existential labelled and should not be instantiated by a concrete type

Instances

Instances details

Monad m => Monad (Diagram d a m) Source #
Instance details Defined in Data.ZSDD.Internal Methods (>>=) :: Diagram d a m a0 -> (a0 -> Diagram d a m b) -> Diagram d a m b # (>>) :: Diagram d a m a0 -> Diagram d a m b -> Diagram d a m b # return :: a0 -> Diagram d a m a0 #
Functor m => Functor (Diagram d a m) Source #
Instance details Defined in Data.ZSDD.Internal Methods fmap :: (a0 -> b) -> Diagram d a m a0 -> Diagram d a m b # (<$) :: a0 -> Diagram d a m b -> Diagram d a m a0 #
Monad m => Applicative (Diagram d a m) Source #
Instance details Defined in Data.ZSDD.Internal Methods pure :: a0 -> Diagram d a m a0 # (<>) :: Diagram d a m (a0 -> b) -> Diagram d a m a0 -> Diagram d a m b # liftA2 :: (a0 -> b -> c) -> Diagram d a m a0 -> Diagram d a m b -> Diagram d a m c # (>) :: Diagram d a m a0 -> Diagram d a m b -> Diagram d a m b # (<*) :: Diagram d a m a0 -> Diagram d a m b -> Diagram d a m a0 #

runDiagram :: Monad m => (forall d. Diagram d a m r) -> m r Source #

Extract information that does not depend on the digram

Propositions

data Prop d a Source #

A proposition parameterised by it's diagram and atom type

Constructors

Top
Bot

Instances

Instances details

Eq (Prop d a) Source #
Instance details Defined in Data.ZSDD.Internal Methods (==) :: Prop d a -> Prop d a -> Bool # (/=) :: Prop d a -> Prop d a -> Bool #
Ord (Prop d a) Source #
Instance details Defined in Data.ZSDD.Internal Methods compare :: Prop d a -> Prop d a -> Ordering # (<) :: Prop d a -> Prop d a -> Bool # (<=) :: Prop d a -> Prop d a -> Bool # (>) :: Prop d a -> Prop d a -> Bool # (>=) :: Prop d a -> Prop d a -> Bool # max :: Prop d a -> Prop d a -> Prop d a # min :: Prop d a -> Prop d a -> Prop d a #
Generic (Prop d a) Source #
Instance details Defined in Data.ZSDD.Internal Associated Types type Rep (Prop d a) :: Type -> Type # Methods from :: Prop d a -> Rep (Prop d a) x # to :: Rep (Prop d a) x -> Prop d a #
Hashable (Prop d a) Source #
Instance details Defined in Data.ZSDD.Internal Methods hashWithSalt :: Int -> Prop d a -> Int # hash :: Prop d a -> Int #
type Rep (Prop d a) Source #
Instance details Defined in Data.ZSDD.Internal type Rep (Prop d a) = D1 ('MetaData "Prop" "Data.ZSDD.Internal" "zsdd-0.1.0.0-inplace" 'False) (C1 ('MetaCons "Top" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Bot" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ID" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ID))))

class Invertible a Source #

Atom types where every atom has an inverse. This is only required by the difference operation

Minimal complete definition

neg

Construction

atomic :: (Ord a, Hashable a, Monad m) => a -> Diagram d a m (Prop d a) Source #

Construct a proposition from an atom

negate :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Diagram d a m (Prop d a) Source #

Negate every occurance of an atom

assign :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Bool -> Diagram d a m (Prop d a) Source #

Instantiating an atom

union :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a) Source #

Union of two propositions

intersect :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a) Source #

Intersection of two propositions

difference :: (Ord a, Invertible a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a) Source #

Difference between two propositions

Query

isEmpty :: Monad m => Prop d a -> Diagram d a m Bool Source #

Does the proposition have any models?

isNotEmpty :: Monad m => Prop d a -> Diagram d a m Bool Source #

Does the proposition have any models?

count :: Monad m => Prop d a -> Diagram d a m Int Source #

Count the number of models

Map

mapAtom :: (Eq a, Hashable a, Monad m) => (a -> a) -> Prop d a -> Diagram d a m (Prop d a) Source #

Map between atoms

bindAtom :: (Eq a, Hashable a, Monad m) => (a -> Diagram d a m (Prop d a)) -> Prop d a -> Diagram d a m (Prop d a) Source #

Instantiate an atom with a non-atomic proposition