abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions | Variables
cuddPriority.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Macros

#define DD_DEBUG   1
 

Functions

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)
 
DdNode * Cudd_PrioritySelect (DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DD_PRFP Pifunc)
 
DdNode * Cudd_Xgty (DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y)
 
DdNode * Cudd_Xeqy (DdManager *dd, int N, DdNode **x, DdNode **y)
 
DdNode * Cudd_addXeqy (DdManager *dd, int N, DdNode **x, DdNode **y)
 
DdNode * Cudd_Dxygtdxz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
 
DdNode * Cudd_Dxygtdyz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
 
DdNode * Cudd_Inequality (DdManager *dd, int N, int c, DdNode **x, DdNode **y)
 
DdNode * Cudd_Disequality (DdManager *dd, int N, int c, DdNode **x, DdNode **y)
 
DdNode * Cudd_bddInterval (DdManager *dd, int N, DdNode **x, unsigned int lowerB, unsigned int upperB)
 
DdNode * Cudd_CProjection (DdManager *dd, DdNode *R, DdNode *Y)
 
DdNode * Cudd_addHamming (DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars)
 
int Cudd_MinHammingDist (DdManager *dd, DdNode *f, int *minterm, int upperBound)
 
DdNode * Cudd_bddClosestCube (DdManager *dd, DdNode *f, DdNode *g, int *distance)
 
DdNode * cuddCProjectionRecur (DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)
 
DdNode * cuddBddClosestCube (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)
 

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $"
 

Macro Definition Documentation

#define DD_DEBUG   1

CFile***********************************************************************

FileName [cuddPriority.c]

PackageName [cudd]

Synopsis [Priority functions.]

Description [External procedures included in this file:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso []

Author [Fabio Somenzi]

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.]

Definition at line 88 of file cuddPriority.c.

Function Documentation

static DdNode * createResult ( DdManager *  dd,
unsigned int  index,
unsigned int  phase,
DdNode *  cube,
CUDD_VALUE_TYPE  distance 
)
static

Function********************************************************************

Synopsis [Builds a result for cache storage.]

Description [Builds a result for cache storage. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddBddClosestCube separateCube]

Definition at line 1987 of file cuddPriority.c.

1993 {
1994  DdNode *res, *constant;
1995 
1996  /* Special case. The cube is either one or zero, and we do not
1997  ** add any variables. Hence, the result is also one or zero,
1998  ** and the distance remains implied by the value of the constant. */
1999  if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);
2000 
2001  constant = cuddUniqueConst(dd,-distance);
2002  if (constant == NULL) return(NULL);
2003  cuddRef(constant);
2004 
2005  if (index == CUDD_CONST_INDEX) {
2006  /* Replace the top node. */
2007  if (cuddT(cube) == DD_ZERO(dd)) {
2008  res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
2009  } else {
2010  res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
2011  }
2012  } else {
2013  /* Add a new top node. */
2014 #ifdef DD_DEBUG
2015  assert(cuddI(dd,index) < cuddI(dd,cube->index));
2016 #endif
2017  if (phase) {
2018  res = cuddUniqueInter(dd,index,cube,constant);
2019  } else {
2020  res = cuddUniqueInter(dd,index,constant,cube);
2021  }
2022  }
2023  if (res == NULL) {
2024  Cudd_RecursiveDeref(dd, constant);
2025  return(NULL);
2026  }
2027  cuddDeref(constant); /* safe because constant is part of res */
2028 
2029  return(res);
2030 
2031 } /* end of createResult */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
CUDD_CONST_INDEX
#define CUDD_CONST_INDEX
Definition: cudd.h:117
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
phase
static pcube phase
Definition: cvrm.c:405
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addHamming ( DdManager *  dd,
DdNode **  xVars,
DdNode **  yVars,
int  nVars 
)

Function********************************************************************

Synopsis [Computes the Hamming distance ADD.]

Description [Computes the Hamming distance ADD. Returns an ADD that gives the Hamming distance between its two arguments if successful; NULL otherwise. The two vectors xVars and yVars identify the variables that form the two arguments.]

SideEffects [None]

SeeAlso []

Definition at line 1255 of file cuddPriority.c.

1260 {
1261  DdNode *result,*tempBdd;
1262  DdNode *tempAdd,*temp;
1263  int i;
1264 
1265  result = DD_ZERO(dd);
1266  cuddRef(result);
1267 
1268  for (i = 0; i < nVars; i++) {
1269  tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
1270  if (tempBdd == NULL) {
1271  Cudd_RecursiveDeref(dd,result);
1272  return(NULL);
1273  }
1274  cuddRef(tempBdd);
1275  tempAdd = Cudd_BddToAdd(dd,tempBdd);
1276  if (tempAdd == NULL) {
1277  Cudd_RecursiveDeref(dd,tempBdd);
1278  Cudd_RecursiveDeref(dd,result);
1279  return(NULL);
1280  }
1281  cuddRef(tempAdd);
1282  Cudd_RecursiveDeref(dd,tempBdd);
1283  temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
1284  if (temp == NULL) {
1285  Cudd_RecursiveDeref(dd,tempAdd);
1286  Cudd_RecursiveDeref(dd,result);
1287  return(NULL);
1288  }
1289  cuddRef(temp);
1290  Cudd_RecursiveDeref(dd,tempAdd);
1291  Cudd_RecursiveDeref(dd,result);
1292  result = temp;
1293  }
1294 
1295  cuddDeref(result);
1296  return(result);
1297 
1298 } /* end of Cudd_addHamming */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_addApply
DdNode * Cudd_addApply(DdManager *dd, DdNode *(*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Cudd_addPlus
DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:168
Cudd_BddToAdd
DdNode * Cudd_BddToAdd(DdManager *dd, DdNode *B)
Definition: cuddBridge.c:349
result
static int result
Definition: cuddGenetic.c:125
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_addXeqy ( DdManager *  dd,
int  N,
DdNode **  x,
DdNode **  y 
)

Function********************************************************************

Synopsis [Generates an ADD for the function x==y.]

Description [This function generates an ADD for the function x==y. 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: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1]. ]

SideEffects [None]

SeeAlso [Cudd_Xeqy]

Definition at line 408 of file cuddPriority.c.

413 {
414  DdNode *one, *zero;
415  DdNode *u, *v, *w;
416  int i;
417 
418  one = DD_ONE(dd);
419  zero = DD_ZERO(dd);
420 
421  /* Build bottom part of ADD outside loop. */
422  v = Cudd_addIte(dd, y[N-1], one, zero);
423  if (v == NULL) return(NULL);
424  cuddRef(v);
425  w = Cudd_addIte(dd, y[N-1], zero, one);
426  if (w == NULL) {
427  Cudd_RecursiveDeref(dd, v);
428  return(NULL);
429  }
430  cuddRef(w);
431  u = Cudd_addIte(dd, x[N-1], v, w);
432  if (u == NULL) {
433  Cudd_RecursiveDeref(dd, v);
434  Cudd_RecursiveDeref(dd, w);
435  return(NULL);
436  }
437  cuddRef(u);
438  Cudd_RecursiveDeref(dd, v);
439  Cudd_RecursiveDeref(dd, w);
440 
441  /* Loop to build the rest of the ADD. */
442  for (i = N-2; i >= 0; i--) {
443  v = Cudd_addIte(dd, y[i], u, zero);
444  if (v == NULL) {
445  Cudd_RecursiveDeref(dd, u);
446  return(NULL);
447  }
448  cuddRef(v);
449  w = Cudd_addIte(dd, y[i], zero, u);
450  if (w == NULL) {
451  Cudd_RecursiveDeref(dd, u);
452  Cudd_RecursiveDeref(dd, v);
453  return(NULL);
454  }
455  cuddRef(w);
456  Cudd_RecursiveDeref(dd, u);
457  u = Cudd_addIte(dd, x[i], v, w);
458  if (w == NULL) {
459  Cudd_RecursiveDeref(dd, v);
460  Cudd_RecursiveDeref(dd, w);
461  return(NULL);
462  }
463  cuddRef(u);
464  Cudd_RecursiveDeref(dd, v);
465  Cudd_RecursiveDeref(dd, w);
466  }
467  cuddDeref(u);
468  return(u);
469 
470 } /* end of Cudd_addXeqy */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
one
static DdNode * one
Definition: cuddDecomp.c:112
Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* Cudd_bddClosestCube ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
int *  distance 
)

