From e7b544f11151f09a4a3fbe39b4a176795a82f677 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 13:42:25 -0800 Subject: Upgrade to the latest CUDD 2.4.2. --- src/bdd/cudd/cuddZddFuncs.c | 1298 ++++++++++++++++++++++--------------------- 1 file changed, 664 insertions(+), 634 deletions(-) (limited to 'src/bdd/cudd/cuddZddFuncs.c') diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c index 2560159c..41f7c64c 100644 --- a/src/bdd/cudd/cuddZddFuncs.c +++ b/src/bdd/cudd/cuddZddFuncs.c @@ -7,53 +7,81 @@ Synopsis [Functions to manipulate covers represented as ZDDs.] Description [External procedures included in this module: - - Internal procedures included in this module: - - Static procedures included in this module: - - ] + + Internal procedures included in this module: + + Static procedures included in this module: + + ] 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.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -74,7 +102,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.16 2008/04/25 07:39:33 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -113,17 +141,17 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23: SeeAlso [Cudd_zddUnateProduct] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddProduct( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddProduct(dd, f, g); + dd->reordered = 0; + res = cuddZddProduct(dd, f, g); } while (dd->reordered == 1); return(res); @@ -144,17 +172,17 @@ Cudd_zddProduct( SeeAlso [Cudd_zddProduct] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddUnateProduct( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddUnateProduct(dd, f, g); + dd->reordered = 0; + res = cuddZddUnateProduct(dd, f, g); } while (dd->reordered == 1); return(res); @@ -178,17 +206,17 @@ Cudd_zddUnateProduct( SeeAlso [Cudd_zddDivide] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddWeakDiv( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddWeakDiv(dd, f, g); + dd->reordered = 0; + res = cuddZddWeakDiv(dd, f, g); } while (dd->reordered == 1); return(res); @@ -209,17 +237,17 @@ Cudd_zddWeakDiv( SeeAlso [Cudd_zddWeakDiv] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddDivide( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddDivide(dd, f, g); + dd->reordered = 0; + res = cuddZddDivide(dd, f, g); } while (dd->reordered == 1); return(res); @@ -238,17 +266,17 @@ Cudd_zddDivide( SeeAlso [Cudd_zddWeakDiv] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddWeakDivF( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddWeakDivF(dd, f, g); + dd->reordered = 0; + res = cuddZddWeakDivF(dd, f, g); } while (dd->reordered == 1); return(res); @@ -267,17 +295,17 @@ Cudd_zddWeakDivF( SeeAlso [] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddDivideF( DdManager * dd, DdNode * f, DdNode * g) { - DdNode *res; + DdNode *res; do { - dd->reordered = 0; - res = cuddZddDivideF(dd, f, g); + dd->reordered = 0; + res = cuddZddDivideF(dd, f, g); } while (dd->reordered == 1); return(res); @@ -300,26 +328,26 @@ Cudd_zddDivideF( SeeAlso [] ******************************************************************************/ -DdNode * +DdNode * Cudd_zddComplement( DdManager *dd, DdNode *node) { - DdNode *b, *isop, *zdd_I; + DdNode *b, *isop, *zdd_I; /* Check cache */ zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); if (zdd_I) - return(zdd_I); + return(zdd_I); b = Cudd_MakeBddFromZddCover(dd, node); if (!b) - return(NULL); + 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_RecursiveDeref(dd, b); + return(NULL); } Cudd_Ref(isop); Cudd_Ref(zdd_I); @@ -348,21 +376,21 @@ Cudd_zddComplement( SeeAlso [Cudd_zddProduct] ******************************************************************************/ -DdNode * +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; + 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) @@ -376,26 +404,26 @@ cuddZddProduct( top_g = dd->permZ[g->index]; if (top_f > top_g) - return(cuddZddProduct(dd, g, f)); + return(cuddZddProduct(dd, g, f)); /* Check cache */ r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g); if (r) - return(r); + return(r); - v = f->index; /* either yi or zi */ + v = f->index; /* either yi or zi */ flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); if (flag == 1) - return(NULL); + 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_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); } Cudd_Ref(g1); Cudd_Ref(g0); @@ -405,95 +433,95 @@ cuddZddProduct( 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_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_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_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_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_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_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_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); @@ -501,35 +529,35 @@ cuddZddProduct( 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_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_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_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); @@ -538,30 +566,30 @@ cuddZddProduct( 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_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_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_RecursiveDerefZdd(dd, N0); + Cudd_RecursiveDerefZdd(dd, R1); + return(NULL); } Cudd_Ref(N1); Cudd_RecursiveDerefZdd(dd, R1); @@ -585,20 +613,20 @@ cuddZddProduct( SeeAlso [Cudd_zddUnateProduct] ******************************************************************************/ -DdNode * +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; + 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) @@ -612,68 +640,68 @@ cuddZddUnateProduct( top_g = dd->permZ[g->index]; if (top_f > top_g) - return(cuddZddUnateProduct(dd, g, f)); + return(cuddZddUnateProduct(dd, g, f)); /* Check cache */ r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g); if (r) - return(r); + return(r); - v = f->index; /* either yi or zi */ + v = f->index; /* either yi or zi */ flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); if (flag == 1) - return(NULL); + 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_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_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_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_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_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); @@ -682,30 +710,30 @@ cuddZddUnateProduct( 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_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_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_RecursiveDerefZdd(dd, term4); + Cudd_RecursiveDerefZdd(dd, sum2); + return(NULL); } Cudd_Ref(r); Cudd_RecursiveDerefZdd(dd, sum2); @@ -729,47 +757,47 @@ cuddZddUnateProduct( SeeAlso [Cudd_zddWeakDiv] ******************************************************************************/ -DdNode * +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; + 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); + return(f); if (f == zero || f == one) - return(zero); + return(zero); if (f == g) - return(one); + return(one); /* Check cache. */ r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g); if (r) - return(r); + return(r); v = g->index; flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); if (flag == 1) - return(NULL); + 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_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); } Cudd_Ref(g1); Cudd_Ref(g0); @@ -778,98 +806,98 @@ cuddZddWeakDiv( 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); + 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_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); + cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero); + Cudd_Deref(q); + return(zero); } - 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); + + 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); } - Cudd_Ref(q); - Cudd_RecursiveDerefZdd(dd, tmp); - } } else { - Cudd_RecursiveDerefZdd(dd, f1); - Cudd_RecursiveDerefZdd(dd, g1); + 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); + 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, 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); - 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); + 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); } - Cudd_Ref(q); - Cudd_RecursiveDerefZdd(dd, tmp); - } } else { - Cudd_RecursiveDerefZdd(dd, fd); - Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); } cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q); @@ -890,34 +918,34 @@ cuddZddWeakDiv( SeeAlso [Cudd_zddWeakDivF] ******************************************************************************/ -DdNode * +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; + 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); + return(f); if (f == zero || f == one) - return(zero); + return(zero); if (f == g) - return(one); + return(one); /* Check cache. */ r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g); if (r) - return(r); + return(r); top_f = dd->permZ[f->index]; top_g = dd->permZ[g->index]; @@ -926,87 +954,87 @@ cuddZddWeakDivF( 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) { + 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); - 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); + 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); - return(NULL); - } - Cudd_Ref(tmp); - Cudd_RecursiveDerefZdd(dd, term0); - Cudd_RecursiveDerefZdd(dd, termd); - q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */ - if (q == NULL) { + 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); - return(NULL); - } - Cudd_Ref(q); - Cudd_RecursiveDerefZdd(dd, term1); - Cudd_RecursiveDerefZdd(dd, tmp); - cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); - Cudd_Deref(q); - return(q); + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); + Cudd_Deref(q); + return(q); } if (v == top_f) - v = f->index; + v = f->index; else - v = g->index; + v = g->index; flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd); if (flag == 1) - return(NULL); + 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_RecursiveDerefZdd(dd, f1); + Cudd_RecursiveDerefZdd(dd, f0); + Cudd_RecursiveDerefZdd(dd, fd); + return(NULL); } Cudd_Ref(g1); Cudd_Ref(g0); @@ -1015,98 +1043,98 @@ cuddZddWeakDivF( 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); + 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_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); + cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero); + Cudd_Deref(q); + return(zero); } - 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); + + 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); } - Cudd_Ref(q); - Cudd_RecursiveDerefZdd(dd, tmp); - } } else { - Cudd_RecursiveDerefZdd(dd, f1); - Cudd_RecursiveDerefZdd(dd, g1); + 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); + 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, 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); - 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); + 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); } - Cudd_Ref(q); - Cudd_RecursiveDerefZdd(dd, tmp); - } } else { - Cudd_RecursiveDerefZdd(dd, fd); - Cudd_RecursiveDerefZdd(dd, gd); + Cudd_RecursiveDerefZdd(dd, fd); + Cudd_RecursiveDerefZdd(dd, gd); } cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q); @@ -1127,81 +1155,81 @@ cuddZddWeakDivF( SeeAlso [Cudd_zddDivide] ******************************************************************************/ -DdNode * +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; + 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); + return(f); if (f == zero || f == one) - return(zero); + return(zero); if (f == g) - return(one); + return(one); /* Check cache. */ r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g); if (r) - return(r); + return(r); v = g->index; flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); if (flag == 1) - return(NULL); + 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_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); + + 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); @@ -1227,81 +1255,81 @@ cuddZddDivide( SeeAlso [Cudd_zddDivideF] ******************************************************************************/ -DdNode * +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; + 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); + return(f); if (f == zero || f == one) - return(zero); + return(zero); if (f == g) - return(one); + return(one); /* Check cache. */ r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g); if (r) - return(r); + return(r); v = g->index; flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0); if (flag == 1) - return(NULL); + 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_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); + + 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); @@ -1321,7 +1349,7 @@ cuddZddDivideF( 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.] + by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.] SideEffects [The results are returned in f1, f0, and fd.] @@ -1337,10 +1365,10 @@ cuddZddGetCofactors3( DdNode ** f0, DdNode ** fd) { - DdNode *pc, *nc; - DdNode *zero = DD_ZERO(dd); - int top, hv, ht, pv, nv; - int level; + 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]; @@ -1348,96 +1376,96 @@ cuddZddGetCofactors3( ht = top >> 1; if (hv < ht) { - *f1 = zero; - *f0 = zero; - *fd = f; + *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); + 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, *f0); + 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_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); + Cudd_Deref(*f1); + Cudd_Deref(*f0); + Cudd_Deref(*fd); } return(0); @@ -1465,11 +1493,11 @@ cuddZddGetCofactors2( { *f1 = cuddZddSubset1(dd, f, v); if (*f1 == NULL) - return(1); + return(1); *f0 = cuddZddSubset0(dd, f, v); if (*f0 == NULL) { - Cudd_RecursiveDerefZdd(dd, *f1); - return(1); + Cudd_RecursiveDerefZdd(dd, *f1); + return(1); } return(0); @@ -1490,26 +1518,26 @@ cuddZddGetCofactors2( SeeAlso [] ******************************************************************************/ -DdNode * +DdNode * cuddZddComplement( DdManager * dd, DdNode *node) { - DdNode *b, *isop, *zdd_I; + DdNode *b, *isop, *zdd_I; /* Check cache */ zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node); if (zdd_I) - return(zdd_I); + return(zdd_I); b = cuddMakeBddFromZddCover(dd, node); if (!b) - return(NULL); + return(NULL); cuddRef(b); isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I); if (!isop) { - Cudd_RecursiveDeref(dd, b); - return(NULL); + Cudd_RecursiveDeref(dd, b); + return(NULL); } cuddRef(isop); cuddRef(zdd_I); @@ -1538,7 +1566,7 @@ cuddZddGetPosVarIndex( DdManager * dd, int index) { - int pv = (index >> 1) << 1; + int pv = (index >> 1) << 1; return(pv); } /* end of cuddZddGetPosVarIndex */ @@ -1559,7 +1587,7 @@ cuddZddGetNegVarIndex( DdManager * dd, int index) { - int nv = index | 0x1; + int nv = index | 0x1; return(nv); } /* end of cuddZddGetPosVarIndex */ @@ -1580,7 +1608,7 @@ cuddZddGetPosVarLevel( DdManager * dd, int index) { - int pv = cuddZddGetPosVarIndex(dd, index); + int pv = cuddZddGetPosVarIndex(dd, index); return(dd->permZ[pv]); } /* end of cuddZddGetPosVarLevel */ @@ -1601,8 +1629,10 @@ cuddZddGetNegVarLevel( DdManager * dd, int index) { - int nv = cuddZddGetNegVarIndex(dd, index); + int nv = cuddZddGetNegVarIndex(dd, index); return(dd->permZ[nv]); } /* end of cuddZddGetNegVarLevel */ + + ABC_NAMESPACE_IMPL_END -- cgit v1.2.3