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/cuddPriority.c | 1628 +++++++++++++++++++++++++++++-------------- 1 file changed, 1091 insertions(+), 537 deletions(-) (limited to 'src/bdd/cudd/cuddPriority.c') diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c index f67fb88a..188d2c9e 100644 --- a/src/bdd/cudd/cuddPriority.c +++ b/src/bdd/cudd/cuddPriority.c @@ -7,39 +7,69 @@ Synopsis [Priority functions.] Description [External procedures included in this file: - - 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 [Fabio Somenzi] - 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.] ******************************************************************************/ @@ -50,10 +80,12 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ +#define DD_DEBUG 1 /*---------------------------------------------------------------------------*/ /* Stucture declarations */ @@ -70,7 +102,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -83,9 +115,9 @@ static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.1.1.1 2003/02/24 22:23: /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int cuddMinHammingDistRecur ARGS((DdNode * f, int *minterm, DdHashTable * table, int upperBound)); -static DdNode * separateCube ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance)); -static DdNode * createResult ARGS((DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance)); +static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound); +static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance); +static DdNode * createResult (DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance); /**AutomaticEnd***************************************************************/ @@ -148,7 +180,7 @@ Cudd_PrioritySelect( DdNode ** z /* array of z variables (optional: may be NULL) */, DdNode * Pi /* BDD of the priority function (optional: may be NULL) */, int n /* size of x, y, and z */, - DdNode * (*Pifunc)(DdManager *, int, DdNode **, DdNode **, DdNode **) /* function used to build Pi if it is NULL */) + DD_PRFP Pifunc /* function used to build Pi if it is NULL */) { DdNode *res = NULL; DdNode *zcube = NULL; @@ -159,38 +191,38 @@ Cudd_PrioritySelect( /* Create z variables if needed. */ if (z == NULL) { - if (Pi != NULL) return(NULL); - z = ABC_ALLOC(DdNode *,n); - if (z == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - createdZ = 1; - for (i = 0; i < n; i++) { - if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame; - z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); - if (z[i] == NULL) goto endgame; - } + if (Pi != NULL) return(NULL); + z = ABC_ALLOC(DdNode *,n); + if (z == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + createdZ = 1; + for (i = 0; i < n; i++) { + if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame; + z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); + if (z[i] == NULL) goto endgame; + } } /* Create priority function BDD if needed. */ if (Pi == NULL) { - Pi = Pifunc(dd,n,x,y,z); - if (Pi == NULL) goto endgame; - createdPi = 1; - cuddRef(Pi); + Pi = Pifunc(dd,n,x,y,z); + if (Pi == NULL) goto endgame; + createdPi = 1; + cuddRef(Pi); } /* Initialize abstraction cube. */ zcube = DD_ONE(dd); cuddRef(zcube); for (i = n - 1; i >= 0; i--) { - DdNode *tmpp; - tmpp = Cudd_bddAnd(dd,z[i],zcube); - if (tmpp == NULL) goto endgame; - cuddRef(tmpp); - Cudd_RecursiveDeref(dd,zcube); - zcube = tmpp; + DdNode *tmpp; + tmpp = Cudd_bddAnd(dd,z[i],zcube); + if (tmpp == NULL) goto endgame; + cuddRef(tmpp); + Cudd_RecursiveDeref(dd,zcube); + zcube = tmpp; } /* Compute subset of (x,y) pairs. */ @@ -199,15 +231,15 @@ Cudd_PrioritySelect( cuddRef(Rxz); Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube); if (Q == NULL) { - Cudd_RecursiveDeref(dd,Rxz); - goto endgame; + Cudd_RecursiveDeref(dd,Rxz); + goto endgame; } cuddRef(Q); Cudd_RecursiveDeref(dd,Rxz); res = Cudd_bddAnd(dd,R,Cudd_Not(Q)); if (res == NULL) { - Cudd_RecursiveDeref(dd,Q); - goto endgame; + Cudd_RecursiveDeref(dd,Q); + goto endgame; } cuddRef(res); Cudd_RecursiveDeref(dd,Q); @@ -215,10 +247,10 @@ Cudd_PrioritySelect( endgame: if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube); if (createdZ) { - ABC_FREE(z); + ABC_FREE(z); } if (createdPi) { - Cudd_RecursiveDeref(dd,Pi); + Cudd_RecursiveDeref(dd,Pi); } if (res != NULL) cuddDeref(res); return(res); @@ -234,7 +266,7 @@ endgame: Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The BDD is built bottom-up. - It has 3*N-1 internal nodes, if the variables are ordered as follows: + It has 3*N-1 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. Argument z is not used by Cudd_Xgty: it is included to make it call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.] @@ -262,29 +294,29 @@ Cudd_Xgty( /* Loop to build the rest of the BDD. */ for (i = N-2; i >= 0; i--) { - v = Cudd_bddAnd(dd, y[i], Cudd_Not(u)); - if (v == NULL) { - Cudd_RecursiveDeref(dd, u); - return(NULL); - } - cuddRef(v); - w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); - if (w == NULL) { + v = Cudd_bddAnd(dd, y[i], Cudd_Not(u)); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); Cudd_RecursiveDeref(dd, u); - Cudd_RecursiveDeref(dd, v); - return(NULL); - } - cuddRef(w); - Cudd_RecursiveDeref(dd, u); - u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w); - if (u == NULL) { + u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w); + if (u == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); Cudd_RecursiveDeref(dd, v); Cudd_RecursiveDeref(dd, w); - return(NULL); - } - cuddRef(u); - Cudd_RecursiveDeref(dd, v); - Cudd_RecursiveDeref(dd, w); } cuddDeref(u); @@ -301,7 +333,7 @@ Cudd_Xgty( Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The BDD is built bottom-up. - It has 3*N-1 internal nodes, if the variables are ordered as follows: + It has 3*N-1 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] SideEffects [None] @@ -326,29 +358,29 @@ Cudd_Xeqy( /* Loop to build the rest of the BDD. */ for (i = N-2; i >= 0; i--) { - v = Cudd_bddAnd(dd, y[i], u); - if (v == NULL) { - Cudd_RecursiveDeref(dd, u); - return(NULL); - } - cuddRef(v); - w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); - if (w == NULL) { + v = Cudd_bddAnd(dd, y[i], u); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); Cudd_RecursiveDeref(dd, u); - Cudd_RecursiveDeref(dd, v); - return(NULL); - } - cuddRef(w); - Cudd_RecursiveDeref(dd, u); - u = Cudd_bddIte(dd, x[i], v, w); - if (u == NULL) { + u = Cudd_bddIte(dd, x[i], v, w); + if (u == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); Cudd_RecursiveDeref(dd, v); Cudd_RecursiveDeref(dd, w); - return(NULL); - } - cuddRef(u); - Cudd_RecursiveDeref(dd, v); - Cudd_RecursiveDeref(dd, w); } cuddDeref(u); return(u); @@ -364,7 +396,7 @@ Cudd_Xeqy( Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. The ADD is built bottom-up. - It has 3*N-1 internal nodes, if the variables are ordered as follows: + It has 3*N-1 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] SideEffects [None] @@ -392,15 +424,15 @@ Cudd_addXeqy( cuddRef(v); w = Cudd_addIte(dd, y[N-1], zero, one); if (w == NULL) { - Cudd_RecursiveDeref(dd, v); - return(NULL); + Cudd_RecursiveDeref(dd, v); + return(NULL); } cuddRef(w); u = Cudd_addIte(dd, x[N-1], v, w); - if (w == NULL) { - Cudd_RecursiveDeref(dd, v); - Cudd_RecursiveDeref(dd, w); - return(NULL); + if (u == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); } cuddRef(u); Cudd_RecursiveDeref(dd, v); @@ -408,29 +440,29 @@ Cudd_addXeqy( /* Loop to build the rest of the ADD. */ for (i = N-2; i >= 0; i--) { - v = Cudd_addIte(dd, y[i], u, zero); - if (v == NULL) { - Cudd_RecursiveDeref(dd, u); - return(NULL); - } - cuddRef(v); - w = Cudd_addIte(dd, y[i], zero, u); - if (w == NULL) { + v = Cudd_addIte(dd, y[i], u, zero); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_addIte(dd, y[i], zero, u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); Cudd_RecursiveDeref(dd, u); - Cudd_RecursiveDeref(dd, v); - return(NULL); - } - cuddRef(w); - Cudd_RecursiveDeref(dd, u); - u = Cudd_addIte(dd, x[i], v, w); - if (w == NULL) { + u = Cudd_addIte(dd, x[i], v, w); + if (w == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); Cudd_RecursiveDeref(dd, v); Cudd_RecursiveDeref(dd, w); - return(NULL); - } - cuddRef(u); - Cudd_RecursiveDeref(dd, v); - Cudd_RecursiveDeref(dd, w); } cuddDeref(u); return(u); @@ -448,9 +480,9 @@ Cudd_addXeqy( y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], with 0 the most significant bit. The distance d(x,y) is defined as: - \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). + \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). The BDD is built bottom-up. - It has 7*N-3 internal nodes, if the variables are ordered as follows: + It has 7*N-3 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] SideEffects [None] @@ -479,15 +511,15 @@ Cudd_Dxygtdxz( cuddRef(y1_); y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one); if (y2 == NULL) { - Cudd_RecursiveDeref(dd, y1_); - return(NULL); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); } cuddRef(y2); x1 = Cudd_bddIte(dd, x[N-1], y1_, y2); if (x1 == NULL) { - Cudd_RecursiveDeref(dd, y1_); - Cudd_RecursiveDeref(dd, y2); - return(NULL); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); } cuddRef(x1); Cudd_RecursiveDeref(dd, y1_); @@ -495,69 +527,69 @@ Cudd_Dxygtdxz( /* Loop to build the rest of the BDD. */ for (i = N-2; i >= 0; i--) { - z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); - if (z1 == NULL) { - Cudd_RecursiveDeref(dd, x1); - return(NULL); - } - cuddRef(z1); - z2 = Cudd_bddIte(dd, z[i], x1, one); - if (z2 == NULL) { - Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - return(NULL); - } - cuddRef(z2); - z3 = Cudd_bddIte(dd, z[i], one, x1); - if (z3 == NULL) { - Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - return(NULL); - } - cuddRef(z3); - z4 = Cudd_bddIte(dd, z[i], x1, zero); - if (z4 == NULL) { + z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); + if (z1 == NULL) { + Cudd_RecursiveDeref(dd, x1); + return(NULL); + } + cuddRef(z1); + z2 = Cudd_bddIte(dd, z[i], x1, one); + if (z2 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + return(NULL); + } + cuddRef(z2); + z3 = Cudd_bddIte(dd, z[i], one, x1); + if (z3 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + return(NULL); + } + cuddRef(z3); + z4 = Cudd_bddIte(dd, z[i], x1, zero); + if (z4 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + return(NULL); + } + cuddRef(z4); Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - return(NULL); - } - cuddRef(z4); - Cudd_RecursiveDeref(dd, x1); - y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1)); - if (y1_ == NULL) { - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - Cudd_RecursiveDeref(dd, z4); - return(NULL); - } - cuddRef(y1_); - y2 = Cudd_bddIte(dd, y[i], z4, z3); - if (y2 == NULL) { + y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1)); + if (y1_ == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + return(NULL); + } + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[i], z4, z3); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); Cudd_RecursiveDeref(dd, z1); Cudd_RecursiveDeref(dd, z2); Cudd_RecursiveDeref(dd, z3); Cudd_RecursiveDeref(dd, z4); - Cudd_RecursiveDeref(dd, y1_); - return(NULL); - } - cuddRef(y2); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - Cudd_RecursiveDeref(dd, z4); - x1 = Cudd_bddIte(dd, x[i], y1_, y2); - if (x1 == NULL) { + x1 = Cudd_bddIte(dd, x[i], y1_, y2); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); Cudd_RecursiveDeref(dd, y1_); Cudd_RecursiveDeref(dd, y2); - return(NULL); - } - cuddRef(x1); - Cudd_RecursiveDeref(dd, y1_); - Cudd_RecursiveDeref(dd, y2); } cuddDeref(x1); return(Cudd_Not(x1)); @@ -575,9 +607,9 @@ Cudd_Dxygtdxz( y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], with 0 the most significant bit. The distance d(x,y) is defined as: - \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). + \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). The BDD is built bottom-up. - It has 7*N-3 internal nodes, if the variables are ordered as follows: + It has 7*N-3 internal nodes, if the variables are ordered as follows: x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] SideEffects [None] @@ -606,15 +638,15 @@ Cudd_Dxygtdyz( cuddRef(y1_); y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero); if (y2 == NULL) { - Cudd_RecursiveDeref(dd, y1_); - return(NULL); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); } cuddRef(y2); x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2)); if (x1 == NULL) { - Cudd_RecursiveDeref(dd, y1_); - Cudd_RecursiveDeref(dd, y2); - return(NULL); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); } cuddRef(x1); Cudd_RecursiveDeref(dd, y1_); @@ -622,69 +654,69 @@ Cudd_Dxygtdyz( /* Loop to build the rest of the BDD. */ for (i = N-2; i >= 0; i--) { - z1 = Cudd_bddIte(dd, z[i], x1, zero); - if (z1 == NULL) { - Cudd_RecursiveDeref(dd, x1); - return(NULL); - } - cuddRef(z1); - z2 = Cudd_bddIte(dd, z[i], x1, one); - if (z2 == NULL) { - Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - return(NULL); - } - cuddRef(z2); - z3 = Cudd_bddIte(dd, z[i], one, x1); - if (z3 == NULL) { - Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - return(NULL); - } - cuddRef(z3); - z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); - if (z4 == NULL) { + z1 = Cudd_bddIte(dd, z[i], x1, zero); + if (z1 == NULL) { + Cudd_RecursiveDeref(dd, x1); + return(NULL); + } + cuddRef(z1); + z2 = Cudd_bddIte(dd, z[i], x1, one); + if (z2 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + return(NULL); + } + cuddRef(z2); + z3 = Cudd_bddIte(dd, z[i], one, x1); + if (z3 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + return(NULL); + } + cuddRef(z3); + z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); + if (z4 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + return(NULL); + } + cuddRef(z4); Cudd_RecursiveDeref(dd, x1); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - return(NULL); - } - cuddRef(z4); - Cudd_RecursiveDeref(dd, x1); - y1_ = Cudd_bddIte(dd, y[i], z2, z1); - if (y1_ == NULL) { - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - Cudd_RecursiveDeref(dd, z4); - return(NULL); - } - cuddRef(y1_); - y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3)); - if (y2 == NULL) { + y1_ = Cudd_bddIte(dd, y[i], z2, z1); + if (y1_ == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + return(NULL); + } + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3)); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); Cudd_RecursiveDeref(dd, z1); Cudd_RecursiveDeref(dd, z2); Cudd_RecursiveDeref(dd, z3); Cudd_RecursiveDeref(dd, z4); - Cudd_RecursiveDeref(dd, y1_); - return(NULL); - } - cuddRef(y2); - Cudd_RecursiveDeref(dd, z1); - Cudd_RecursiveDeref(dd, z2); - Cudd_RecursiveDeref(dd, z3); - Cudd_RecursiveDeref(dd, z4); - x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2)); - if (x1 == NULL) { + x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2)); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); Cudd_RecursiveDeref(dd, y1_); Cudd_RecursiveDeref(dd, y2); - return(NULL); - } - cuddRef(x1); - Cudd_RecursiveDeref(dd, y1_); - Cudd_RecursiveDeref(dd, y2); } cuddDeref(x1); return(Cudd_Not(x1)); @@ -692,6 +724,464 @@ Cudd_Dxygtdyz( } /* end of Cudd_Dxygtdyz */ +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function x - y ≥ c.] + + Description [This function generates a BDD for the function x -y ≥ c. + Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and + y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. + The BDD is built bottom-up. + It has a linear number of nodes if the variables are ordered as follows: + x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] + + SideEffects [None] + + SeeAlso [Cudd_Xgty] + +******************************************************************************/ +DdNode * +Cudd_Inequality( + DdManager * dd /* DD manager */, + int N /* number of x and y variables */, + int c /* right-hand side constant */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */) +{ + /* The nodes at level i represent values of the difference that are + ** multiples of 2^i. We use variables with names starting with k + ** to denote the multipliers of 2^i in such multiples. */ + int kTrue = c; + int kFalse = c - 1; + /* Mask used to compute the ceiling function. Since we divide by 2^i, + ** we want to know whether the dividend is a multiple of 2^i. If it is, + ** then ceiling and floor coincide; otherwise, they differ by one. */ + int mask = 1; + int i; + + DdNode *f = NULL; /* the eventual result */ + DdNode *one = DD_ONE(dd); + DdNode *zero = Cudd_Not(one); + + /* Two x-labeled nodes are created at most at each iteration. They are + ** stored, along with their k values, in these variables. At each level, + ** the old nodes are freed and the new nodes are copied into the old map. + */ + DdNode *map[2] = {0}; + int invalidIndex = 1 << (N-1); + int index[2] = {invalidIndex, invalidIndex}; + + /* This should never happen. */ + if (N < 0) return(NULL); + + /* If there are no bits, both operands are 0. The result depends on c. */ + if (N == 0) { + if (c >= 0) return(one); + else return(zero); + } + + /* The maximum or the minimum difference comparing to c can generate the terminal case */ + if ((1 << N) - 1 < c) return(zero); + else if ((-(1 << N) + 1) >= c) return(one); + + /* Build the result bottom up. */ + for (i = 1; i <= N; i++) { + int kTrueLower, kFalseLower; + int leftChild, middleChild, rightChild; + DdNode *g0, *g1, *fplus, *fequal, *fminus; + int j; + DdNode *newMap[2]; + int newIndex[2]; + + kTrueLower = kTrue; + kFalseLower = kFalse; + /* kTrue = ceiling((c-1)/2^i) + 1 */ + kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; + mask = (mask << 1) | 1; + /* kFalse = floor(c/2^i) - 1 */ + kFalse = (c >> i) - 1; + newIndex[0] = invalidIndex; + newIndex[1] = invalidIndex; + + for (j = kFalse + 1; j < kTrue; j++) { + /* Skip if node is not reachable from top of BDD. */ + if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; + + /* Find f- */ + leftChild = (j << 1) - 1; + if (leftChild >= kTrueLower) { + fminus = one; + } else if (leftChild <= kFalseLower) { + fminus = zero; + } else { + assert(leftChild == index[0] || leftChild == index[1]); + if (leftChild == index[0]) { + fminus = map[0]; + } else { + fminus = map[1]; + } + } + + /* Find f= */ + middleChild = j << 1; + if (middleChild >= kTrueLower) { + fequal = one; + } else if (middleChild <= kFalseLower) { + fequal = zero; + } else { + assert(middleChild == index[0] || middleChild == index[1]); + if (middleChild == index[0]) { + fequal = map[0]; + } else { + fequal = map[1]; + } + } + + /* Find f+ */ + rightChild = (j << 1) + 1; + if (rightChild >= kTrueLower) { + fplus = one; + } else if (rightChild <= kFalseLower) { + fplus = zero; + } else { + assert(rightChild == index[0] || rightChild == index[1]); + if (rightChild == index[0]) { + fplus = map[0]; + } else { + fplus = map[1]; + } + } + + /* Build new nodes. */ + g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus); + if (g1 == NULL) { + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(g1); + g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal); + if (g0 == NULL) { + Cudd_IterDerefBdd(dd, g1); + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(g0); + f = Cudd_bddIte(dd, x[N - i], g1, g0); + if (f == NULL) { + Cudd_IterDerefBdd(dd, g1); + Cudd_IterDerefBdd(dd, g0); + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(f); + Cudd_IterDerefBdd(dd, g1); + Cudd_IterDerefBdd(dd, g0); + + /* Save newly computed node in map. */ + assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); + if (newIndex[0] == invalidIndex) { + newIndex[0] = j; + newMap[0] = f; + } else { + newIndex[1] = j; + newMap[1] = f; + } + } + + /* Copy new map to map. */ + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + map[0] = newMap[0]; + map[1] = newMap[1]; + index[0] = newIndex[0]; + index[1] = newIndex[1]; + } + + cuddDeref(f); + return(f); + +} /* end of Cudd_Inequality */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function x - y != c.] + + Description [This function generates a BDD for the function x -y != c. + Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and + y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. + The BDD is built bottom-up. + It has a linear number of nodes if the variables are ordered as follows: + x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] + + SideEffects [None] + + SeeAlso [Cudd_Xgty] + +******************************************************************************/ +DdNode * +Cudd_Disequality( + DdManager * dd /* DD manager */, + int N /* number of x and y variables */, + int c /* right-hand side constant */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */) +{ + /* The nodes at level i represent values of the difference that are + ** multiples of 2^i. We use variables with names starting with k + ** to denote the multipliers of 2^i in such multiples. */ + int kTrueLb = c + 1; + int kTrueUb = c - 1; + int kFalse = c; + /* Mask used to compute the ceiling function. Since we divide by 2^i, + ** we want to know whether the dividend is a multiple of 2^i. If it is, + ** then ceiling and floor coincide; otherwise, they differ by one. */ + int mask = 1; + int i; + + DdNode *f = NULL; /* the eventual result */ + DdNode *one = DD_ONE(dd); + DdNode *zero = Cudd_Not(one); + + /* Two x-labeled nodes are created at most at each iteration. They are + ** stored, along with their k values, in these variables. At each level, + ** the old nodes are freed and the new nodes are copied into the old map. + */ + DdNode *map[2] = {0}; + int invalidIndex = 1 << (N-1); + int index[2] = {invalidIndex, invalidIndex}; + + /* This should never happen. */ + if (N < 0) return(NULL); + + /* If there are no bits, both operands are 0. The result depends on c. */ + if (N == 0) { + if (c != 0) return(one); + else return(zero); + } + + /* The maximum or the minimum difference comparing to c can generate the terminal case */ + if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(one); + + /* Build the result bottom up. */ + for (i = 1; i <= N; i++) { + int kTrueLbLower, kTrueUbLower; + int leftChild, middleChild, rightChild; + DdNode *g0, *g1, *fplus, *fequal, *fminus; + int j; + DdNode *newMap[2]; + int newIndex[2]; + + kTrueLbLower = kTrueLb; + kTrueUbLower = kTrueUb; + /* kTrueLb = floor((c-1)/2^i) + 2 */ + kTrueLb = ((c-1) >> i) + 2; + /* kTrueUb = ceiling((c+1)/2^i) - 2 */ + kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2; + mask = (mask << 1) | 1; + newIndex[0] = invalidIndex; + newIndex[1] = invalidIndex; + + for (j = kTrueUb + 1; j < kTrueLb; j++) { + /* Skip if node is not reachable from top of BDD. */ + if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; + + /* Find f- */ + leftChild = (j << 1) - 1; + if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) { + fminus = one; + } else if (i == 1 && leftChild == kFalse) { + fminus = zero; + } else { + assert(leftChild == index[0] || leftChild == index[1]); + if (leftChild == index[0]) { + fminus = map[0]; + } else { + fminus = map[1]; + } + } + + /* Find f= */ + middleChild = j << 1; + if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) { + fequal = one; + } else if (i == 1 && middleChild == kFalse) { + fequal = zero; + } else { + assert(middleChild == index[0] || middleChild == index[1]); + if (middleChild == index[0]) { + fequal = map[0]; + } else { + fequal = map[1]; + } + } + + /* Find f+ */ + rightChild = (j << 1) + 1; + if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) { + fplus = one; + } else if (i == 1 && rightChild == kFalse) { + fplus = zero; + } else { + assert(rightChild == index[0] || rightChild == index[1]); + if (rightChild == index[0]) { + fplus = map[0]; + } else { + fplus = map[1]; + } + } + + /* Build new nodes. */ + g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus); + if (g1 == NULL) { + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(g1); + g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal); + if (g0 == NULL) { + Cudd_IterDerefBdd(dd, g1); + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(g0); + f = Cudd_bddIte(dd, x[N - i], g1, g0); + if (f == NULL) { + Cudd_IterDerefBdd(dd, g1); + Cudd_IterDerefBdd(dd, g0); + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); + if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); + return(NULL); + } + cuddRef(f); + Cudd_IterDerefBdd(dd, g1); + Cudd_IterDerefBdd(dd, g0); + + /* Save newly computed node in map. */ + assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); + if (newIndex[0] == invalidIndex) { + newIndex[0] = j; + newMap[0] = f; + } else { + newIndex[1] = j; + newMap[1] = f; + } + } + + /* Copy new map to map. */ + if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); + if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); + map[0] = newMap[0]; + map[1] = newMap[1]; + index[0] = newIndex[0]; + index[1] = newIndex[1]; + } + + cuddDeref(f); + return(f); + +} /* end of Cudd_Disequality */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function lowerB ≤ x ≤ upperB.] + + Description [This function generates a BDD for the function + lowerB ≤ x ≤ upperB, where x is an N-bit number, + x\[0\] x\[1\] ... x\[N-1\], with 0 the most significant bit (important!). + The number of variables N should be sufficient to represent the bounds; + otherwise, the bounds are truncated to their N least significant bits. + Two BDDs are built bottom-up for lowerB ≤ x and x ≤ upperB, and they + are finally conjoined.] + + SideEffects [None] + + SeeAlso [Cudd_Xgty] + +******************************************************************************/ +DdNode * +Cudd_bddInterval( + DdManager * dd /* DD manager */, + int N /* number of x variables */, + DdNode ** x /* array of x variables */, + unsigned int lowerB /* lower bound */, + unsigned int upperB /* upper bound */) +{ + DdNode *one, *zero; + DdNode *r, *rl, *ru; + int i; + + one = DD_ONE(dd); + zero = Cudd_Not(one); + + rl = one; + cuddRef(rl); + ru = one; + cuddRef(ru); + + /* Loop to build the rest of the BDDs. */ + for (i = N-1; i >= 0; i--) { + DdNode *vl, *vu; + vl = Cudd_bddIte(dd, x[i], + lowerB&1 ? rl : one, + lowerB&1 ? zero : rl); + if (vl == NULL) { + Cudd_IterDerefBdd(dd, rl); + Cudd_IterDerefBdd(dd, ru); + return(NULL); + } + cuddRef(vl); + Cudd_IterDerefBdd(dd, rl); + rl = vl; + lowerB >>= 1; + vu = Cudd_bddIte(dd, x[i], + upperB&1 ? ru : zero, + upperB&1 ? one : ru); + if (vu == NULL) { + Cudd_IterDerefBdd(dd, rl); + Cudd_IterDerefBdd(dd, ru); + return(NULL); + } + cuddRef(vu); + Cudd_IterDerefBdd(dd, ru); + ru = vu; + upperB >>= 1; + } + + /* Conjoin the two bounds. */ + r = Cudd_bddAnd(dd, rl, ru); + if (r == NULL) { + Cudd_IterDerefBdd(dd, rl); + Cudd_IterDerefBdd(dd, ru); + return(NULL); + } + cuddRef(r); + Cudd_IterDerefBdd(dd, rl); + Cudd_IterDerefBdd(dd, ru); + cuddDeref(r); + return(r); + +} /* end of Cudd_bddInterval */ + + /**Function******************************************************************** Synopsis [Computes the compatible projection of R w.r.t. cube Y.] @@ -716,10 +1206,10 @@ Cudd_CProjection( DdNode *support; if (cuddCheckCube(dd,Y) == 0) { - (void) fprintf(dd->err, - "Error: The third argument of Cudd_CProjection should be a cube\n"); - dd->errorCode = CUDD_INVALID_ARG; - return(NULL); + (void) fprintf(dd->err, + "Error: The third argument of Cudd_CProjection should be a cube\n"); + dd->errorCode = CUDD_INVALID_ARG; + return(NULL); } /* Compute the support of Y, which is used by the abstraction step @@ -730,13 +1220,13 @@ Cudd_CProjection( cuddRef(support); do { - dd->reordered = 0; - res = cuddCProjectionRecur(dd,R,Y,support); + dd->reordered = 0; + res = cuddCProjectionRecur(dd,R,Y,support); } while (dd->reordered == 1); if (res == NULL) { - Cudd_RecursiveDeref(dd,support); - return(NULL); + Cudd_RecursiveDeref(dd,support); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(dd,support); @@ -776,30 +1266,30 @@ Cudd_addHamming( cuddRef(result); for (i = 0; i < nVars; i++) { - tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]); - if (tempBdd == NULL) { - Cudd_RecursiveDeref(dd,result); - return(NULL); - } - cuddRef(tempBdd); - tempAdd = Cudd_BddToAdd(dd,tempBdd); - if (tempAdd == NULL) { + tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]); + if (tempBdd == NULL) { + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(tempBdd); + tempAdd = Cudd_BddToAdd(dd,tempBdd); + if (tempAdd == NULL) { + Cudd_RecursiveDeref(dd,tempBdd); + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(tempAdd); Cudd_RecursiveDeref(dd,tempBdd); - Cudd_RecursiveDeref(dd,result); - return(NULL); - } - cuddRef(tempAdd); - Cudd_RecursiveDeref(dd,tempBdd); - temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result); - if (temp == NULL) { + temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result); + if (temp == NULL) { + Cudd_RecursiveDeref(dd,tempAdd); + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(temp); Cudd_RecursiveDeref(dd,tempAdd); Cudd_RecursiveDeref(dd,result); - return(NULL); - } - cuddRef(temp); - Cudd_RecursiveDeref(dd,tempAdd); - Cudd_RecursiveDeref(dd,result); - result = temp; + result = temp; } cuddDeref(result); @@ -837,7 +1327,7 @@ Cudd_MinHammingDist( table = cuddHashTableInit(dd,1,2); if (table == NULL) { - return(CUDD_OUT_OF_MEM); + return(CUDD_OUT_OF_MEM); } epsilon = Cudd_ReadEpsilon(dd); Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0); @@ -846,7 +1336,7 @@ Cudd_MinHammingDist( Cudd_SetEpsilon(dd,epsilon); return(res); - + } /* end of Cudd_MinHammingDist */ @@ -877,32 +1367,32 @@ Cudd_bddClosestCube( /* Compute the cube and distance as a single ADD. */ do { - dd->reordered = 0; - res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0); + dd->reordered = 0; + res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0); } while (dd->reordered == 1); if (res == NULL) return(NULL); cuddRef(res); /* Unpack distance and cube. */ do { - dd->reordered = 0; - acube = separateCube(dd, res, &rdist); + dd->reordered = 0; + acube = separateCube(dd, res, &rdist); } while (dd->reordered == 1); if (acube == NULL) { - Cudd_RecursiveDeref(dd, res); - return(NULL); + Cudd_RecursiveDeref(dd, res); + return(NULL); } cuddRef(acube); Cudd_RecursiveDeref(dd, res); /* Convert cube from ADD to BDD. */ do { - dd->reordered = 0; - res = cuddAddBddDoPattern(dd, acube); + dd->reordered = 0; + res = cuddAddBddDoPattern(dd, acube); } while (dd->reordered == 1); if (res == NULL) { - Cudd_RecursiveDeref(dd, acube); - return(NULL); + Cudd_RecursiveDeref(dd, acube); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(dd, acube); @@ -940,8 +1430,7 @@ cuddCProjectionRecur( { DdNode *res, *res1, *res2, *resA; DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha; - unsigned int topR, topY, top; - unsigned int index = 0; // Suppress "might be used uninitialized" + unsigned int topR, topY, top, index; DdNode *one = DD_ONE(dd); statLine(dd); @@ -965,114 +1454,114 @@ cuddCProjectionRecur( /* Compute the cofactors of R */ if (topR == top) { - index = r->index; - RT = cuddT(r); - RE = cuddE(r); - if (r != R) { - RT = Cudd_Not(RT); RE = Cudd_Not(RE); - } + index = r->index; + RT = cuddT(r); + RE = cuddE(r); + if (r != R) { + RT = Cudd_Not(RT); RE = Cudd_Not(RE); + } } else { - RT = RE = R; + RT = RE = R; } if (topY > top) { - /* Y does not depend on the current top variable. - ** We just need to compute the results on the two cofactors of R - ** and make them the children of a node labeled r->index. - */ - res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp); - if (res1 == NULL) return(NULL); - cuddRef(res1); - res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp); - if (res2 == NULL) { - Cudd_RecursiveDeref(dd,res1); - return(NULL); - } - cuddRef(res2); - res = cuddBddIteRecur(dd, dd->vars[index], res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,res2); - return(NULL); - } - /* If we have reached this point, res1 and res2 are now - ** incorporated in res. cuddDeref is therefore sufficient. - */ - cuddDeref(res1); - cuddDeref(res2); - } else { - /* Compute the cofactors of Y */ - index = y->index; - YT = cuddT(y); - YE = cuddE(y); - if (y != Y) { - YT = Cudd_Not(YT); YE = Cudd_Not(YE); - } - if (YT == Cudd_Not(one)) { - Alpha = Cudd_Not(dd->vars[index]); - Yrest = YE; - Ra = RE; - Ran = RT; - } else { - Alpha = dd->vars[index]; - Yrest = YT; - Ra = RT; - Ran = RE; - } - Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp)); - if (Gamma == NULL) return(NULL); - if (Gamma == one) { - res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); + /* Y does not depend on the current top variable. + ** We just need to compute the results on the two cofactors of R + ** and make them the children of a node labeled r->index. + */ + res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp); if (res1 == NULL) return(NULL); cuddRef(res1); - res = cuddBddAndRecur(dd, Alpha, res1); - if (res == NULL) { - Cudd_RecursiveDeref(dd,res1); - return(NULL); + res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp); + if (res2 == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); } - cuddDeref(res1); - } else if (Gamma == Cudd_Not(one)) { - res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); - if (res1 == NULL) return(NULL); - cuddRef(res1); - res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1); + cuddRef(res2); + res = cuddBddIteRecur(dd, dd->vars[index], res1, res2); if (res == NULL) { - Cudd_RecursiveDeref(dd,res1); - return(NULL); + Cudd_RecursiveDeref(dd,res1); + Cudd_RecursiveDeref(dd,res2); + return(NULL); } + /* If we have reached this point, res1 and res2 are now + ** incorporated in res. cuddDeref is therefore sufficient. + */ cuddDeref(res1); + cuddDeref(res2); } else { - cuddRef(Gamma); - resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); - if (resA == NULL) { - Cudd_RecursiveDeref(dd,Gamma); - return(NULL); - } - cuddRef(resA); - res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA); - if (res2 == NULL) { - Cudd_RecursiveDeref(dd,Gamma); - Cudd_RecursiveDeref(dd,resA); - return(NULL); + /* Compute the cofactors of Y */ + index = y->index; + YT = cuddT(y); + YE = cuddE(y); + if (y != Y) { + YT = Cudd_Not(YT); YE = Cudd_Not(YE); } - cuddRef(res2); - Cudd_RecursiveDeref(dd,Gamma); - Cudd_RecursiveDeref(dd,resA); - res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); - if (res1 == NULL) { - Cudd_RecursiveDeref(dd,res2); - return(NULL); + if (YT == Cudd_Not(one)) { + Alpha = Cudd_Not(dd->vars[index]); + Yrest = YE; + Ra = RE; + Ran = RT; + } else { + Alpha = dd->vars[index]; + Yrest = YT; + Ra = RT; + Ran = RE; } - cuddRef(res1); - res = cuddBddIteRecur(dd, Alpha, res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(dd,res1); - Cudd_RecursiveDeref(dd,res2); - return(NULL); + Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp)); + if (Gamma == NULL) return(NULL); + if (Gamma == one) { + res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res = cuddBddAndRecur(dd, Alpha, res1); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); + } + cuddDeref(res1); + } else if (Gamma == Cudd_Not(one)) { + res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); + } + cuddDeref(res1); + } else { + cuddRef(Gamma); + resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); + if (resA == NULL) { + Cudd_RecursiveDeref(dd,Gamma); + return(NULL); + } + cuddRef(resA); + res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA); + if (res2 == NULL) { + Cudd_RecursiveDeref(dd,Gamma); + Cudd_RecursiveDeref(dd,resA); + return(NULL); + } + cuddRef(res2); + Cudd_RecursiveDeref(dd,Gamma); + Cudd_RecursiveDeref(dd,resA); + res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); + if (res1 == NULL) { + Cudd_RecursiveDeref(dd,res2); + return(NULL); + } + cuddRef(res1); + res = cuddBddIteRecur(dd, Alpha, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + Cudd_RecursiveDeref(dd,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); } - cuddDeref(res1); - cuddDeref(res2); - } } cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res); @@ -1089,14 +1578,64 @@ cuddCProjectionRecur( Description [Performs the recursive step of Cudd_bddClosestCube. Returns the cube if succesful; NULL otherwise. The procedure uses a four-way recursion to examine all four combinations of cofactors of - f and g. The most interesting feature of this function is the - scheme used for caching the results in the global computed table. - Since we have a cube and a distance, we combine them to form an ADD. - The combination replaces the zero child of the top node of the cube - with the negative of the distance. (The use of the negative is to - avoid ambiguity with 1.) The degenerate cases (zero and one) are - treated specially because the distance is known (0 for one, and - infinity for zero).] + f and g according to the following formula. + 
+    H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
+
+ Bounding is based on the following observations. + + The variable bound is set at the largest value of the distance + that we are still interested in. Therefore, we desist when + 
+    (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
+
+ If we were maximally aggressive in using the bound, we would always + set the bound to the minimum distance seen thus far minus one. That + is, we would maintain the invariant + 
+    bound < minD,
+
+ except at the very beginning, when we have no value for + minD.

+ + However, we do not use bound < minD when examining the + two negative cofactors, because we try to find a large cube at + minimum distance. To do so, we try to find a cube in the negative + cofactors at the same or smaller distance from the cube found in the + positive cofactors.

+ + When we compute H(ft,ge) and H(fe,gt) we + know that we are going to add 1 to the result of the recursive call + to account for the difference in the splitting variable. Therefore, + we decrease the bound correspondingly.

+ + Another important observation concerns the need of examining all + four pairs of cofators only when both f and + g depend on the top variable.

+ + Suppose gt == ge == g. (That is, g does + not depend on the top variable.) Then + 

+    H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
+           = min(H(ft,g), H(fe,g)) .
+
+ Therefore, under these circumstances, we skip the two "cross" cases.

+ + An interesting feature of this function is the scheme used for + caching the results in the global computed table. Since we have a + cube and a distance, we combine them to form an ADD. The + combination replaces the zero child of the top node of the cube with + the negative of the distance. (The use of the negative is to avoid + ambiguity with 1.) The degenerate cases (zero and one) are treated + specially because the distance is known (0 for one, and infinity for + zero).] SideEffects [None] @@ -1119,7 +1658,7 @@ cuddBddClosestCube( unsigned int topf, topg, index; statLine(dd); - if (bound < (f == Cudd_Not(g))) return(azero); + if (bound < (int)(f == Cudd_Not(g))) return(azero); /* Terminal cases. */ if (g == lzero || f == lzero) return(azero); if (f == one && g == one) return(one); @@ -1128,9 +1667,8 @@ cuddBddClosestCube( F = Cudd_Regular(f); G = Cudd_Regular(g); if (F->ref != 1 || G->ref != 1) { - res = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *, - DdNode *)) Cudd_bddClosestCube, f, g); - if (res != NULL) return(res); + res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g); + if (res != NULL) return(res); } topf = cuddI(dd,F->index); @@ -1138,27 +1676,27 @@ cuddBddClosestCube( /* Compute cofactors. */ if (topf <= topg) { - index = F->index; - ft = cuddT(F); - fe = cuddE(F); - if (Cudd_IsComplement(f)) { - ft = Cudd_Not(ft); - fe = Cudd_Not(fe); - } + index = F->index; + ft = cuddT(F); + fe = cuddE(F); + if (Cudd_IsComplement(f)) { + ft = Cudd_Not(ft); + fe = Cudd_Not(fe); + } } else { - index = G->index; - ft = fe = f; + index = G->index; + ft = fe = f; } if (topg <= topf) { - gt = cuddT(G); - ge = cuddE(G); - if (Cudd_IsComplement(g)) { - gt = Cudd_Not(gt); - ge = Cudd_Not(ge); - } + gt = cuddT(G); + ge = cuddE(G); + if (Cudd_IsComplement(g)) { + gt = Cudd_Not(gt); + ge = Cudd_Not(ge); + } } else { - gt = ge = g; + gt = ge = g; } tt = cuddBddClosestCube(dd,ft,gt,bound); @@ -1166,8 +1704,8 @@ cuddBddClosestCube( cuddRef(tt); ctt = separateCube(dd,tt,&dtt); if (ctt == NULL) { - Cudd_RecursiveDeref(dd, tt); - return(NULL); + Cudd_RecursiveDeref(dd, tt); + return(NULL); } cuddRef(ctt); Cudd_RecursiveDeref(dd, tt); @@ -1176,86 +1714,99 @@ cuddBddClosestCube( ee = cuddBddClosestCube(dd,fe,ge,bound); if (ee == NULL) { - Cudd_RecursiveDeref(dd, ctt); - return(NULL); + Cudd_RecursiveDeref(dd, ctt); + return(NULL); } cuddRef(ee); cee = separateCube(dd,ee,&dee); if (cee == NULL) { - Cudd_RecursiveDeref(dd, ctt); - Cudd_RecursiveDeref(dd, ee); - return(NULL); + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, ee); + return(NULL); } cuddRef(cee); Cudd_RecursiveDeref(dd, ee); minD = ddMin(dtt, dee); - bound = ddMin(bound,minD-1); + if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); if (minD > 0 && topf == topg) { - DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1); - if (te == NULL) { - Cudd_RecursiveDeref(dd, ctt); - Cudd_RecursiveDeref(dd, cee); - return(NULL); - } - cuddRef(te); - cte = separateCube(dd,te,&dte); - if (cte == NULL) { - Cudd_RecursiveDeref(dd, ctt); - Cudd_RecursiveDeref(dd, cee); + DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1); + if (te == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + return(NULL); + } + cuddRef(te); + cte = separateCube(dd,te,&dte); + if (cte == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, te); + return(NULL); + } + cuddRef(cte); Cudd_RecursiveDeref(dd, te); - return(NULL); - } - cuddRef(cte); - Cudd_RecursiveDeref(dd, te); - dte += 1.0; - minD = ddMin(minD, dte); + dte += 1.0; + minD = ddMin(minD, dte); } else { - cte = azero; - cuddRef(cte); - dte = CUDD_CONST_INDEX + 1.0; + cte = azero; + cuddRef(cte); + dte = CUDD_CONST_INDEX + 1.0; } - bound = ddMin(bound,minD-1); + if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); if (minD > 0 && topf == topg) { - DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1); - if (et == NULL) { - Cudd_RecursiveDeref(dd, ctt); - Cudd_RecursiveDeref(dd, cee); - Cudd_RecursiveDeref(dd, cte); - return(NULL); - } - cuddRef(et); - cet = separateCube(dd,et,&det); - if (cet == NULL) { - Cudd_RecursiveDeref(dd, ctt); - Cudd_RecursiveDeref(dd, cee); - Cudd_RecursiveDeref(dd, cte); + DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1); + if (et == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + return(NULL); + } + cuddRef(et); + cet = separateCube(dd,et,&det); + if (cet == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + Cudd_RecursiveDeref(dd, et); + return(NULL); + } + cuddRef(cet); Cudd_RecursiveDeref(dd, et); - return(NULL); - } - cuddRef(cet); - Cudd_RecursiveDeref(dd, et); - det += 1.0; - minD = ddMin(minD, det); + det += 1.0; + minD = ddMin(minD, det); } else { - cet = azero; - cuddRef(cet); - det = CUDD_CONST_INDEX + 1.0; + cet = azero; + cuddRef(cet); + det = CUDD_CONST_INDEX + 1.0; } if (minD == dtt) { - if (dtt == dee && ctt == cee) { - res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt); - } else { - res = createResult(dd,index,1,ctt,dtt); - } + if (dtt == dee && ctt == cee) { + res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt); + } else { + res = createResult(dd,index,1,ctt,dtt); + } } else if (minD == dee) { - res = createResult(dd,index,0,cee,dee); + res = createResult(dd,index,0,cee,dee); } else if (minD == dte) { - res = createResult(dd,index,(topf <= topg),cte,dte); +#ifdef DD_DEBUG + assert(topf == topg); +#endif + res = createResult(dd,index,1,cte,dte); } else { - res = createResult(dd,index,(topf > topg),cet,det); +#ifdef DD_DEBUG + assert(topf == topg); +#endif + res = createResult(dd,index,0,cet,det); + } + if (res == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + Cudd_RecursiveDeref(dd, cet); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(dd, ctt); @@ -1263,9 +1814,10 @@ cuddBddClosestCube( Cudd_RecursiveDeref(dd, cte); Cudd_RecursiveDeref(dd, cet); - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, - DdNode *)) Cudd_bddClosestCube, f, g, res); + /* Only cache results that are different from azero to avoid + ** storing results that depend on the value of the bound. */ + if ((F->ref != 1 || G->ref != 1) && res != azero) + cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res); cuddDeref(res); return(res); @@ -1309,10 +1861,10 @@ cuddMinHammingDistRecur( DdHashTable * table, int upperBound) { - DdNode *F, *Ft, *Fe; - double h, hT, hE; - DdNode *zero, *res; - DdManager *dd = table->manager; + DdNode *F, *Ft, *Fe; + double h, hT, hE; + DdNode *zero, *res; + DdManager *dd = table->manager; statLine(dd); if (upperBound == 0) return(0); @@ -1320,49 +1872,49 @@ cuddMinHammingDistRecur( F = Cudd_Regular(f); if (cuddIsConstant(F)) { - zero = Cudd_Not(DD_ONE(dd)); - if (f == dd->background || f == zero) { - return(upperBound); - } else { - return(0); - } + zero = Cudd_Not(DD_ONE(dd)); + if (f == dd->background || f == zero) { + return(upperBound); + } else { + return(0); + } } if ((res = cuddHashTableLookup1(table,f)) != NULL) { - h = cuddV(res); - if (res->ref == 0) { - dd->dead++; - dd->constants.dead++; - } - return((int) h); + h = cuddV(res); + if (res->ref == 0) { + dd->dead++; + dd->constants.dead++; + } + return((int) h); } Ft = cuddT(F); Fe = cuddE(F); if (Cudd_IsComplement(f)) { - Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe); + Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe); } if (minterm[F->index] == 0) { - DdNode *temp = Ft; - Ft = Fe; Fe = temp; + DdNode *temp = Ft; + Ft = Fe; Fe = temp; } hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound); if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); if (hT == 0) { - hE = upperBound; + hE = upperBound; } else { - hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1); - if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); + hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1); + if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); } h = ddMin(hT, hE + 1); if (F->ref != 1) { - ptrint fanout = (ptrint) F->ref; - cuddSatDec(fanout); - res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h); - if (!cuddHashTableInsert1(table,f,res,fanout)) { - cuddRef(res); Cudd_RecursiveDeref(dd, res); - return(CUDD_OUT_OF_MEM); - } + ptrint fanout = (ptrint) F->ref; + cuddSatDec(fanout); + res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h); + if (!cuddHashTableInsert1(table,f,res,fanout)) { + cuddRef(res); Cudd_RecursiveDeref(dd, res); + return(CUDD_OUT_OF_MEM); + } } return((int) h); @@ -1392,9 +1944,9 @@ separateCube( /* One and zero are special cases because the distance is implied. */ if (Cudd_IsConstant(f)) { - *distance = (f == DD_ONE(dd)) ? 0.0 : - (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX); - return(f); + *distance = (f == DD_ONE(dd)) ? 0.0 : + (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX); + return(f); } /* Find out which branch points to the distance and replace the top @@ -1402,16 +1954,16 @@ separateCube( t = cuddT(f); if (Cudd_IsConstant(t) && cuddV(t) <= 0) { #ifdef DD_DEBUG - assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd)); + assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd)); #endif - *distance = -cuddV(t); - cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f)); + *distance = -cuddV(t); + cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f)); } else { #ifdef DD_DEBUG - assert(!Cudd_IsConstant(t) || t == DD_ONE(dd)); + assert(!Cudd_IsConstant(t) || t == DD_ONE(dd)); #endif - *distance = -cuddV(cuddE(f)); - cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd)); + *distance = -cuddV(cuddE(f)); + cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd)); } return(cube); @@ -1443,7 +1995,7 @@ createResult( /* Special case. The cube is either one or zero, and we do not ** add any variables. Hence, the result is also one or zero, - ** and the distance remains implied by teh value of the constant. */ + ** and the distance remains implied by the value of the constant. */ if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube); constant = cuddUniqueConst(dd,-distance); @@ -1451,31 +2003,33 @@ createResult( cuddRef(constant); if (index == CUDD_CONST_INDEX) { - /* Replace the top node. */ - if (cuddT(cube) == DD_ZERO(dd)) { - res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube)); - } else { - res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant); - } + /* Replace the top node. */ + if (cuddT(cube) == DD_ZERO(dd)) { + res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube)); + } else { + res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant); + } } else { - /* Add a new top node. */ + /* Add a new top node. */ #ifdef DD_DEBUG - assert(cuddI(dd,index) < cuddI(dd,cube->index)); + assert(cuddI(dd,index) < cuddI(dd,cube->index)); #endif - if (phase) { - res = cuddUniqueInter(dd,index,cube,constant); - } else { - res = cuddUniqueInter(dd,index,constant,cube); - } + if (phase) { + res = cuddUniqueInter(dd,index,cube,constant); + } else { + res = cuddUniqueInter(dd,index,constant,cube); + } } if (res == NULL) { - Cudd_RecursiveDeref(dd, constant); - return(NULL); + Cudd_RecursiveDeref(dd, constant); + return(NULL); } cuddDeref(constant); /* safe because constant is part of res */ return(res); } /* end of createResult */ + + ABC_NAMESPACE_IMPL_END -- cgit v1.2.3