Function********************************************************************

Synopsis [Finds a cube of f at minimum Hamming distance from g.]

Description [Finds a cube of f at minimum Hamming distance from the minterms of g. All the minterms of the cube are at the minimum distance. If the distance is 0, the cube belongs to the intersection of f and g. Returns the cube if successful; NULL otherwise.]

SideEffects [The distance is returned as a side effect.]

SeeAlso [Cudd_MinHammingDist]

Definition at line 1359 of file cuddPriority.c.

1364 {
1365  DdNode *res, *acube;
1366  CUDD_VALUE_TYPE rdist;
1367 
1368  /* Compute the cube and distance as a single ADD. */
1369  do {
1370  dd->reordered = 0;
1371  res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
1372  } while (dd->reordered == 1);
1373  if (res == NULL) return(NULL);
1374  cuddRef(res);
1375 
1376  /* Unpack distance and cube. */
1377  do {
1378  dd->reordered = 0;
1379  acube = separateCube(dd, res, &rdist);
1380  } while (dd->reordered == 1);
1381  if (acube == NULL) {
1382  Cudd_RecursiveDeref(dd, res);
1383  return(NULL);
1384  }
1385  cuddRef(acube);
1386  Cudd_RecursiveDeref(dd, res);
1387 
1388  /* Convert cube from ADD to BDD. */
1389  do {
1390  dd->reordered = 0;
1391  res = cuddAddBddDoPattern(dd, acube);
1392  } while (dd->reordered == 1);
1393  if (res == NULL) {
1394  Cudd_RecursiveDeref(dd, acube);
1395  return(NULL);
1396  }
1397  cuddRef(res);
1398  Cudd_RecursiveDeref(dd, acube);
1399 
1400  *distance = (int) rdist;
1401  cuddDeref(res);
1402  return(res);
1403 
1404 } /* end of Cudd_bddClosestCube */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
separateCube
static DdNode * separateCube(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance)
Definition: cuddPriority.c:1938
DdManager::reordered
int reordered
Definition: cuddInt.h:409
cuddAddBddDoPattern
DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f)
Definition: cuddBridge.c:493
CUDD_CONST_INDEX
#define CUDD_CONST_INDEX
Definition: cudd.h:117
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
cuddBddClosestCube
DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)
Definition: cuddPriority.c:1646
DdNode* Cudd_bddInterval ( DdManager *  dd,
int  N,
DdNode **  x,
unsigned int  lowerB,
unsigned int  upperB 
)

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]

Definition at line 1121 of file cuddPriority.c.

1127 {
1128  DdNode *one, *zero;
1129  DdNode *r, *rl, *ru;
1130  int i;
1131 
1132  one = DD_ONE(dd);
1133  zero = Cudd_Not(one);
1134 
1135  rl = one;
1136  cuddRef(rl);
1137  ru = one;
1138  cuddRef(ru);
1139 
1140  /* Loop to build the rest of the BDDs. */
1141  for (i = N-1; i >= 0; i--) {
1142  DdNode *vl, *vu;
1143  vl = Cudd_bddIte(dd, x[i],
1144  lowerB&1 ? rl : one,
1145  lowerB&1 ? zero : rl);
1146  if (vl == NULL) {
1147  Cudd_IterDerefBdd(dd, rl);
1148  Cudd_IterDerefBdd(dd, ru);
1149  return(NULL);
1150  }
1151  cuddRef(vl);
1152  Cudd_IterDerefBdd(dd, rl);
1153  rl = vl;
1154  lowerB >>= 1;
1155  vu = Cudd_bddIte(dd, x[i],
1156  upperB&1 ? ru : zero,
1157  upperB&1 ? one : ru);
1158  if (vu == NULL) {
1159  Cudd_IterDerefBdd(dd, rl);
1160  Cudd_IterDerefBdd(dd, ru);
1161  return(NULL);
1162  }
1163  cuddRef(vu);
1164  Cudd_IterDerefBdd(dd, ru);
1165  ru = vu;
1166  upperB >>= 1;
1167  }
1168 
1169  /* Conjoin the two bounds. */
1170  r = Cudd_bddAnd(dd, rl, ru);
1171  if (r == NULL) {
1172  Cudd_IterDerefBdd(dd, rl);
1173  Cudd_IterDerefBdd(dd, ru);
1174  return(NULL);
1175  }
1176  cuddRef(r);
1177  Cudd_IterDerefBdd(dd, rl);
1178  Cudd_IterDerefBdd(dd, ru);
1179  cuddDeref(r);
1180  return(r);
1181 
1182 } /* end of Cudd_bddInterval */
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
one
static DdNode * one
Definition: cuddDecomp.c:112
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DdNode* Cudd_CProjection ( DdManager *  dd,
DdNode *  R,
DdNode *  Y 
)

Function********************************************************************

Synopsis [Computes the compatible projection of R w.r.t. cube Y.]

Description [Computes the compatible projection of relation R with respect to cube Y. Returns a pointer to the c-projection if successful; NULL otherwise. For a comparison between Cudd_CProjection and Cudd_PrioritySelect, see the documentation of the latter.]

SideEffects [None]

SeeAlso [Cudd_PrioritySelect]

Definition at line 1200 of file cuddPriority.c.

1204 {
1205  DdNode *res;
1206  DdNode *support;
1207 
1208  if (cuddCheckCube(dd,Y) == 0) {
1209  (void) fprintf(dd->err,
1210  "Error: The third argument of Cudd_CProjection should be a cube\n");
1211  dd->errorCode = CUDD_INVALID_ARG;
1212  return(NULL);
1213  }
1214 
1215  /* Compute the support of Y, which is used by the abstraction step
1216  ** in cuddCProjectionRecur.
1217  */
1218  support = Cudd_Support(dd,Y);
1219  if (support == NULL) return(NULL);
1220  cuddRef(support);
1221 
1222  do {
1223  dd->reordered = 0;
1224  res = cuddCProjectionRecur(dd,R,Y,support);
1225  } while (dd->reordered == 1);
1226 
1227  if (res == NULL) {
1228  Cudd_RecursiveDeref(dd,support);
1229  return(NULL);
1230  }
1231  cuddRef(res);
1232  Cudd_RecursiveDeref(dd,support);
1233  cuddDeref(res);
1234 
1235  return(res);
1236 
1237 } /* end of Cudd_CProjection */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
DdManager::err
FILE * err
Definition: cuddInt.h:442
cuddCheckCube
int cuddCheckCube(DdManager *dd, DdNode *g)
Definition: cuddCof.c:193
cuddCProjectionRecur
DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)
Definition: cuddPriority.c:1425
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
DdNode* Cudd_Disequality ( DdManager *  dd,
int  N,
int  c,
DdNode **  x,
DdNode **  y 
)

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]

Definition at line 932 of file cuddPriority.c.

