summaryrefslogtreecommitdiffstats
path: root/abc70930/src/bdd/cudd/cuddZddFuncs.c
diff options
context:
space:
mode:
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddZddFuncs.c')
-rw-r--r--abc70930/src/bdd/cudd/cuddZddFuncs.c1603
1 files changed, 1603 insertions, 0 deletions
diff --git a/abc70930/src/bdd/cudd/cuddZddFuncs.c b/abc70930/src/bdd/cudd/cuddZddFuncs.c
new file mode 100644
index 00000000..9dc27a95
--- /dev/null
+++ b/abc70930/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 */