31 #if __SIZEOF_POINTER__ == 8 37 #include "../DdSpec.hpp" 50 int var2level(
int var)
const {
51 return BDD_LevOfVar(var) - offset;
54 int level2var(
int level)
const {
55 return BDD_VarOfLev(level + offset);
60 : root(f), offset(offset) {
63 int getRoot(ZBDD& f)
const {
66 int level = BDD_LevOfVar(f.Top()) - offset;
67 if (level >= 1)
return level;
69 while (BDD_LevOfVar(f.Top()) >= 1) {
70 f = f.OffSet(BDD_VarOfLev(f.Top()));
72 return (f == 1) ? -1 : 0;
75 int getChild(ZBDD& f,
int level,
int take)
const {
76 int var = BDD_VarOfLev(level + offset);
77 f = take ? f.OnSet0(var) : f.OffSet(var);
79 int nextLevel = BDD_LevOfVar(f.Top()) - offset;
80 assert(nextLevel < level);
81 if (nextLevel >= 1)
return nextLevel;
83 while (BDD_LevOfVar(f.Top()) >= 1) {
84 f = f.OffSet(BDD_VarOfLev(f.Top()));
86 return (f == 1) ? -1 : 0;
89 size_t hashCode(ZBDD
const& f)
const {
90 return const_cast<ZBDD*
>(&f)->GetID();
Abstract class of DD specifications using scalar states.