Copyright | (c) Eddie Jones 2020 |
---|---|
License | BSD-3 |
Maintainer | eddiejones2108@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
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
- 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
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
Monad m => Monad (Diagram d a m) Source # | |
Functor m => Functor (Diagram d a m) Source # | |
Monad m => Applicative (Diagram d a m) Source # | |
Defined in Data.ZSDD.Internal 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
A proposition parameterised by it's diagram and atom type
Instances
Eq (Prop d a) Source # | |
Ord (Prop d a) Source # | |
Defined in Data.ZSDD.Internal | |
Generic (Prop d a) Source # | |
Hashable (Prop d a) Source # | |
Defined in Data.ZSDD.Internal | |
type Rep (Prop d a) Source # | |
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
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
isNotEmpty :: Monad m => Prop d a -> Diagram d a m Bool Source #
Does the proposition have any models?