[13] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [cuddPriority.c] |
---|
| 4 | |
---|
| 5 | PackageName [cudd] |
---|
| 6 | |
---|
| 7 | Synopsis [Priority functions.] |
---|
| 8 | |
---|
| 9 | Description [External procedures included in this file: |
---|
| 10 | <ul> |
---|
| 11 | <li> Cudd_PrioritySelect() |
---|
| 12 | <li> Cudd_Xgty() |
---|
| 13 | <li> Cudd_Xeqy() |
---|
| 14 | <li> Cudd_addXeqy() |
---|
| 15 | <li> Cudd_Dxygtdxz() |
---|
| 16 | <li> Cudd_Dxygtdyz() |
---|
| 17 | <li> Cudd_Inequality() |
---|
| 18 | <li> Cudd_Disequality() |
---|
| 19 | <li> Cudd_bddInterval() |
---|
| 20 | <li> Cudd_CProjection() |
---|
| 21 | <li> Cudd_addHamming() |
---|
| 22 | <li> Cudd_MinHammingDist() |
---|
| 23 | <li> Cudd_bddClosestCube() |
---|
| 24 | </ul> |
---|
| 25 | Internal procedures included in this module: |
---|
| 26 | <ul> |
---|
| 27 | <li> cuddCProjectionRecur() |
---|
| 28 | <li> cuddBddClosestCube() |
---|
| 29 | </ul> |
---|
| 30 | Static procedures included in this module: |
---|
| 31 | <ul> |
---|
| 32 | <li> cuddMinHammingDistRecur() |
---|
| 33 | <li> separateCube() |
---|
| 34 | <li> createResult() |
---|
| 35 | </ul> |
---|
| 36 | ] |
---|
| 37 | |
---|
| 38 | SeeAlso [] |
---|
| 39 | |
---|
| 40 | Author [Fabio Somenzi] |
---|
| 41 | |
---|
| 42 | Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado |
---|
| 43 | |
---|
| 44 | All rights reserved. |
---|
| 45 | |
---|
| 46 | Redistribution and use in source and binary forms, with or without |
---|
| 47 | modification, are permitted provided that the following conditions |
---|
| 48 | are met: |
---|
| 49 | |
---|
| 50 | Redistributions of source code must retain the above copyright |
---|
| 51 | notice, this list of conditions and the following disclaimer. |
---|
| 52 | |
---|
| 53 | Redistributions in binary form must reproduce the above copyright |
---|
| 54 | notice, this list of conditions and the following disclaimer in the |
---|
| 55 | documentation and/or other materials provided with the distribution. |
---|
| 56 | |
---|
| 57 | Neither the name of the University of Colorado nor the names of its |
---|
| 58 | contributors may be used to endorse or promote products derived from |
---|
| 59 | this software without specific prior written permission. |
---|
| 60 | |
---|
| 61 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 62 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 63 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 64 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 65 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 66 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 67 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 68 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 69 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 70 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 71 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 72 | POSSIBILITY OF SUCH DAMAGE.] |
---|
| 73 | |
---|
| 74 | ******************************************************************************/ |
---|
| 75 | |
---|
| 76 | #include "util.h" |
---|
| 77 | #include "cuddInt.h" |
---|
| 78 | |
---|
| 79 | |
---|
| 80 | /*---------------------------------------------------------------------------*/ |
---|
| 81 | /* Constant declarations */ |
---|
| 82 | /*---------------------------------------------------------------------------*/ |
---|
| 83 | |
---|
| 84 | #define DD_DEBUG 1 |
---|
| 85 | |
---|
| 86 | /*---------------------------------------------------------------------------*/ |
---|
| 87 | /* Stucture declarations */ |
---|
| 88 | /*---------------------------------------------------------------------------*/ |
---|
| 89 | |
---|
| 90 | |
---|
| 91 | /*---------------------------------------------------------------------------*/ |
---|
| 92 | /* Type declarations */ |
---|
| 93 | /*---------------------------------------------------------------------------*/ |
---|
| 94 | |
---|
| 95 | |
---|
| 96 | /*---------------------------------------------------------------------------*/ |
---|
| 97 | /* Variable declarations */ |
---|
| 98 | /*---------------------------------------------------------------------------*/ |
---|
| 99 | |
---|
| 100 | #ifndef lint |
---|
| 101 | static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $"; |
---|
| 102 | #endif |
---|
| 103 | |
---|
| 104 | /*---------------------------------------------------------------------------*/ |
---|
| 105 | /* Macro declarations */ |
---|
| 106 | /*---------------------------------------------------------------------------*/ |
---|
| 107 | |
---|
| 108 | |
---|
| 109 | /**AutomaticStart*************************************************************/ |
---|
| 110 | |
---|
| 111 | /*---------------------------------------------------------------------------*/ |
---|
| 112 | /* Static function prototypes */ |
---|
| 113 | /*---------------------------------------------------------------------------*/ |
---|
| 114 | static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound); |
---|
| 115 | static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance); |
---|
| 116 | static DdNode * createResult (DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance); |
---|
| 117 | |
---|
| 118 | /**AutomaticEnd***************************************************************/ |
---|
| 119 | |
---|
| 120 | |
---|
| 121 | /*---------------------------------------------------------------------------*/ |
---|
| 122 | /* Definition of exported functions */ |
---|
| 123 | /*---------------------------------------------------------------------------*/ |
---|
| 124 | |
---|
| 125 | |
---|
| 126 | /**Function******************************************************************** |
---|
| 127 | |
---|
| 128 | Synopsis [Selects pairs from R using a priority function.] |
---|
| 129 | |
---|
| 130 | Description [Selects pairs from a relation R(x,y) (given as a BDD) |
---|
| 131 | in such a way that a given x appears in one pair only. Uses a |
---|
| 132 | priority function to determine which y should be paired to a given x. |
---|
| 133 | Cudd_PrioritySelect returns a pointer to |
---|
| 134 | the selected function if successful; NULL otherwise. |
---|
| 135 | Three of the arguments--x, y, and z--are vectors of BDD variables. |
---|
| 136 | The first two are the variables on which R depends. The third vectore |
---|
| 137 | is a vector of auxiliary variables, used during the computation. This |
---|
| 138 | vector is optional. If a NULL value is passed instead, |
---|
| 139 | Cudd_PrioritySelect will create the working variables on the fly. |
---|
| 140 | The sizes of x and y (and z if it is not NULL) should equal n. |
---|
| 141 | The priority function Pi can be passed as a BDD, or can be built by |
---|
| 142 | Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, |
---|
| 143 | parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the |
---|
| 144 | priority function. (Pifunc is a pointer to a C function.) If Pi is not |
---|
| 145 | NULL, then Pifunc is ignored. Pifunc should have the same interface as |
---|
| 146 | the standard priority functions (e.g., Cudd_Dxygtdxz). |
---|
| 147 | Cudd_PrioritySelect and Cudd_CProjection can sometimes be used |
---|
| 148 | interchangeably. Specifically, calling Cudd_PrioritySelect with |
---|
| 149 | Cudd_Xgty as Pifunc produces the same result as calling |
---|
| 150 | Cudd_CProjection with the all-zero minterm as reference minterm. |
---|
| 151 | However, depending on the application, one or the other may be |
---|
| 152 | preferable: |
---|
| 153 | <ul> |
---|
| 154 | <li> When extracting representatives from an equivalence relation, |
---|
| 155 | Cudd_CProjection has the advantage of nor requiring the auxiliary |
---|
| 156 | variables. |
---|
| 157 | <li> When computing matchings in general bipartite graphs, |
---|
| 158 | Cudd_PrioritySelect normally obtains better results because it can use |
---|
| 159 | more powerful matching schemes (e.g., Cudd_Dxygtdxz). |
---|
| 160 | </ul> |
---|
| 161 | ] |
---|
| 162 | |
---|
| 163 | SideEffects [If called with z == NULL, will create new variables in |
---|
| 164 | the manager.] |
---|
| 165 | |
---|
| 166 | SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty |
---|
| 167 | Cudd_bddAdjPermuteX Cudd_CProjection] |
---|
| 168 | |
---|
| 169 | ******************************************************************************/ |
---|
| 170 | DdNode * |
---|
| 171 | Cudd_PrioritySelect( |
---|
| 172 | DdManager * dd /* manager */, |
---|
| 173 | DdNode * R /* BDD of the relation */, |
---|
| 174 | DdNode ** x /* array of x variables */, |
---|
| 175 | DdNode ** y /* array of y variables */, |
---|
| 176 | DdNode ** z /* array of z variables (optional: may be NULL) */, |
---|
| 177 | DdNode * Pi /* BDD of the priority function (optional: may be NULL) */, |
---|
| 178 | int n /* size of x, y, and z */, |
---|
| 179 | DD_PRFP Pifunc /* function used to build Pi if it is NULL */) |
---|
| 180 | { |
---|
| 181 | DdNode *res = NULL; |
---|
| 182 | DdNode *zcube = NULL; |
---|
| 183 | DdNode *Rxz, *Q; |
---|
| 184 | int createdZ = 0; |
---|
| 185 | int createdPi = 0; |
---|
| 186 | int i; |
---|
| 187 | |
---|
| 188 | /* Create z variables if needed. */ |
---|
| 189 | if (z == NULL) { |
---|
| 190 | if (Pi != NULL) return(NULL); |
---|
| 191 | z = ALLOC(DdNode *,n); |
---|
| 192 | if (z == NULL) { |
---|
| 193 | dd->errorCode = CUDD_MEMORY_OUT; |
---|
| 194 | return(NULL); |
---|
| 195 | } |
---|
| 196 | createdZ = 1; |
---|
| 197 | for (i = 0; i < n; i++) { |
---|
| 198 | if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame; |
---|
| 199 | z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); |
---|
| 200 | if (z[i] == NULL) goto endgame; |
---|
| 201 | } |
---|
| 202 | } |
---|
| 203 | |
---|
| 204 | /* Create priority function BDD if needed. */ |
---|
| 205 | if (Pi == NULL) { |
---|
| 206 | Pi = Pifunc(dd,n,x,y,z); |
---|
| 207 | if (Pi == NULL) goto endgame; |
---|
| 208 | createdPi = 1; |
---|
| 209 | cuddRef(Pi); |
---|
| 210 | } |
---|
| 211 | |
---|
| 212 | /* Initialize abstraction cube. */ |
---|
| 213 | zcube = DD_ONE(dd); |
---|
| 214 | cuddRef(zcube); |
---|
| 215 | for (i = n - 1; i >= 0; i--) { |
---|
| 216 | DdNode *tmpp; |
---|
| 217 | tmpp = Cudd_bddAnd(dd,z[i],zcube); |
---|
| 218 | if (tmpp == NULL) goto endgame; |
---|
| 219 | cuddRef(tmpp); |
---|
| 220 | Cudd_RecursiveDeref(dd,zcube); |
---|
| 221 | zcube = tmpp; |
---|
| 222 | } |
---|
| 223 | |
---|
| 224 | /* Compute subset of (x,y) pairs. */ |
---|
| 225 | Rxz = Cudd_bddSwapVariables(dd,R,y,z,n); |
---|
| 226 | if (Rxz == NULL) goto endgame; |
---|
| 227 | cuddRef(Rxz); |
---|
| 228 | Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube); |
---|
| 229 | if (Q == NULL) { |
---|
| 230 | Cudd_RecursiveDeref(dd,Rxz); |
---|
| 231 | goto endgame; |
---|
| 232 | } |
---|
| 233 | cuddRef(Q); |
---|
| 234 | Cudd_RecursiveDeref(dd,Rxz); |
---|
| 235 | res = Cudd_bddAnd(dd,R,Cudd_Not(Q)); |
---|
| 236 | if (res == NULL) { |
---|
| 237 | Cudd_RecursiveDeref(dd,Q); |
---|
| 238 | goto endgame; |
---|
| 239 | } |
---|
| 240 | cuddRef(res); |
---|
| 241 | Cudd_RecursiveDeref(dd,Q); |
---|
| 242 | |
---|
| 243 | endgame: |
---|
| 244 | if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube); |
---|
| 245 | if (createdZ) { |
---|
| 246 | FREE(z); |
---|
| 247 | } |
---|
| 248 | if (createdPi) { |
---|
| 249 | Cudd_RecursiveDeref(dd,Pi); |
---|
| 250 | } |
---|
| 251 | if (res != NULL) cuddDeref(res); |
---|
| 252 | return(res); |
---|
| 253 | |
---|
| 254 | } /* Cudd_PrioritySelect */ |
---|
| 255 | |
---|
| 256 | |
---|
| 257 | /**Function******************************************************************** |
---|
| 258 | |
---|
| 259 | Synopsis [Generates a BDD for the function x > y.] |
---|
| 260 | |
---|
| 261 | Description [This function generates a BDD for the function x > y. |
---|
| 262 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
| 263 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
| 264 | The BDD is built bottom-up. |
---|
| 265 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
| 266 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. |
---|
| 267 | Argument z is not used by Cudd_Xgty: it is included to make it |
---|
| 268 | call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.] |
---|
| 269 | |
---|
| 270 | SideEffects [None] |
---|
| 271 | |
---|
| 272 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz] |
---|
| 273 | |
---|
| 274 | ******************************************************************************/ |
---|
| 275 | DdNode * |
---|
| 276 | Cudd_Xgty( |
---|
| 277 | DdManager * dd /* DD manager */, |
---|
| 278 | int N /* number of x and y variables */, |
---|
| 279 | DdNode ** z /* array of z variables: unused */, |
---|
| 280 | DdNode ** x /* array of x variables */, |
---|
| 281 | DdNode ** y /* array of y variables */) |
---|
| 282 | { |
---|
| 283 | DdNode *u, *v, *w; |
---|
| 284 | int i; |
---|
| 285 | |
---|
| 286 | /* Build bottom part of BDD outside loop. */ |
---|
| 287 | u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1])); |
---|
| 288 | if (u == NULL) return(NULL); |
---|
| 289 | cuddRef(u); |
---|
| 290 | |
---|
| 291 | /* Loop to build the rest of the BDD. */ |
---|
| 292 | for (i = N-2; i >= 0; i--) { |
---|
| 293 | v = Cudd_bddAnd(dd, y[i], Cudd_Not(u)); |
---|
| 294 | if (v == NULL) { |
---|
| 295 | Cudd_RecursiveDeref(dd, u); |
---|
| 296 | return(NULL); |
---|
| 297 | } |
---|
| 298 | cuddRef(v); |
---|
| 299 | w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); |
---|
| 300 | if (w == NULL) { |
---|
| 301 | Cudd_RecursiveDeref(dd, u); |
---|
| 302 | Cudd_RecursiveDeref(dd, v); |
---|
| 303 | return(NULL); |
---|
| 304 | } |
---|
| 305 | cuddRef(w); |
---|
| 306 | Cudd_RecursiveDeref(dd, u); |
---|
| 307 | u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w); |
---|
| 308 | if (u == NULL) { |
---|
| 309 | Cudd_RecursiveDeref(dd, v); |
---|
| 310 | Cudd_RecursiveDeref(dd, w); |
---|
| 311 | return(NULL); |
---|
| 312 | } |
---|
| 313 | cuddRef(u); |
---|
| 314 | Cudd_RecursiveDeref(dd, v); |
---|
| 315 | Cudd_RecursiveDeref(dd, w); |
---|
| 316 | |
---|
| 317 | } |
---|
| 318 | cuddDeref(u); |
---|
| 319 | return(u); |
---|
| 320 | |
---|
| 321 | } /* end of Cudd_Xgty */ |
---|
| 322 | |
---|
| 323 | |
---|
| 324 | /**Function******************************************************************** |
---|
| 325 | |
---|
| 326 | Synopsis [Generates a BDD for the function x==y.] |
---|
| 327 | |
---|
| 328 | Description [This function generates a BDD for the function x==y. |
---|
| 329 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
| 330 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
| 331 | The BDD is built bottom-up. |
---|
| 332 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
| 333 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] |
---|
| 334 | |
---|
| 335 | SideEffects [None] |
---|
| 336 | |
---|
| 337 | SeeAlso [Cudd_addXeqy] |
---|
| 338 | |
---|
| 339 | ******************************************************************************/ |
---|
| 340 | DdNode * |
---|
| 341 | Cudd_Xeqy( |
---|
| 342 | DdManager * dd /* DD manager */, |
---|
| 343 | int N /* number of x and y variables */, |
---|
| 344 | DdNode ** x /* array of x variables */, |
---|
| 345 | DdNode ** y /* array of y variables */) |
---|
| 346 | { |
---|
| 347 | DdNode *u, *v, *w; |
---|
| 348 | int i; |
---|
| 349 | |
---|
| 350 | /* Build bottom part of BDD outside loop. */ |
---|
| 351 | u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1])); |
---|
| 352 | if (u == NULL) return(NULL); |
---|
| 353 | cuddRef(u); |
---|
| 354 | |
---|
| 355 | /* Loop to build the rest of the BDD. */ |
---|
| 356 | for (i = N-2; i >= 0; i--) { |
---|
| 357 | v = Cudd_bddAnd(dd, y[i], u); |
---|
| 358 | if (v == NULL) { |
---|
| 359 | Cudd_RecursiveDeref(dd, u); |
---|
| 360 | return(NULL); |
---|
| 361 | } |
---|
| 362 | cuddRef(v); |
---|
| 363 | w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); |
---|
| 364 | if (w == NULL) { |
---|
| 365 | Cudd_RecursiveDeref(dd, u); |
---|
| 366 | Cudd_RecursiveDeref(dd, v); |
---|
| 367 | return(NULL); |
---|
| 368 | } |
---|
| 369 | cuddRef(w); |
---|
| 370 | Cudd_RecursiveDeref(dd, u); |
---|
| 371 | u = Cudd_bddIte(dd, x[i], v, w); |
---|
| 372 | if (u == NULL) { |
---|
| 373 | Cudd_RecursiveDeref(dd, v); |
---|
| 374 | Cudd_RecursiveDeref(dd, w); |
---|
| 375 | return(NULL); |
---|
| 376 | } |
---|
| 377 | cuddRef(u); |
---|
| 378 | Cudd_RecursiveDeref(dd, v); |
---|
| 379 | Cudd_RecursiveDeref(dd, w); |
---|
| 380 | } |
---|
| 381 | cuddDeref(u); |
---|
| 382 | return(u); |
---|
| 383 | |
---|
| 384 | } /* end of Cudd_Xeqy */ |
---|
| 385 | |
---|
| 386 | |
---|
| 387 | /**Function******************************************************************** |
---|
| 388 | |
---|
| 389 | Synopsis [Generates an ADD for the function x==y.] |
---|
| 390 | |
---|
| 391 | Description [This function generates an ADD for the function x==y. |
---|
| 392 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
| 393 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
| 394 | The ADD is built bottom-up. |
---|
| 395 | It has 3*N-1 internal nodes, if the variables are ordered as follows: |
---|
| 396 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] |
---|
| 397 | |
---|
| 398 | SideEffects [None] |
---|
| 399 | |
---|
| 400 | SeeAlso [Cudd_Xeqy] |
---|
| 401 | |
---|
| 402 | ******************************************************************************/ |
---|
| 403 | DdNode * |
---|
| 404 | Cudd_addXeqy( |
---|
| 405 | DdManager * dd /* DD manager */, |
---|
| 406 | int N /* number of x and y variables */, |
---|
| 407 | DdNode ** x /* array of x variables */, |
---|
| 408 | DdNode ** y /* array of y variables */) |
---|
| 409 | { |
---|
| 410 | DdNode *one, *zero; |
---|
| 411 | DdNode *u, *v, *w; |
---|
| 412 | int i; |
---|
| 413 | |
---|
| 414 | one = DD_ONE(dd); |
---|
| 415 | zero = DD_ZERO(dd); |
---|
| 416 | |
---|
| 417 | /* Build bottom part of ADD outside loop. */ |
---|
| 418 | v = Cudd_addIte(dd, y[N-1], one, zero); |
---|
| 419 | if (v == NULL) return(NULL); |
---|
| 420 | cuddRef(v); |
---|
| 421 | w = Cudd_addIte(dd, y[N-1], zero, one); |
---|
| 422 | if (w == NULL) { |
---|
| 423 | Cudd_RecursiveDeref(dd, v); |
---|
| 424 | return(NULL); |
---|
| 425 | } |
---|
| 426 | cuddRef(w); |
---|
| 427 | u = Cudd_addIte(dd, x[N-1], v, w); |
---|
| 428 | if (u == NULL) { |
---|
| 429 | Cudd_RecursiveDeref(dd, v); |
---|
| 430 | Cudd_RecursiveDeref(dd, w); |
---|
| 431 | return(NULL); |
---|
| 432 | } |
---|
| 433 | cuddRef(u); |
---|
| 434 | Cudd_RecursiveDeref(dd, v); |
---|
| 435 | Cudd_RecursiveDeref(dd, w); |
---|
| 436 | |
---|
| 437 | /* Loop to build the rest of the ADD. */ |
---|
| 438 | for (i = N-2; i >= 0; i--) { |
---|
| 439 | v = Cudd_addIte(dd, y[i], u, zero); |
---|
| 440 | if (v == NULL) { |
---|
| 441 | Cudd_RecursiveDeref(dd, u); |
---|
| 442 | return(NULL); |
---|
| 443 | } |
---|
| 444 | cuddRef(v); |
---|
| 445 | w = Cudd_addIte(dd, y[i], zero, u); |
---|
| 446 | if (w == NULL) { |
---|
| 447 | Cudd_RecursiveDeref(dd, u); |
---|
| 448 | Cudd_RecursiveDeref(dd, v); |
---|
| 449 | return(NULL); |
---|
| 450 | } |
---|
| 451 | cuddRef(w); |
---|
| 452 | Cudd_RecursiveDeref(dd, u); |
---|
| 453 | u = Cudd_addIte(dd, x[i], v, w); |
---|
| 454 | if (w == NULL) { |
---|
| 455 | Cudd_RecursiveDeref(dd, v); |
---|
| 456 | Cudd_RecursiveDeref(dd, w); |
---|
| 457 | return(NULL); |
---|
| 458 | } |
---|
| 459 | cuddRef(u); |
---|
| 460 | Cudd_RecursiveDeref(dd, v); |
---|
| 461 | Cudd_RecursiveDeref(dd, w); |
---|
| 462 | } |
---|
| 463 | cuddDeref(u); |
---|
| 464 | return(u); |
---|
| 465 | |
---|
| 466 | } /* end of Cudd_addXeqy */ |
---|
| 467 | |
---|
| 468 | |
---|
| 469 | /**Function******************************************************************** |
---|
| 470 | |
---|
| 471 | Synopsis [Generates a BDD for the function d(x,y) > d(x,z).] |
---|
| 472 | |
---|
| 473 | Description [This function generates a BDD for the function d(x,y) |
---|
| 474 | > d(x,z); |
---|
| 475 | x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], |
---|
| 476 | y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], |
---|
| 477 | with 0 the most significant bit. |
---|
| 478 | The distance d(x,y) is defined as: |
---|
| 479 | \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). |
---|
| 480 | The BDD is built bottom-up. |
---|
| 481 | It has 7*N-3 internal nodes, if the variables are ordered as follows: |
---|
| 482 | x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] |
---|
| 483 | |
---|
| 484 | SideEffects [None] |
---|
| 485 | |
---|
| 486 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX] |
---|
| 487 | |
---|
| 488 | ******************************************************************************/ |
---|
| 489 | DdNode * |
---|
| 490 | Cudd_Dxygtdxz( |
---|
| 491 | DdManager * dd /* DD manager */, |
---|
| 492 | int N /* number of x, y, and z variables */, |
---|
| 493 | DdNode ** x /* array of x variables */, |
---|
| 494 | DdNode ** y /* array of y variables */, |
---|
| 495 | DdNode ** z /* array of z variables */) |
---|
| 496 | { |
---|
| 497 | DdNode *one, *zero; |
---|
| 498 | DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; |
---|
| 499 | int i; |
---|
| 500 | |
---|
| 501 | one = DD_ONE(dd); |
---|
| 502 | zero = Cudd_Not(one); |
---|
| 503 | |
---|
| 504 | /* Build bottom part of BDD outside loop. */ |
---|
| 505 | y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1])); |
---|
| 506 | if (y1_ == NULL) return(NULL); |
---|
| 507 | cuddRef(y1_); |
---|
| 508 | y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one); |
---|
| 509 | if (y2 == NULL) { |
---|
| 510 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 511 | return(NULL); |
---|
| 512 | } |
---|
| 513 | cuddRef(y2); |
---|
| 514 | x1 = Cudd_bddIte(dd, x[N-1], y1_, y2); |
---|
| 515 | if (x1 == NULL) { |
---|
| 516 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 517 | Cudd_RecursiveDeref(dd, y2); |
---|
| 518 | return(NULL); |
---|
| 519 | } |
---|
| 520 | cuddRef(x1); |
---|
| 521 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 522 | Cudd_RecursiveDeref(dd, y2); |
---|
| 523 | |
---|
| 524 | /* Loop to build the rest of the BDD. */ |
---|
| 525 | for (i = N-2; i >= 0; i--) { |
---|
| 526 | z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); |
---|
| 527 | if (z1 == NULL) { |
---|
| 528 | Cudd_RecursiveDeref(dd, x1); |
---|
| 529 | return(NULL); |
---|
| 530 | } |
---|
| 531 | cuddRef(z1); |
---|
| 532 | z2 = Cudd_bddIte(dd, z[i], x1, one); |
---|
| 533 | if (z2 == NULL) { |
---|
| 534 | Cudd_RecursiveDeref(dd, x1); |
---|
| 535 | Cudd_RecursiveDeref(dd, z1); |
---|
| 536 | return(NULL); |
---|
| 537 | } |
---|
| 538 | cuddRef(z2); |
---|
| 539 | z3 = Cudd_bddIte(dd, z[i], one, x1); |
---|
| 540 | if (z3 == NULL) { |
---|
| 541 | Cudd_RecursiveDeref(dd, x1); |
---|
| 542 | Cudd_RecursiveDeref(dd, z1); |
---|
| 543 | Cudd_RecursiveDeref(dd, z2); |
---|
| 544 | return(NULL); |
---|
| 545 | } |
---|
| 546 | cuddRef(z3); |
---|
| 547 | z4 = Cudd_bddIte(dd, z[i], x1, zero); |
---|
| 548 | if (z4 == NULL) { |
---|
| 549 | Cudd_RecursiveDeref(dd, x1); |
---|
| 550 | Cudd_RecursiveDeref(dd, z1); |
---|
| 551 | Cudd_RecursiveDeref(dd, z2); |
---|
| 552 | Cudd_RecursiveDeref(dd, z3); |
---|
| 553 | return(NULL); |
---|
| 554 | } |
---|
| 555 | cuddRef(z4); |
---|
| 556 | Cudd_RecursiveDeref(dd, x1); |
---|
| 557 | y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1)); |
---|
| 558 | if (y1_ == NULL) { |
---|
| 559 | Cudd_RecursiveDeref(dd, z1); |
---|
| 560 | Cudd_RecursiveDeref(dd, z2); |
---|
| 561 | Cudd_RecursiveDeref(dd, z3); |
---|
| 562 | Cudd_RecursiveDeref(dd, z4); |
---|
| 563 | return(NULL); |
---|
| 564 | } |
---|
| 565 | cuddRef(y1_); |
---|
| 566 | y2 = Cudd_bddIte(dd, y[i], z4, z3); |
---|
| 567 | if (y2 == NULL) { |
---|
| 568 | Cudd_RecursiveDeref(dd, z1); |
---|
| 569 | Cudd_RecursiveDeref(dd, z2); |
---|
| 570 | Cudd_RecursiveDeref(dd, z3); |
---|
| 571 | Cudd_RecursiveDeref(dd, z4); |
---|
| 572 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 573 | return(NULL); |
---|
| 574 | } |
---|
| 575 | cuddRef(y2); |
---|
| 576 | Cudd_RecursiveDeref(dd, z1); |
---|
| 577 | Cudd_RecursiveDeref(dd, z2); |
---|
| 578 | Cudd_RecursiveDeref(dd, z3); |
---|
| 579 | Cudd_RecursiveDeref(dd, z4); |
---|
| 580 | x1 = Cudd_bddIte(dd, x[i], y1_, y2); |
---|
| 581 | if (x1 == NULL) { |
---|
| 582 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 583 | Cudd_RecursiveDeref(dd, y2); |
---|
| 584 | return(NULL); |
---|
| 585 | } |
---|
| 586 | cuddRef(x1); |
---|
| 587 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 588 | Cudd_RecursiveDeref(dd, y2); |
---|
| 589 | } |
---|
| 590 | cuddDeref(x1); |
---|
| 591 | return(Cudd_Not(x1)); |
---|
| 592 | |
---|
| 593 | } /* end of Cudd_Dxygtdxz */ |
---|
| 594 | |
---|
| 595 | |
---|
| 596 | /**Function******************************************************************** |
---|
| 597 | |
---|
| 598 | Synopsis [Generates a BDD for the function d(x,y) > d(y,z).] |
---|
| 599 | |
---|
| 600 | Description [This function generates a BDD for the function d(x,y) |
---|
| 601 | > d(y,z); |
---|
| 602 | x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], |
---|
| 603 | y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], |
---|
| 604 | with 0 the most significant bit. |
---|
| 605 | The distance d(x,y) is defined as: |
---|
| 606 | \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). |
---|
| 607 | The BDD is built bottom-up. |
---|
| 608 | It has 7*N-3 internal nodes, if the variables are ordered as follows: |
---|
| 609 | x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] |
---|
| 610 | |
---|
| 611 | SideEffects [None] |
---|
| 612 | |
---|
| 613 | SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX] |
---|
| 614 | |
---|
| 615 | ******************************************************************************/ |
---|
| 616 | DdNode * |
---|
| 617 | Cudd_Dxygtdyz( |
---|
| 618 | DdManager * dd /* DD manager */, |
---|
| 619 | int N /* number of x, y, and z variables */, |
---|
| 620 | DdNode ** x /* array of x variables */, |
---|
| 621 | DdNode ** y /* array of y variables */, |
---|
| 622 | DdNode ** z /* array of z variables */) |
---|
| 623 | { |
---|
| 624 | DdNode *one, *zero; |
---|
| 625 | DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; |
---|
| 626 | int i; |
---|
| 627 | |
---|
| 628 | one = DD_ONE(dd); |
---|
| 629 | zero = Cudd_Not(one); |
---|
| 630 | |
---|
| 631 | /* Build bottom part of BDD outside loop. */ |
---|
| 632 | y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]); |
---|
| 633 | if (y1_ == NULL) return(NULL); |
---|
| 634 | cuddRef(y1_); |
---|
| 635 | y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero); |
---|
| 636 | if (y2 == NULL) { |
---|
| 637 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 638 | return(NULL); |
---|
| 639 | } |
---|
| 640 | cuddRef(y2); |
---|
| 641 | x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2)); |
---|
| 642 | if (x1 == NULL) { |
---|
| 643 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 644 | Cudd_RecursiveDeref(dd, y2); |
---|
| 645 | return(NULL); |
---|
| 646 | } |
---|
| 647 | cuddRef(x1); |
---|
| 648 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 649 | Cudd_RecursiveDeref(dd, y2); |
---|
| 650 | |
---|
| 651 | /* Loop to build the rest of the BDD. */ |
---|
| 652 | for (i = N-2; i >= 0; i--) { |
---|
| 653 | z1 = Cudd_bddIte(dd, z[i], x1, zero); |
---|
| 654 | if (z1 == NULL) { |
---|
| 655 | Cudd_RecursiveDeref(dd, x1); |
---|
| 656 | return(NULL); |
---|
| 657 | } |
---|
| 658 | cuddRef(z1); |
---|
| 659 | z2 = Cudd_bddIte(dd, z[i], x1, one); |
---|
| 660 | if (z2 == NULL) { |
---|
| 661 | Cudd_RecursiveDeref(dd, x1); |
---|
| 662 | Cudd_RecursiveDeref(dd, z1); |
---|
| 663 | return(NULL); |
---|
| 664 | } |
---|
| 665 | cuddRef(z2); |
---|
| 666 | z3 = Cudd_bddIte(dd, z[i], one, x1); |
---|
| 667 | if (z3 == NULL) { |
---|
| 668 | Cudd_RecursiveDeref(dd, x1); |
---|
| 669 | Cudd_RecursiveDeref(dd, z1); |
---|
| 670 | Cudd_RecursiveDeref(dd, z2); |
---|
| 671 | return(NULL); |
---|
| 672 | } |
---|
| 673 | cuddRef(z3); |
---|
| 674 | z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); |
---|
| 675 | if (z4 == NULL) { |
---|
| 676 | Cudd_RecursiveDeref(dd, x1); |
---|
| 677 | Cudd_RecursiveDeref(dd, z1); |
---|
| 678 | Cudd_RecursiveDeref(dd, z2); |
---|
| 679 | Cudd_RecursiveDeref(dd, z3); |
---|
| 680 | return(NULL); |
---|
| 681 | } |
---|
| 682 | cuddRef(z4); |
---|
| 683 | Cudd_RecursiveDeref(dd, x1); |
---|
| 684 | y1_ = Cudd_bddIte(dd, y[i], z2, z1); |
---|
| 685 | if (y1_ == NULL) { |
---|
| 686 | Cudd_RecursiveDeref(dd, z1); |
---|
| 687 | Cudd_RecursiveDeref(dd, z2); |
---|
| 688 | Cudd_RecursiveDeref(dd, z3); |
---|
| 689 | Cudd_RecursiveDeref(dd, z4); |
---|
| 690 | return(NULL); |
---|
| 691 | } |
---|
| 692 | cuddRef(y1_); |
---|
| 693 | y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3)); |
---|
| 694 | if (y2 == NULL) { |
---|
| 695 | Cudd_RecursiveDeref(dd, z1); |
---|
| 696 | Cudd_RecursiveDeref(dd, z2); |
---|
| 697 | Cudd_RecursiveDeref(dd, z3); |
---|
| 698 | Cudd_RecursiveDeref(dd, z4); |
---|
| 699 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 700 | return(NULL); |
---|
| 701 | } |
---|
| 702 | cuddRef(y2); |
---|
| 703 | Cudd_RecursiveDeref(dd, z1); |
---|
| 704 | Cudd_RecursiveDeref(dd, z2); |
---|
| 705 | Cudd_RecursiveDeref(dd, z3); |
---|
| 706 | Cudd_RecursiveDeref(dd, z4); |
---|
| 707 | x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2)); |
---|
| 708 | if (x1 == NULL) { |
---|
| 709 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 710 | Cudd_RecursiveDeref(dd, y2); |
---|
| 711 | return(NULL); |
---|
| 712 | } |
---|
| 713 | cuddRef(x1); |
---|
| 714 | Cudd_RecursiveDeref(dd, y1_); |
---|
| 715 | Cudd_RecursiveDeref(dd, y2); |
---|
| 716 | } |
---|
| 717 | cuddDeref(x1); |
---|
| 718 | return(Cudd_Not(x1)); |
---|
| 719 | |
---|
| 720 | } /* end of Cudd_Dxygtdyz */ |
---|
| 721 | |
---|
| 722 | |
---|
| 723 | /**Function******************************************************************** |
---|
| 724 | |
---|
| 725 | Synopsis [Generates a BDD for the function x - y ≥ c.] |
---|
| 726 | |
---|
| 727 | Description [This function generates a BDD for the function x -y ≥ c. |
---|
| 728 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
| 729 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
| 730 | The BDD is built bottom-up. |
---|
| 731 | It has a linear number of nodes if the variables are ordered as follows: |
---|
| 732 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] |
---|
| 733 | |
---|
| 734 | SideEffects [None] |
---|
| 735 | |
---|
| 736 | SeeAlso [Cudd_Xgty] |
---|
| 737 | |
---|
| 738 | ******************************************************************************/ |
---|
| 739 | DdNode * |
---|
| 740 | Cudd_Inequality( |
---|
| 741 | DdManager * dd /* DD manager */, |
---|
| 742 | int N /* number of x and y variables */, |
---|
| 743 | int c /* right-hand side constant */, |
---|
| 744 | DdNode ** x /* array of x variables */, |
---|
| 745 | DdNode ** y /* array of y variables */) |
---|
| 746 | { |
---|
| 747 | /* The nodes at level i represent values of the difference that are |
---|
| 748 | ** multiples of 2^i. We use variables with names starting with k |
---|
| 749 | ** to denote the multipliers of 2^i in such multiples. */ |
---|
| 750 | int kTrue = c; |
---|
| 751 | int kFalse = c - 1; |
---|
| 752 | /* Mask used to compute the ceiling function. Since we divide by 2^i, |
---|
| 753 | ** we want to know whether the dividend is a multiple of 2^i. If it is, |
---|
| 754 | ** then ceiling and floor coincide; otherwise, they differ by one. */ |
---|
| 755 | int mask = 1; |
---|
| 756 | int i; |
---|
| 757 | |
---|
| 758 | DdNode *f = NULL; /* the eventual result */ |
---|
| 759 | DdNode *one = DD_ONE(dd); |
---|
| 760 | DdNode *zero = Cudd_Not(one); |
---|
| 761 | |
---|
| 762 | /* Two x-labeled nodes are created at most at each iteration. They are |
---|
| 763 | ** stored, along with their k values, in these variables. At each level, |
---|
| 764 | ** the old nodes are freed and the new nodes are copied into the old map. |
---|
| 765 | */ |
---|
| 766 | DdNode *map[2]; |
---|
| 767 | int invalidIndex = 1 << (N-1); |
---|
| 768 | int index[2] = {invalidIndex, invalidIndex}; |
---|
| 769 | |
---|
| 770 | /* This should never happen. */ |
---|
| 771 | if (N < 0) return(NULL); |
---|
| 772 | |
---|
| 773 | /* If there are no bits, both operands are 0. The result depends on c. */ |
---|
| 774 | if (N == 0) { |
---|
| 775 | if (c >= 0) return(one); |
---|
| 776 | else return(zero); |
---|
| 777 | } |
---|
| 778 | |
---|
| 779 | /* The maximum or the minimum difference comparing to c can generate the terminal case */ |
---|
| 780 | if ((1 << N) - 1 < c) return(zero); |
---|
| 781 | else if ((-(1 << N) + 1) >= c) return(one); |
---|
| 782 | |
---|
| 783 | /* Build the result bottom up. */ |
---|
| 784 | for (i = 1; i <= N; i++) { |
---|
| 785 | int kTrueLower, kFalseLower; |
---|
| 786 | int leftChild, middleChild, rightChild; |
---|
| 787 | DdNode *g0, *g1, *fplus, *fequal, *fminus; |
---|
| 788 | int j; |
---|
| 789 | DdNode *newMap[2]; |
---|
| 790 | int newIndex[2]; |
---|
| 791 | |
---|
| 792 | kTrueLower = kTrue; |
---|
| 793 | kFalseLower = kFalse; |
---|
| 794 | /* kTrue = ceiling((c-1)/2^i) + 1 */ |
---|
| 795 | kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1; |
---|
| 796 | mask = (mask << 1) | 1; |
---|
| 797 | /* kFalse = floor(c/2^i) - 1 */ |
---|
| 798 | kFalse = (c >> i) - 1; |
---|
| 799 | newIndex[0] = invalidIndex; |
---|
| 800 | newIndex[1] = invalidIndex; |
---|
| 801 | |
---|
| 802 | for (j = kFalse + 1; j < kTrue; j++) { |
---|
| 803 | /* Skip if node is not reachable from top of BDD. */ |
---|
| 804 | if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; |
---|
| 805 | |
---|
| 806 | /* Find f- */ |
---|
| 807 | leftChild = (j << 1) - 1; |
---|
| 808 | if (leftChild >= kTrueLower) { |
---|
| 809 | fminus = one; |
---|
| 810 | } else if (leftChild <= kFalseLower) { |
---|
| 811 | fminus = zero; |
---|
| 812 | } else { |
---|
| 813 | assert(leftChild == index[0] || leftChild == index[1]); |
---|
| 814 | if (leftChild == index[0]) { |
---|
| 815 | fminus = map[0]; |
---|
| 816 | } else { |
---|
| 817 | fminus = map[1]; |
---|
| 818 | } |
---|
| 819 | } |
---|
| 820 | |
---|
| 821 | /* Find f= */ |
---|
| 822 | middleChild = j << 1; |
---|
| 823 | if (middleChild >= kTrueLower) { |
---|
| 824 | fequal = one; |
---|
| 825 | } else if (middleChild <= kFalseLower) { |
---|
| 826 | fequal = zero; |
---|
| 827 | } else { |
---|
| 828 | assert(middleChild == index[0] || middleChild == index[1]); |
---|
| 829 | if (middleChild == index[0]) { |
---|
| 830 | fequal = map[0]; |
---|
| 831 | } else { |
---|
| 832 | fequal = map[1]; |
---|
| 833 | } |
---|
| 834 | } |
---|
| 835 | |
---|
| 836 | /* Find f+ */ |
---|
| 837 | rightChild = (j << 1) + 1; |
---|
| 838 | if (rightChild >= kTrueLower) { |
---|
| 839 | fplus = one; |
---|
| 840 | } else if (rightChild <= kFalseLower) { |
---|
| 841 | fplus = zero; |
---|
| 842 | } else { |
---|
| 843 | assert(rightChild == index[0] || rightChild == index[1]); |
---|
| 844 | if (rightChild == index[0]) { |
---|
| 845 | fplus = map[0]; |
---|
| 846 | } else { |
---|
| 847 | fplus = map[1]; |
---|
| 848 | } |
---|
| 849 | } |
---|
| 850 | |
---|
| 851 | /* Build new nodes. */ |
---|
| 852 | g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus); |
---|
| 853 | if (g1 == NULL) { |
---|
| 854 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 855 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 856 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 857 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 858 | return(NULL); |
---|
| 859 | } |
---|
| 860 | cuddRef(g1); |
---|
| 861 | g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal); |
---|
| 862 | if (g0 == NULL) { |
---|
| 863 | Cudd_IterDerefBdd(dd, g1); |
---|
| 864 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 865 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 866 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 867 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 868 | return(NULL); |
---|
| 869 | } |
---|
| 870 | cuddRef(g0); |
---|
| 871 | f = Cudd_bddIte(dd, x[N - i], g1, g0); |
---|
| 872 | if (f == NULL) { |
---|
| 873 | Cudd_IterDerefBdd(dd, g1); |
---|
| 874 | Cudd_IterDerefBdd(dd, g0); |
---|
| 875 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 876 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 877 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 878 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 879 | return(NULL); |
---|
| 880 | } |
---|
| 881 | cuddRef(f); |
---|
| 882 | Cudd_IterDerefBdd(dd, g1); |
---|
| 883 | Cudd_IterDerefBdd(dd, g0); |
---|
| 884 | |
---|
| 885 | /* Save newly computed node in map. */ |
---|
| 886 | assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); |
---|
| 887 | if (newIndex[0] == invalidIndex) { |
---|
| 888 | newIndex[0] = j; |
---|
| 889 | newMap[0] = f; |
---|
| 890 | } else { |
---|
| 891 | newIndex[1] = j; |
---|
| 892 | newMap[1] = f; |
---|
| 893 | } |
---|
| 894 | } |
---|
| 895 | |
---|
| 896 | /* Copy new map to map. */ |
---|
| 897 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 898 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 899 | map[0] = newMap[0]; |
---|
| 900 | map[1] = newMap[1]; |
---|
| 901 | index[0] = newIndex[0]; |
---|
| 902 | index[1] = newIndex[1]; |
---|
| 903 | } |
---|
| 904 | |
---|
| 905 | cuddDeref(f); |
---|
| 906 | return(f); |
---|
| 907 | |
---|
| 908 | } /* end of Cudd_Inequality */ |
---|
| 909 | |
---|
| 910 | |
---|
| 911 | /**Function******************************************************************** |
---|
| 912 | |
---|
| 913 | Synopsis [Generates a BDD for the function x - y != c.] |
---|
| 914 | |
---|
| 915 | Description [This function generates a BDD for the function x -y != c. |
---|
| 916 | Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and |
---|
| 917 | y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. |
---|
| 918 | The BDD is built bottom-up. |
---|
| 919 | It has a linear number of nodes if the variables are ordered as follows: |
---|
| 920 | x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].] |
---|
| 921 | |
---|
| 922 | SideEffects [None] |
---|
| 923 | |
---|
| 924 | SeeAlso [Cudd_Xgty] |
---|
| 925 | |
---|
| 926 | ******************************************************************************/ |
---|
| 927 | DdNode * |
---|
| 928 | Cudd_Disequality( |
---|
| 929 | DdManager * dd /* DD manager */, |
---|
| 930 | int N /* number of x and y variables */, |
---|
| 931 | int c /* right-hand side constant */, |
---|
| 932 | DdNode ** x /* array of x variables */, |
---|
| 933 | DdNode ** y /* array of y variables */) |
---|
| 934 | { |
---|
| 935 | /* The nodes at level i represent values of the difference that are |
---|
| 936 | ** multiples of 2^i. We use variables with names starting with k |
---|
| 937 | ** to denote the multipliers of 2^i in such multiples. */ |
---|
| 938 | int kTrueLb = c + 1; |
---|
| 939 | int kTrueUb = c - 1; |
---|
| 940 | int kFalse = c; |
---|
| 941 | /* Mask used to compute the ceiling function. Since we divide by 2^i, |
---|
| 942 | ** we want to know whether the dividend is a multiple of 2^i. If it is, |
---|
| 943 | ** then ceiling and floor coincide; otherwise, they differ by one. */ |
---|
| 944 | int mask = 1; |
---|
| 945 | int i; |
---|
| 946 | |
---|
| 947 | DdNode *f = NULL; /* the eventual result */ |
---|
| 948 | DdNode *one = DD_ONE(dd); |
---|
| 949 | DdNode *zero = Cudd_Not(one); |
---|
| 950 | |
---|
| 951 | /* Two x-labeled nodes are created at most at each iteration. They are |
---|
| 952 | ** stored, along with their k values, in these variables. At each level, |
---|
| 953 | ** the old nodes are freed and the new nodes are copied into the old map. |
---|
| 954 | */ |
---|
| 955 | DdNode *map[2]; |
---|
| 956 | int invalidIndex = 1 << (N-1); |
---|
| 957 | int index[2] = {invalidIndex, invalidIndex}; |
---|
| 958 | |
---|
| 959 | /* This should never happen. */ |
---|
| 960 | if (N < 0) return(NULL); |
---|
| 961 | |
---|
| 962 | /* If there are no bits, both operands are 0. The result depends on c. */ |
---|
| 963 | if (N == 0) { |
---|
| 964 | if (c != 0) return(one); |
---|
| 965 | else return(zero); |
---|
| 966 | } |
---|
| 967 | |
---|
| 968 | /* The maximum or the minimum difference comparing to c can generate the terminal case */ |
---|
| 969 | if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(one); |
---|
| 970 | |
---|
| 971 | /* Build the result bottom up. */ |
---|
| 972 | for (i = 1; i <= N; i++) { |
---|
| 973 | int kTrueLbLower, kTrueUbLower; |
---|
| 974 | int leftChild, middleChild, rightChild; |
---|
| 975 | DdNode *g0, *g1, *fplus, *fequal, *fminus; |
---|
| 976 | int j; |
---|
| 977 | DdNode *newMap[2]; |
---|
| 978 | int newIndex[2]; |
---|
| 979 | |
---|
| 980 | kTrueLbLower = kTrueLb; |
---|
| 981 | kTrueUbLower = kTrueUb; |
---|
| 982 | /* kTrueLb = floor((c-1)/2^i) + 2 */ |
---|
| 983 | kTrueLb = ((c-1) >> i) + 2; |
---|
| 984 | /* kTrueUb = ceiling((c+1)/2^i) - 2 */ |
---|
| 985 | kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2; |
---|
| 986 | mask = (mask << 1) | 1; |
---|
| 987 | newIndex[0] = invalidIndex; |
---|
| 988 | newIndex[1] = invalidIndex; |
---|
| 989 | |
---|
| 990 | for (j = kTrueUb + 1; j < kTrueLb; j++) { |
---|
| 991 | /* Skip if node is not reachable from top of BDD. */ |
---|
| 992 | if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue; |
---|
| 993 | |
---|
| 994 | /* Find f- */ |
---|
| 995 | leftChild = (j << 1) - 1; |
---|
| 996 | if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) { |
---|
| 997 | fminus = one; |
---|
| 998 | } else if (i == 1 && leftChild == kFalse) { |
---|
| 999 | fminus = zero; |
---|
| 1000 | } else { |
---|
| 1001 | assert(leftChild == index[0] || leftChild == index[1]); |
---|
| 1002 | if (leftChild == index[0]) { |
---|
| 1003 | fminus = map[0]; |
---|
| 1004 | } else { |
---|
| 1005 | fminus = map[1]; |
---|
| 1006 | } |
---|
| 1007 | } |
---|
| 1008 | |
---|
| 1009 | /* Find f= */ |
---|
| 1010 | middleChild = j << 1; |
---|
| 1011 | if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) { |
---|
| 1012 | fequal = one; |
---|
| 1013 | } else if (i == 1 && middleChild == kFalse) { |
---|
| 1014 | fequal = zero; |
---|
| 1015 | } else { |
---|
| 1016 | assert(middleChild == index[0] || middleChild == index[1]); |
---|
| 1017 | if (middleChild == index[0]) { |
---|
| 1018 | fequal = map[0]; |
---|
| 1019 | } else { |
---|
| 1020 | fequal = map[1]; |
---|
| 1021 | } |
---|
| 1022 | } |
---|
| 1023 | |
---|
| 1024 | /* Find f+ */ |
---|
| 1025 | rightChild = (j << 1) + 1; |
---|
| 1026 | if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) { |
---|
| 1027 | fplus = one; |
---|
| 1028 | } else if (i == 1 && rightChild == kFalse) { |
---|
| 1029 | fplus = zero; |
---|
| 1030 | } else { |
---|
| 1031 | assert(rightChild == index[0] || rightChild == index[1]); |
---|
| 1032 | if (rightChild == index[0]) { |
---|
| 1033 | fplus = map[0]; |
---|
| 1034 | } else { |
---|
| 1035 | fplus = map[1]; |
---|
| 1036 | } |
---|
| 1037 | } |
---|
| 1038 | |
---|
| 1039 | /* Build new nodes. */ |
---|
| 1040 | g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus); |
---|
| 1041 | if (g1 == NULL) { |
---|
| 1042 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 1043 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 1044 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 1045 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 1046 | return(NULL); |
---|
| 1047 | } |
---|
| 1048 | cuddRef(g1); |
---|
| 1049 | g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal); |
---|
| 1050 | if (g0 == NULL) { |
---|
| 1051 | Cudd_IterDerefBdd(dd, g1); |
---|
| 1052 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 1053 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 1054 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 1055 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 1056 | return(NULL); |
---|
| 1057 | } |
---|
| 1058 | cuddRef(g0); |
---|
| 1059 | f = Cudd_bddIte(dd, x[N - i], g1, g0); |
---|
| 1060 | if (f == NULL) { |
---|
| 1061 | Cudd_IterDerefBdd(dd, g1); |
---|
| 1062 | Cudd_IterDerefBdd(dd, g0); |
---|
| 1063 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 1064 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 1065 | if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]); |
---|
| 1066 | if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]); |
---|
| 1067 | return(NULL); |
---|
| 1068 | } |
---|
| 1069 | cuddRef(f); |
---|
| 1070 | Cudd_IterDerefBdd(dd, g1); |
---|
| 1071 | Cudd_IterDerefBdd(dd, g0); |
---|
| 1072 | |
---|
| 1073 | /* Save newly computed node in map. */ |
---|
| 1074 | assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex); |
---|
| 1075 | if (newIndex[0] == invalidIndex) { |
---|
| 1076 | newIndex[0] = j; |
---|
| 1077 | newMap[0] = f; |
---|
| 1078 | } else { |
---|
| 1079 | newIndex[1] = j; |
---|
| 1080 | newMap[1] = f; |
---|
| 1081 | } |
---|
| 1082 | } |
---|
| 1083 | |
---|
| 1084 | /* Copy new map to map. */ |
---|
| 1085 | if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]); |
---|
| 1086 | if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]); |
---|
| 1087 | map[0] = newMap[0]; |
---|
| 1088 | map[1] = newMap[1]; |
---|
| 1089 | index[0] = newIndex[0]; |
---|
| 1090 | index[1] = newIndex[1]; |
---|
| 1091 | } |
---|
| 1092 | |
---|
| 1093 | cuddDeref(f); |
---|
| 1094 | return(f); |
---|
| 1095 | |
---|
| 1096 | } /* end of Cudd_Disequality */ |
---|
| 1097 | |
---|
| 1098 | |
---|
| 1099 | /**Function******************************************************************** |
---|
| 1100 | |
---|
| 1101 | Synopsis [Generates a BDD for the function lowerB ≤ x ≤ upperB.] |
---|
| 1102 | |
---|
| 1103 | Description [This function generates a BDD for the function |
---|
| 1104 | lowerB ≤ x ≤ upperB, where x is an N-bit number, |
---|
| 1105 | x\[0\] x\[1\] ... x\[N-1\], with 0 the most significant bit (important!). |
---|
| 1106 | The number of variables N should be sufficient to represent the bounds; |
---|
| 1107 | otherwise, the bounds are truncated to their N least significant bits. |
---|
| 1108 | Two BDDs are built bottom-up for lowerB ≤ x and x ≤ upperB, and they |
---|
| 1109 | are finally conjoined.] |
---|
| 1110 | |
---|
| 1111 | SideEffects [None] |
---|
| 1112 | |
---|
| 1113 | SeeAlso [Cudd_Xgty] |
---|
| 1114 | |
---|
| 1115 | ******************************************************************************/ |
---|
| 1116 | DdNode * |
---|
| 1117 | Cudd_bddInterval( |
---|
| 1118 | DdManager * dd /* DD manager */, |
---|
| 1119 | int N /* number of x variables */, |
---|
| 1120 | DdNode ** x /* array of x variables */, |
---|
| 1121 | unsigned int lowerB /* lower bound */, |
---|
| 1122 | unsigned int upperB /* upper bound */) |
---|
| 1123 | { |
---|
| 1124 | DdNode *one, *zero; |
---|
| 1125 | DdNode *r, *rl, *ru; |
---|
| 1126 | int i; |
---|
| 1127 | |
---|
| 1128 | one = DD_ONE(dd); |
---|
| 1129 | zero = Cudd_Not(one); |
---|
| 1130 | |
---|
| 1131 | rl = one; |
---|
| 1132 | cuddRef(rl); |
---|
| 1133 | ru = one; |
---|
| 1134 | cuddRef(ru); |
---|
| 1135 | |
---|
| 1136 | /* Loop to build the rest of the BDDs. */ |
---|
| 1137 | for (i = N-1; i >= 0; i--) { |
---|
| 1138 | DdNode *vl, *vu; |
---|
| 1139 | vl = Cudd_bddIte(dd, x[i], |
---|
| 1140 | lowerB&1 ? rl : one, |
---|
| 1141 | lowerB&1 ? zero : rl); |
---|
| 1142 | if (vl == NULL) { |
---|
| 1143 | Cudd_IterDerefBdd(dd, rl); |
---|
| 1144 | Cudd_IterDerefBdd(dd, ru); |
---|
| 1145 | return(NULL); |
---|
| 1146 | } |
---|
| 1147 | cuddRef(vl); |
---|
| 1148 | Cudd_IterDerefBdd(dd, rl); |
---|
| 1149 | rl = vl; |
---|
| 1150 | lowerB >>= 1; |
---|
| 1151 | vu = Cudd_bddIte(dd, x[i], |
---|
| 1152 | upperB&1 ? ru : zero, |
---|
| 1153 | upperB&1 ? one : ru); |
---|
| 1154 | if (vu == NULL) { |
---|
| 1155 | Cudd_IterDerefBdd(dd, rl); |
---|
| 1156 | Cudd_IterDerefBdd(dd, ru); |
---|
| 1157 | return(NULL); |
---|
| 1158 | } |
---|
| 1159 | cuddRef(vu); |
---|
| 1160 | Cudd_IterDerefBdd(dd, ru); |
---|
| 1161 | ru = vu; |
---|
| 1162 | upperB >>= 1; |
---|
| 1163 | } |
---|
| 1164 | |
---|
| 1165 | /* Conjoin the two bounds. */ |
---|
| 1166 | r = Cudd_bddAnd(dd, rl, ru); |
---|
| 1167 | if (r == NULL) { |
---|
| 1168 | Cudd_IterDerefBdd(dd, rl); |
---|
| 1169 | Cudd_IterDerefBdd(dd, ru); |
---|
| 1170 | return(NULL); |
---|
| 1171 | } |
---|
| 1172 | cuddRef(r); |
---|
| 1173 | Cudd_IterDerefBdd(dd, rl); |
---|
| 1174 | Cudd_IterDerefBdd(dd, ru); |
---|
| 1175 | cuddDeref(r); |
---|
| 1176 | return(r); |
---|
| 1177 | |
---|
| 1178 | } /* end of Cudd_bddInterval */ |
---|
| 1179 | |
---|
| 1180 | |
---|
| 1181 | /**Function******************************************************************** |
---|
| 1182 | |
---|
| 1183 | Synopsis [Computes the compatible projection of R w.r.t. cube Y.] |
---|
| 1184 | |
---|
| 1185 | Description [Computes the compatible projection of relation R with |
---|
| 1186 | respect to cube Y. Returns a pointer to the c-projection if |
---|
| 1187 | successful; NULL otherwise. For a comparison between Cudd_CProjection |
---|
| 1188 | and Cudd_PrioritySelect, see the documentation of the latter.] |
---|
| 1189 | |
---|
| 1190 | SideEffects [None] |
---|
| 1191 | |
---|
| 1192 | SeeAlso [Cudd_PrioritySelect] |
---|
| 1193 | |
---|
| 1194 | ******************************************************************************/ |
---|
| 1195 | DdNode * |
---|
| 1196 | Cudd_CProjection( |
---|
| 1197 | DdManager * dd, |
---|
| 1198 | DdNode * R, |
---|
| 1199 | DdNode * Y) |
---|
| 1200 | { |
---|
| 1201 | DdNode *res; |
---|
| 1202 | DdNode *support; |
---|
| 1203 | |
---|
| 1204 | if (cuddCheckCube(dd,Y) == 0) { |
---|
| 1205 | (void) fprintf(dd->err, |
---|
| 1206 | "Error: The third argument of Cudd_CProjection should be a cube\n"); |
---|
| 1207 | dd->errorCode = CUDD_INVALID_ARG; |
---|
| 1208 | return(NULL); |
---|
| 1209 | } |
---|
| 1210 | |
---|
| 1211 | /* Compute the support of Y, which is used by the abstraction step |
---|
| 1212 | ** in cuddCProjectionRecur. |
---|
| 1213 | */ |
---|
| 1214 | support = Cudd_Support(dd,Y); |
---|
| 1215 | if (support == NULL) return(NULL); |
---|
| 1216 | cuddRef(support); |
---|
| 1217 | |
---|
| 1218 | do { |
---|
| 1219 | dd->reordered = 0; |
---|
| 1220 | res = cuddCProjectionRecur(dd,R,Y,support); |
---|
| 1221 | } while (dd->reordered == 1); |
---|
| 1222 | |
---|
| 1223 | if (res == NULL) { |
---|
| 1224 | Cudd_RecursiveDeref(dd,support); |
---|
| 1225 | return(NULL); |
---|
| 1226 | } |
---|
| 1227 | cuddRef(res); |
---|
| 1228 | Cudd_RecursiveDeref(dd,support); |
---|
| 1229 | cuddDeref(res); |
---|
| 1230 | |
---|
| 1231 | return(res); |
---|
| 1232 | |
---|
| 1233 | } /* end of Cudd_CProjection */ |
---|
| 1234 | |
---|
| 1235 | |
---|
| 1236 | /**Function******************************************************************** |
---|
| 1237 | |
---|
| 1238 | Synopsis [Computes the Hamming distance ADD.] |
---|
| 1239 | |
---|
| 1240 | Description [Computes the Hamming distance ADD. Returns an ADD that |
---|
| 1241 | gives the Hamming distance between its two arguments if successful; |
---|
| 1242 | NULL otherwise. The two vectors xVars and yVars identify the variables |
---|
| 1243 | that form the two arguments.] |
---|
| 1244 | |
---|
| 1245 | SideEffects [None] |
---|
| 1246 | |
---|
| 1247 | SeeAlso [] |
---|
| 1248 | |
---|
| 1249 | ******************************************************************************/ |
---|
| 1250 | DdNode * |
---|
| 1251 | Cudd_addHamming( |
---|
| 1252 | DdManager * dd, |
---|
| 1253 | DdNode ** xVars, |
---|
| 1254 | DdNode ** yVars, |
---|
| 1255 | int nVars) |
---|
| 1256 | { |
---|
| 1257 | DdNode *result,*tempBdd; |
---|
| 1258 | DdNode *tempAdd,*temp; |
---|
| 1259 | int i; |
---|
| 1260 | |
---|
| 1261 | result = DD_ZERO(dd); |
---|
| 1262 | cuddRef(result); |
---|
| 1263 | |
---|
| 1264 | for (i = 0; i < nVars; i++) { |
---|
| 1265 | tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]); |
---|
| 1266 | if (tempBdd == NULL) { |
---|
| 1267 | Cudd_RecursiveDeref(dd,result); |
---|
| 1268 | return(NULL); |
---|
| 1269 | } |
---|
| 1270 | cuddRef(tempBdd); |
---|
| 1271 | tempAdd = Cudd_BddToAdd(dd,tempBdd); |
---|
| 1272 | if (tempAdd == NULL) { |
---|
| 1273 | Cudd_RecursiveDeref(dd,tempBdd); |
---|
| 1274 | Cudd_RecursiveDeref(dd,result); |
---|
| 1275 | return(NULL); |
---|
| 1276 | } |
---|
| 1277 | cuddRef(tempAdd); |
---|
| 1278 | Cudd_RecursiveDeref(dd,tempBdd); |
---|
| 1279 | temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result); |
---|
| 1280 | if (temp == NULL) { |
---|
| 1281 | Cudd_RecursiveDeref(dd,tempAdd); |
---|
| 1282 | Cudd_RecursiveDeref(dd,result); |
---|
| 1283 | return(NULL); |
---|
| 1284 | } |
---|
| 1285 | cuddRef(temp); |
---|
| 1286 | Cudd_RecursiveDeref(dd,tempAdd); |
---|
| 1287 | Cudd_RecursiveDeref(dd,result); |
---|
| 1288 | result = temp; |
---|
| 1289 | } |
---|
| 1290 | |
---|
| 1291 | cuddDeref(result); |
---|
| 1292 | return(result); |
---|
| 1293 | |
---|
| 1294 | } /* end of Cudd_addHamming */ |
---|
| 1295 | |
---|
| 1296 | |
---|
| 1297 | /**Function******************************************************************** |
---|
| 1298 | |
---|
| 1299 | Synopsis [Returns the minimum Hamming distance between f and minterm.] |
---|
| 1300 | |
---|
| 1301 | Description [Returns the minimum Hamming distance between the |
---|
| 1302 | minterms of a function f and a reference minterm. The function is |
---|
| 1303 | given as a BDD; the minterm is given as an array of integers, one |
---|
| 1304 | for each variable in the manager. Returns the minimum distance if |
---|
| 1305 | it is less than the upper bound; the upper bound if the minimum |
---|
| 1306 | distance is at least as large; CUDD_OUT_OF_MEM in case of failure.] |
---|
| 1307 | |
---|
| 1308 | SideEffects [None] |
---|
| 1309 | |
---|
| 1310 | SeeAlso [Cudd_addHamming Cudd_bddClosestCube] |
---|
| 1311 | |
---|
| 1312 | ******************************************************************************/ |
---|
| 1313 | int |
---|
| 1314 | Cudd_MinHammingDist( |
---|
| 1315 | DdManager *dd /* DD manager */, |
---|
| 1316 | DdNode *f /* function to examine */, |
---|
| 1317 | int *minterm /* reference minterm */, |
---|
| 1318 | int upperBound /* distance above which an approximate answer is OK */) |
---|
| 1319 | { |
---|
| 1320 | DdHashTable *table; |
---|
| 1321 | CUDD_VALUE_TYPE epsilon; |
---|
| 1322 | int res; |
---|
| 1323 | |
---|
| 1324 | table = cuddHashTableInit(dd,1,2); |
---|
| 1325 | if (table == NULL) { |
---|
| 1326 | return(CUDD_OUT_OF_MEM); |
---|
| 1327 | } |
---|
| 1328 | epsilon = Cudd_ReadEpsilon(dd); |
---|
| 1329 | Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0); |
---|
| 1330 | res = cuddMinHammingDistRecur(f,minterm,table,upperBound); |
---|
| 1331 | cuddHashTableQuit(table); |
---|
| 1332 | Cudd_SetEpsilon(dd,epsilon); |
---|
| 1333 | |
---|
| 1334 | return(res); |
---|
| 1335 | |
---|
| 1336 | } /* end of Cudd_MinHammingDist */ |
---|
| 1337 | |
---|
| 1338 | |
---|
| 1339 | /**Function******************************************************************** |
---|
| 1340 | |
---|
| 1341 | Synopsis [Finds a cube of f at minimum Hamming distance from g.] |
---|
| 1342 | |
---|
| 1343 | Description [Finds a cube of f at minimum Hamming distance from the |
---|
| 1344 | minterms of g. All the minterms of the cube are at the minimum |
---|
| 1345 | distance. If the distance is 0, the cube belongs to the |
---|
| 1346 | intersection of f and g. Returns the cube if successful; NULL |
---|
| 1347 | otherwise.] |
---|
| 1348 | |
---|
| 1349 | SideEffects [The distance is returned as a side effect.] |
---|
| 1350 | |
---|
| 1351 | SeeAlso [Cudd_MinHammingDist] |
---|
| 1352 | |
---|
| 1353 | ******************************************************************************/ |
---|
| 1354 | DdNode * |
---|
| 1355 | Cudd_bddClosestCube( |
---|
| 1356 | DdManager *dd, |
---|
| 1357 | DdNode * f, |
---|
| 1358 | DdNode *g, |
---|
| 1359 | int *distance) |
---|
| 1360 | { |
---|
| 1361 | DdNode *res, *acube; |
---|
| 1362 | CUDD_VALUE_TYPE rdist; |
---|
| 1363 | |
---|
| 1364 | /* Compute the cube and distance as a single ADD. */ |
---|
| 1365 | do { |
---|
| 1366 | dd->reordered = 0; |
---|
| 1367 | res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0); |
---|
| 1368 | } while (dd->reordered == 1); |
---|
| 1369 | if (res == NULL) return(NULL); |
---|
| 1370 | cuddRef(res); |
---|
| 1371 | |
---|
| 1372 | /* Unpack distance and cube. */ |
---|
| 1373 | do { |
---|
| 1374 | dd->reordered = 0; |
---|
| 1375 | acube = separateCube(dd, res, &rdist); |
---|
| 1376 | } while (dd->reordered == 1); |
---|
| 1377 | if (acube == NULL) { |
---|
| 1378 | Cudd_RecursiveDeref(dd, res); |
---|
| 1379 | return(NULL); |
---|
| 1380 | } |
---|
| 1381 | cuddRef(acube); |
---|
| 1382 | Cudd_RecursiveDeref(dd, res); |
---|
| 1383 | |
---|
| 1384 | /* Convert cube from ADD to BDD. */ |
---|
| 1385 | do { |
---|
| 1386 | dd->reordered = 0; |
---|
| 1387 | res = cuddAddBddDoPattern(dd, acube); |
---|
| 1388 | } while (dd->reordered == 1); |
---|
| 1389 | if (res == NULL) { |
---|
| 1390 | Cudd_RecursiveDeref(dd, acube); |
---|
| 1391 | return(NULL); |
---|
| 1392 | } |
---|
| 1393 | cuddRef(res); |
---|
| 1394 | Cudd_RecursiveDeref(dd, acube); |
---|
| 1395 | |
---|
| 1396 | *distance = (int) rdist; |
---|
| 1397 | cuddDeref(res); |
---|
| 1398 | return(res); |
---|
| 1399 | |
---|
| 1400 | } /* end of Cudd_bddClosestCube */ |
---|
| 1401 | |
---|
| 1402 | |
---|
| 1403 | /*---------------------------------------------------------------------------*/ |
---|
| 1404 | /* Definition of internal functions */ |
---|
| 1405 | /*---------------------------------------------------------------------------*/ |
---|
| 1406 | |
---|
| 1407 | |
---|
| 1408 | /**Function******************************************************************** |
---|
| 1409 | |
---|
| 1410 | Synopsis [Performs the recursive step of Cudd_CProjection.] |
---|
| 1411 | |
---|
| 1412 | Description [Performs the recursive step of Cudd_CProjection. Returns |
---|
| 1413 | the projection if successful; NULL otherwise.] |
---|
| 1414 | |
---|
| 1415 | SideEffects [None] |
---|
| 1416 | |
---|
| 1417 | SeeAlso [Cudd_CProjection] |
---|
| 1418 | |
---|
| 1419 | ******************************************************************************/ |
---|
| 1420 | DdNode * |
---|
| 1421 | cuddCProjectionRecur( |
---|
| 1422 | DdManager * dd, |
---|
| 1423 | DdNode * R, |
---|
| 1424 | DdNode * Y, |
---|
| 1425 | DdNode * Ysupp) |
---|
| 1426 | { |
---|
| 1427 | DdNode *res, *res1, *res2, *resA; |
---|
| 1428 | DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha; |
---|
| 1429 | unsigned int topR, topY, top, index; |
---|
| 1430 | DdNode *one = DD_ONE(dd); |
---|
| 1431 | |
---|
| 1432 | statLine(dd); |
---|
| 1433 | if (Y == one) return(R); |
---|
| 1434 | |
---|
| 1435 | #ifdef DD_DEBUG |
---|
| 1436 | assert(!Cudd_IsConstant(Y)); |
---|
| 1437 | #endif |
---|
| 1438 | |
---|
| 1439 | if (R == Cudd_Not(one)) return(R); |
---|
| 1440 | |
---|
| 1441 | res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y); |
---|
| 1442 | if (res != NULL) return(res); |
---|
| 1443 | |
---|
| 1444 | r = Cudd_Regular(R); |
---|
| 1445 | topR = cuddI(dd,r->index); |
---|
| 1446 | y = Cudd_Regular(Y); |
---|
| 1447 | topY = cuddI(dd,y->index); |
---|
| 1448 | |
---|
| 1449 | top = ddMin(topR, topY); |
---|
| 1450 | |
---|
| 1451 | /* Compute the cofactors of R */ |
---|
| 1452 | if (topR == top) { |
---|
| 1453 | index = r->index; |
---|
| 1454 | RT = cuddT(r); |
---|
| 1455 | RE = cuddE(r); |
---|
| 1456 | if (r != R) { |
---|
| 1457 | RT = Cudd_Not(RT); RE = Cudd_Not(RE); |
---|
| 1458 | } |
---|
| 1459 | } else { |
---|
| 1460 | RT = RE = R; |
---|
| 1461 | } |
---|
| 1462 | |
---|
| 1463 | if (topY > top) { |
---|
| 1464 | /* Y does not depend on the current top variable. |
---|
| 1465 | ** We just need to compute the results on the two cofactors of R |
---|
| 1466 | ** and make them the children of a node labeled r->index. |
---|
| 1467 | */ |
---|
| 1468 | res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp); |
---|
| 1469 | if (res1 == NULL) return(NULL); |
---|
| 1470 | cuddRef(res1); |
---|
| 1471 | res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp); |
---|
| 1472 | if (res2 == NULL) { |
---|
| 1473 | Cudd_RecursiveDeref(dd,res1); |
---|
| 1474 | return(NULL); |
---|
| 1475 | } |
---|
| 1476 | cuddRef(res2); |
---|
| 1477 | res = cuddBddIteRecur(dd, dd->vars[index], res1, res2); |
---|
| 1478 | if (res == NULL) { |
---|
| 1479 | Cudd_RecursiveDeref(dd,res1); |
---|
| 1480 | Cudd_RecursiveDeref(dd,res2); |
---|
| 1481 | return(NULL); |
---|
| 1482 | } |
---|
| 1483 | /* If we have reached this point, res1 and res2 are now |
---|
| 1484 | ** incorporated in res. cuddDeref is therefore sufficient. |
---|
| 1485 | */ |
---|
| 1486 | cuddDeref(res1); |
---|
| 1487 | cuddDeref(res2); |
---|
| 1488 | } else { |
---|
| 1489 | /* Compute the cofactors of Y */ |
---|
| 1490 | index = y->index; |
---|
| 1491 | YT = cuddT(y); |
---|
| 1492 | YE = cuddE(y); |
---|
| 1493 | if (y != Y) { |
---|
| 1494 | YT = Cudd_Not(YT); YE = Cudd_Not(YE); |
---|
| 1495 | } |
---|
| 1496 | if (YT == Cudd_Not(one)) { |
---|
| 1497 | Alpha = Cudd_Not(dd->vars[index]); |
---|
| 1498 | Yrest = YE; |
---|
| 1499 | Ra = RE; |
---|
| 1500 | Ran = RT; |
---|
| 1501 | } else { |
---|
| 1502 | Alpha = dd->vars[index]; |
---|
| 1503 | Yrest = YT; |
---|
| 1504 | Ra = RT; |
---|
| 1505 | Ran = RE; |
---|
| 1506 | } |
---|
| 1507 | Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp)); |
---|
| 1508 | if (Gamma == NULL) return(NULL); |
---|
| 1509 | if (Gamma == one) { |
---|
| 1510 | res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); |
---|
| 1511 | if (res1 == NULL) return(NULL); |
---|
| 1512 | cuddRef(res1); |
---|
| 1513 | res = cuddBddAndRecur(dd, Alpha, res1); |
---|
| 1514 | if (res == NULL) { |
---|
| 1515 | Cudd_RecursiveDeref(dd,res1); |
---|
| 1516 | return(NULL); |
---|
| 1517 | } |
---|
| 1518 | cuddDeref(res1); |
---|
| 1519 | } else if (Gamma == Cudd_Not(one)) { |
---|
| 1520 | res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); |
---|
| 1521 | if (res1 == NULL) return(NULL); |
---|
| 1522 | cuddRef(res1); |
---|
| 1523 | res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1); |
---|
| 1524 | if (res == NULL) { |
---|
| 1525 | Cudd_RecursiveDeref(dd,res1); |
---|
| 1526 | return(NULL); |
---|
| 1527 | } |
---|
| 1528 | cuddDeref(res1); |
---|
| 1529 | } else { |
---|
| 1530 | cuddRef(Gamma); |
---|
| 1531 | resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); |
---|
| 1532 | if (resA == NULL) { |
---|
| 1533 | Cudd_RecursiveDeref(dd,Gamma); |
---|
| 1534 | return(NULL); |
---|
| 1535 | } |
---|
| 1536 | cuddRef(resA); |
---|
| 1537 | res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA); |
---|
| 1538 | if (res2 == NULL) { |
---|
| 1539 | Cudd_RecursiveDeref(dd,Gamma); |
---|
| 1540 | Cudd_RecursiveDeref(dd,resA); |
---|
| 1541 | return(NULL); |
---|
| 1542 | } |
---|
| 1543 | cuddRef(res2); |
---|
| 1544 | Cudd_RecursiveDeref(dd,Gamma); |
---|
| 1545 | Cudd_RecursiveDeref(dd,resA); |
---|
| 1546 | res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); |
---|
| 1547 | if (res1 == NULL) { |
---|
| 1548 | Cudd_RecursiveDeref(dd,res2); |
---|
| 1549 | return(NULL); |
---|
| 1550 | } |
---|
| 1551 | cuddRef(res1); |
---|
| 1552 | res = cuddBddIteRecur(dd, Alpha, res1, res2); |
---|
| 1553 | if (res == NULL) { |
---|
| 1554 | Cudd_RecursiveDeref(dd,res1); |
---|
| 1555 | Cudd_RecursiveDeref(dd,res2); |
---|
| 1556 | return(NULL); |
---|
| 1557 | } |
---|
| 1558 | cuddDeref(res1); |
---|
| 1559 | cuddDeref(res2); |
---|
| 1560 | } |
---|
| 1561 | } |
---|
| 1562 | |
---|
| 1563 | cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res); |
---|
| 1564 | |
---|
| 1565 | return(res); |
---|
| 1566 | |
---|
| 1567 | } /* end of cuddCProjectionRecur */ |
---|
| 1568 | |
---|
| 1569 | |
---|
| 1570 | /**Function******************************************************************** |
---|
| 1571 | |
---|
| 1572 | Synopsis [Performs the recursive step of Cudd_bddClosestCube.] |
---|
| 1573 | |
---|
| 1574 | Description [Performs the recursive step of Cudd_bddClosestCube. |
---|
| 1575 | Returns the cube if succesful; NULL otherwise. The procedure uses a |
---|
| 1576 | four-way recursion to examine all four combinations of cofactors of |
---|
| 1577 | <code>f</code> and <code>g</code> according to the following formula. |
---|
| 1578 | <pre> |
---|
| 1579 | H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1) |
---|
| 1580 | </pre> |
---|
| 1581 | Bounding is based on the following observations. |
---|
| 1582 | <ul> |
---|
| 1583 | <li> If we already found two points at distance 0, there is no point in |
---|
| 1584 | continuing. Furthermore, |
---|
| 1585 | <li> If F == not(G) then the best we can hope for is a minimum distance |
---|
| 1586 | of 1. If we have already found two points at distance 1, there is |
---|
| 1587 | no point in continuing. (Indeed, H(F,G) == 1 in this case. We |
---|
| 1588 | have to continue, though, to find the cube.) |
---|
| 1589 | </ul> |
---|
| 1590 | The variable <code>bound</code> is set at the largest value of the distance |
---|
| 1591 | that we are still interested in. Therefore, we desist when |
---|
| 1592 | <pre> |
---|
| 1593 | (bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)). |
---|
| 1594 | </pre> |
---|
| 1595 | If we were maximally aggressive in using the bound, we would always |
---|
| 1596 | set the bound to the minimum distance seen thus far minus one. That |
---|
| 1597 | is, we would maintain the invariant |
---|
| 1598 | <pre> |
---|
| 1599 | bound < minD, |
---|
| 1600 | </pre> |
---|
| 1601 | except at the very beginning, when we have no value for |
---|
| 1602 | <code>minD</code>.<p> |
---|
| 1603 | |
---|
| 1604 | However, we do not use <code>bound < minD</code> when examining the |
---|
| 1605 | two negative cofactors, because we try to find a large cube at |
---|
| 1606 | minimum distance. To do so, we try to find a cube in the negative |
---|
| 1607 | cofactors at the same or smaller distance from the cube found in the |
---|
| 1608 | positive cofactors.<p> |
---|
| 1609 | |
---|
| 1610 | When we compute <code>H(ft,ge)</code> and <code>H(fe,gt)</code> we |
---|
| 1611 | know that we are going to add 1 to the result of the recursive call |
---|
| 1612 | to account for the difference in the splitting variable. Therefore, |
---|
| 1613 | we decrease the bound correspondingly.<p> |
---|
| 1614 | |
---|
| 1615 | Another important observation concerns the need of examining all |
---|
| 1616 | four pairs of cofators only when both <code>f</code> and |
---|
| 1617 | <code>g</code> depend on the top variable.<p> |
---|
| 1618 | |
---|
| 1619 | Suppose <code>gt == ge == g</code>. (That is, <code>g</code> does |
---|
| 1620 | not depend on the top variable.) Then |
---|
| 1621 | <pre> |
---|
| 1622 | H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1) |
---|
| 1623 | = min(H(ft,g), H(fe,g)) . |
---|
| 1624 | </pre> |
---|
| 1625 | Therefore, under these circumstances, we skip the two "cross" cases.<p> |
---|
| 1626 | |
---|
| 1627 | An interesting feature of this function is the scheme used for |
---|
| 1628 | caching the results in the global computed table. Since we have a |
---|
| 1629 | cube and a distance, we combine them to form an ADD. The |
---|
| 1630 | combination replaces the zero child of the top node of the cube with |
---|
| 1631 | the negative of the distance. (The use of the negative is to avoid |
---|
| 1632 | ambiguity with 1.) The degenerate cases (zero and one) are treated |
---|
| 1633 | specially because the distance is known (0 for one, and infinity for |
---|
| 1634 | zero).] |
---|
| 1635 | |
---|
| 1636 | SideEffects [None] |
---|
| 1637 | |
---|
| 1638 | SeeAlso [Cudd_bddClosestCube] |
---|
| 1639 | |
---|
| 1640 | ******************************************************************************/ |
---|
| 1641 | DdNode * |
---|
| 1642 | cuddBddClosestCube( |
---|
| 1643 | DdManager *dd, |
---|
| 1644 | DdNode *f, |
---|
| 1645 | DdNode *g, |
---|
| 1646 | CUDD_VALUE_TYPE bound) |
---|
| 1647 | { |
---|
| 1648 | DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee; |
---|
| 1649 | DdNode *ctt, *cee, *cte, *cet; |
---|
| 1650 | CUDD_VALUE_TYPE minD, dtt, dee, dte, det; |
---|
| 1651 | DdNode *one = DD_ONE(dd); |
---|
| 1652 | DdNode *lzero = Cudd_Not(one); |
---|
| 1653 | DdNode *azero = DD_ZERO(dd); |
---|
| 1654 | unsigned int topf, topg, index; |
---|
| 1655 | |
---|
| 1656 | statLine(dd); |
---|
| 1657 | if (bound < (f == Cudd_Not(g))) return(azero); |
---|
| 1658 | /* Terminal cases. */ |
---|
| 1659 | if (g == lzero || f == lzero) return(azero); |
---|
| 1660 | if (f == one && g == one) return(one); |
---|
| 1661 | |
---|
| 1662 | /* Check cache. */ |
---|
| 1663 | F = Cudd_Regular(f); |
---|
| 1664 | G = Cudd_Regular(g); |
---|
| 1665 | if (F->ref != 1 || G->ref != 1) { |
---|
| 1666 | res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g); |
---|
| 1667 | if (res != NULL) return(res); |
---|
| 1668 | } |
---|
| 1669 | |
---|
| 1670 | topf = cuddI(dd,F->index); |
---|
| 1671 | topg = cuddI(dd,G->index); |
---|
| 1672 | |
---|
| 1673 | /* Compute cofactors. */ |
---|
| 1674 | if (topf <= topg) { |
---|
| 1675 | index = F->index; |
---|
| 1676 | ft = cuddT(F); |
---|
| 1677 | fe = cuddE(F); |
---|
| 1678 | if (Cudd_IsComplement(f)) { |
---|
| 1679 | ft = Cudd_Not(ft); |
---|
| 1680 | fe = Cudd_Not(fe); |
---|
| 1681 | } |
---|
| 1682 | } else { |
---|
| 1683 | index = G->index; |
---|
| 1684 | ft = fe = f; |
---|
| 1685 | } |
---|
| 1686 | |
---|
| 1687 | if (topg <= topf) { |
---|
| 1688 | gt = cuddT(G); |
---|
| 1689 | ge = cuddE(G); |
---|
| 1690 | if (Cudd_IsComplement(g)) { |
---|
| 1691 | gt = Cudd_Not(gt); |
---|
| 1692 | ge = Cudd_Not(ge); |
---|
| 1693 | } |
---|
| 1694 | } else { |
---|
| 1695 | gt = ge = g; |
---|
| 1696 | } |
---|
| 1697 | |
---|
| 1698 | tt = cuddBddClosestCube(dd,ft,gt,bound); |
---|
| 1699 | if (tt == NULL) return(NULL); |
---|
| 1700 | cuddRef(tt); |
---|
| 1701 | ctt = separateCube(dd,tt,&dtt); |
---|
| 1702 | if (ctt == NULL) { |
---|
| 1703 | Cudd_RecursiveDeref(dd, tt); |
---|
| 1704 | return(NULL); |
---|
| 1705 | } |
---|
| 1706 | cuddRef(ctt); |
---|
| 1707 | Cudd_RecursiveDeref(dd, tt); |
---|
| 1708 | minD = dtt; |
---|
| 1709 | bound = ddMin(bound,minD); |
---|
| 1710 | |
---|
| 1711 | ee = cuddBddClosestCube(dd,fe,ge,bound); |
---|
| 1712 | if (ee == NULL) { |
---|
| 1713 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1714 | return(NULL); |
---|
| 1715 | } |
---|
| 1716 | cuddRef(ee); |
---|
| 1717 | cee = separateCube(dd,ee,&dee); |
---|
| 1718 | if (cee == NULL) { |
---|
| 1719 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1720 | Cudd_RecursiveDeref(dd, ee); |
---|
| 1721 | return(NULL); |
---|
| 1722 | } |
---|
| 1723 | cuddRef(cee); |
---|
| 1724 | Cudd_RecursiveDeref(dd, ee); |
---|
| 1725 | minD = ddMin(dtt, dee); |
---|
| 1726 | if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); |
---|
| 1727 | |
---|
| 1728 | if (minD > 0 && topf == topg) { |
---|
| 1729 | DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1); |
---|
| 1730 | if (te == NULL) { |
---|
| 1731 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1732 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1733 | return(NULL); |
---|
| 1734 | } |
---|
| 1735 | cuddRef(te); |
---|
| 1736 | cte = separateCube(dd,te,&dte); |
---|
| 1737 | if (cte == NULL) { |
---|
| 1738 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1739 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1740 | Cudd_RecursiveDeref(dd, te); |
---|
| 1741 | return(NULL); |
---|
| 1742 | } |
---|
| 1743 | cuddRef(cte); |
---|
| 1744 | Cudd_RecursiveDeref(dd, te); |
---|
| 1745 | dte += 1.0; |
---|
| 1746 | minD = ddMin(minD, dte); |
---|
| 1747 | } else { |
---|
| 1748 | cte = azero; |
---|
| 1749 | cuddRef(cte); |
---|
| 1750 | dte = CUDD_CONST_INDEX + 1.0; |
---|
| 1751 | } |
---|
| 1752 | if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1); |
---|
| 1753 | |
---|
| 1754 | if (minD > 0 && topf == topg) { |
---|
| 1755 | DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1); |
---|
| 1756 | if (et == NULL) { |
---|
| 1757 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1758 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1759 | Cudd_RecursiveDeref(dd, cte); |
---|
| 1760 | return(NULL); |
---|
| 1761 | } |
---|
| 1762 | cuddRef(et); |
---|
| 1763 | cet = separateCube(dd,et,&det); |
---|
| 1764 | if (cet == NULL) { |
---|
| 1765 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1766 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1767 | Cudd_RecursiveDeref(dd, cte); |
---|
| 1768 | Cudd_RecursiveDeref(dd, et); |
---|
| 1769 | return(NULL); |
---|
| 1770 | } |
---|
| 1771 | cuddRef(cet); |
---|
| 1772 | Cudd_RecursiveDeref(dd, et); |
---|
| 1773 | det += 1.0; |
---|
| 1774 | minD = ddMin(minD, det); |
---|
| 1775 | } else { |
---|
| 1776 | cet = azero; |
---|
| 1777 | cuddRef(cet); |
---|
| 1778 | det = CUDD_CONST_INDEX + 1.0; |
---|
| 1779 | } |
---|
| 1780 | |
---|
| 1781 | if (minD == dtt) { |
---|
| 1782 | if (dtt == dee && ctt == cee) { |
---|
| 1783 | res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt); |
---|
| 1784 | } else { |
---|
| 1785 | res = createResult(dd,index,1,ctt,dtt); |
---|
| 1786 | } |
---|
| 1787 | } else if (minD == dee) { |
---|
| 1788 | res = createResult(dd,index,0,cee,dee); |
---|
| 1789 | } else if (minD == dte) { |
---|
| 1790 | #ifdef DD_DEBUG |
---|
| 1791 | assert(topf == topg); |
---|
| 1792 | #endif |
---|
| 1793 | res = createResult(dd,index,1,cte,dte); |
---|
| 1794 | } else { |
---|
| 1795 | #ifdef DD_DEBUG |
---|
| 1796 | assert(topf == topg); |
---|
| 1797 | #endif |
---|
| 1798 | res = createResult(dd,index,0,cet,det); |
---|
| 1799 | } |
---|
| 1800 | if (res == NULL) { |
---|
| 1801 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1802 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1803 | Cudd_RecursiveDeref(dd, cte); |
---|
| 1804 | Cudd_RecursiveDeref(dd, cet); |
---|
| 1805 | return(NULL); |
---|
| 1806 | } |
---|
| 1807 | cuddRef(res); |
---|
| 1808 | Cudd_RecursiveDeref(dd, ctt); |
---|
| 1809 | Cudd_RecursiveDeref(dd, cee); |
---|
| 1810 | Cudd_RecursiveDeref(dd, cte); |
---|
| 1811 | Cudd_RecursiveDeref(dd, cet); |
---|
| 1812 | |
---|
| 1813 | /* Only cache results that are different from azero to avoid |
---|
| 1814 | ** storing results that depend on the value of the bound. */ |
---|
| 1815 | if ((F->ref != 1 || G->ref != 1) && res != azero) |
---|
| 1816 | cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res); |
---|
| 1817 | |
---|
| 1818 | cuddDeref(res); |
---|
| 1819 | return(res); |
---|
| 1820 | |
---|
| 1821 | } /* end of cuddBddClosestCube */ |
---|
| 1822 | |
---|
| 1823 | |
---|
| 1824 | /*---------------------------------------------------------------------------*/ |
---|
| 1825 | /* Definition of static functions */ |
---|
| 1826 | /*---------------------------------------------------------------------------*/ |
---|
| 1827 | |
---|
| 1828 | |
---|
| 1829 | /**Function******************************************************************** |
---|
| 1830 | |
---|
| 1831 | Synopsis [Performs the recursive step of Cudd_MinHammingDist.] |
---|
| 1832 | |
---|
| 1833 | Description [Performs the recursive step of Cudd_MinHammingDist. |
---|
| 1834 | It is based on the following identity. Let H(f) be the |
---|
| 1835 | minimum Hamming distance of the minterms of f from the reference |
---|
| 1836 | minterm. Then: |
---|
| 1837 | <xmp> |
---|
| 1838 | H(f) = min(H(f0)+h0,H(f1)+h1) |
---|
| 1839 | </xmp> |
---|
| 1840 | where f0 and f1 are the two cofactors of f with respect to its top |
---|
| 1841 | variable; h0 is 1 if the minterm assigns 1 to the top variable of f; |
---|
| 1842 | h1 is 1 if the minterm assigns 0 to the top variable of f. |
---|
| 1843 | The upper bound on the distance is used to bound the depth of the |
---|
| 1844 | recursion. |
---|
| 1845 | Returns the minimum distance unless it exceeds the upper bound or |
---|
| 1846 | computation fails.] |
---|
| 1847 | |
---|
| 1848 | SideEffects [None] |
---|
| 1849 | |
---|
| 1850 | SeeAlso [Cudd_MinHammingDist] |
---|
| 1851 | |
---|
| 1852 | ******************************************************************************/ |
---|
| 1853 | static int |
---|
| 1854 | cuddMinHammingDistRecur( |
---|
| 1855 | DdNode * f, |
---|
| 1856 | int *minterm, |
---|
| 1857 | DdHashTable * table, |
---|
| 1858 | int upperBound) |
---|
| 1859 | { |
---|
| 1860 | DdNode *F, *Ft, *Fe; |
---|
| 1861 | double h, hT, hE; |
---|
| 1862 | DdNode *zero, *res; |
---|
| 1863 | DdManager *dd = table->manager; |
---|
| 1864 | |
---|
| 1865 | statLine(dd); |
---|
| 1866 | if (upperBound == 0) return(0); |
---|
| 1867 | |
---|
| 1868 | F = Cudd_Regular(f); |
---|
| 1869 | |
---|
| 1870 | if (cuddIsConstant(F)) { |
---|
| 1871 | zero = Cudd_Not(DD_ONE(dd)); |
---|
| 1872 | if (f == dd->background || f == zero) { |
---|
| 1873 | return(upperBound); |
---|
| 1874 | } else { |
---|
| 1875 | return(0); |
---|
| 1876 | } |
---|
| 1877 | } |
---|
| 1878 | if ((res = cuddHashTableLookup1(table,f)) != NULL) { |
---|
| 1879 | h = cuddV(res); |
---|
| 1880 | if (res->ref == 0) { |
---|
| 1881 | dd->dead++; |
---|
| 1882 | dd->constants.dead++; |
---|
| 1883 | } |
---|
| 1884 | return((int) h); |
---|
| 1885 | } |
---|
| 1886 | |
---|
| 1887 | Ft = cuddT(F); Fe = cuddE(F); |
---|
| 1888 | if (Cudd_IsComplement(f)) { |
---|
| 1889 | Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe); |
---|
| 1890 | } |
---|
| 1891 | if (minterm[F->index] == 0) { |
---|
| 1892 | DdNode *temp = Ft; |
---|
| 1893 | Ft = Fe; Fe = temp; |
---|
| 1894 | } |
---|
| 1895 | |
---|
| 1896 | hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound); |
---|
| 1897 | if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); |
---|
| 1898 | if (hT == 0) { |
---|
| 1899 | hE = upperBound; |
---|
| 1900 | } else { |
---|
| 1901 | hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1); |
---|
| 1902 | if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); |
---|
| 1903 | } |
---|
| 1904 | h = ddMin(hT, hE + 1); |
---|
| 1905 | |
---|
| 1906 | if (F->ref != 1) { |
---|
| 1907 | ptrint fanout = (ptrint) F->ref; |
---|
| 1908 | cuddSatDec(fanout); |
---|
| 1909 | res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h); |
---|
| 1910 | if (!cuddHashTableInsert1(table,f,res,fanout)) { |
---|
| 1911 | cuddRef(res); Cudd_RecursiveDeref(dd, res); |
---|
| 1912 | return(CUDD_OUT_OF_MEM); |
---|
| 1913 | } |
---|
| 1914 | } |
---|
| 1915 | |
---|
| 1916 | return((int) h); |
---|
| 1917 | |
---|
| 1918 | } /* end of cuddMinHammingDistRecur */ |
---|
| 1919 | |
---|
| 1920 | |
---|
| 1921 | /**Function******************************************************************** |
---|
| 1922 | |
---|
| 1923 | Synopsis [Separates cube from distance.] |
---|
| 1924 | |
---|
| 1925 | Description [Separates cube from distance. Returns the cube if |
---|
| 1926 | successful; NULL otherwise.] |
---|
| 1927 | |
---|
| 1928 | SideEffects [The distance is returned as a side effect.] |
---|
| 1929 | |
---|
| 1930 | SeeAlso [cuddBddClosestCube createResult] |
---|
| 1931 | |
---|
| 1932 | ******************************************************************************/ |
---|
| 1933 | static DdNode * |
---|
| 1934 | separateCube( |
---|
| 1935 | DdManager *dd, |
---|
| 1936 | DdNode *f, |
---|
| 1937 | CUDD_VALUE_TYPE *distance) |
---|
| 1938 | { |
---|
| 1939 | DdNode *cube, *t; |
---|
| 1940 | |
---|
| 1941 | /* One and zero are special cases because the distance is implied. */ |
---|
| 1942 | if (Cudd_IsConstant(f)) { |
---|
| 1943 | *distance = (f == DD_ONE(dd)) ? 0.0 : |
---|
| 1944 | (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX); |
---|
| 1945 | return(f); |
---|
| 1946 | } |
---|
| 1947 | |
---|
| 1948 | /* Find out which branch points to the distance and replace the top |
---|
| 1949 | ** node with one pointing to zero instead. */ |
---|
| 1950 | t = cuddT(f); |
---|
| 1951 | if (Cudd_IsConstant(t) && cuddV(t) <= 0) { |
---|
| 1952 | #ifdef DD_DEBUG |
---|
| 1953 | assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd)); |
---|
| 1954 | #endif |
---|
| 1955 | *distance = -cuddV(t); |
---|
| 1956 | cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f)); |
---|
| 1957 | } else { |
---|
| 1958 | #ifdef DD_DEBUG |
---|
| 1959 | assert(!Cudd_IsConstant(t) || t == DD_ONE(dd)); |
---|
| 1960 | #endif |
---|
| 1961 | *distance = -cuddV(cuddE(f)); |
---|
| 1962 | cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd)); |
---|
| 1963 | } |
---|
| 1964 | |
---|
| 1965 | return(cube); |
---|
| 1966 | |
---|
| 1967 | } /* end of separateCube */ |
---|
| 1968 | |
---|
| 1969 | |
---|
| 1970 | /**Function******************************************************************** |
---|
| 1971 | |
---|
| 1972 | Synopsis [Builds a result for cache storage.] |
---|
| 1973 | |
---|
| 1974 | Description [Builds a result for cache storage. Returns a pointer |
---|
| 1975 | to the resulting ADD if successful; NULL otherwise.] |
---|
| 1976 | |
---|
| 1977 | SideEffects [None] |
---|
| 1978 | |
---|
| 1979 | SeeAlso [cuddBddClosestCube separateCube] |
---|
| 1980 | |
---|
| 1981 | ******************************************************************************/ |
---|
| 1982 | static DdNode * |
---|
| 1983 | createResult( |
---|
| 1984 | DdManager *dd, |
---|
| 1985 | unsigned int index, |
---|
| 1986 | unsigned int phase, |
---|
| 1987 | DdNode *cube, |
---|
| 1988 | CUDD_VALUE_TYPE distance) |
---|
| 1989 | { |
---|
| 1990 | DdNode *res, *constant; |
---|
| 1991 | |
---|
| 1992 | /* Special case. The cube is either one or zero, and we do not |
---|
| 1993 | ** add any variables. Hence, the result is also one or zero, |
---|
| 1994 | ** and the distance remains implied by the value of the constant. */ |
---|
| 1995 | if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube); |
---|
| 1996 | |
---|
| 1997 | constant = cuddUniqueConst(dd,-distance); |
---|
| 1998 | if (constant == NULL) return(NULL); |
---|
| 1999 | cuddRef(constant); |
---|
| 2000 | |
---|
| 2001 | if (index == CUDD_CONST_INDEX) { |
---|
| 2002 | /* Replace the top node. */ |
---|
| 2003 | if (cuddT(cube) == DD_ZERO(dd)) { |
---|
| 2004 | res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube)); |
---|
| 2005 | } else { |
---|
| 2006 | res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant); |
---|
| 2007 | } |
---|
| 2008 | } else { |
---|
| 2009 | /* Add a new top node. */ |
---|
| 2010 | #ifdef DD_DEBUG |
---|
| 2011 | assert(cuddI(dd,index) < cuddI(dd,cube->index)); |
---|
| 2012 | #endif |
---|
| 2013 | if (phase) { |
---|
| 2014 | res = cuddUniqueInter(dd,index,cube,constant); |
---|
| 2015 | } else { |
---|
| 2016 | res = cuddUniqueInter(dd,index,constant,cube); |
---|
| 2017 | } |
---|
| 2018 | } |
---|
| 2019 | if (res == NULL) { |
---|
| 2020 | Cudd_RecursiveDeref(dd, constant); |
---|
| 2021 | return(NULL); |
---|
| 2022 | } |
---|
| 2023 | cuddDeref(constant); /* safe because constant is part of res */ |
---|
| 2024 | |
---|
| 2025 | return(res); |
---|
| 2026 | |
---|
| 2027 | } /* end of createResult */ |
---|