938 {
939  /* The nodes at level i represent values of the difference that are
940  ** multiples of 2^i. We use variables with names starting with k
941  ** to denote the multipliers of 2^i in such multiples. */
942  int kTrueLb = c + 1;
943  int kTrueUb = c - 1;
944  int kFalse = c;
945  /* Mask used to compute the ceiling function. Since we divide by 2^i,
946  ** we want to know whether the dividend is a multiple of 2^i. If it is,
947  ** then ceiling and floor coincide; otherwise, they differ by one. */
948  int mask = 1;
949  int i;
950 
951  DdNode *f = NULL; /* the eventual result */
952  DdNode *one = DD_ONE(dd);
953  DdNode *zero = Cudd_Not(one);
954 
955  /* Two x-labeled nodes are created at most at each iteration. They are
956  ** stored, along with their k values, in these variables. At each level,
957  ** the old nodes are freed and the new nodes are copied into the old map.
958  */
959  DdNode *map[2] = {0};
960  int invalidIndex = 1 << (N-1);
961  int index[2] = {invalidIndex, invalidIndex};
962 
963  /* This should never happen. */
964  if (N < 0) return(NULL);
965 
966  /* If there are no bits, both operands are 0. The result depends on c. */
967  if (N == 0) {
968  if (c != 0) return(one);
969  else return(zero);
970  }
971 
972  /* The maximum or the minimum difference comparing to c can generate the terminal case */
973  if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(one);
974 
975  /* Build the result bottom up. */
976  for (i = 1; i <= N; i++) {
977  int kTrueLbLower, kTrueUbLower;
978  int leftChild, middleChild, rightChild;
979  DdNode *g0, *g1, *fplus, *fequal, *fminus;
980  int j;
981  DdNode *newMap[2] = {NULL};
982  int newIndex[2];
983 
984  kTrueLbLower = kTrueLb;
985  kTrueUbLower = kTrueUb;
986  /* kTrueLb = floor((c-1)/2^i) + 2 */
987  kTrueLb = ((c-1) >> i) + 2;
988  /* kTrueUb = ceiling((c+1)/2^i) - 2 */
989  kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2;
990  mask = (mask << 1) | 1;
991  newIndex[0] = invalidIndex;
992  newIndex[1] = invalidIndex;
993 
994  for (j = kTrueUb + 1; j < kTrueLb; j++) {
995  /* Skip if node is not reachable from top of BDD. */
996  if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
997 
998  /* Find f- */
999  leftChild = (j << 1) - 1;
1000  if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
1001  fminus = one;
1002  } else if (i == 1 && leftChild == kFalse) {
1003  fminus = zero;
1004  } else {
1005  assert(leftChild == index[0] || leftChild == index[1]);
1006  if (leftChild == index[0]) {
1007  fminus = map[0];
1008  } else {
1009  fminus = map[1];
1010  }
1011  }
1012 
1013  /* Find f= */
1014  middleChild = j << 1;
1015  if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
1016  fequal = one;
1017  } else if (i == 1 && middleChild == kFalse) {
1018  fequal = zero;
1019  } else {
1020  assert(middleChild == index[0] || middleChild == index[1]);
1021  if (middleChild == index[0]) {
1022  fequal = map[0];
1023  } else {
1024  fequal = map[1];
1025  }
1026  }
1027 
1028  /* Find f+ */
1029  rightChild = (j << 1) + 1;
1030  if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
1031  fplus = one;
1032  } else if (i == 1 && rightChild == kFalse) {
1033  fplus = zero;
1034  } else {
1035  assert(rightChild == index[0] || rightChild == index[1]);
1036  if (rightChild == index[0]) {
1037  fplus = map[0];
1038  } else {
1039  fplus = map[1];
1040  }
1041  }
1042 
1043  /* Build new nodes. */
1044  g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
1045  if (g1 == NULL) {
1046  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1047  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1048  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1049  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1050  return(NULL);
1051  }
1052  cuddRef(g1);
1053  g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
1054  if (g0 == NULL) {
1055  Cudd_IterDerefBdd(dd, g1);
1056  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1057  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1058  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1059  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1060  return(NULL);
1061  }
1062  cuddRef(g0);
1063  f = Cudd_bddIte(dd, x[N - i], g1, g0);
1064  if (f == NULL) {
1065  Cudd_IterDerefBdd(dd, g1);
1066  Cudd_IterDerefBdd(dd, g0);
1067  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1068  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1069  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
1070  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
1071  return(NULL);
1072  }
1073  cuddRef(f);
1074  Cudd_IterDerefBdd(dd, g1);
1075  Cudd_IterDerefBdd(dd, g0);
1076 
1077  /* Save newly computed node in map. */
1078  assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
1079  if (newIndex[0] == invalidIndex) {
1080  newIndex[0] = j;
1081  newMap[0] = f;
1082  } else {
1083  newIndex[1] = j;
1084  newMap[1] = f;
1085  }
1086  }
1087 
1088  /* Copy new map to map. */
1089  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
1090  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
1091  map[0] = newMap[0];
1092  map[1] = newMap[1];
1093  index[0] = newIndex[0];
1094  index[1] = newIndex[1];
1095  }
1096 
1097  cuddDeref(f);
1098  return(f);
1099 
1100 } /* end of Cudd_Disequality */
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
map
void map()
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
one
static DdNode * one
Definition: cuddDecomp.c:112
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DdNode* Cudd_Dxygtdxz ( DdManager *  dd,
int  N,
DdNode **  x,
DdNode **  y,
DdNode **  z 
)

Function********************************************************************

Synopsis [Generates a BDD for the function d(x,y) > d(x,z).]

Description [This function generates a BDD for the function d(x,y) > d(x,z); x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1], 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: {i=0}^{N-1}(|x_i - y_i| 2^{N-i-1}). The BDD is built bottom-up. 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]

SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX]

Definition at line 494 of file cuddPriority.c.

500 {
501  DdNode *one, *zero;
502  DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
503  int i;
504 
505  one = DD_ONE(dd);
506  zero = Cudd_Not(one);
507 
508  /* Build bottom part of BDD outside loop. */
509  y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1]));
510  if (y1_ == NULL) return(NULL);
511  cuddRef(y1_);
512  y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
513  if (y2 == NULL) {
514  Cudd_RecursiveDeref(dd, y1_);
515  return(NULL);
516  }
517  cuddRef(y2);
518  x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
519  if (x1 == NULL) {
520  Cudd_RecursiveDeref(dd, y1_);
521  Cudd_RecursiveDeref(dd, y2);
522  return(NULL);
523  }
524  cuddRef(x1);
525  Cudd_RecursiveDeref(dd, y1_);
526  Cudd_RecursiveDeref(dd, y2);
527 
528  /* Loop to build the rest of the BDD. */
529  for (i = N-2; i >= 0; i--) {
530  z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
531  if (z1 == NULL) {
532  Cudd_RecursiveDeref(dd, x1);
533  return(NULL);
534  }
535  cuddRef(z1);
536  z2 = Cudd_bddIte(dd, z[i], x1, one);
537  if (z2 == NULL) {
538  Cudd_RecursiveDeref(dd, x1);
539  Cudd_RecursiveDeref(dd, z1);
540  return(NULL);
541  }
542  cuddRef(z2);
543  z3 = Cudd_bddIte(dd, z[i], one, x1);
544  if (z3 == NULL) {
545  Cudd_RecursiveDeref(dd, x1);
546  Cudd_RecursiveDeref(dd, z1);
547  Cudd_RecursiveDeref(dd, z2);
548  return(NULL);
549  }
550  cuddRef(z3);
551  z4 = Cudd_bddIte(dd, z[i], x1, zero);
552  if (z4 == NULL) {
553  Cudd_RecursiveDeref(dd, x1);
554  Cudd_RecursiveDeref(dd, z1);
555  Cudd_RecursiveDeref(dd, z2);
556  Cudd_RecursiveDeref(dd, z3);
557  return(NULL);
558  }
559  cuddRef(z4);
560  Cudd_RecursiveDeref(dd, x1);
561  y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
562  if (y1_ == NULL) {
563  Cudd_RecursiveDeref(dd, z1);
564  Cudd_RecursiveDeref(dd, z2);
565  Cudd_RecursiveDeref(dd, z3);
566  Cudd_RecursiveDeref(dd, z4);
567  return(NULL);
568  }
569  cuddRef(y1_);
570  y2 = Cudd_bddIte(dd, y[i], z4, z3);
571  if (y2 == NULL) {
572  Cudd_RecursiveDeref(dd, z1);
573  Cudd_RecursiveDeref(dd, z2);
574  Cudd_RecursiveDeref(dd, z3);
575  Cudd_RecursiveDeref(dd, z4);
576  Cudd_RecursiveDeref(dd, y1_);
577  return(NULL);
578  }
579  cuddRef(y2);
580  Cudd_RecursiveDeref(dd, z1);
581  Cudd_RecursiveDeref(dd, z2);
582  Cudd_RecursiveDeref(dd, z3);
583  Cudd_RecursiveDeref(dd, z4);
584  x1 = Cudd_bddIte(dd, x[i], y1_, y2);
585  if (x1 == NULL) {
586  Cudd_RecursiveDeref(dd, y1_);
587  Cudd_RecursiveDeref(dd, y2);
588  return(NULL);
589  }
590  cuddRef(x1);
591  Cudd_RecursiveDeref(dd, y1_);
592  Cudd_RecursiveDeref(dd, y2);
593  }
594  cuddDeref(x1);
595  return(Cudd_Not(x1));
596 
597 } /* end of Cudd_Dxygtdxz */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
z1
#define z1
Definition: extraBdd.h:78
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
one
static DdNode * one
Definition: cuddDecomp.c:112
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DdNode* Cudd_Dxygtdyz ( DdManager *  dd,
int  N,
DdNode **  x,
DdNode **  y,
DdNode **  z 
)

