F.applyCase(t1->G1,..,tp->Gp) apply MDD Gi if F=ti, thus we must have p=|terminals|
F.applyCase(t1->G1,..,tp->Gp) apply MDD Gi if F=ti, thus we must have p=|terminals|
gives for each terminal ti of F the corresponding alternative
the resulting MDD after application of alternatives
apply the case operator by giving the alternative in order according to the mdd terminals order
apply the case operator by giving the alternative in order according to the mdd terminals order
alternative fo terminal i
the resulting MDD
If the selector is a node then we apply the formula of "Algorithms for Discrete Function Manipulation" (doi: 10.1109/ICCAD.1990.129849) F.applyCase(t1->G1,..,tp->Gp)= (v, v1->F.coFactor(v,v1).applyCase(t1->G1.cofactor(v,v1),...,tp->Gp.cofactor(v,v1)), ..., vn->F.coFactor(v,vn).applyCase(t1->G1.cofactor(v,vn),...,tp->Gp.cofactor(v,vn))) where v is the lowest var in {F,G1,...,Gp} and its domain is {v1..vn} and terminal is a subset of {t1,...,tp}.
If the selector is a node then we apply the formula of "Algorithms for Discrete Function Manipulation" (doi: 10.1109/ICCAD.1990.129849) F.applyCase(t1->G1,..,tp->Gp)= (v, v1->F.coFactor(v,v1).applyCase(t1->G1.cofactor(v,v1),...,tp->Gp.cofactor(v,v1)), ..., vn->F.coFactor(v,vn).applyCase(t1->G1.cofactor(v,vn),...,tp->Gp.cofactor(v,vn))) where v is the lowest var in {F,G1,...,Gp} and its domain is {v1..vn} and terminal is a subset of {t1,...,tp}. Indeed for an applyCase, the MDD is build only if for each possible terminal the alternative is specified
the resulting MDD after application of alternatives
apply the case operator by setting all terminals alternatives which are not in altsMap to the default value
apply the case operator by setting all terminals alternatives which are not in altsMap to the default value
the alternative map
the default value
the resulting MDD
apply the case operator by setting all terminals alternatives which are not in altsMap to the trash terminal
apply the case operator by setting all terminals alternatives which are not in altsMap to the trash terminal
the alternative map
the resulting MDD
For a node(w,kid1,...kidp) the coFactor over v=vi could be : -himself if the v < w (since v will not appear in kids) -kidi if v = w (since the decision is done on this label) -(w,kid1.coFactor(v=vi),...,kidp.coFactor(v=vi)) if v > w (since v could appear in kids we must rebuild a node where the decision v=vi has been applied)
For a node(w,kid1,...kidp) the coFactor over v=vi could be : -himself if the v < w (since v will not appear in kids) -kidi if v = w (since the decision is done on this label) -(w,kid1.coFactor(v=vi),...,kidp.coFactor(v=vi)) if v > w (since v could appear in kids we must rebuild a node where the decision v=vi has been applied)
the label to assign
the value to assign
the coFactor of this BDD
Reference based equality.
Reference based equality.
the kids for each possible value of topVar (accessible from the main MDDMap)
the decision label of this Node
adds all the path to the terminal as forbidden values and returns the result
adds all the path to the terminal as forbidden values and returns the result
the terminal to remove
adds all the path to the terminal as forbidden values and returns the result
adds all the path to the terminal as forbidden values and returns the result
the terminals to remove
(Changed in version 2.9.0) The behavior of scanRight
has changed. The previous behavior can be reproduced with scanRight.reverse.
(Changed in version 2.9.0) transpose
throws an IllegalArgumentException
if collections are not uniformly sized.
case class for Node of a MDD