smcdel-1.3.0: Symbolic Model Checking for Dynamic Epistemic Logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

SMCDEL.Internal.TaggedBDD

Synopsis

Tagged BDDs

class TagForBDDs a where Source #

Operations on tagged BDDs. The tag a is meant to be an empty type.

Minimal complete definition

Nothing

Methods

multiplier :: Tagged a Bdd -> Int Source #

How many copies of the vocabulary do we have? This is the number of markers + 1.

unmvBdd :: Tagged a Bdd -> Bdd Source #

Move back, must be without markers!

mv :: Bdd -> Tagged a Bdd Source #

Move into double vocabulary, but do not add marker

cp :: Bdd -> Tagged a Bdd Source #

Move into extended vocabulary, add one marker

cpMany :: Int -> Bdd -> Tagged a Bdd Source #

Move into extended vocabulary, add k many markers, MUST be available!

tagBddEval :: [Prp] -> Tagged a Bdd -> Bool Source #

Evaluate a tagged BDD.

Instances

Instances details
TagForBDDs Dubbel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Dubbel Bdd -> Int Source #

unmvBdd :: Tagged Dubbel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Dubbel Bdd Source #

cp :: Bdd -> Tagged Dubbel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Dubbel Bdd Source #

tagBddEval :: [Prp] -> Tagged Dubbel Bdd -> Bool Source #

TagForBDDs Quadrupel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Quadrupel Bdd -> Int Source #

unmvBdd :: Tagged Quadrupel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Quadrupel Bdd Source #

cp :: Bdd -> Tagged Quadrupel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Quadrupel Bdd Source #

tagBddEval :: [Prp] -> Tagged Quadrupel Bdd -> Bool Source #

TagForBDDs Tripel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Tripel Bdd -> Int Source #

unmvBdd :: Tagged Tripel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Tripel Bdd Source #

cp :: Bdd -> Tagged Tripel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Tripel Bdd Source #

tagBddEval :: [Prp] -> Tagged Tripel Bdd -> Bool Source #

Pre-defined tags

data Dubbel Source #

Tag for BDDs using the duplicated vocabulary \(V \cup V'\).

Instances

Instances details
TagForBDDs Dubbel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Dubbel Bdd -> Int Source #

unmvBdd :: Tagged Dubbel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Dubbel Bdd Source #

cp :: Bdd -> Tagged Dubbel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Dubbel Bdd Source #

tagBddEval :: [Prp] -> Tagged Dubbel Bdd -> Bool Source #

data Tripel Source #

Tag for BDDs using the triple vocabulary \(V \cup V' \cup V''\).

Instances

Instances details
TagForBDDs Tripel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Tripel Bdd -> Int Source #

unmvBdd :: Tagged Tripel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Tripel Bdd Source #

cp :: Bdd -> Tagged Tripel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Tripel Bdd Source #

tagBddEval :: [Prp] -> Tagged Tripel Bdd -> Bool Source #

data Quadrupel Source #

Tag for BDDs using the quadruple vocabulary \(V \cup V' \cup V'' \cup V'''\).

Instances

Instances details
TagForBDDs Quadrupel Source # 
Instance details

Defined in SMCDEL.Internal.TaggedBDD

Methods

multiplier :: Tagged Quadrupel Bdd -> Int Source #

unmvBdd :: Tagged Quadrupel Bdd -> Bdd Source #

mv :: Bdd -> Tagged Quadrupel Bdd Source #

cp :: Bdd -> Tagged Quadrupel Bdd Source #

cpMany :: Int -> Bdd -> Tagged Quadrupel Bdd Source #

tagBddEval :: [Prp] -> Tagged Quadrupel Bdd -> Bool Source #

Generic definition for tagged BDDs

totalRelBdd :: Tagged a Bdd Source #

The total relation as a tagged BDD.

emptyRelBdd :: Tagged a Bdd Source #

The empty relation as a tagged BDD.

allsamebdd :: TagForBDDs a => [Prp] -> Tagged a Bdd Source #

Given a vocabulary, make a tagged BDD to say that each plain variable \(p\) and the corresponding marked variable \(p'\) variable have the same value: \( \wedge_p (p \leftrightarrow p') \). This encodes the identity relation.