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