Function********************************************************************

Synopsis [Generates a BDD for the function d(x,y) > d(y,z).]

Description [This function generates a BDD for the function d(x,y) > d(y,z); x, y, and z are N-bit numbers, x[0] x[1] ... x[N-1], 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: {i=0}^{N-1}(|x_i - y_i| 2^{N-i-1}). The BDD is built bottom-up. 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]

SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX]

Definition at line 621 of file cuddPriority.c.

627 {
628  DdNode *one, *zero;
629  DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
630  int i;
631 
632  one = DD_ONE(dd);
633  zero = Cudd_Not(one);
634 
635  /* Build bottom part of BDD outside loop. */
636  y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);
637  if (y1_ == NULL) return(NULL);
638  cuddRef(y1_);
639  y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
640  if (y2 == NULL) {
641  Cudd_RecursiveDeref(dd, y1_);
642  return(NULL);
643  }
644  cuddRef(y2);
645  x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
646  if (x1 == NULL) {
647  Cudd_RecursiveDeref(dd, y1_);
648  Cudd_RecursiveDeref(dd, y2);
649  return(NULL);
650  }
651  cuddRef(x1);
652  Cudd_RecursiveDeref(dd, y1_);
653  Cudd_RecursiveDeref(dd, y2);
654 
655  /* Loop to build the rest of the BDD. */
656  for (i = N-2; i >= 0; i--) {
657  z1 = Cudd_bddIte(dd, z[i], x1, zero);
658  if (z1 == NULL) {
659  Cudd_RecursiveDeref(dd, x1);
660  return(NULL);
661  }
662  cuddRef(z1);
663  z2 = Cudd_bddIte(dd, z[i], x1, one);
664  if (z2 == NULL) {
665  Cudd_RecursiveDeref(dd, x1);
666  Cudd_RecursiveDeref(dd, z1);
667  return(NULL);
668  }
669  cuddRef(z2);
670  z3 = Cudd_bddIte(dd, z[i], one, x1);
671  if (z3 == NULL) {
672  Cudd_RecursiveDeref(dd, x1);
673  Cudd_RecursiveDeref(dd, z1);
674  Cudd_RecursiveDeref(dd, z2);
675  return(NULL);
676  }
677  cuddRef(z3);
678  z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
679  if (z4 == NULL) {
680  Cudd_RecursiveDeref(dd, x1);
681  Cudd_RecursiveDeref(dd, z1);
682  Cudd_RecursiveDeref(dd, z2);
683  Cudd_RecursiveDeref(dd, z3);
684  return(NULL);
685  }
686  cuddRef(z4);
687  Cudd_RecursiveDeref(dd, x1);
688  y1_ = Cudd_bddIte(dd, y[i], z2, z1);
689  if (y1_ == NULL) {
690  Cudd_RecursiveDeref(dd, z1);
691  Cudd_RecursiveDeref(dd, z2);
692  Cudd_RecursiveDeref(dd, z3);
693  Cudd_RecursiveDeref(dd, z4);
694  return(NULL);
695  }
696  cuddRef(y1_);
697  y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
698  if (y2 == NULL) {
699  Cudd_RecursiveDeref(dd, z1);
700  Cudd_RecursiveDeref(dd, z2);
701  Cudd_RecursiveDeref(dd, z3);
702  Cudd_RecursiveDeref(dd, z4);
703  Cudd_RecursiveDeref(dd, y1_);
704  return(NULL);
705  }
706  cuddRef(y2);
707  Cudd_RecursiveDeref(dd, z1);
708  Cudd_RecursiveDeref(dd, z2);
709  Cudd_RecursiveDeref(dd, z3);
710  Cudd_RecursiveDeref(dd, z4);
711  x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2));
712  if (x1 == NULL) {
713  Cudd_RecursiveDeref(dd, y1_);
714  Cudd_RecursiveDeref(dd, y2);
715  return(NULL);
716  }
717  cuddRef(x1);
718  Cudd_RecursiveDeref(dd, y1_);
719  Cudd_RecursiveDeref(dd, y2);
720  }
721  cuddDeref(x1);
722  return(Cudd_Not(x1));
723 
724 } /* end of Cudd_Dxygtdyz */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
z1
#define z1
Definition: extraBdd.h:78
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
one
static DdNode * one
Definition: cuddDecomp.c:112
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DdNode* Cudd_Inequality ( DdManager *  dd,
int  N,
int  c,
DdNode **  x,
DdNode **  y 
)

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]

Definition at line 744 of file cuddPriority.c.

