diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddFuncs.c')
| -rw-r--r-- | src/bdd/cudd/cuddZddFuncs.c | 1603 |
1 files changed, 1603 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c new file mode 100644 index 00000000..9dc27a95 --- /dev/null +++ b/src/bdd/cudd/cuddZddFuncs.c @@ -0,0 +1,1603 @@ +/**CFile*********************************************************************** + + FileName [cuddZddFuncs.c] + + PackageName [cudd] + + Synopsis [Functions to manipulate covers represented as ZDDs.] + + Description [External procedures included in this module: + <ul> + <li> Cudd_zddProduct(); + <li> Cudd_zddUnateProduct(); + <li> Cudd_zddWeakDiv(); + <li> Cudd_zddWeakDivF(); + <li> Cudd_zddDivide(); + <li> Cudd_zddDivideF(); + <li> Cudd_zddComplement(); + </ul> + Internal procedures included in this module: + <ul> + <li> cuddZddProduct(); + <li> cuddZddUnateProduct(); + <li> cuddZddWeakDiv(); + <li> cuddZddWeakDivF(); + <li> cuddZddDivide(); + <li> cuddZddDivideF(); + <li> cuddZddGetCofactors3() + <li> cuddZddGetCofactors2() + <li> cuddZddComplement(); + <li> cuddZddGetPosVarIndex(); + <li> cuddZddGetNegVarIndex(); + <li> cuddZddGetPosVarLevel(); + <li> cuddZddGetNegVarLevel(); + </ul> + Static procedures included in this module: + <ul> + </ul> + ] + + SeeAlso [] + + Author [In-Ho Moon] + + Copyright [ This file was created at the University of Colorado at + Boulder. The University of Colorado at Boulder makes no warranty + about the suitability of this software for any purpose. It is + presented on an AS IS basis.] + +******************************************************************************/ + +#include "util_hack.h" +#include "cuddInt.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Computes the product of two covers represented by ZDDs.] + + Description [Computes the product of two covers represented by + ZDDs. The result is also a ZDD. Returns a pointer to the result if + successful; NULL otherwise. The covers on which Cudd_zddProduct + operates use two ZDD variables for each function variable (one ZDD + variable for each literal of the variable). Those two ZDD variables + should be adjacent in the order.] + + SideEffects [None] + + SeeAlso [Cudd_zddUnateProduct] + +******************************************************************************/ +DdNode * +Cudd_zddProduct( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddProduct(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddProduct */ + + +/**Function******************************************************************** + + Synopsis [Computes the product of two unate covers.] + + Description [Computes the product of two unate covers represented as + ZDDs. Unate covers use one ZDD variable for each BDD + variable. Returns a pointer to the result if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_zddProduct] + +******************************************************************************/ +DdNode * +Cudd_zddUnateProduct( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddUnateProduct(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddUnateProduct */ + + +/**Function******************************************************************** + + Synopsis [Applies weak division to two covers.] + + Description [Applies weak division to two ZDDs representing two + covers. Returns a pointer to the ZDD representing the result if + successful; NULL otherwise. The result of weak division depends on + the variable order. The covers on which Cudd_zddWeakDiv operates use + two ZDD variables for each function variable (one ZDD variable for + each literal of the variable). Those two ZDD variables should be + adjacent in the order.] + + SideEffects [None] + + SeeAlso [Cudd_zddDivide] + +******************************************************************************/ +DdNode * +Cudd_zddWeakDiv( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddWeakDiv(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddWeakDiv */ + + +/**Function******************************************************************** + + Synopsis [Computes the quotient of two unate covers.] + + Description [Computes the quotient of two unate covers represented + by ZDDs. Unate covers use one ZDD variable for each BDD + variable. Returns a pointer to the resulting ZDD if successful; NULL + otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_zddWeakDiv] + +******************************************************************************/ +DdNode * +Cudd_zddDivide( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddDivide(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddDivide */ + + +/**Function******************************************************************** + + Synopsis [Modified version of Cudd_zddWeakDiv.] + + Description [Modified version of Cudd_zddWeakDiv. This function may + disappear in future releases.] + + SideEffects [None] + + SeeAlso [Cudd_zddWeakDiv] + +******************************************************************************/ +DdNode * +Cudd_zddWeakDivF( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddWeakDivF(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddWeakDivF */ + + +/**Function******************************************************************** + + Synopsis [Modified version of Cudd_zddDivide.] + + Description [Modified version of Cudd_zddDivide. This function may + disappear in future releases.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +Cudd_zddDivideF( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddZddDivideF(dd, f, g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_zddDivideF */ + + +/**Function******************************************************************** + + Synopsis [Computes a complement cover for a ZDD node.] + + Description [Computes a complement cover for a ZDD node. For lack of a + better method, we first extract the function BDD from the ZDD cover, + then make the complement of the ZDD cover from the complement of the + BDD node by using ISOP. Returns a pointer to the resulting cover if + successful; NULL otherwise. The result depends on current variable + order.] + + SideEffects [The result depends on current variable order.] + + SeeAlso [] + +******************************************************************************/ +DdNode * +Cudd_zddComplement( + DdManager *dd, + DdNode *node) +{ + DdNode *b, *isop, *zdd_I; + + /* Check cache */ + zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); + if (zdd_I) + return(zdd_I); + + b = Cudd_MakeBddFromZddCover(dd, node); + if (!b) + return(NULL); + Cudd_Ref(b); + isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); + if (!isop) { + Cudd_RecursiveDeref(dd, b); + return(NULL); + } + Cudd_Ref(isop); + Cudd_Ref(zdd_I); + Cudd_RecursiveDeref(dd, b); + Cudd_RecursiveDeref(dd, isop); + + cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); + Cudd_Deref(zdd_I); + return(zdd_I); +} /* end of Cudd_zddComplement */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddProduct] + +******************************************************************************/ +DdNode * +cuddZddProduct( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v, top_f, top_g; + DdNode *tmp, *term1, *term2, *term3; + DdNode *f0, *f1, *fd, *g0, *g1, *gd; + DdNode *R0, *R1, *Rd, *N0, *N1; + DdNode *r; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + int flag; + int pv, nv; + + statLine(dd); + if (f == zero || g == zero) + return(zero); + if (f == one) + return(g); + if (g == one) + return(f); + + top_f = dd->permZ[f->index]; + top_g = dd->permZ[g->index]; + + if (top_f > top_g) + return(cuddZddProduct(dd, g, f)); + + /* Check cache */ + r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g); + if (r) + return(r); + + v = f->index; /* either yi or zi */ + flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + Cudd_Ref(fd); + flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + Cudd_Ref(gd); + pv = cuddZddGetPosVarIndex(dd, v); + nv = cuddZddGetNegVarIndex(dd, v); + + Rd = cuddZddProduct(dd, fd, gd); + if (Rd == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(Rd); + + term1 = cuddZddProduct(dd, f0, g0); + if (term1 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + return(NULL); + } + Cudd_Ref(term1); + term2 = cuddZddProduct(dd, f0, gd); + if (term2 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + Cudd_RecursiveDerefZdd(dd, term1); + return(NULL); + } + Cudd_Ref(term2); + term3 = cuddZddProduct(dd, fd, g0); + if (term3 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + return(NULL); + } + Cudd_Ref(term3); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g0); + tmp = cuddZddUnion(dd, term1, term2); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + Cudd_RecursiveDerefZdd(dd, term3); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + R0 = cuddZddUnion(dd, tmp, term3); + if (R0 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + Cudd_RecursiveDerefZdd(dd, term3); + Cudd_RecursiveDerefZdd(dd, tmp); + return(NULL); + } + Cudd_Ref(R0); + Cudd_RecursiveDerefZdd(dd, tmp); + Cudd_RecursiveDerefZdd(dd, term3); + N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */ + if (N0 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, Rd); + Cudd_RecursiveDerefZdd(dd, R0); + return(NULL); + } + Cudd_Ref(N0); + Cudd_RecursiveDerefZdd(dd, R0); + Cudd_RecursiveDerefZdd(dd, Rd); + + term1 = cuddZddProduct(dd, f1, g1); + if (term1 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, N0); + return(NULL); + } + Cudd_Ref(term1); + term2 = cuddZddProduct(dd, f1, gd); + if (term2 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, term1); + return(NULL); + } + Cudd_Ref(term2); + term3 = cuddZddProduct(dd, fd, g1); + if (term3 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + return(NULL); + } + Cudd_Ref(term3); + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + tmp = cuddZddUnion(dd, term1, term2); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + Cudd_RecursiveDerefZdd(dd, term3); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + R1 = cuddZddUnion(dd, tmp, term3); + if (R1 == NULL) { + Cudd_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, term3); + Cudd_RecursiveDerefZdd(dd, tmp); + return(NULL); + } + Cudd_Ref(R1); + Cudd_RecursiveDerefZdd(dd, tmp); + Cudd_RecursiveDerefZdd(dd, term3); + N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */ + if (N1 == NULL) { + Cudd_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, R1); + return(NULL); + } + Cudd_Ref(N1); + Cudd_RecursiveDerefZdd(dd, R1); + Cudd_RecursiveDerefZdd(dd, N0); + + cuddCacheInsert2(dd, cuddZddProduct, f, g, N1); + Cudd_Deref(N1); + return(N1); + +} /* end of cuddZddProduct */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddUnateProduct.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddUnateProduct] + +******************************************************************************/ +DdNode * +cuddZddUnateProduct( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v, top_f, top_g; + DdNode *term1, *term2, *term3, *term4; + DdNode *sum1, *sum2; + DdNode *f0, *f1, *g0, *g1; + DdNode *r; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + int flag; + + statLine(dd); + if (f == zero || g == zero) + return(zero); + if (f == one) + return(g); + if (g == one) + return(f); + + top_f = dd->permZ[f->index]; + top_g = dd->permZ[g->index]; + + if (top_f > top_g) + return(cuddZddUnateProduct(dd, g, f)); + + /* Check cache */ + r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g); + if (r) + return(r); + + v = f->index; /* either yi or zi */ + flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + + term1 = cuddZddUnateProduct(dd, f1, g1); + if (term1 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + return(NULL); + } + Cudd_Ref(term1); + term2 = cuddZddUnateProduct(dd, f1, g0); + if (term2 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, term1); + return(NULL); + } + Cudd_Ref(term2); + term3 = cuddZddUnateProduct(dd, f0, g1); + if (term3 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + return(NULL); + } + Cudd_Ref(term3); + term4 = cuddZddUnateProduct(dd, f0, g0); + if (term4 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + Cudd_RecursiveDerefZdd(dd, term3); + return(NULL); + } + Cudd_Ref(term4); + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + sum1 = cuddZddUnion(dd, term1, term2); + if (sum1 == NULL) { + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + Cudd_RecursiveDerefZdd(dd, term3); + Cudd_RecursiveDerefZdd(dd, term4); + return(NULL); + } + Cudd_Ref(sum1); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term2); + sum2 = cuddZddUnion(dd, sum1, term3); + if (sum2 == NULL) { + Cudd_RecursiveDerefZdd(dd, term3); + Cudd_RecursiveDerefZdd(dd, term4); + Cudd_RecursiveDerefZdd(dd, sum1); + return(NULL); + } + Cudd_Ref(sum2); + Cudd_RecursiveDerefZdd(dd, sum1); + Cudd_RecursiveDerefZdd(dd, term3); + r = cuddZddGetNode(dd, v, sum2, term4); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, term4); + Cudd_RecursiveDerefZdd(dd, sum2); + return(NULL); + } + Cudd_Ref(r); + Cudd_RecursiveDerefZdd(dd, sum2); + Cudd_RecursiveDerefZdd(dd, term4); + + cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r); + Cudd_Deref(r); + return(r); + +} /* end of cuddZddUnateProduct */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddWeakDiv.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddWeakDiv] + +******************************************************************************/ +DdNode * +cuddZddWeakDiv( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + DdNode *f0, *f1, *fd, *g0, *g1, *gd; + DdNode *q, *tmp; + DdNode *r; + int flag; + + statLine(dd); + if (g == one) + return(f); + if (f == zero || f == one) + return(zero); + if (f == g) + return(one); + + /* Check cache. */ + r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g); + if (r) + return(r); + + v = g->index; + + flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + Cudd_Ref(fd); + flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + Cudd_Ref(gd); + + q = g; + + if (g0 != zero) { + q = cuddZddWeakDiv(dd, f0, g0); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(q); + } + else + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g0); + + if (q == zero) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); + Cudd_Deref(q); + return(zero); + } + + if (g1 != zero) { + Cudd_RecursiveDerefZdd(dd, q); + tmp = cuddZddWeakDiv(dd, f1, g1); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + if (q == g) + q = tmp; + else { + q = cuddZddIntersect(dd, q, tmp); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + } + else { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + } + + if (q == zero) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); + Cudd_Deref(q); + return(zero); + } + + if (gd != zero) { + Cudd_RecursiveDerefZdd(dd, q); + tmp = cuddZddWeakDiv(dd, fd, gd); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + if (q == g) + q = tmp; + else { + q = cuddZddIntersect(dd, q, tmp); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, tmp); + return(NULL); + } + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + } + else { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + } + + cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q); + Cudd_Deref(q); + return(q); + +} /* end of cuddZddWeakDiv */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddWeakDivF.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddWeakDivF] + +******************************************************************************/ +DdNode * +cuddZddWeakDivF( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v, top_f, top_g, vf, vg; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + DdNode *f0, *f1, *fd, *g0, *g1, *gd; + DdNode *q, *tmp; + DdNode *r; + DdNode *term1, *term0, *termd; + int flag; + int pv, nv; + + statLine(dd); + if (g == one) + return(f); + if (f == zero || f == one) + return(zero); + if (f == g) + return(one); + + /* Check cache. */ + r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g); + if (r) + return(r); + + top_f = dd->permZ[f->index]; + top_g = dd->permZ[g->index]; + vf = top_f >> 1; + vg = top_g >> 1; + v = ddMin(top_f, top_g); + + if (v == top_f && vf < vg) { + v = f->index; + flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + Cudd_Ref(fd); + + pv = cuddZddGetPosVarIndex(dd, v); + nv = cuddZddGetNegVarIndex(dd, v); + + term1 = cuddZddWeakDivF(dd, f1, g); + if (term1 == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); + } + Cudd_Ref(term1); + Cudd_RecursiveDerefZdd(dd, f1); + term0 = cuddZddWeakDivF(dd, f0, g); + if (term0 == NULL) { + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, term1); + return(NULL); + } + Cudd_Ref(term0); + Cudd_RecursiveDerefZdd(dd, f0); + termd = cuddZddWeakDivF(dd, fd, g); + if (termd == NULL) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term0); + return(NULL); + } + Cudd_Ref(termd); + Cudd_RecursiveDerefZdd(dd, fd); + + tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */ + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, term0); + Cudd_RecursiveDerefZdd(dd, termd); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, term0); + Cudd_RecursiveDerefZdd(dd, termd); + q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */ + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, tmp); + return(NULL); + } + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, term1); + Cudd_RecursiveDerefZdd(dd, tmp); + + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); + Cudd_Deref(q); + return(q); + } + + if (v == top_f) + v = f->index; + else + v = g->index; + + flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + Cudd_Ref(fd); + flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd); + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + Cudd_Ref(gd); + + q = g; + + if (g0 != zero) { + q = cuddZddWeakDivF(dd, f0, g0); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(q); + } + else + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g0); + + if (q == zero) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); + Cudd_Deref(q); + return(zero); + } + + if (g1 != zero) { + Cudd_RecursiveDerefZdd(dd, q); + tmp = cuddZddWeakDivF(dd, f1, g1); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + if (q == g) + q = tmp; + else { + q = cuddZddIntersect(dd, q, tmp); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + } + else { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, g1); + } + + if (q == zero) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); + Cudd_Deref(q); + return(zero); + } + + if (gd != zero) { + Cudd_RecursiveDerefZdd(dd, q); + tmp = cuddZddWeakDivF(dd, fd, gd); + if (tmp == NULL) { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + return(NULL); + } + Cudd_Ref(tmp); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + if (q == g) + q = tmp; + else { + q = cuddZddIntersect(dd, q, tmp); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, tmp); + return(NULL); + } + Cudd_Ref(q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + } + else { + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); + } + + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); + Cudd_Deref(q); + return(q); + +} /* end of cuddZddWeakDivF */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddDivide.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddDivide] + +******************************************************************************/ +DdNode * +cuddZddDivide( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + DdNode *f0, *f1, *g0, *g1; + DdNode *q, *r, *tmp; + int flag; + + statLine(dd); + if (g == one) + return(f); + if (f == zero || f == one) + return(zero); + if (f == g) + return(one); + + /* Check cache. */ + r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g); + if (r) + return(r); + + v = g->index; + + flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + + r = cuddZddDivide(dd, f1, g1); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + return(NULL); + } + Cudd_Ref(r); + + if (r != zero && g0 != zero) { + tmp = r; + q = cuddZddDivide(dd, f0, g0); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + return(NULL); + } + Cudd_Ref(q); + r = cuddZddIntersect(dd, r, q); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, q); + return(NULL); + } + Cudd_Ref(r); + Cudd_RecursiveDerefZdd(dd, q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + + cuddCacheInsert2(dd, cuddZddDivide, f, g, r); + Cudd_Deref(r); + return(r); + +} /* end of cuddZddDivide */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_zddDivideF.] + + Description [] + + SideEffects [None] + + SeeAlso [Cudd_zddDivideF] + +******************************************************************************/ +DdNode * +cuddZddDivideF( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + int v; + DdNode *one = DD_ONE(dd); + DdNode *zero = DD_ZERO(dd); + DdNode *f0, *f1, *g0, *g1; + DdNode *q, *r, *tmp; + int flag; + + statLine(dd); + if (g == one) + return(f); + if (f == zero || f == one) + return(zero); + if (f == g) + return(one); + + /* Check cache. */ + r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g); + if (r) + return(r); + + v = g->index; + + flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); + if (flag == 1) + return(NULL); + Cudd_Ref(f1); + Cudd_Ref(f0); + flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0); /* g1 != zero */ + if (flag == 1) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + return(NULL); + } + Cudd_Ref(g1); + Cudd_Ref(g0); + + r = cuddZddDivideF(dd, f1, g1); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + return(NULL); + } + Cudd_Ref(r); + + if (r != zero && g0 != zero) { + tmp = r; + q = cuddZddDivideF(dd, f0, g0); + if (q == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + return(NULL); + } + Cudd_Ref(q); + r = cuddZddIntersect(dd, r, q); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + Cudd_RecursiveDerefZdd(dd, q); + return(NULL); + } + Cudd_Ref(r); + Cudd_RecursiveDerefZdd(dd, q); + Cudd_RecursiveDerefZdd(dd, tmp); + } + + Cudd_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, g1); + Cudd_RecursiveDerefZdd(dd, g0); + + cuddCacheInsert2(dd, cuddZddDivideF, f, g, r); + Cudd_Deref(r); + return(r); + +} /* end of cuddZddDivideF */ + + +/**Function******************************************************************** + + Synopsis [Computes the three-way decomposition of f w.r.t. v.] + + Description [Computes the three-way decomposition of function f (represented + by a ZDD) wit respect to variable v.] + + SideEffects [The results are returned in f1, f0, and fd.] + + SeeAlso [cuddZddGetCofactors2] + +******************************************************************************/ +int +cuddZddGetCofactors3( + DdManager * dd, + DdNode * f, + int v, + DdNode ** f1, + DdNode ** f0, + DdNode ** fd) +{ + DdNode *pc, *nc; + DdNode *zero = DD_ZERO(dd); + int top, hv, ht, pv, nv; + int level; + + top = dd->permZ[f->index]; + level = dd->permZ[v]; + hv = level >> 1; + ht = top >> 1; + + if (hv < ht) { + *f1 = zero; + *f0 = zero; + *fd = f; + } + else { + pv = cuddZddGetPosVarIndex(dd, v); + nv = cuddZddGetNegVarIndex(dd, v); + + /* not to create intermediate ZDD node */ + if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) { + pc = cuddZddSubset1(dd, f, pv); + if (pc == NULL) + return(1); + Cudd_Ref(pc); + nc = cuddZddSubset0(dd, f, pv); + if (nc == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + return(1); + } + Cudd_Ref(nc); + + *f1 = cuddZddSubset0(dd, pc, nv); + if (*f1 == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + return(1); + } + Cudd_Ref(*f1); + *f0 = cuddZddSubset1(dd, nc, nv); + if (*f0 == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + Cudd_RecursiveDerefZdd(dd, *f1); + return(1); + } + Cudd_Ref(*f0); + + *fd = cuddZddSubset0(dd, nc, nv); + if (*fd == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + Cudd_RecursiveDerefZdd(dd, *f1); + Cudd_RecursiveDerefZdd(dd, *f0); + return(1); + } + Cudd_Ref(*fd); + } else { + pc = cuddZddSubset1(dd, f, nv); + if (pc == NULL) + return(1); + Cudd_Ref(pc); + nc = cuddZddSubset0(dd, f, nv); + if (nc == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + return(1); + } + Cudd_Ref(nc); + + *f0 = cuddZddSubset0(dd, pc, pv); + if (*f0 == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + return(1); + } + Cudd_Ref(*f0); + *f1 = cuddZddSubset1(dd, nc, pv); + if (*f1 == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + Cudd_RecursiveDerefZdd(dd, *f1); + return(1); + } + Cudd_Ref(*f1); + + *fd = cuddZddSubset0(dd, nc, pv); + if (*fd == NULL) { + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + Cudd_RecursiveDerefZdd(dd, *f1); + Cudd_RecursiveDerefZdd(dd, *f0); + return(1); + } + Cudd_Ref(*fd); + } + + Cudd_RecursiveDerefZdd(dd, pc); + Cudd_RecursiveDerefZdd(dd, nc); + Cudd_Deref(*f1); + Cudd_Deref(*f0); + Cudd_Deref(*fd); + } + return(0); + +} /* end of cuddZddGetCofactors3 */ + + +/**Function******************************************************************** + + Synopsis [Computes the two-way decomposition of f w.r.t. v.] + + Description [] + + SideEffects [The results are returned in f1 and f0.] + + SeeAlso [cuddZddGetCofactors3] + +******************************************************************************/ +int +cuddZddGetCofactors2( + DdManager * dd, + DdNode * f, + int v, + DdNode ** f1, + DdNode ** f0) +{ + *f1 = cuddZddSubset1(dd, f, v); + if (*f1 == NULL) + return(1); + *f0 = cuddZddSubset0(dd, f, v); + if (*f0 == NULL) { + Cudd_RecursiveDerefZdd(dd, *f1); + return(1); + } + return(0); + +} /* end of cuddZddGetCofactors2 */ + + +/**Function******************************************************************** + + Synopsis [Computes a complement of a ZDD node.] + + Description [Computes the complement of a ZDD node. So far, since we + couldn't find a direct way to get the complement of a ZDD cover, we first + convert a ZDD cover to a BDD, then make the complement of the ZDD cover + from the complement of the BDD node by using ISOP.] + + SideEffects [The result depends on current variable order.] + + SeeAlso [] + +******************************************************************************/ +DdNode * +cuddZddComplement( + DdManager * dd, + DdNode *node) +{ + DdNode *b, *isop, *zdd_I; + + /* Check cache */ + zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); + if (zdd_I) + return(zdd_I); + + b = cuddMakeBddFromZddCover(dd, node); + if (!b) + return(NULL); + cuddRef(b); + isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); + if (!isop) { + Cudd_RecursiveDeref(dd, b); + return(NULL); + } + cuddRef(isop); + cuddRef(zdd_I); + Cudd_RecursiveDeref(dd, b); + Cudd_RecursiveDeref(dd, isop); + + cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I); + cuddDeref(zdd_I); + return(zdd_I); +} /* end of cuddZddComplement */ + + +/**Function******************************************************************** + + Synopsis [Returns the index of positive ZDD variable.] + + Description [Returns the index of positive ZDD variable.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +cuddZddGetPosVarIndex( + DdManager * dd, + int index) +{ + int pv = (index >> 1) << 1; + return(pv); +} /* end of cuddZddGetPosVarIndex */ + + +/**Function******************************************************************** + + Synopsis [Returns the index of negative ZDD variable.] + + Description [Returns the index of negative ZDD variable.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +cuddZddGetNegVarIndex( + DdManager * dd, + int index) +{ + int nv = index | 0x1; + return(nv); +} /* end of cuddZddGetPosVarIndex */ + + +/**Function******************************************************************** + + Synopsis [Returns the level of positive ZDD variable.] + + Description [Returns the level of positive ZDD variable.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +cuddZddGetPosVarLevel( + DdManager * dd, + int index) +{ + int pv = cuddZddGetPosVarIndex(dd, index); + return(dd->permZ[pv]); +} /* end of cuddZddGetPosVarLevel */ + + +/**Function******************************************************************** + + Synopsis [Returns the level of negative ZDD variable.] + + Description [Returns the level of negative ZDD variable.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int +cuddZddGetNegVarLevel( + DdManager * dd, + int index) +{ + int nv = cuddZddGetNegVarIndex(dd, index); + return(dd->permZ[nv]); +} /* end of cuddZddGetNegVarLevel */ |