1 /** 2 @file 3 4 @ingroup cudd 5 6 @brief Internal data structures of the CUDD package. 7 8 @author Fabio Somenzi 9 10 @copyright@parblock 11 Copyright (c) 1995-2015, Regents of the University of Colorado 12 13 All rights reserved. 14 15 Redistribution and use in source and binary forms, with or without 16 modification, are permitted provided that the following conditions 17 are met: 18 19 Redistributions of source code must retain the above copyright 20 notice, this list of conditions and the following disclaimer. 21 22 Redistributions in binary form must reproduce the above copyright 23 notice, this list of conditions and the following disclaimer in the 24 documentation and/or other materials provided with the distribution. 25 26 Neither the name of the University of Colorado nor the names of its 27 contributors may be used to endorse or promote products derived from 28 this software without specific prior written permission. 29 30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 41 POSSIBILITY OF SUCH DAMAGE. 42 @endparblock 43 44 */ 45 46 #ifndef CUDD_INT_H_ 47 #define CUDD_INT_H_ 48 49 50 /*---------------------------------------------------------------------------*/ 51 /* Nested includes */ 52 /*---------------------------------------------------------------------------*/ 53 54 #include <math.h> 55 #include "config.h" 56 #include "st.h" 57 #include "mtr.h" 58 #include "epd.h" 59 #include "cudd.h" 60 61 /*---------------------------------------------------------------------------*/ 62 /* Constant declarations */ 63 /*---------------------------------------------------------------------------*/ 64 65 #define CUDD_VERSION PACKAGE_VERSION 66 67 #define DD_MAXREF ((DdHalfWord) ~0) 68 69 #define DD_DEFAULT_RESIZE 10 /* how many extra variables */ 70 /* should be added when resizing */ 71 #define DD_MEM_CHUNK 1022 72 73 /* These definitions work for CUDD_VALUE_TYPE == double */ 74 #define DD_ONE_VAL (1.0) 75 #define DD_ZERO_VAL (0.0) 76 #define DD_EPSILON (1.0e-12) 77 78 /* The definitions of +/- infinity in terms of HUGE_VAL work on 79 ** the DECstations and on many other combinations of OS/compiler. 80 */ 81 #ifdef HAVE_IEEE_754 82 # define DD_PLUS_INF_VAL (HUGE_VAL) 83 #else 84 # define DD_PLUS_INF_VAL (10e301) 85 # define DD_CRI_HI_MARK (10e150) 86 # define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK)) 87 #endif 88 #define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL)) 89 90 #define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */ 91 92 /* Unique table and cache management constants. */ 93 #define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */ 94 /* gc when this percent are dead (measured w.r.t. slots, not keys) 95 ** The first limit (LO) applies normally. The second limit applies when 96 ** the package believes more space for the unique table (i.e., more dead 97 ** nodes) would improve performance, and the unique table is not already 98 ** too large. The third limit applies when memory is low. 99 */ 100 #define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25 101 #define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0 102 #define DD_GC_FRAC_MIN 0.2 103 #define DD_MIN_HIT 30 /* resize cache when hit ratio 104 above this percentage (default) */ 105 #define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for 106 unique table in fast growth mode) */ 107 #define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for 108 computed table if resizing enabled) */ 109 #define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set 110 aside for emergencies) */ 111 #define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */ 112 113 /* Variable ordering default parameter values. */ 114 #define DD_SIFT_MAX_VAR 1000 115 #define DD_SIFT_MAX_SWAPS 2000000 116 #define DD_DEFAULT_RECOMB 0 117 #define DD_MAX_REORDER_GROWTH 1.2 118 #define DD_FIRST_REORDER 4004 /* 4 for the constants */ 119 #define DD_DYN_RATIO 2 /* when to dynamically reorder */ 120 121 /* Primes for cache hash functions. */ 122 #define DD_P1 12582917 123 #define DD_P2 4256249 124 #define DD_P3 741457 125 #define DD_P4 1618033999 126 127 /* Cache tags for 3-operand operators. These tags are stored in the 128 ** least significant bits of the cache operand pointers according to 129 ** the following scheme. The tag consists of two hex digits. Both digits 130 ** must be even, so that they do not interfere with complementation bits. 131 ** The least significant one is stored in Bits 3:1 of the f operand in the 132 ** cache entry. Bit 1 is always 1, so that we can differentiate 133 ** three-operand operations from one- and two-operand operations. 134 ** Therefore, the least significant digit is one of {2,6,a,e}. The most 135 ** significant digit occupies Bits 3:1 of the g operand in the cache 136 ** entry. It can by any even digit between 0 and e. This gives a total 137 ** of 5 bits for the tag proper, which means a maximum of 32 three-operand 138 ** operations. */ 139 #define DD_ADD_ITE_TAG 0x02 140 #define DD_BDD_AND_ABSTRACT_TAG 0x06 141 #define DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a 142 #define DD_BDD_ITE_TAG 0x0e 143 #define DD_ADD_BDD_DO_INTERVAL_TAG 0x22 144 #define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26 145 #define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a 146 #define DD_BDD_COMPOSE_RECUR_TAG 0x2e 147 #define DD_ADD_COMPOSE_RECUR_TAG 0x42 148 #define DD_ADD_NON_SIM_COMPOSE_TAG 0x46 149 #define DD_EQUIV_DC_TAG 0x4a 150 #define DD_ZDD_ITE_TAG 0x4e 151 #define DD_ADD_ITE_CONSTANT_TAG 0x62 152 #define DD_ADD_EVAL_CONST_TAG 0x66 153 #define DD_BDD_ITE_CONSTANT_TAG 0x6a 154 #define DD_ADD_OUT_SUM_TAG 0x6e 155 #define DD_BDD_LEQ_UNLESS_TAG 0x82 156 #define DD_ADD_TRIANGLE_TAG 0x86 157 #define DD_BDD_MAX_EXP_TAG 0x8a 158 #define DD_VARS_SYMM_BEFORE_TAG 0x8e 159 #define DD_VARS_SYMM_BETWEEN_TAG 0xa2 160 161 /* Generator constants. */ 162 #define CUDD_GEN_CUBES 0 163 #define CUDD_GEN_PRIMES 1 164 #define CUDD_GEN_NODES 2 165 #define CUDD_GEN_ZDD_PATHS 3 166 #define CUDD_GEN_EMPTY 0 167 #define CUDD_GEN_NONEMPTY 1 168 169 /** 170 ** @brief Maximum variable index. 171 ** 172 ** @details CUDD_MAXINDEX is defined in such a way that on 32-bit and 173 ** 64-bit machines one can cast an index to (int) without generating 174 ** a negative number. 175 */ 176 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 177 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1) 178 #else 179 #define CUDD_MAXINDEX ((DdHalfWord) ~0) 180 #endif 181 182 /** 183 ** @brief The index of constant nodes. 184 ** 185 ** @details This is a synonim for CUDD_MAXINDEX. 186 */ 187 #define CUDD_CONST_INDEX CUDD_MAXINDEX 188 189 /** 190 ** @brief Size of the random number generator shuffle table. 191 */ 192 #define STAB_SIZE 64 193 194 /** 195 ** @brief Mask for periodic check of termination and timeout. 196 ** 197 ** @see checkWhetherToGiveUp 198 */ 199 #define CUDD_CHECK_MASK 0x7ff 200 201 /*---------------------------------------------------------------------------*/ 202 /* Type declarations */ 203 /*---------------------------------------------------------------------------*/ 204 205 /** 206 @brief Type that is half the size of a pointer. 207 */ 208 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 209 typedef uint32_t DdHalfWord; 210 #else 211 typedef uint16_t DdHalfWord; 212 #endif 213 214 /** 215 * @brief Signed integer that is the size of a pointer. 216 * 217 * @details The only platforms on which CUDD has been tested define 218 * intptr_t and uintptr_t in inttypes.h and satisfy the condition 219 * 220 * sizeof(intptr_t) == sizeof(uintptr_t) == sizeof(void *) 221 * 222 * Neither of these is guaranteed by the C standard. 223 */ 224 typedef intptr_t ptrint; 225 226 /** 227 * @brief Unsigned integer that is the size of a pointer. 228 * 229 * @see ptrint 230 */ 231 typedef uintptr_t ptruint; 232 233 typedef struct DdChildren DdChildren; 234 typedef struct DdHook DdHook; 235 typedef struct DdSubtable DdSubtable; 236 typedef struct DdCache DdCache; 237 typedef struct DdLocalCacheItem DdLocalCacheItem; 238 typedef struct DdLocalCache DdLocalCache; 239 typedef struct DdHashItem DdHashItem; 240 typedef struct DdHashTable DdHashTable; 241 typedef struct Move Move; 242 typedef struct IndexKey IndexKey; 243 typedef struct DdQueueItem DdQueueItem; 244 typedef struct DdLevelQueue DdLevelQueue; 245 246 /*---------------------------------------------------------------------------*/ 247 /* Stucture declarations */ 248 /*---------------------------------------------------------------------------*/ 249 250 /** 251 * @brief The two children of a non-terminal node. 252 */ 253 struct DdChildren { 254 struct DdNode *T; /**< then (true) child */ 255 struct DdNode *E; /**< else (false) child */ 256 }; 257 258 /** 259 * @brief Decision diagram node. 260 */ 261 struct DdNode { 262 DdHalfWord index; /**< variable index */ 263 DdHalfWord ref; /**< reference count */ 264 DdNode *next; /**< next pointer for unique table */ 265 union { 266 CUDD_VALUE_TYPE value; /**< for constant (terminal) nodes */ 267 DdChildren kids; /**< for internal nodes */ 268 } type; /**< terminal or internal */ 269 }; 270 271 /** 272 * @brief CUDD generator. 273 */ 274 struct DdGen { 275 DdManager *manager; 276 int type; 277 int status; 278 union { 279 struct { 280 int *cube; 281 CUDD_VALUE_TYPE value; 282 } cubes; 283 struct { 284 int *cube; 285 DdNode *ub; 286 } primes; 287 struct { 288 int size; 289 } nodes; 290 } gen; 291 struct { 292 int sp; 293 DdNode **stack; 294 } stack; 295 DdNode *node; 296 }; 297 298 /** 299 ** @brief CUDD hook 300 ** 301 ** Hooks in CUDD are functions that the application registers with the 302 ** manager so that they are called at appropriate times. The functions 303 ** are passed the manager as argument; they should return 1 if 304 ** successful and 0 otherwise. 305 */ 306 struct DdHook { 307 DD_HFP f; /**< function to be called */ 308 struct DdHook *next; /**< next element in the list */ 309 }; 310 311 /** 312 * @brief Generic local cache item. 313 */ 314 struct DdLocalCacheItem { 315 DdNode *value; 316 #ifdef DD_CACHE_PROFILE 317 ptrint count; 318 #endif 319 DdNode *key[1]; 320 }; 321 322 /** 323 * @brief Local cache. 324 */ 325 struct DdLocalCache { 326 DdLocalCacheItem *item; 327 unsigned int itemsize; 328 unsigned int keysize; 329 unsigned int slots; 330 int shift; 331 double lookUps; 332 double minHit; 333 double hits; 334 unsigned int maxslots; 335 DdManager *manager; 336 struct DdLocalCache *next; 337 }; 338 339 /** 340 * @brief Local hash table item. 341 */ 342 struct DdHashItem { 343 struct DdHashItem *next; /**< collision list link */ 344 ptrint count; /**< reference count of item */ 345 DdNode *value; /**< value %DD */ 346 DdNode *key[1]; /**< key pointers */ 347 }; 348 349 /** 350 * @brief Local hash table. 351 */ 352 struct DdHashTable { 353 unsigned int keysize; /**< number of pointers in the key */ 354 unsigned int itemsize; /**< size of hash table item in bytes */ 355 DdHashItem **bucket; /**< array of buckets */ 356 DdHashItem *nextFree; /**< item free list */ 357 DdHashItem **memoryList; /**< list of memory blocks for items */ 358 unsigned int numBuckets; /**< number of buckets in array */ 359 int shift; /**< shift used in hash function */ 360 unsigned int size; /**< number of items stored in table */ 361 unsigned int maxsize; /**< threshold for table resizing */ 362 DdManager *manager; /**< %DD manager */ 363 }; 364 365 /** 366 * @brief Computed table. 367 */ 368 struct DdCache { 369 DdNode *f,*g; /**< DDs */ 370 ptruint h; /**< either operator or %DD */ 371 DdNode *data; /**< already constructed %DD */ 372 #ifdef DD_CACHE_PROFILE 373 ptrint count; /**< statistical counter */ 374 #endif 375 }; 376 377 /** 378 * @brief Subtable for one index. 379 */ 380 struct DdSubtable { 381 DdNode **nodelist; /**< hash table */ 382 int shift; /**< shift for hash function */ 383 unsigned int slots; /**< size of the hash table */ 384 unsigned int keys; /**< number of nodes stored in this table */ 385 unsigned int maxKeys; /**< slots * DD_MAX_SUBTABLE_DENSITY */ 386 unsigned int dead; /**< number of dead nodes in this table */ 387 unsigned int next; /**< index of next variable in group */ 388 int bindVar; /**< flag to bind this variable to its level */ 389 /* Fields for lazy sifting. */ 390 Cudd_VariableType varType; /**< variable type (ps, ns, pi) */ 391 int pairIndex; /**< corresponding variable index (ps <-> ns) */ 392 int varHandled; /**< flag: 1 means variable is already handled */ 393 Cudd_LazyGroupType varToBeGrouped; /**< tells what grouping to apply */ 394 }; 395 396 /** 397 * @brief Specialized %DD symbol table. 398 */ 399 struct DdManager { 400 /* Constants */ 401 DdNode sentinel; /**< for collision lists */ 402 DdNode *one; /**< constant 1 */ 403 DdNode *zero; /**< constant 0 */ 404 DdNode *plusinfinity; /**< plus infinity */ 405 DdNode *minusinfinity; /**< minus infinity */ 406 DdNode *background; /**< background value */ 407 /* Computed Table */ 408 DdCache *acache; /**< address of allocated memory for cache */ 409 DdCache *cache; /**< the cache-based computed table */ 410 unsigned int cacheSlots; /**< total number of cache entries */ 411 int cacheShift; /**< shift value for cache hash function */ 412 double cacheMisses; /**< number of cache misses (since resizing) */ 413 double cacheHits; /**< number of cache hits (since resizing) */ 414 double minHit; /**< hit percentage above which to resize */ 415 int cacheSlack; /**< slots still available for resizing */ 416 unsigned int maxCacheHard; /**< hard limit for cache size */ 417 /* Unique Table */ 418 int size; /**< number of unique subtables */ 419 int sizeZ; /**< for %ZDD */ 420 int maxSize; /**< max number of subtables before resizing */ 421 int maxSizeZ; /**< for %ZDD */ 422 DdSubtable *subtables; /**< array of unique subtables */ 423 DdSubtable *subtableZ; /**< for %ZDD */ 424 DdSubtable constants; /**< unique subtable for the constants */ 425 unsigned int slots; /**< total number of hash buckets */ 426 unsigned int keys; /**< total number of %BDD and %ADD nodes */ 427 unsigned int keysZ; /**< total number of %ZDD nodes */ 428 unsigned int dead; /**< total number of dead %BDD and %ADD nodes */ 429 unsigned int deadZ; /**< total number of dead %ZDD nodes */ 430 unsigned int maxLive; /**< maximum number of live nodes */ 431 unsigned int minDead; /**< do not GC if fewer than these dead */ 432 int gcEnabled; /**< gc is enabled */ 433 double gcFrac; /**< gc when this fraction is dead */ 434 unsigned int looseUpTo; /**< slow growth beyond this limit */ 435 /**< (measured w.r.t. slots, not keys) */ 436 unsigned int initSlots; /**< initial size of a subtable */ 437 DdNode **stack; /**< stack for iterative procedures */ 438 double allocated; /**< number of nodes allocated */ 439 /**< (not during reordering) */ 440 double reclaimed; /**< number of nodes brought back from the dead */ 441 int *perm; /**< current variable perm. (index to level) */ 442 int *permZ; /**< for %ZDD */ 443 int *invperm; /**< current inv. var. perm. (level to index) */ 444 int *invpermZ; /**< for %ZDD */ 445 DdNode **vars; /**< projection functions */ 446 int *map; /**< variable map for fast swap */ 447 DdNode **univ; /**< %ZDD 1 for each variable */ 448 unsigned int isolated; /**< isolated projection functions */ 449 unsigned int originalSize; /**< used by lazy sifting */ 450 int linearSize; /**< number of rows and columns of linear */ 451 ptruint *interact; /**< interacting variable matrix */ 452 ptruint *linear; /**< linear transform matrix */ 453 /* Memory Management */ 454 DdNode **memoryList; /**< memory manager for symbol table */ 455 DdNode *nextFree; /**< list of free nodes */ 456 char *stash; /**< memory reserve */ 457 #ifndef DD_NO_DEATH_ROW 458 DdNode **deathRow; /**< queue for dereferencing */ 459 int deathRowDepth; /**< number of slots in the queue */ 460 int nextDead; /**< index in the queue */ 461 unsigned deadMask; /**< mask for circular index update */ 462 #endif 463 /* General Parameters */ 464 CUDD_VALUE_TYPE epsilon; /**< tolerance on comparisons */ 465 /* Dynamic Reordering Parameters */ 466 int reordered; /**< flag set at the end of reordering */ 467 unsigned int reorderings; /**< number of calls to Cudd_ReduceHeap */ 468 unsigned int maxReorderings;/**< maximum number of calls to Cudd_ReduceHeap */ 469 int siftMaxVar; /**< maximum number of vars sifted */ 470 int siftMaxSwap; /**< maximum number of swaps per sifting */ 471 int ddTotalNumberSwapping; /**< number of %BDD/%ADD swaps completed */ 472 int zddTotalNumberSwapping; /**< number of %ZDD swaps completed */ 473 int reordCycle; /**< how often to apply alternate threshold */ 474 double maxGrowth; /**< maximum growth during reordering */ 475 double maxGrowthAlt; /**< alternate maximum growth for reordering */ 476 int autoDyn; /**< automatic dynamic reordering flag (BDD) */ 477 int autoDynZ; /**< automatic dynamic reordering flag (ZDD) */ 478 Cudd_ReorderingType autoMethod; /**< default reordering method */ 479 Cudd_ReorderingType autoMethodZ; /**< default reordering method (ZDD) */ 480 int realign; /**< realign %ZDD order after %BDD reordering */ 481 int realignZ; /**< realign %BDD order after %ZDD reordering */ 482 unsigned int nextDyn; /**< reorder if this size is reached */ 483 unsigned int countDead; /**< if 0, count deads to trigger reordering */ 484 MtrNode *tree; /**< variable group tree (BDD) */ 485 MtrNode *treeZ; /**< variable group tree (ZDD) */ 486 Cudd_AggregationType groupcheck; /**< used during group sifting */ 487 int recomb; /**< used during group sifting */ 488 int symmviolation; /**< used during group sifting */ 489 int arcviolation; /**< used during group sifting */ 490 int populationSize; /**< population size for GA */ 491 int numberXovers; /**< number of crossovers for GA */ 492 unsigned int randomizeOrder; /**< perturb the next reordering threshold */ 493 DdLocalCache *localCaches; /**< local caches currently in existence */ 494 void *hooks; /**< application-specific field (used by vis) */ 495 DdHook *preGCHook; /**< hooks to be called before GC */ 496 DdHook *postGCHook; /**< hooks to be called after GC */ 497 DdHook *preReorderingHook; /**< hooks to be called before reordering */ 498 DdHook *postReorderingHook; /**< hooks to be called after reordering */ 499 FILE *out; /**< stdout for this manager */ 500 FILE *err; /**< stderr for this manager */ 501 Cudd_ErrorType errorCode; /**< info on last error */ 502 unsigned long startTime; /**< start time in milliseconds */ 503 unsigned long timeLimit; /**< CPU time limit */ 504 DD_THFP terminationCallback; /**< termination callback */ 505 void * tcbArg; /**< second argument passed to termination handler */ 506 DD_OOMFP outOfMemCallback; /**< out-of-memory callback */ 507 DD_TOHFP timeoutHandler; /**< timeout handler */ 508 void * tohArg; /**< second argument passed to timeout handler */ 509 /* Statistical counters. */ 510 size_t memused; /**< total memory allocated for the manager */ 511 size_t maxmem; /**< target maximum memory */ 512 size_t maxmemhard; /**< hard limit for maximum memory */ 513 int garbageCollections; /**< number of garbage collections */ 514 unsigned long GCTime; /**< total time spent in garbage collection */ 515 unsigned long reordTime; /**< total time spent in reordering */ 516 double totCachehits; /**< total number of cache hits */ 517 double totCacheMisses; /**< total number of cache misses */ 518 double cachecollisions; /**< number of cache collisions */ 519 double cacheinserts; /**< number of cache insertions */ 520 double cacheLastInserts; /**< insertions at the last cache resizing */ 521 double cachedeletions; /**< number of deletions during garbage coll. */ 522 unsigned int peakLiveNodes; /**< maximum number of live nodes */ 523 /* Random number generator. */ 524 int32_t cuddRand; /**< state of the random number generator */ 525 int32_t cuddRand2; /**< state of the random number generator */ 526 int32_t shuffleSelect; /**< state of the random number generator */ 527 int32_t shuffleTable[STAB_SIZE]; /**< state of the random number generator */ 528 #ifdef DD_STATS 529 double nodesFreed; /**< number of nodes returned to the free list */ 530 double nodesDropped; /**< number of nodes killed by dereferencing */ 531 int totalNISwaps; /**< number of non-interacting (cheap) swaps */ 532 int extsymmcalls; /**< number of calls to symmetry check fn */ 533 int extsymm; /**< number of successful symmetry checks */ 534 int secdiffcalls; /**< number of calls to second difference fn */ 535 int secdiff; /**< number of successful second diff. checks */ 536 int secdiffmisfire; /**< number of misfired second diff. checks */ 537 int tosses; /**< number of coin tosses in annealing */ 538 int acceptances; /**< number of acceptances in annealing */ 539 int totalShuffles; /**< number of shuffles in exact reordering */ 540 int totalNumberLinearTr; /**< number of linear transformations */ 541 int num_calls; /**< should equal 2n-1 (n is the # of nodes) */ 542 #endif 543 #ifdef DD_UNIQUE_PROFILE 544 double uniqueLookUps; /**< number of unique table lookups */ 545 double uniqueLinks; /**< total distance traveled in coll. chains */ 546 #endif 547 #ifdef DD_COUNT 548 double recursiveCalls; /**< number of recursive calls */ 549 #ifdef DD_STATS 550 double nextSample; /**< when to write next line of stats */ 551 #endif 552 double swapSteps; /**< number of elementary reordering steps */ 553 #endif 554 #ifdef DD_DEBUG 555 int addPermuteRecurHits; /**< debug variable for variable permutation */ 556 int bddPermuteRecurHits; /**< debug variable for variable permutation */ 557 int bddVectorComposeHits; /**< debug variable for vector composition */ 558 int addVectorComposeHits; /**< debug variable for vector composition */ 559 int addGeneralVectorComposeHits; /**< debug var. for vector composition */ 560 int enableExtraDebug; /**< deposit a 1 here to enable more debugging */ 561 #endif 562 }; 563 564 /** 565 * @brief Reordering move record. 566 */ 567 struct Move { 568 DdHalfWord x; 569 DdHalfWord y; 570 unsigned int flags; 571 int size; 572 struct Move *next; 573 }; 574 575 /** 576 * @brief Used to sort variables for reordering. 577 */ 578 struct IndexKey { 579 int index; 580 int keys; 581 }; 582 583 /** 584 * @brief Generic level queue item. 585 */ 586 struct DdQueueItem { 587 struct DdQueueItem *next; 588 struct DdQueueItem *cnext; 589 void *key; 590 }; 591 592 /** 593 * @brief Level queue. 594 */ 595 struct DdLevelQueue { 596 void *first; 597 DdQueueItem **last; 598 DdQueueItem *freelist; 599 DdQueueItem **buckets; 600 int levels; 601 int itemsize; 602 int size; 603 int maxsize; 604 int numBuckets; 605 int shift; 606 DdManager *manager; 607 }; 608 609 /*---------------------------------------------------------------------------*/ 610 /* Variable declarations */ 611 /*---------------------------------------------------------------------------*/ 612 613 614 /*---------------------------------------------------------------------------*/ 615 /* Macro declarations */ 616 /*---------------------------------------------------------------------------*/ 617 618 /** 619 @brief Adds node to the head of the free list. 620 621 @details Does not deallocate memory chunks that become free. This 622 function is also used by the dynamic reordering functions. 623 624 @sideeffect None 625 626 @see cuddAllocNode cuddDynamicAllocNode cuddDeallocMove 627 628 */ 629 #define cuddDeallocNode(unique,node) \ 630 (node)->next = (unique)->nextFree; \ 631 (unique)->nextFree = node; 632 633 /** 634 @brief Adds node to the head of the free list. 635 636 @details Does not deallocate memory chunks that become free. This 637 function is also used by the dynamic reordering functions. 638 639 @sideeffect None 640 641 @see cuddDeallocNode cuddDynamicAllocNode 642 643 */ 644 #define cuddDeallocMove(unique,node) \ 645 ((DdNode *)(node))->ref = 0; \ 646 ((DdNode *)(node))->next = (unique)->nextFree; \ 647 (unique)->nextFree = (DdNode *)(node); 648 649 650 /** 651 @brief Increases the reference count of a node, if it is not 652 saturated. 653 654 @details This being a macro, it is faster than Cudd_Ref, but it 655 cannot be used in constructs like cuddRef(a = b()). 656 657 @sideeffect none 658 659 @see Cudd_Ref 660 661 */ 662 #define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref) 663 664 665 /** 666 @brief Decreases the reference count of a node, if it is not 667 saturated. 668 669 @details It is primarily used in recursive procedures to decrease 670 the ref count of a result node before returning it. This 671 accomplishes the goal of removing the protection applied by a 672 previous cuddRef. This being a macro, it is faster than Cudd_Deref, 673 but it cannot be used in constructs like cuddDeref(a = b()). 674 675 @sideeffect none 676 677 @see Cudd_Deref 678 679 */ 680 #define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref) 681 682 683 /** 684 @brief Returns 1 if the node is a constant node. 685 686 @details Returns 1 if the node is a constant node (rather than an 687 internal node). All constant nodes have the same index 688 (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstantInt may be either 689 regular or complemented. 690 691 @sideeffect none 692 693 @see cuddIsConstant Cudd_IsConstant 694 695 */ 696 #define Cudd_IsConstantInt(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX) 697 698 699 /** 700 @brief Returns 1 if the node is a constant node. 701 702 @details Returns 1 if the node is a constant node (rather than an 703 internal node). All constant nodes have the same index 704 (CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular. 705 706 @sideeffect none 707 708 @see Cudd_IsConstant Cudd_IsConstantInt 709 710 */ 711 #define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX) 712 713 714 /** 715 @brief Returns the then child of an internal node. 716 717 @details If <code>node</code> is a constant node, the result is 718 unpredictable. The pointer passed to cuddT must be regular. 719 720 @sideeffect none 721 722 @see Cudd_T 723 724 */ 725 #define cuddT(node) ((node)->type.kids.T) 726 727 728 /** 729 @brief Returns the else child of an internal node. 730 731 @details If <code>node</code> is a constant node, the result is 732 unpredictable. The pointer passed to cuddE must be regular. 733 734 @sideeffect none 735 736 @see Cudd_E 737 738 */ 739 #define cuddE(node) ((node)->type.kids.E) 740 741 742 /** 743 @brief Returns the value of a constant node. 744 745 @details If <code>node</code> is an internal node, the result is 746 unpredictable. The pointer passed to cuddV must be regular. 747 748 @sideeffect none 749 750 @see Cudd_V 751 752 */ 753 #define cuddV(node) ((node)->type.value) 754 755 756 /** 757 @brief Finds the current position of variable index in the 758 order. 759 760 @details This macro duplicates the functionality of Cudd_ReadPerm, 761 but it does not check for out-of-bounds indices and it is more 762 efficient. 763 764 @sideeffect none 765 766 @see Cudd_ReadPerm 767 768 */ 769 #define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)]) 770 771 772 /** 773 @brief Finds the current position of %ZDD variable index in the 774 order. 775 776 @details This macro duplicates the functionality of 777 Cudd_ReadPermZdd, but it does not check for out-of-bounds indices 778 and it is more efficient. 779 780 @sideeffect none 781 782 @see Cudd_ReadPermZdd 783 784 */ 785 #define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)]) 786 787 788 /** 789 @brief Hash function for the unique table. 790 791 @details 792 793 @sideeffect none 794 795 @see ddCHash ddCHash2 796 797 */ 798 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 799 #define ddHash(f,g,s) \ 800 ((((unsigned)(ptruint)(f) * DD_P1 + \ 801 (unsigned)(ptruint)(g)) * DD_P2) >> (s)) 802 #else 803 #define ddHash(f,g,s) \ 804 ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) 805 #endif 806 807 808 /** 809 @brief Hash function for the cache. 810 811 @sideeffect none 812 813 @see ddHash ddCHash2 814 815 */ 816 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 817 #define ddCHash(o,f,g,h,s) \ 818 ((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ 819 (unsigned)(ptruint)(g)) * DD_P2 + \ 820 (unsigned)(ptruint)(h)) * DD_P3) >> (s)) 821 #else 822 #define ddCHash(o,f,g,h,s) \ 823 ((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \ 824 (unsigned)(h)) * DD_P3) >> (s)) 825 #endif 826 827 828 /** 829 @brief Hash function for the cache for functions with two operands. 830 831 @sideeffect none 832 833 @see ddHash ddCHash 834 835 */ 836 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 837 #define ddCHash2(o,f,g,s) \ 838 (((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \ 839 (unsigned)(ptruint)(g)) * DD_P2) >> (s)) 840 #else 841 #define ddCHash2(o,f,g,s) \ 842 (((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) 843 #endif 844 845 846 /** 847 @brief Clears the 4 least significant bits of a pointer. 848 849 @sideeffect none 850 851 */ 852 #define cuddClean(p) ((DdNode *)((ptruint)(p) & ~ (ptruint) 0xf)) 853 854 855 /** 856 @brief Computes the minimum of two numbers. 857 858 @sideeffect none 859 860 @see ddMax 861 862 */ 863 #define ddMin(x,y) (((y) < (x)) ? (y) : (x)) 864 865 866 /** 867 @brief Computes the maximum of two numbers. 868 869 @sideeffect none 870 871 @see ddMin 872 873 */ 874 #define ddMax(x,y) (((y) > (x)) ? (y) : (x)) 875 876 877 /** 878 @brief Computes the absolute value of a number. 879 880 @sideeffect none 881 882 */ 883 #define ddAbs(x) (((x)<0) ? -(x) : (x)) 884 885 886 /** 887 @brief Returns 1 if the absolute value of the difference of the two 888 arguments x and y is less than e. 889 890 @sideeffect none 891 892 */ 893 #define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e)) 894 895 896 /** 897 @brief Saturating increment operator. 898 899 @details Saturation is only necessary on 32-bit machines, where the 900 reference count is only 16-bit wide. 901 902 @sideeffect none 903 904 @see cuddSatDec 905 906 */ 907 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 908 #define cuddSatInc(x) ((x)++) 909 #else 910 #define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF) 911 #endif 912 913 914 /** 915 @brief Saturating decrement operator. 916 917 @details Saturation is only necessary on 32-bit machines, where the 918 reference count is only 16-bit wide. 919 920 @sideeffect none 921 922 @see cuddSatInc 923 924 */ 925 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 926 #define cuddSatDec(x) ((x)--) 927 #else 928 #define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF) 929 #endif 930 931 932 /** 933 @brief Returns the constant 1 node. 934 935 @sideeffect none 936 937 @see DD_ZERO DD_PLUS_INFINITY DD_MINUS_INFINITY 938 939 */ 940 #define DD_ONE(dd) ((dd)->one) 941 942 943 /** 944 @brief Returns the arithmetic 0 constant node. 945 946 @details This is different from the logical zero. The latter is 947 obtained by Cudd_Not(DD_ONE(dd)). 948 949 @sideeffect none 950 951 @see DD_ONE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY 952 953 */ 954 #define DD_ZERO(dd) ((dd)->zero) 955 956 957 /** 958 @brief Returns the plus infinity constant node. 959 960 @sideeffect none 961 962 @see DD_ONE DD_ZERO DD_MINUS_INFINITY 963 964 */ 965 #define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity) 966 967 968 /** 969 @brief Returns the minus infinity constant node. 970 971 @sideeffect none 972 973 @see DD_ONE DD_ZERO DD_PLUS_INFINITY 974 975 */ 976 #define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity) 977 978 979 /** 980 @brief Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL. 981 982 @details Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to 983 DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to 984 DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if 985 HAVE_IEEE_754 is not defined, it makes sure that a value does not 986 get larger than infinity in absolute value, and once it gets to 987 infinity, stays there. If the value overflows before this macro is 988 applied, no recovery is possible. 989 990 @sideeffect none 991 992 */ 993 #ifdef HAVE_IEEE_754 994 #define cuddAdjust(x) 995 #else 996 #define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x))) 997 #endif 998 999 1000 /** 1001 @brief Outputs a line of stats. 1002 1003 @details Outputs a line of stats if DD_COUNT and DD_STATS are 1004 defined. Increments the number of recursive calls if DD_COUNT is 1005 defined. 1006 1007 @sideeffect None 1008 1009 */ 1010 #ifdef DD_COUNT 1011 #ifdef DD_STATS 1012 #define statLine(dd) \ 1013 do { \ 1014 (dd)->recursiveCalls++; \ 1015 if ((dd)->recursiveCalls == (dd)->nextSample) { \ 1016 (void) fprintf((dd)->err, \ 1017 "@%.0f: %u nodes %u live %.0f dropped" \ 1018 " %.0f reclaimed\n", \ 1019 (dd)->recursiveCalls, (dd)->keys, \ 1020 (dd)->keys - (dd)->dead, \ 1021 (dd)->nodesDropped, (dd)->reclaimed); \ 1022 (dd)->nextSample += 250000;} \ 1023 } while (0) 1024 #else 1025 #define statLine(dd) (dd)->recursiveCalls++ 1026 #endif 1027 #else 1028 #define statLine(dd) 1029 #endif 1030 1031 1032 /** 1033 @brief Checks for termination or timeout. 1034 */ 1035 #define checkWhetherToGiveUp(dd) \ 1036 do { \ 1037 if (((int64_t) CUDD_CHECK_MASK & (int64_t) (dd)->cacheMisses) == 0) { \ 1038 if ((dd)->terminationCallback != NULL && \ 1039 (dd)->terminationCallback((dd)->tcbArg)) { \ 1040 (dd)->errorCode = CUDD_TERMINATION; \ 1041 return(NULL); \ 1042 } \ 1043 if (util_cpu_time() - (dd)->startTime > (dd)->timeLimit) { \ 1044 (dd)->errorCode = CUDD_TIMEOUT_EXPIRED; \ 1045 return(NULL); \ 1046 } \ 1047 } \ 1048 } while (0) 1049 1050 1051 /** \cond */ 1052 1053 /*---------------------------------------------------------------------------*/ 1054 /* Function prototypes */ 1055 /*---------------------------------------------------------------------------*/ 1056 1057 #ifdef __cplusplus 1058 extern "C" { 1059 #endif 1060 1061 extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); 1062 extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); 1063 extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); 1064 extern DdNode * cuddAddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g); 1065 extern DdNode * cuddAddMonadicApplyRecur(DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f); 1066 extern DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon); 1067 extern DdNode * cuddAddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h); 1068 extern DdNode * cuddAddCmplRecur(DdManager *dd, DdNode *f); 1069 extern DdNode * cuddAddNegateRecur(DdManager *dd, DdNode *f); 1070 extern DdNode * cuddAddRoundOffRecur(DdManager *dd, DdNode *f, double trunc); 1071 extern DdNode * cuddUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality); 1072 extern DdNode * cuddRemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality); 1073 extern DdNode * cuddBiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0); 1074 extern DdNode * cuddBddAndAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube); 1075 extern int cuddAnnealing(DdManager *table, int lower, int upper); 1076 extern DdNode * cuddBddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube); 1077 extern DdNode * cuddBddXorExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube); 1078 extern DdNode * cuddBddBooleanDiffRecur(DdManager *manager, DdNode *f, DdNode *var); 1079 extern DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h); 1080 extern DdNode * cuddBddIntersectRecur(DdManager *dd, DdNode *f, DdNode *g); 1081 extern DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g); 1082 extern DdNode * cuddBddXorRecur(DdManager *manager, DdNode *f, DdNode *g); 1083 extern DdNode * cuddBddTransfer(DdManager *ddS, DdManager *ddD, DdNode *f); 1084 extern DdNode * cuddAddBddDoPattern(DdManager *dd, DdNode *f); 1085 extern int cuddInitCache(DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize); 1086 extern void cuddCacheInsert(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data); 1087 extern void cuddCacheInsert2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data); 1088 extern void cuddCacheInsert1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data); 1089 extern DdNode * cuddCacheLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h); 1090 extern DdNode * cuddCacheLookupZdd(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h); 1091 extern DdNode * cuddCacheLookup2(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g); 1092 extern DdNode * cuddCacheLookup1(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f); 1093 extern DdNode * cuddCacheLookup2Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g); 1094 extern DdNode * cuddCacheLookup1Zdd(DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f); 1095 extern DdNode * cuddConstantLookup(DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h); 1096 extern int cuddCacheProfile(DdManager *table, FILE *fp); 1097 extern void cuddCacheResize(DdManager *table); 1098 extern void cuddCacheFlush(DdManager *table); 1099 extern int cuddComputeFloorLog2(unsigned int value); 1100 extern int cuddHeapProfile(DdManager *dd); 1101 extern void cuddPrintNode(DdNode *f, FILE *fp); 1102 extern void cuddPrintVarGroups(DdManager * dd, MtrNode * root, int zdd, int silent); 1103 extern DdNode * cuddBddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction); 1104 extern DdNode * cuddBddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction); 1105 extern void cuddGetBranches(DdNode *g, DdNode **g1, DdNode **g0); 1106 extern DdNode * cuddCofactorRecur(DdManager *dd, DdNode *f, DdNode *g); 1107 extern DdNode * cuddBddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj); 1108 extern DdNode * cuddAddComposeRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *proj); 1109 extern int cuddExact(DdManager *table, int lower, int upper); 1110 extern DdNode * cuddBddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c); 1111 extern DdNode * cuddBddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c); 1112 extern DdNode * cuddBddNPAndRecur(DdManager *dd, DdNode *f, DdNode *c); 1113 extern DdNode * cuddAddConstrainRecur(DdManager *dd, DdNode *f, DdNode *c); 1114 extern DdNode * cuddAddRestrictRecur(DdManager *dd, DdNode *f, DdNode *c); 1115 extern DdNode * cuddBddLICompaction(DdManager *dd, DdNode *f, DdNode *c); 1116 extern int cuddGa(DdManager *table, int lower, int upper); 1117 extern int cuddTreeSifting(DdManager *table, Cudd_ReorderingType method); 1118 extern int cuddZddInitUniv(DdManager *zdd); 1119 extern void cuddZddFreeUniv(DdManager *zdd); 1120 extern void cuddSetInteract(DdManager *table, int x, int y); 1121 extern int cuddTestInteract(DdManager *table, int x, int y); 1122 extern int cuddInitInteract(DdManager *table); 1123 extern DdLocalCache * cuddLocalCacheInit(DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize); 1124 extern void cuddLocalCacheQuit(DdLocalCache *cache); 1125 extern void cuddLocalCacheInsert(DdLocalCache *cache, DdNodePtr *key, DdNode *value); 1126 extern DdNode * cuddLocalCacheLookup(DdLocalCache *cache, DdNodePtr *key); 1127 extern void cuddLocalCacheClearDead(DdManager *manager); 1128 extern int cuddIsInDeathRow(DdManager *dd, DdNode *f); 1129 extern int cuddTimesInDeathRow(DdManager *dd, DdNode *f); 1130 extern void cuddLocalCacheClearAll(DdManager *manager); 1131 #ifdef DD_CACHE_PROFILE 1132 extern int cuddLocalCacheProfile(DdLocalCache *cache); 1133 #endif 1134 extern DdHashTable * cuddHashTableInit(DdManager *manager, unsigned int keySize, unsigned int initSize); 1135 extern void cuddHashTableQuit(DdHashTable *hash); 1136 extern void cuddHashTableGenericQuit(DdHashTable *hash); 1137 extern int cuddHashTableInsert(DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count); 1138 extern DdNode * cuddHashTableLookup(DdHashTable *hash, DdNodePtr *key); 1139 extern int cuddHashTableInsert1(DdHashTable *hash, DdNode *f, DdNode *value, ptrint count); 1140 extern DdNode * cuddHashTableLookup1(DdHashTable *hash, DdNode *f); 1141 extern int cuddHashTableInsert2(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count); 1142 extern DdNode * cuddHashTableLookup2(DdHashTable *hash, DdNode *f, DdNode *g); 1143 extern int cuddHashTableInsert3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count); 1144 extern DdNode * cuddHashTableLookup3(DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h); 1145 extern int cuddHashTableGenericInsert(DdHashTable * hash, DdNode * f, void * value); 1146 extern void * cuddHashTableGenericLookup(DdHashTable * hash, DdNode * f); 1147 extern DdLevelQueue * cuddLevelQueueInit(int levels, int itemSize, int numBuckets, DdManager * manager); 1148 extern void cuddLevelQueueQuit(DdLevelQueue *queue); 1149 extern void * cuddLevelQueueFirst(DdLevelQueue * queue, void * key, int level); 1150 extern void * cuddLevelQueueEnqueue(DdLevelQueue *queue, void *key, int level); 1151 extern void cuddLevelQueueDequeue(DdLevelQueue *queue, int level); 1152 extern int cuddLinearAndSifting(DdManager *table, int lower, int upper); 1153 extern int cuddLinearInPlace(DdManager * table, int x, int y); 1154 extern void cuddUpdateInteractionMatrix(DdManager * table, int xindex, int yindex); 1155 extern int cuddInitLinear(DdManager *table); 1156 extern int cuddResizeLinear(DdManager *table); 1157 extern DdNode * cuddBddLiteralSetIntersectionRecur(DdManager *dd, DdNode *f, DdNode *g); 1158 extern DdNode * cuddCProjectionRecur(DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp); 1159 extern DdNode * cuddBddClosestCube(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound); 1160 extern void cuddReclaim(DdManager *table, DdNode *n); 1161 extern void cuddReclaimZdd(DdManager *table, DdNode *n); 1162 extern void cuddClearDeathRow(DdManager *table); 1163 extern void cuddShrinkDeathRow(DdManager *table); 1164 extern DdNode * cuddDynamicAllocNode(DdManager *table); 1165 extern int cuddSifting(DdManager *table, int lower, int upper); 1166 extern int cuddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic); 1167 extern int cuddNextHigh(DdManager *table, int x); 1168 extern int cuddNextLow(DdManager *table, int x); 1169 extern int cuddSwapInPlace(DdManager *table, int x, int y); 1170 extern int cuddBddAlignToZdd(DdManager *table); 1171 extern DdNode * cuddBddMakePrime(DdManager *dd, DdNode *cube, DdNode *f); 1172 extern DdNode * cuddSolveEqnRecur(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i); 1173 extern DdNode * cuddVerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n); 1174 #ifdef ST_H_ 1175 extern DdNode* cuddSplitSetRecur(DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index); 1176 #endif 1177 extern DdNode * cuddSubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold); 1178 extern DdNode * cuddSubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit); 1179 extern int cuddSymmCheck(DdManager *table, int x, int y); 1180 extern int cuddSymmSifting(DdManager *table, int lower, int upper); 1181 extern int cuddSymmSiftingConv(DdManager *table, int lower, int upper); 1182 extern DdNode * cuddAllocNode(DdManager *unique); 1183 extern DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo); 1184 extern void cuddFreeTable(DdManager *unique); 1185 extern int cuddGarbageCollect(DdManager *unique, int clearCache); 1186 extern DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E); 1187 extern DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h); 1188 extern DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E); 1189 extern DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E); 1190 extern DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E); 1191 extern DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value); 1192 extern void cuddRehash(DdManager *unique, int i); 1193 extern void cuddShrinkSubtable(DdManager *unique, int i); 1194 extern int cuddInsertSubtables(DdManager *unique, int n, int level); 1195 extern int cuddDestroySubtables(DdManager *unique, int n); 1196 extern int cuddResizeTableZdd(DdManager *unique, int index); 1197 extern void cuddSlowTableGrowth(DdManager *unique); 1198 extern int cuddP(DdManager *dd, DdNode *f); 1199 #ifdef ST_H_ 1200 extern enum st_retval cuddStCountfree(void *key, void *value, void *arg); 1201 extern int cuddCollectNodes(DdNode *f, st_table *visited); 1202 #endif 1203 extern DdNodePtr * cuddNodeArray(DdNode *f, int *n); 1204 extern int cuddWindowReorder(DdManager *table, int low, int high, Cudd_ReorderingType submethod); 1205 extern DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g); 1206 extern DdNode * cuddZddUnateProduct(DdManager *dd, DdNode *f, DdNode *g); 1207 extern DdNode * cuddZddWeakDiv(DdManager *dd, DdNode *f, DdNode *g); 1208 extern DdNode * cuddZddWeakDivF(DdManager *dd, DdNode *f, DdNode *g); 1209 extern DdNode * cuddZddDivide(DdManager *dd, DdNode *f, DdNode *g); 1210 extern DdNode * cuddZddDivideF(DdManager *dd, DdNode *f, DdNode *g); 1211 extern int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd); 1212 extern int cuddZddGetCofactors2(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0); 1213 extern DdNode * cuddZddComplement(DdManager *dd, DdNode *node); 1214 extern int cuddZddGetPosVarIndex(DdManager * dd, int index); 1215 extern int cuddZddGetNegVarIndex(DdManager * dd, int index); 1216 extern int cuddZddGetPosVarLevel(DdManager * dd, int index); 1217 extern int cuddZddGetNegVarLevel(DdManager * dd, int index); 1218 extern int cuddZddTreeSifting(DdManager *table, Cudd_ReorderingType method); 1219 extern DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I); 1220 extern DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U); 1221 extern DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node); 1222 extern int cuddZddLinearSifting(DdManager *table, int lower, int upper); 1223 extern int cuddZddAlignToBdd(DdManager *table); 1224 extern int cuddZddNextHigh(DdManager *table, int x); 1225 extern int cuddZddNextLow(DdManager *table, int x); 1226 extern int cuddZddUniqueCompare(void const *ptr_x, void const *ptr_y); 1227 extern int cuddZddSwapInPlace(DdManager *table, int x, int y); 1228 extern int cuddZddSwapping(DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic); 1229 extern int cuddZddSifting(DdManager *table, int lower, int upper); 1230 extern DdNode * cuddZddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h); 1231 extern DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q); 1232 extern DdNode * cuddZddIntersect(DdManager *zdd, DdNode *P, DdNode *Q); 1233 extern DdNode * cuddZddDiff(DdManager *zdd, DdNode *P, DdNode *Q); 1234 extern DdNode * cuddZddChangeAux(DdManager *zdd, DdNode *P, DdNode *zvar); 1235 extern DdNode * cuddZddSubset1(DdManager *dd, DdNode *P, int var); 1236 extern DdNode * cuddZddSubset0(DdManager *dd, DdNode *P, int var); 1237 extern DdNode * cuddZddChange(DdManager *dd, DdNode *P, int var); 1238 extern int cuddZddSymmCheck(DdManager *table, int x, int y); 1239 extern int cuddZddSymmSifting(DdManager *table, int lower, int upper); 1240 extern int cuddZddSymmSiftingConv(DdManager *table, int lower, int upper); 1241 extern int cuddZddP(DdManager *zdd, DdNode *f); 1242 1243 #ifdef __cplusplus 1244 } /* end of extern "C" */ 1245 #endif 1246 1247 /** \endcond */ 1248 1249 #endif /* CUDD_INT_H_ */ 1250