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

Data.ZSDD.Internal

Contents

Diagrams
Internal Nodes
Propositions

Description

WARNING

This module is internal and may be frequently changed.

Synopsis

newtype Diagram d a m r = Diagram {
- getState :: StateT (ID, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int, IntMap (Node d a)) m r
}
data Ops a
- = Atomic a
- | Union ID ID
- | Intersect ID ID
- | Difference ID ID
- | DifferenceT ID
- | Negate ID a
- | Assign ID a Bool
runDiagram :: Monad m => (forall d. Diagram d a m r) -> m r
type ID = Int
data Node d a = Node {
- atom :: a
- lo :: Prop d a
- hi :: Prop d a
}
withNode :: Monad m => ID -> (Node d a -> Diagram d a m r) -> Diagram d a m r
insertNode :: (Eq a, Hashable a, Monad m) => ID -> Node d a -> Diagram d a m ()
lookupNode :: (Eq a, Hashable a, Monad m) => Node d a -> Diagram d a m (Maybe ID)
data Prop d a
- = Top
- | Bot
- | ID ID
class Invertible a where
- neg :: a -> a
makeProp :: (Eq a, Hashable a, Monad m) => Node d a -> Diagram d a m (Prop d 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

newtype 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

Constructors

Diagram
Fields getState :: StateT (ID, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int, IntMap (Node d a)) m r

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 #

data Ops a Source #

Operation DSL for cache

Constructors

Atomic a
Union ID ID
Intersect ID ID
Difference ID ID
DifferenceT ID
Negate ID a
Assign ID a Bool

Instances

Instances details

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

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

Extract information that does not depend on the digram

Internal Nodes

type ID = Int Source #

A unique node identifier

data Node d a Source #

An internal node of the diagram graph

Constructors

Node
Fields atom :: a lo :: Prop d a hi :: Prop d a

Instances

Instances details

Eq a => Eq (Node d a) Source #
Instance details Defined in Data.ZSDD.Internal Methods (==) :: Node d a -> Node d a -> Bool # (/=) :: Node d a -> Node d a -> Bool #
Generic (Node d a) Source #
Instance details Defined in Data.ZSDD.Internal Associated Types type Rep (Node d a) :: Type -> Type # Methods from :: Node d a -> Rep (Node d a) x # to :: Rep (Node d a) x -> Node d a #
Hashable a => Hashable (Node d a) Source #
Instance details Defined in Data.ZSDD.Internal Methods hashWithSalt :: Int -> Node d a -> Int # hash :: Node d a -> Int #
type Rep (Node d a) Source #
Instance details Defined in Data.ZSDD.Internal type Rep (Node d a) = D1 ('MetaData "Node" "Data.ZSDD.Internal" "zsdd-0.1.0.0-inplace" 'False) (C1 ('MetaCons "Node" 'PrefixI 'True) (S1 ('MetaSel ('Just "atom") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Just "lo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Prop d a)) :: S1 ('MetaSel ('Just "hi") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Prop d a)))))

withNode :: Monad m => ID -> (Node d a -> Diagram d a m r) -> Diagram d a m r Source #

Extract internal node information from it's ID

insertNode :: (Eq a, Hashable a, Monad m) => ID -> Node d a -> Diagram d a m () Source #

Insert a new node

lookupNode :: (Eq a, Hashable a, Monad m) => Node d a -> Diagram d a m (Maybe ID) Source #

Find the ID of an existing node

Propositions

data Prop d a Source #

A proposition parameterised by it's diagram and atom type

Constructors

Top
Bot
ID ID

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 where Source #

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

Methods

neg :: a -> a Source #

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

Make a new proposition (if not already present) from a node

Construction

Non-trivial propositions are constructed within a diagram. Although propositions use information from the diagram, they are independant; each operation is applied to the supplied proposition leaving others untouched.

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