750 {
751  /* The nodes at level i represent values of the difference that are
752  ** multiples of 2^i. We use variables with names starting with k
753  ** to denote the multipliers of 2^i in such multiples. */
754  int kTrue = c;
755  int kFalse = c - 1;
756  /* Mask used to compute the ceiling function. Since we divide by 2^i,
757  ** we want to know whether the dividend is a multiple of 2^i. If it is,
758  ** then ceiling and floor coincide; otherwise, they differ by one. */
759  int mask = 1;
760  int i;
761 
762  DdNode *f = NULL; /* the eventual result */
763  DdNode *one = DD_ONE(dd);
764  DdNode *zero = Cudd_Not(one);
765 
766  /* Two x-labeled nodes are created at most at each iteration. They are
767  ** stored, along with their k values, in these variables. At each level,
768  ** the old nodes are freed and the new nodes are copied into the old map.
769  */
770  DdNode *map[2] = {0};
771  int invalidIndex = 1 << (N-1);
772  int index[2] = {invalidIndex, invalidIndex};
773 
774  /* This should never happen. */
775  if (N < 0) return(NULL);
776 
777  /* If there are no bits, both operands are 0. The result depends on c. */
778  if (N == 0) {
779  if (c >= 0) return(one);
780  else return(zero);
781  }
782 
783  /* The maximum or the minimum difference comparing to c can generate the terminal case */
784  if ((1 << N) - 1 < c) return(zero);
785  else if ((-(1 << N) + 1) >= c) return(one);
786 
787  /* Build the result bottom up. */
788  for (i = 1; i <= N; i++) {
789  int kTrueLower, kFalseLower;
790  int leftChild, middleChild, rightChild;
791  DdNode *g0, *g1, *fplus, *fequal, *fminus;
792  int j;
793  DdNode *newMap[2] = {NULL};
794  int newIndex[2];
795 
796  kTrueLower = kTrue;
797  kFalseLower = kFalse;
798  /* kTrue = ceiling((c-1)/2^i) + 1 */
799  kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1;
800  mask = (mask << 1) | 1;
801  /* kFalse = floor(c/2^i) - 1 */
802  kFalse = (c >> i) - 1;
803  newIndex[0] = invalidIndex;
804  newIndex[1] = invalidIndex;
805 
806  for (j = kFalse + 1; j < kTrue; j++) {
807  /* Skip if node is not reachable from top of BDD. */
808  if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
809 
810  /* Find f- */
811  leftChild = (j << 1) - 1;
812  if (leftChild >= kTrueLower) {
813  fminus = one;
814  } else if (leftChild <= kFalseLower) {
815  fminus = zero;
816  } else {
817  assert(leftChild == index[0] || leftChild == index[1]);
818  if (leftChild == index[0]) {
819  fminus = map[0];
820  } else {
821  fminus = map[1];
822  }
823  }
824 
825  /* Find f= */
826  middleChild = j << 1;
827  if (middleChild >= kTrueLower) {
828  fequal = one;
829  } else if (middleChild <= kFalseLower) {
830  fequal = zero;
831  } else {
832  assert(middleChild == index[0] || middleChild == index[1]);
833  if (middleChild == index[0]) {
834  fequal = map[0];
835  } else {
836  fequal = map[1];
837  }
838  }
839 
840  /* Find f+ */
841  rightChild = (j << 1) + 1;
842  if (rightChild >= kTrueLower) {
843  fplus = one;
844  } else if (rightChild <= kFalseLower) {
845  fplus = zero;
846  } else {
847  assert(rightChild == index[0] || rightChild == index[1]);
848  if (rightChild == index[0]) {
849  fplus = map[0];
850  } else {
851  fplus = map[1];
852  }
853  }
854 
855  /* Build new nodes. */
856  g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
857  if (g1 == NULL) {
858  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
859  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
860  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
861  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
862  return(NULL);
863  }
864  cuddRef(g1);
865  g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
866  if (g0 == NULL) {
867  Cudd_IterDerefBdd(dd, g1);
868  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
869  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
870  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
871  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
872  return(NULL);
873  }
874  cuddRef(g0);
875  f = Cudd_bddIte(dd, x[N - i], g1, g0);
876  if (f == NULL) {
877  Cudd_IterDerefBdd(dd, g1);
878  Cudd_IterDerefBdd(dd, g0);
879  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
880  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
881  if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
882  if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
883  return(NULL);
884  }
885  cuddRef(f);
886  Cudd_IterDerefBdd(dd, g1);
887  Cudd_IterDerefBdd(dd, g0);
888 
889  /* Save newly computed node in map. */
890  assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
891  if (newIndex[0] == invalidIndex) {
892  newIndex[0] = j;
893  newMap[0] = f;
894  } else {
895  newIndex[1] = j;
896  newMap[1] = f;
897  }
898  }
899 
900  /* Copy new map to map. */
901  if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
902  if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
903  map[0] = newMap[0];
904  map[1] = newMap[1];
905  index[0] = newIndex[0];
906  index[1] = newIndex[1];
907  }
908 
909  cuddDeref(f);
910  return(f);
911 
912 } /* end of Cudd_Inequality */
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
map
void map()
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
one
static DdNode * one
Definition: cuddDecomp.c:112
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
int Cudd_MinHammingDist ( DdManager *  dd,
DdNode *  f,
int *  minterm,
int  upperBound 
)

Function********************************************************************

Synopsis [Returns the minimum Hamming distance between f and minterm.]

Description [Returns the minimum Hamming distance between the minterms of a function f and a reference minterm. The function is given as a BDD; the minterm is given as an array of integers, one for each variable in the manager. Returns the minimum distance if it is less than the upper bound; the upper bound if the minimum distance is at least as large; CUDD_OUT_OF_MEM in case of failure.]

SideEffects [None]

SeeAlso [Cudd_addHamming Cudd_bddClosestCube]

Definition at line 1318 of file cuddPriority.c.

1323 {
1324  DdHashTable *table;
1325  CUDD_VALUE_TYPE epsilon;
1326  int res;
1327 
1328  table = cuddHashTableInit(dd,1,2);
1329  if (table == NULL) {
1330  return(CUDD_OUT_OF_MEM);
1331  }
1332  epsilon = Cudd_ReadEpsilon(dd);
1333  Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
1334  res = cuddMinHammingDistRecur(f,minterm,table,upperBound);
1335  cuddHashTableQuit(table);
1336  Cudd_SetEpsilon(dd,epsilon);
1337 
1338  return(res);
1339 
1340 } /* end of Cudd_MinHammingDist */
CUDD_OUT_OF_MEM
#define CUDD_OUT_OF_MEM
Definition: cudd.h:95
cuddMinHammingDistRecur
static int cuddMinHammingDistRecur(DdNode *f, int *minterm, DdHashTable *table, int upperBound)
Definition: cuddPriority.c:1858
Cudd_SetEpsilon
void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep)
Definition: cuddAPI.c:2451
cuddHashTableQuit
void cuddHashTableQuit(DdHashTable *hash)
Definition: cuddLCache.c:595
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
cuddHashTableInit
DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize)
Definition: cuddLCache.c:538
Cudd_ReadEpsilon
CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd)
Definition: cuddAPI.c:2430
DdNode* Cudd_PrioritySelect ( DdManager *  dd,
DdNode *  R,
DdNode **  x,
DdNode **  y,
DdNode **  z,
DdNode *  Pi,
int  n,
DD_PRFP  Pifunc 
)

AutomaticEnd Function********************************************************************

Synopsis [Selects pairs from R using a priority function.]

Description [Selects pairs from a relation R(x,y) (given as a BDD) in such a way that a given x appears in one pair only. Uses a priority function to determine which y should be paired to a given x. Cudd_PrioritySelect returns a pointer to the selected function if successful; NULL otherwise. Three of the arguments–x, y, and z–are vectors of BDD variables. The first two are the variables on which R depends. The third vectore is a vector of auxiliary variables, used during the computation. This vector is optional. If a NULL value is passed instead, Cudd_PrioritySelect will create the working variables on the fly. The sizes of x and y (and z if it is not NULL) should equal n. The priority function Pi can be passed as a BDD, or can be built by Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the priority function. (Pifunc is a pointer to a C function.) If Pi is not NULL, then Pifunc is ignored. Pifunc should have the same interface as the standard priority functions (e.g., Cudd_Dxygtdxz). Cudd_PrioritySelect and Cudd_CProjection can sometimes be used interchangeably. Specifically, calling Cudd_PrioritySelect with Cudd_Xgty as Pifunc produces the same result as calling Cudd_CProjection with the all-zero minterm as reference minterm. However, depending on the application, one or the other may be preferable:

  • When extracting representatives from an equivalence relation, Cudd_CProjection has the advantage of nor requiring the auxiliary variables.
  • When computing matchings in general bipartite graphs, Cudd_PrioritySelect normally obtains better results because it can use more powerful matching schemes (e.g., Cudd_Dxygtdxz).

]

SideEffects [If called with z == NULL, will create new variables in the manager.]

SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX Cudd_CProjection]

Definition at line 175 of file cuddPriority.c.

184 {
185  DdNode *res = NULL;
186  DdNode *zcube = NULL;
187  DdNode *Rxz, *Q;
188  int createdZ = 0;
189  int createdPi = 0;
190  int i;
191 
192  /* Create z variables if needed. */
193  if (z == NULL) {
194  if (Pi != NULL) return(NULL);
195  z = ABC_ALLOC(DdNode *,n);
196  if (z == NULL) {
197  dd->errorCode = CUDD_MEMORY_OUT;
198  return(NULL);
199  }
200  createdZ = 1;
201  for (i = 0; i < n; i++) {
202  if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;
203  z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
204  if (z[i] == NULL) goto endgame;
205  }
206  }
207 
208  /* Create priority function BDD if needed. */
209  if (Pi == NULL) {
210  Pi = Pifunc(dd,n,x,y,z);
211  if (Pi == NULL) goto endgame;
212  createdPi = 1;
213  cuddRef(Pi);
214  }
215 
216  /* Initialize abstraction cube. */
217  zcube = DD_ONE(dd);
218  cuddRef(zcube);
219  for (i = n - 1; i >= 0; i--) {
220  DdNode *tmpp;
221  tmpp = Cudd_bddAnd(dd,z[i],zcube);
222  if (tmpp == NULL) goto endgame;
223  cuddRef(tmpp);
224  Cudd_RecursiveDeref(dd,zcube);
225  zcube = tmpp;
226  }
227 
228  /* Compute subset of (x,y) pairs. */
229  Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
230  if (Rxz == NULL) goto endgame;
231  cuddRef(Rxz);
232  Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
233  if (Q == NULL) {
234  Cudd_RecursiveDeref(dd,Rxz);
235  goto endgame;
236  }
237  cuddRef(Q);
238  Cudd_RecursiveDeref(dd,Rxz);
239  res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
240  if (res == NULL) {
241  Cudd_RecursiveDeref(dd,Q);
242  goto endgame;
243  }
244  cuddRef(res);
245  Cudd_RecursiveDeref(dd,Q);
246 
247 endgame:
248  if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
249  if (createdZ) {
250  ABC_FREE(z);
251  }
252  if (createdPi) {
253  Cudd_RecursiveDeref(dd,Pi);
254  }
255  if (res != NULL) cuddDeref(res);
256  return(res);
257 
258 } /* Cudd_PrioritySelect */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
DdManager::size
int size
Definition: cuddInt.h:361
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Cudd_bddSwapVariables
DdNode * Cudd_bddSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:464
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager::one
DdNode * one
Definition: cuddInt.h:345
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DdNode* Cudd_Xeqy ( DdManager *  dd,
int  N,
DdNode **  x,
DdNode **  y 
)

Function********************************************************************

Synopsis [Generates a BDD for the function x==y.]

Description [This function generates a BDD for the function x==y. 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: x[0] y[0] x[1] y[1] ... x[N-1] y[N-1]. ]

SideEffects [None]

SeeAlso [Cudd_addXeqy]

Definition at line 345 of file cuddPriority.c.

350 {
351  DdNode *u, *v, *w;
352  int i;
353 
354  /* Build bottom part of BDD outside loop. */
355  u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1]));
356  if (u == NULL) return(NULL);
357  cuddRef(u);
358 
359  /* Loop to build the rest of the BDD. */
360  for (i = N-2; i >= 0; i--) {
361  v = Cudd_bddAnd(dd, y[i], u);
362  if (v == NULL) {
363  Cudd_RecursiveDeref(dd, u);
364  return(NULL);
365  }
366  cuddRef(v);
367  w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
368  if (w == NULL) {
369  Cudd_RecursiveDeref(dd, u);
370  Cudd_RecursiveDeref(dd, v);
371  return(NULL);
372  }
373  cuddRef(w);
374  Cudd_RecursiveDeref(dd, u);
375  u = Cudd_bddIte(dd, x[i], v, w);
376  if (u == NULL) {
377  Cudd_RecursiveDeref(dd, v);
378  Cudd_RecursiveDeref(dd, w);
379  return(NULL);
380  }
381  cuddRef(u);
382  Cudd_RecursiveDeref(dd, v);
383  Cudd_RecursiveDeref(dd, w);
384  }
385  cuddDeref(u);
386  return(u);
387 
388 } /* end of Cudd_Xeqy */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
DdNode* Cudd_Xgty ( DdManager *  dd,
int  N,
DdNode **  z,
DdNode **  x,
DdNode **  y 
)

Function********************************************************************

Synopsis [Generates a BDD for the function x > y.]

Description [This function generates a BDD for the function x > y. 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: 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.]

SideEffects [None]

SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]

Definition at line 280 of file cuddPriority.c.

286 {
287  DdNode *u, *v, *w;
288  int i;
289 
290  /* Build bottom part of BDD outside loop. */
291  u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
292  if (u == NULL) return(NULL);
293  cuddRef(u);
294 
295  /* Loop to build the rest of the BDD. */
296  for (i = N-2; i >= 0; i--) {
297  v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
298  if (v == NULL) {
299  Cudd_RecursiveDeref(dd, u);
300  return(NULL);
301  }
302  cuddRef(v);
303  w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
304  if (w == NULL) {
305  Cudd_RecursiveDeref(dd, u);
306  Cudd_RecursiveDeref(dd, v);
307  return(NULL);
308  }
309  cuddRef(w);
310  Cudd_RecursiveDeref(dd, u);
311  u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
312  if (u == NULL) {
313  Cudd_RecursiveDeref(dd, v);
314  Cudd_RecursiveDeref(dd, w);
315  return(NULL);
316  }
317  cuddRef(u);
318  Cudd_RecursiveDeref(dd, v);
319  Cudd_RecursiveDeref(dd, w);
320 
321  }
322  cuddDeref(u);
323  return(u);
324 
325 } /* end of Cudd_Xgty */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
DdNode* cuddBddClosestCube ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
CUDD_VALUE_TYPE  bound 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_bddClosestCube.]

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 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.

  • If we already found two points at distance 0, there is no point in continuing. Furthermore,
  • If F == not(G) then the best we can hope for is a minimum distance of 1. If we have already found two points at distance 1, there is no point in continuing. (Indeed, H(F,G) == 1 in this case. We have to continue, though, to find the cube.)

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]

SeeAlso [Cudd_bddClosestCube]

Definition at line 1646 of file cuddPriority.c.

1651 {
1652  DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee;
1653  DdNode *ctt, *cee, *cte, *cet;
1654  CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
1655  DdNode *one = DD_ONE(dd);
1656  DdNode *lzero = Cudd_Not(one);
1657  DdNode *azero = DD_ZERO(dd);
1658  unsigned int topf, topg, index;
1659 
1660  statLine(dd);
1661  if (bound < (int)(f == Cudd_Not(g))) return(azero);
1662  /* Terminal cases. */
1663  if (g == lzero || f == lzero) return(azero);
1664  if (f == one && g == one) return(one);
1665 
1666  /* Check cache. */
1667  F = Cudd_Regular(f);
1668  G = Cudd_Regular(g);
1669  if (F->ref != 1 || G->ref != 1) {
1670  res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g);
1671  if (res != NULL) return(res);
1672  }
1673 
1674  topf = cuddI(dd,F->index);
1675  topg = cuddI(dd,G->index);
1676 
1677  /* Compute cofactors. */
1678  if (topf <= topg) {
1679  index = F->index;
1680  ft = cuddT(F);
1681  fe = cuddE(F);
1682  if (Cudd_IsComplement(f)) {
1683  ft = Cudd_Not(ft);
1684  fe = Cudd_Not(fe);
1685  }
1686  } else {
1687  index = G->index;
1688  ft = fe = f;
1689  }
1690 
1691  if (topg <= topf) {
1692  gt = cuddT(G);
1693  ge = cuddE(G);
1694  if (Cudd_IsComplement(g)) {
1695  gt = Cudd_Not(gt);
1696  ge = Cudd_Not(ge);
1697  }
1698  } else {
1699  gt = ge = g;
1700  }
1701 
1702  tt = cuddBddClosestCube(dd,ft,gt,bound);
1703  if (tt == NULL) return(NULL);
1704  cuddRef(tt);
1705  ctt = separateCube(dd,tt,&dtt);
1706  if (ctt == NULL) {
1707  Cudd_RecursiveDeref(dd, tt);
1708  return(NULL);
1709  }
1710  cuddRef(ctt);
1711  Cudd_RecursiveDeref(dd, tt);
1712  minD = dtt;
1713  bound = ddMin(bound,minD);
1714 
1715  ee = cuddBddClosestCube(dd,fe,ge,bound);
1716  if (ee == NULL) {
1717  Cudd_RecursiveDeref(dd, ctt);
1718  return(NULL);
1719  }
1720  cuddRef(ee);
1721  cee = separateCube(dd,ee,&dee);
1722  if (cee == NULL) {
1723  Cudd_RecursiveDeref(dd, ctt);
1724  Cudd_RecursiveDeref(dd, ee);
1725  return(NULL);
1726  }
1727  cuddRef(cee);
1728  Cudd_RecursiveDeref(dd, ee);
1729  minD = ddMin(dtt, dee);
1730  if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1731 
1732  if (minD > 0 && topf == topg) {
1733  DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
1734  if (te == NULL) {
1735  Cudd_RecursiveDeref(dd, ctt);
1736  Cudd_RecursiveDeref(dd, cee);
1737  return(NULL);
1738  }
1739  cuddRef(te);
1740  cte = separateCube(dd,te,&dte);
1741  if (cte == NULL) {
1742  Cudd_RecursiveDeref(dd, ctt);
1743  Cudd_RecursiveDeref(dd, cee);
1744  Cudd_RecursiveDeref(dd, te);
1745  return(NULL);
1746  }
1747  cuddRef(cte);
1748  Cudd_RecursiveDeref(dd, te);
1749  dte += 1.0;
1750  minD = ddMin(minD, dte);
1751  } else {
1752  cte = azero;
1753  cuddRef(cte);
1754  dte = CUDD_CONST_INDEX + 1.0;
1755  }
1756  if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
1757 
1758  if (minD > 0 && topf == topg) {
1759  DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
1760  if (et == NULL) {
1761  Cudd_RecursiveDeref(dd, ctt);
1762  Cudd_RecursiveDeref(dd, cee);
1763  Cudd_RecursiveDeref(dd, cte);
1764  return(NULL);
1765  }
1766  cuddRef(et);
1767  cet = separateCube(dd,et,&det);
1768  if (cet == NULL) {
1769  Cudd_RecursiveDeref(dd, ctt);
1770  Cudd_RecursiveDeref(dd, cee);
1771  Cudd_RecursiveDeref(dd, cte);
1772  Cudd_RecursiveDeref(dd, et);
1773  return(NULL);
1774  }
1775  cuddRef(cet);
1776  Cudd_RecursiveDeref(dd, et);
1777  det += 1.0;
1778  minD = ddMin(minD, det);
1779  } else {
1780  cet = azero;
1781  cuddRef(cet);
1782  det = CUDD_CONST_INDEX + 1.0;
1783  }
1784 
1785  if (minD == dtt) {
1786  if (dtt == dee && ctt == cee) {
1787  res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
1788  } else {
1789  res = createResult(dd,index,1,ctt,dtt);
1790  }
1791  } else if (minD == dee) {
1792  res = createResult(dd,index,0,cee,dee);
1793  } else if (minD == dte) {
1794 #ifdef DD_DEBUG
1795  assert(topf == topg);
1796 #endif
1797  res = createResult(dd,index,1,cte,dte);
1798  } else {
1799 #ifdef DD_DEBUG
1800  assert(topf == topg);
1801 #endif
1802  res = createResult(dd,index,0,cet,det);
1803  }
1804  if (res == NULL) {
1805  Cudd_RecursiveDeref(dd, ctt);
1806  Cudd_RecursiveDeref(dd, cee);
1807  Cudd_RecursiveDeref(dd, cte);
1808  Cudd_RecursiveDeref(dd, cet);
1809  return(NULL);
1810  }
1811  cuddRef(res);
1812  Cudd_RecursiveDeref(dd, ctt);
1813  Cudd_RecursiveDeref(dd, cee);
1814  Cudd_RecursiveDeref(dd, cte);
1815  Cudd_RecursiveDeref(dd, cet);
1816 
1817  /* Only cache results that are different from azero to avoid
1818  ** storing results that depend on the value of the bound. */
1819  if ((F->ref != 1 || G->ref != 1) && res != azero)
1820  cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res);
1821 
1822  cuddDeref(res);
1823  return(res);
1824 
1825 } /* end of cuddBddClosestCube */
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
Cudd_bddClosestCube
DdNode * Cudd_bddClosestCube(DdManager *dd, DdNode *f, DdNode *g, int *distance)
Definition: cuddPriority.c:1359
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DD_CTFP
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
Definition: cudd.h:321
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
separateCube
static DdNode * separateCube(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance)
Definition: cuddPriority.c:1938
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
one
static DdNode * one
Definition: cuddDecomp.c:112
CUDD_CONST_INDEX
#define CUDD_CONST_INDEX
Definition: cudd.h:117
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
cuddBddClosestCube
DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound)
Definition: cuddPriority.c:1646
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
createResult
static DdNode * createResult(DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance)
Definition: cuddPriority.c:1987
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
DdNode* cuddCProjectionRecur ( DdManager *  dd,
DdNode *  R,
DdNode *  Y,
DdNode *  Ysupp 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_CProjection.]

Description [Performs the recursive step of Cudd_CProjection. Returns the projection if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_CProjection]

Definition at line 1425 of file cuddPriority.c.

1430 {
1431  DdNode *res, *res1, *res2, *resA;
1432  DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
1433  unsigned int topR, topY, top, index = 0;
1434  DdNode *one = DD_ONE(dd);
1435 
1436  statLine(dd);
1437  if (Y == one) return(R);
1438 
1439 #ifdef DD_DEBUG
1440  assert(!Cudd_IsConstant(Y));
1441 #endif
1442 
1443  if (R == Cudd_Not(one)) return(R);
1444 
1445  res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
1446  if (res != NULL) return(res);
1447 
1448  r = Cudd_Regular(R);
1449  topR = cuddI(dd,r->index);
1450  y = Cudd_Regular(Y);
1451  topY = cuddI(dd,y->index);
1452 
1453  top = ddMin(topR, topY);
1454 
1455  /* Compute the cofactors of R */
1456  if (topR == top) {
1457  index = r->index;
1458  RT = cuddT(r);
1459  RE = cuddE(r);
1460  if (r != R) {
1461  RT = Cudd_Not(RT); RE = Cudd_Not(RE);
1462  }
1463  } else {
1464  RT = RE = R;
1465  }
1466 
1467  if (topY > top) {
1468  /* Y does not depend on the current top variable.
1469  ** We just need to compute the results on the two cofactors of R
1470  ** and make them the children of a node labeled r->index.
1471  */
1472  res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
1473  if (res1 == NULL) return(NULL);
1474  cuddRef(res1);
1475  res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
1476  if (res2 == NULL) {
1477  Cudd_RecursiveDeref(dd,res1);
1478  return(NULL);
1479  }
1480  cuddRef(res2);
1481  res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
1482  if (res == NULL) {
1483  Cudd_RecursiveDeref(dd,res1);
1484  Cudd_RecursiveDeref(dd,res2);
1485  return(NULL);
1486  }
1487  /* If we have reached this point, res1 and res2 are now
1488  ** incorporated in res. cuddDeref is therefore sufficient.
1489  */
1490  cuddDeref(res1);
1491  cuddDeref(res2);
1492  } else {
1493  /* Compute the cofactors of Y */
1494  index = y->index;
1495  YT = cuddT(y);
1496  YE = cuddE(y);
1497  if (y != Y) {
1498  YT = Cudd_Not(YT); YE = Cudd_Not(YE);
1499  }
1500  if (YT == Cudd_Not(one)) {
1501  Alpha = Cudd_Not(dd->vars[index]);
1502  Yrest = YE;
1503  Ra = RE;
1504  Ran = RT;
1505  } else {
1506  Alpha = dd->vars[index];
1507  Yrest = YT;
1508  Ra = RT;
1509  Ran = RE;
1510  }
1511  Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
1512  if (Gamma == NULL) return(NULL);
1513  if (Gamma == one) {
1514  res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1515  if (res1 == NULL) return(NULL);
1516  cuddRef(res1);
1517  res = cuddBddAndRecur(dd, Alpha, res1);
1518  if (res == NULL) {
1519  Cudd_RecursiveDeref(dd,res1);
1520  return(NULL);
1521  }
1522  cuddDeref(res1);
1523  } else if (Gamma == Cudd_Not(one)) {
1524  res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1525  if (res1 == NULL) return(NULL);
1526  cuddRef(res1);
1527  res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
1528  if (res == NULL) {
1529  Cudd_RecursiveDeref(dd,res1);
1530  return(NULL);
1531  }
1532  cuddDeref(res1);
1533  } else {
1534  cuddRef(Gamma);
1535  resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
1536  if (resA == NULL) {
1537  Cudd_RecursiveDeref(dd,Gamma);
1538  return(NULL);
1539  }
1540  cuddRef(resA);
1541  res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
1542  if (res2 == NULL) {
1543  Cudd_RecursiveDeref(dd,Gamma);
1544  Cudd_RecursiveDeref(dd,resA);
1545  return(NULL);
1546  }
1547  cuddRef(res2);
1548  Cudd_RecursiveDeref(dd,Gamma);
1549  Cudd_RecursiveDeref(dd,resA);
1550  res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
1551  if (res1 == NULL) {
1552  Cudd_RecursiveDeref(dd,res2);
1553  return(NULL);
1554  }
1555  cuddRef(res1);
1556  res = cuddBddIteRecur(dd, Alpha, res1, res2);
1557  if (res == NULL) {
1558  Cudd_RecursiveDeref(dd,res1);
1559  Cudd_RecursiveDeref(dd,res2);
1560  return(NULL);
1561  }
1562  cuddDeref(res1);
1563  cuddDeref(res2);
1564  }
1565  }
1566 
1567  cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
1568 
1569  return(res);
1570 
1571 } /* end of cuddCProjectionRecur */
cuddBddExistAbstractRecur
DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:352
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCProjectionRecur
DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp)
Definition: cuddPriority.c:1425
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
one
static DdNode * one
Definition: cuddDecomp.c:112
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdNode::index
DdHalfWord index
Definition: cudd.h:279
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
Cudd_CProjection
DdNode * Cudd_CProjection(DdManager *dd, DdNode *R, DdNode *Y)
Definition: cuddPriority.c:1200
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:633
static int cuddMinHammingDistRecur ( DdNode *  f,
int *  minterm,
DdHashTable *  table,
int  upperBound 
)
static

AutomaticStart

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_MinHammingDist.]

Description [Performs the recursive step of Cudd_MinHammingDist. It is based on the following identity. Let H(f) be the minimum Hamming distance of the minterms of f from the reference minterm. Then: <xmp> H(f) = min(H(f0)+h0,H(f1)+h1) </xmp> where f0 and f1 are the two cofactors of f with respect to its top variable; h0 is 1 if the minterm assigns 1 to the top variable of f; h1 is 1 if the minterm assigns 0 to the top variable of f. The upper bound on the distance is used to bound the depth of the recursion. Returns the minimum distance unless it exceeds the upper bound or computation fails.]

SideEffects [None]

SeeAlso [Cudd_MinHammingDist]

Definition at line 1858 of file cuddPriority.c.

1863 {
1864  DdNode *F, *Ft, *Fe;
1865  double h, hT, hE;
1866  DdNode *zero, *res;
1867  DdManager *dd = table->manager;
1868 
1869  statLine(dd);
1870  if (upperBound == 0) return(0);
1871 
1872  F = Cudd_Regular(f);
1873 
1874  if (cuddIsConstant(F)) {
1875  zero = Cudd_Not(DD_ONE(dd));
1876  if (f == dd->background || f == zero) {
1877  return(upperBound);
1878  } else {
1879  return(0);
1880  }
1881  }
1882  if ((res = cuddHashTableLookup1(table,f)) != NULL) {
1883  h = cuddV(res);
1884  if (res->ref == 0) {
1885  dd->dead++;
1886  dd->constants.dead++;
1887  }
1888  return((int) h);
1889  }
1890 
1891  Ft = cuddT(F); Fe = cuddE(F);
1892  if (Cudd_IsComplement(f)) {
1893  Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
1894  }
1895  if (minterm[F->index] == 0) {
1896  DdNode *temp = Ft;
1897  Ft = Fe; Fe = temp;
1898  }
1899 
1900  hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
1901  if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1902  if (hT == 0) {
1903  hE = upperBound;
1904  } else {
1905  hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
1906  if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
1907  }
1908  h = ddMin(hT, hE + 1);
1909 
1910  if (F->ref != 1) {
1911  ptrint fanout = (ptrint) F->ref;
1912  cuddSatDec(fanout);
1913  res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
1914  if (!cuddHashTableInsert1(table,f,res,fanout)) {
1915  cuddRef(res); Cudd_RecursiveDeref(dd, res);
1916  return(CUDD_OUT_OF_MEM);
1917  }
1918  }
1919 
1920  return((int) h);
1921 
1922 } /* end of cuddMinHammingDistRecur */
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
CUDD_OUT_OF_MEM
#define CUDD_OUT_OF_MEM
Definition: cudd.h:95
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
DdHashTable::manager
DdManager * manager
Definition: cuddInt.h:313
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddMinHammingDistRecur
static int cuddMinHammingDistRecur(DdNode *f, int *minterm, DdHashTable *table, int upperBound)
Definition: cuddPriority.c:1858
cuddHashTableLookup1
DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f)
Definition: cuddLCache.c:819
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
DdSubtable::dead
unsigned int dead
Definition: cuddInt.h:332
ptrint
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
cuddHashTableInsert1
int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count)
Definition: cuddLCache.c:767
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
cuddSatDec
#define cuddSatDec(x)
Definition: cuddInt.h:896
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:367
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
zero
static DdNode * zero
Definition: cuddApa.c:100
DdManager::background
DdNode * background
Definition: cuddInt.h:349
static DdNode * separateCube ( DdManager *  dd,
DdNode *  f,
CUDD_VALUE_TYPE *  distance 
)
static

Function********************************************************************

Synopsis [Separates cube from distance.]

Description [Separates cube from distance. Returns the cube if successful; NULL otherwise.]

SideEffects [The distance is returned as a side effect.]

SeeAlso [cuddBddClosestCube createResult]

Definition at line 1938 of file cuddPriority.c.

1942 {
1943  DdNode *cube, *t;
1944 
1945  /* One and zero are special cases because the distance is implied. */
1946  if (Cudd_IsConstant(f)) {
1947  *distance = (f == DD_ONE(dd)) ? 0.0 :
1948  (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
1949  return(f);
1950  }
1951 
1952  /* Find out which branch points to the distance and replace the top
1953  ** node with one pointing to zero instead. */
1954  t = cuddT(f);
1955  if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
1956 #ifdef DD_DEBUG
1957  assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
1958 #endif
1959  *distance = -cuddV(t);
1960  cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
1961  } else {
1962 #ifdef DD_DEBUG
1963  assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
1964 #endif
1965  *distance = -cuddV(cuddE(f));
1966  cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
1967  }
1968 
1969  return(cube);
1970 
1971 } /* end of separateCube */
DdNode
Definition: cudd.h:278
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
CUDD_CONST_INDEX
#define CUDD_CONST_INDEX
Definition: cudd.h:117
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
assert
#define assert(ex)
Definition: util_old.h:213
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $"
static

Definition at line 105 of file cuddPriority.c.