1 /**CHeaderFile***************************************************************** 2 3 FileName [cudd.h] 4 5 PackageName [cudd] 6 7 Synopsis [The University of Colorado decision diagram package.] 8 9 Description [External functions and data strucures of the CUDD package. 10 <ul> 11 <li> To turn on the gathering of statistics, define DD_STATS. 12 <li> To link with mis, define DD_MIS. 13 </ul> 14 Modified by Abelardo Pardo to interface it to VIS. 15 ] 16 17 SeeAlso [] 18 19 Author [Fabio Somenzi] 20 21 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado 22 23 All rights reserved. 24 25 Redistribution and use in source and binary forms, with or without 26 modification, are permitted provided that the following conditions 27 are met: 28 29 Redistributions of source code must retain the above copyright 30 notice, this list of conditions and the following disclaimer. 31 32 Redistributions in binary form must reproduce the above copyright 33 notice, this list of conditions and the following disclaimer in the 34 documentation and/or other materials provided with the distribution. 35 36 Neither the name of the University of Colorado nor the names of its 37 contributors may be used to endorse or promote products derived from 38 this software without specific prior written permission. 39 40 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 41 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 42 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 43 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 44 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 45 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 46 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 47 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 48 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 49 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 50 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 51 POSSIBILITY OF SUCH DAMAGE.] 52 53 Revision [$Id: cudd.h,v 1.174 2009/02/21 05:55:18 fabio Exp $] 54 55 ******************************************************************************/ 56 57 #ifndef ABC__bdd__cudd__cudd_h 58 #define ABC__bdd__cudd__cudd_h 59 60 61 /*---------------------------------------------------------------------------*/ 62 /* Nested includes */ 63 /*---------------------------------------------------------------------------*/ 64 65 #include "bdd/mtr/mtr.h" 66 #include "bdd/epd/epd.h" 67 68 ABC_NAMESPACE_HEADER_START 69 70 71 /*---------------------------------------------------------------------------*/ 72 /* Constant declarations */ 73 /*---------------------------------------------------------------------------*/ 74 75 #define CUDD_VERSION "2.4.2" 76 77 #ifndef SIZEOF_VOID_P 78 #define SIZEOF_VOID_P 4 79 #endif 80 #ifndef SIZEOF_INT 81 #define SIZEOF_INT 4 82 #endif 83 #ifndef SIZEOF_LONG 84 #define SIZEOF_LONG 4 85 #endif 86 87 #ifndef TRUE 88 #define TRUE 1 89 #endif 90 #ifndef FALSE 91 #define FALSE 0 92 #endif 93 94 #define CUDD_VALUE_TYPE double 95 #define CUDD_OUT_OF_MEM -1 96 /* The sizes of the subtables and the cache must be powers of two. */ 97 #define CUDD_UNIQUE_SLOTS 256 /* initial size of subtables */ 98 #define CUDD_CACHE_SLOTS 262144 /* default size of the cache */ 99 100 /* Constants for residue functions. */ 101 #define CUDD_RESIDUE_DEFAULT 0 102 #define CUDD_RESIDUE_MSB 1 103 #define CUDD_RESIDUE_TC 2 104 105 /* CUDD_MAXINDEX is defined in such a way that on 32-bit and 64-bit 106 ** machines one can cast an index to (int) without generating a negative 107 ** number. 108 */ 109 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 110 #define CUDD_MAXINDEX (((DdHalfWord) ~0) >> 1) 111 #else 112 #define CUDD_MAXINDEX ((DdHalfWord) ~0) 113 #endif 114 115 /* CUDD_CONST_INDEX is the index of constant nodes. Currently this 116 ** is a synonim for CUDD_MAXINDEX. */ 117 #define CUDD_CONST_INDEX CUDD_MAXINDEX 118 119 /* These constants define the digits used in the representation of 120 ** arbitrary precision integers. The configurations tested use 8, 16, 121 ** and 32 bits for each digit. The typedefs should be in agreement 122 ** with these definitions. 123 */ 124 #if SIZEOF_LONG == 8 125 #define DD_APA_BITS 32 126 #define DD_APA_BASE (1L << DD_APA_BITS) 127 #define DD_APA_HEXPRINT "%08x" 128 #else 129 #define DD_APA_BITS 16 130 #define DD_APA_BASE (1 << DD_APA_BITS) 131 #define DD_APA_HEXPRINT "%04x" 132 #endif 133 #define DD_APA_MASK (DD_APA_BASE - 1) 134 135 /*---------------------------------------------------------------------------*/ 136 /* Stucture declarations */ 137 /*---------------------------------------------------------------------------*/ 138 139 140 /*---------------------------------------------------------------------------*/ 141 /* Type declarations */ 142 /*---------------------------------------------------------------------------*/ 143 144 /**Enum************************************************************************ 145 146 Synopsis [Type of reordering algorithm.] 147 148 Description [Type of reordering algorithm.] 149 150 ******************************************************************************/ 151 typedef enum { 152 CUDD_REORDER_SAME, 153 CUDD_REORDER_NONE, 154 CUDD_REORDER_RANDOM, 155 CUDD_REORDER_RANDOM_PIVOT, 156 CUDD_REORDER_SIFT, 157 CUDD_REORDER_SIFT_CONVERGE, 158 CUDD_REORDER_SYMM_SIFT, 159 CUDD_REORDER_SYMM_SIFT_CONV, 160 CUDD_REORDER_WINDOW2, 161 CUDD_REORDER_WINDOW3, 162 CUDD_REORDER_WINDOW4, 163 CUDD_REORDER_WINDOW2_CONV, 164 CUDD_REORDER_WINDOW3_CONV, 165 CUDD_REORDER_WINDOW4_CONV, 166 CUDD_REORDER_GROUP_SIFT, 167 CUDD_REORDER_GROUP_SIFT_CONV, 168 CUDD_REORDER_ANNEALING, 169 CUDD_REORDER_GENETIC, 170 CUDD_REORDER_LINEAR, 171 CUDD_REORDER_LINEAR_CONVERGE, 172 CUDD_REORDER_LAZY_SIFT, 173 CUDD_REORDER_EXACT 174 } Cudd_ReorderingType; 175 176 177 /**Enum************************************************************************ 178 179 Synopsis [Type of aggregation methods.] 180 181 Description [Type of aggregation methods.] 182 183 ******************************************************************************/ 184 typedef enum { 185 CUDD_NO_CHECK, 186 CUDD_GROUP_CHECK, 187 CUDD_GROUP_CHECK2, 188 CUDD_GROUP_CHECK3, 189 CUDD_GROUP_CHECK4, 190 CUDD_GROUP_CHECK5, 191 CUDD_GROUP_CHECK6, 192 CUDD_GROUP_CHECK7, 193 CUDD_GROUP_CHECK8, 194 CUDD_GROUP_CHECK9 195 } Cudd_AggregationType; 196 197 198 /**Enum************************************************************************ 199 200 Synopsis [Type of hooks.] 201 202 Description [Type of hooks.] 203 204 ******************************************************************************/ 205 typedef enum { 206 CUDD_PRE_GC_HOOK, 207 CUDD_POST_GC_HOOK, 208 CUDD_PRE_REORDERING_HOOK, 209 CUDD_POST_REORDERING_HOOK 210 } Cudd_HookType; 211 212 213 /**Enum************************************************************************ 214 215 Synopsis [Type of error codes.] 216 217 Description [Type of error codes.] 218 219 ******************************************************************************/ 220 typedef enum { 221 CUDD_NO_ERROR, 222 CUDD_MEMORY_OUT, 223 CUDD_TOO_MANY_NODES, 224 CUDD_MAX_MEM_EXCEEDED, 225 CUDD_INVALID_ARG, 226 CUDD_INTERNAL_ERROR 227 } Cudd_ErrorType; 228 229 230 /**Enum************************************************************************ 231 232 Synopsis [Group type for lazy sifting.] 233 234 Description [Group type for lazy sifting.] 235 236 ******************************************************************************/ 237 typedef enum { 238 CUDD_LAZY_NONE, 239 CUDD_LAZY_SOFT_GROUP, 240 CUDD_LAZY_HARD_GROUP, 241 CUDD_LAZY_UNGROUP 242 } Cudd_LazyGroupType; 243 244 245 /**Enum************************************************************************ 246 247 Synopsis [Variable type.] 248 249 Description [Variable type. Currently used only in lazy sifting.] 250 251 ******************************************************************************/ 252 typedef enum { 253 CUDD_VAR_PRIMARY_INPUT, 254 CUDD_VAR_PRESENT_STATE, 255 CUDD_VAR_NEXT_STATE 256 } Cudd_VariableType; 257 258 259 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 260 typedef unsigned int DdHalfWord; 261 #else 262 typedef unsigned short DdHalfWord; 263 #endif 264 265 #ifdef __osf__ 266 #pragma pointer_size save 267 #pragma pointer_size short 268 #endif 269 270 typedef struct DdNode DdNode; 271 272 typedef struct DdChildren { 273 struct DdNode *T; 274 struct DdNode *E; 275 } DdChildren; 276 277 /* The DdNode structure is the only one exported out of the package */ 278 struct DdNode { 279 DdHalfWord index; 280 DdHalfWord ref; /* reference count */ 281 DdNode *next; /* next pointer for unique table */ 282 union { 283 CUDD_VALUE_TYPE value; /* for constant nodes */ 284 DdChildren kids; /* for internal nodes */ 285 } type; 286 ABC_INT64_T Id; 287 }; 288 289 #ifdef __osf__ 290 #pragma pointer_size restore 291 #endif 292 293 typedef struct DdManager DdManager; 294 295 typedef struct DdGen DdGen; 296 297 /* These typedefs for arbitrary precision arithmetic should agree with 298 ** the corresponding constant definitions above. */ 299 #if SIZEOF_LONG == 8 300 typedef unsigned int DdApaDigit; 301 typedef unsigned long int DdApaDoubleDigit; 302 #else 303 typedef unsigned short int DdApaDigit; 304 typedef unsigned int DdApaDoubleDigit; 305 #endif 306 typedef DdApaDigit * DdApaNumber; 307 308 /* Return type for function computing two-literal clauses. */ 309 typedef struct DdTlcInfo DdTlcInfo; 310 311 /* Type of hook function. */ 312 typedef int (*DD_HFP)(DdManager *, const char *, void *); 313 /* Type of priority function */ 314 typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **, 315 DdNode **); 316 /* Type of apply operator. */ 317 typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **); 318 /* Type of monadic apply operator. */ 319 typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *); 320 /* Types of cache tag functions. */ 321 typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *); 322 typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *); 323 /* Type of memory-out function. */ 324 typedef void (*DD_OOMFP)(long); 325 /* Type of comparison function for qsort. */ 326 typedef int (*DD_QSFP)(const void *, const void *); 327 328 /*---------------------------------------------------------------------------*/ 329 /* Variable declarations */ 330 /*---------------------------------------------------------------------------*/ 331 332 333 /*---------------------------------------------------------------------------*/ 334 /* Macro declarations */ 335 /*---------------------------------------------------------------------------*/ 336 337 338 /**Macro*********************************************************************** 339 340 Synopsis [Returns 1 if the node is a constant node.] 341 342 Description [Returns 1 if the node is a constant node (rather than an 343 internal node). All constant nodes have the same index 344 (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either 345 regular or complemented.] 346 347 SideEffects [none] 348 349 SeeAlso [] 350 351 ******************************************************************************/ 352 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX) 353 354 355 /**Macro*********************************************************************** 356 357 Synopsis [Complements a DD.] 358 359 Description [Complements a DD by flipping the complement attribute of 360 the pointer (the least significant bit).] 361 362 SideEffects [none] 363 364 SeeAlso [Cudd_NotCond] 365 366 ******************************************************************************/ 367 #define Cudd_Not(node) ((DdNode *)((ptrint)(node) ^ 01)) 368 369 370 /**Macro*********************************************************************** 371 372 Synopsis [Complements a DD if a condition is true.] 373 374 Description [Complements a DD if condition c is true; c should be 375 either 0 or 1, because it is used directly (for efficiency). If in 376 doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".] 377 378 SideEffects [none] 379 380 SeeAlso [Cudd_Not] 381 382 ******************************************************************************/ 383 #define Cudd_NotCond(node,c) ((DdNode *)((ptrint)(node) ^ (c))) 384 385 386 /**Macro*********************************************************************** 387 388 Synopsis [Returns the regular version of a pointer.] 389 390 Description [] 391 392 SideEffects [none] 393 394 SeeAlso [Cudd_Complement Cudd_IsComplement] 395 396 ******************************************************************************/ 397 #define Cudd_Regular(node) ((DdNode *)((ptruint)(node) & ~01)) 398 399 400 /**Macro*********************************************************************** 401 402 Synopsis [Returns the complemented version of a pointer.] 403 404 Description [] 405 406 SideEffects [none] 407 408 SeeAlso [Cudd_Regular Cudd_IsComplement] 409 410 ******************************************************************************/ 411 #define Cudd_Complement(node) ((DdNode *)((ptruint)(node) | 01)) 412 413 414 /**Macro*********************************************************************** 415 416 Synopsis [Returns 1 if a pointer is complemented.] 417 418 Description [] 419 420 SideEffects [none] 421 422 SeeAlso [Cudd_Regular Cudd_Complement] 423 424 ******************************************************************************/ 425 #define Cudd_IsComplement(node) ((int) ((ptrint) (node) & 01)) 426 427 428 /**Macro*********************************************************************** 429 430 Synopsis [Returns the then child of an internal node.] 431 432 Description [Returns the then child of an internal node. If 433 <code>node</code> is a constant node, the result is unpredictable.] 434 435 SideEffects [none] 436 437 SeeAlso [Cudd_E Cudd_V] 438 439 ******************************************************************************/ 440 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T) 441 442 443 /**Macro*********************************************************************** 444 445 Synopsis [Returns the else child of an internal node.] 446 447 Description [Returns the else child of an internal node. If 448 <code>node</code> is a constant node, the result is unpredictable.] 449 450 SideEffects [none] 451 452 SeeAlso [Cudd_T Cudd_V] 453 454 ******************************************************************************/ 455 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E) 456 457 458 /**Macro*********************************************************************** 459 460 Synopsis [Returns the value of a constant node.] 461 462 Description [Returns the value of a constant node. If 463 <code>node</code> is an internal node, the result is unpredictable.] 464 465 SideEffects [none] 466 467 SeeAlso [Cudd_T Cudd_E] 468 469 ******************************************************************************/ 470 #define Cudd_V(node) ((Cudd_Regular(node))->type.value) 471 472 473 /**Macro*********************************************************************** 474 475 Synopsis [Returns the current position in the order of variable 476 index.] 477 478 Description [Returns the current position in the order of variable 479 index. This macro is obsolete and is kept for compatibility. New 480 applications should use Cudd_ReadPerm instead.] 481 482 SideEffects [none] 483 484 SeeAlso [Cudd_ReadPerm] 485 486 ******************************************************************************/ 487 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index)) 488 489 490 /**Macro*********************************************************************** 491 492 Synopsis [Iterates over the cubes of a decision diagram.] 493 494 Description [Iterates over the cubes of a decision diagram f. 495 <ul> 496 <li> DdManager *manager; 497 <li> DdNode *f; 498 <li> DdGen *gen; 499 <li> int *cube; 500 <li> CUDD_VALUE_TYPE value; 501 </ul> 502 Cudd_ForeachCube allocates and frees the generator. Therefore the 503 application should not try to do that. Also, the cube is freed at the 504 end of Cudd_ForeachCube and hence is not available outside of the loop.<p> 505 CAUTION: It is assumed that dynamic reordering will not occur while 506 there are open generators. It is the user's responsibility to make sure 507 that dynamic reordering does not occur. As long as new nodes are not created 508 during generation, and dynamic reordering is not called explicitly, 509 dynamic reordering will not occur. Alternatively, it is sufficient to 510 disable dynamic reordering. It is a mistake to dispose of a diagram 511 on which generation is ongoing.] 512 513 SideEffects [none] 514 515 SeeAlso [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree 516 Cudd_IsGenEmpty Cudd_AutodynDisable] 517 518 ******************************************************************************/ 519 #define Cudd_ForeachCube(manager, f, gen, cube, value)\ 520 for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\ 521 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ 522 (void) Cudd_NextCube(gen, &cube, &value)) 523 524 525 /**Macro*********************************************************************** 526 527 Synopsis [Iterates over the primes of a Boolean function.] 528 529 Description [Iterates over the primes of a Boolean function producing 530 a prime and irredundant cover. 531 <ul> 532 <li> DdManager *manager; 533 <li> DdNode *l; 534 <li> DdNode *u; 535 <li> DdGen *gen; 536 <li> int *cube; 537 </ul> 538 The Boolean function is described by an upper bound and a lower bound. If 539 the function is completely specified, the two bounds coincide. 540 Cudd_ForeachPrime allocates and frees the generator. Therefore the 541 application should not try to do that. Also, the cube is freed at the 542 end of Cudd_ForeachPrime and hence is not available outside of the loop.<p> 543 CAUTION: It is a mistake to change a diagram on which generation is ongoing.] 544 545 SideEffects [none] 546 547 SeeAlso [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree 548 Cudd_IsGenEmpty] 549 550 ******************************************************************************/ 551 #define Cudd_ForeachPrime(manager, l, u, gen, cube)\ 552 for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\ 553 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ 554 (void) Cudd_NextPrime(gen, &cube)) 555 556 557 /**Macro*********************************************************************** 558 559 Synopsis [Iterates over the nodes of a decision diagram.] 560 561 Description [Iterates over the nodes of a decision diagram f. 562 <ul> 563 <li> DdManager *manager; 564 <li> DdNode *f; 565 <li> DdGen *gen; 566 <li> DdNode *node; 567 </ul> 568 The nodes are returned in a seemingly random order. 569 Cudd_ForeachNode allocates and frees the generator. Therefore the 570 application should not try to do that.<p> 571 CAUTION: It is assumed that dynamic reordering will not occur while 572 there are open generators. It is the user's responsibility to make sure 573 that dynamic reordering does not occur. As long as new nodes are not created 574 during generation, and dynamic reordering is not called explicitly, 575 dynamic reordering will not occur. Alternatively, it is sufficient to 576 disable dynamic reordering. It is a mistake to dispose of a diagram 577 on which generation is ongoing.] 578 579 SideEffects [none] 580 581 SeeAlso [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree 582 Cudd_IsGenEmpty Cudd_AutodynDisable] 583 584 ******************************************************************************/ 585 #define Cudd_ForeachNode(manager, f, gen, node)\ 586 for((gen) = Cudd_FirstNode(manager, f, &node);\ 587 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ 588 (void) Cudd_NextNode(gen, &node)) 589 590 591 /**Macro*********************************************************************** 592 593 Synopsis [Iterates over the paths of a ZDD.] 594 595 Description [Iterates over the paths of a ZDD f. 596 <ul> 597 <li> DdManager *manager; 598 <li> DdNode *f; 599 <li> DdGen *gen; 600 <li> int *path; 601 </ul> 602 Cudd_zddForeachPath allocates and frees the generator. Therefore the 603 application should not try to do that. Also, the path is freed at the 604 end of Cudd_zddForeachPath and hence is not available outside of the loop.<p> 605 CAUTION: It is assumed that dynamic reordering will not occur while 606 there are open generators. It is the user's responsibility to make sure 607 that dynamic reordering does not occur. As long as new nodes are not created 608 during generation, and dynamic reordering is not called explicitly, 609 dynamic reordering will not occur. Alternatively, it is sufficient to 610 disable dynamic reordering. It is a mistake to dispose of a diagram 611 on which generation is ongoing.] 612 613 SideEffects [none] 614 615 SeeAlso [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree 616 Cudd_IsGenEmpty Cudd_AutodynDisable] 617 618 ******************************************************************************/ 619 #define Cudd_zddForeachPath(manager, f, gen, path)\ 620 for((gen) = Cudd_zddFirstPath(manager, f, &path);\ 621 Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\ 622 (void) Cudd_zddNextPath(gen, &path)) 623 624 625 626 /**AutomaticStart*************************************************************/ 627 628 /*---------------------------------------------------------------------------*/ 629 /* Function prototypes */ 630 /*---------------------------------------------------------------------------*/ 631 632 extern DdNode * Cudd_addNewVar( DdManager * dd ); 633 extern DdNode * Cudd_addNewVarAtLevel( DdManager * dd, int level ); 634 extern DdNode * Cudd_bddNewVar( DdManager * dd ); 635 extern DdNode * Cudd_bddNewVarAtLevel( DdManager * dd, int level ); 636 extern DdNode * Cudd_addIthVar( DdManager * dd, int i ); 637 extern DdNode * Cudd_bddIthVar( DdManager * dd, int i ); 638 extern DdNode * Cudd_zddIthVar( DdManager * dd, int i ); 639 extern int Cudd_zddVarsFromBddVars( DdManager * dd, int multiplicity ); 640 extern DdNode * Cudd_addConst( DdManager * dd, CUDD_VALUE_TYPE c ); 641 extern int Cudd_IsNonConstant( DdNode * f ); 642 extern void Cudd_AutodynEnable( DdManager * unique, Cudd_ReorderingType method ); 643 extern void Cudd_AutodynDisable( DdManager * unique ); 644 extern int Cudd_ReorderingStatus( DdManager * unique, Cudd_ReorderingType * method ); 645 extern void Cudd_AutodynEnableZdd( DdManager * unique, Cudd_ReorderingType method ); 646 extern void Cudd_AutodynDisableZdd( DdManager * unique ); 647 extern int Cudd_ReorderingStatusZdd( DdManager * unique, Cudd_ReorderingType * method ); 648 extern int Cudd_zddRealignmentEnabled( DdManager * unique ); 649 extern void Cudd_zddRealignEnable( DdManager * unique ); 650 extern void Cudd_zddRealignDisable( DdManager * unique ); 651 extern int Cudd_bddRealignmentEnabled( DdManager * unique ); 652 extern void Cudd_bddRealignEnable( DdManager * unique ); 653 extern void Cudd_bddRealignDisable( DdManager * unique ); 654 extern DdNode * Cudd_ReadOne( DdManager * dd ); 655 extern DdNode * Cudd_ReadZddOne( DdManager * dd, int i ); 656 extern DdNode * Cudd_ReadZero( DdManager * dd ); 657 extern DdNode * Cudd_ReadLogicZero( DdManager * dd ); 658 extern DdNode * Cudd_ReadPlusInfinity( DdManager * dd ); 659 extern DdNode * Cudd_ReadMinusInfinity( DdManager * dd ); 660 extern DdNode * Cudd_ReadBackground( DdManager * dd ); 661 extern void Cudd_SetBackground( DdManager * dd, DdNode * bck ); 662 extern unsigned int Cudd_ReadCacheSlots( DdManager * dd ); 663 extern double Cudd_ReadCacheUsedSlots( DdManager * dd ); 664 extern double Cudd_ReadCacheLookUps( DdManager * dd ); 665 extern double Cudd_ReadCacheHits( DdManager * dd ); 666 extern double Cudd_ReadRecursiveCalls( DdManager * dd ); 667 extern unsigned int Cudd_ReadMinHit( DdManager * dd ); 668 extern void Cudd_SetMinHit( DdManager * dd, unsigned int hr ); 669 extern unsigned int Cudd_ReadLooseUpTo( DdManager * dd ); 670 extern void Cudd_SetLooseUpTo( DdManager * dd, unsigned int lut ); 671 extern unsigned int Cudd_ReadMaxCache( DdManager * dd ); 672 extern unsigned int Cudd_ReadMaxCacheHard( DdManager * dd ); 673 extern void Cudd_SetMaxCacheHard( DdManager * dd, unsigned int mc ); 674 extern int Cudd_ReadSize( DdManager * dd ); 675 extern int Cudd_ReadZddSize( DdManager * dd ); 676 extern unsigned int Cudd_ReadSlots( DdManager * dd ); 677 extern double Cudd_ReadUsedSlots( DdManager * dd ); 678 extern double Cudd_ExpectedUsedSlots( DdManager * dd ); 679 extern unsigned int Cudd_ReadKeys( DdManager * dd ); 680 extern unsigned int Cudd_ReadDead( DdManager * dd ); 681 extern unsigned int Cudd_ReadMinDead( DdManager * dd ); 682 extern int Cudd_ReadReorderings( DdManager * dd ); 683 extern long Cudd_ReadReorderingTime( DdManager * dd ); 684 extern int Cudd_ReadGarbageCollections( DdManager * dd ); 685 extern long Cudd_ReadGarbageCollectionTime( DdManager * dd ); 686 extern double Cudd_ReadNodesFreed( DdManager * dd ); 687 extern double Cudd_ReadNodesDropped( DdManager * dd ); 688 extern double Cudd_ReadUniqueLookUps( DdManager * dd ); 689 extern double Cudd_ReadUniqueLinks( DdManager * dd ); 690 extern int Cudd_ReadSiftMaxVar( DdManager * dd ); 691 extern void Cudd_SetSiftMaxVar( DdManager * dd, int smv ); 692 extern int Cudd_ReadSiftMaxSwap( DdManager * dd ); 693 extern void Cudd_SetSiftMaxSwap( DdManager * dd, int sms ); 694 extern double Cudd_ReadMaxGrowth( DdManager * dd ); 695 extern void Cudd_SetMaxGrowth( DdManager * dd, double mg ); 696 extern double Cudd_ReadMaxGrowthAlternate( DdManager * dd ); 697 extern void Cudd_SetMaxGrowthAlternate( DdManager * dd, double mg ); 698 extern int Cudd_ReadReorderingCycle( DdManager * dd ); 699 extern void Cudd_SetReorderingCycle( DdManager * dd, int cycle ); 700 extern MtrNode * Cudd_ReadTree( DdManager * dd ); 701 extern void Cudd_SetTree( DdManager * dd, MtrNode * tree ); 702 extern void Cudd_FreeTree( DdManager * dd ); 703 extern MtrNode * Cudd_ReadZddTree( DdManager * dd ); 704 extern void Cudd_SetZddTree( DdManager * dd, MtrNode * tree ); 705 extern void Cudd_FreeZddTree( DdManager * dd ); 706 extern unsigned int Cudd_NodeReadIndex( DdNode * node ); 707 extern int Cudd_ReadPerm( DdManager * dd, int i ); 708 extern int Cudd_ReadPermZdd( DdManager * dd, int i ); 709 extern int Cudd_ReadInvPerm( DdManager * dd, int i ); 710 extern int Cudd_ReadInvPermZdd( DdManager * dd, int i ); 711 extern DdNode * Cudd_ReadVars( DdManager * dd, int i ); 712 extern CUDD_VALUE_TYPE Cudd_ReadEpsilon( DdManager * dd ); 713 extern void Cudd_SetEpsilon( DdManager * dd, CUDD_VALUE_TYPE ep ); 714 extern Cudd_AggregationType Cudd_ReadGroupcheck( DdManager * dd ); 715 extern void Cudd_SetGroupcheck( DdManager * dd, Cudd_AggregationType gc ); 716 extern int Cudd_GarbageCollectionEnabled( DdManager * dd ); 717 extern void Cudd_EnableGarbageCollection( DdManager * dd ); 718 extern void Cudd_DisableGarbageCollection( DdManager * dd ); 719 extern int Cudd_DeadAreCounted( DdManager * dd ); 720 extern void Cudd_TurnOnCountDead( DdManager * dd ); 721 extern void Cudd_TurnOffCountDead( DdManager * dd ); 722 extern int Cudd_ReadRecomb( DdManager * dd ); 723 extern void Cudd_SetRecomb( DdManager * dd, int recomb ); 724 extern int Cudd_ReadSymmviolation( DdManager * dd ); 725 extern void Cudd_SetSymmviolation( DdManager * dd, int symmviolation ); 726 extern int Cudd_ReadArcviolation( DdManager * dd ); 727 extern void Cudd_SetArcviolation( DdManager * dd, int arcviolation ); 728 extern int Cudd_ReadPopulationSize( DdManager * dd ); 729 extern void Cudd_SetPopulationSize( DdManager * dd, int populationSize ); 730 extern int Cudd_ReadNumberXovers( DdManager * dd ); 731 extern void Cudd_SetNumberXovers( DdManager * dd, int numberXovers ); 732 extern unsigned long Cudd_ReadMemoryInUse( DdManager * dd ); 733 extern int Cudd_PrintInfo( DdManager * dd, FILE * fp ); 734 extern long Cudd_ReadPeakNodeCount( DdManager * dd ); 735 extern int Cudd_ReadPeakLiveNodeCount( DdManager * dd ); 736 extern long Cudd_ReadNodeCount( DdManager * dd ); 737 extern long Cudd_zddReadNodeCount( DdManager * dd ); 738 extern int Cudd_AddHook( DdManager * dd, DD_HFP f, Cudd_HookType where ); 739 extern int Cudd_RemoveHook( DdManager * dd, DD_HFP f, Cudd_HookType where ); 740 extern int Cudd_IsInHook( DdManager * dd, DD_HFP f, Cudd_HookType where ); 741 extern int Cudd_StdPreReordHook( DdManager * dd, const char * str, void * data ); 742 extern int Cudd_StdPostReordHook( DdManager * dd, const char * str, void * data ); 743 extern int Cudd_EnableReorderingReporting( DdManager * dd ); 744 extern int Cudd_DisableReorderingReporting( DdManager * dd ); 745 extern int Cudd_ReorderingReporting( DdManager * dd ); 746 extern Cudd_ErrorType Cudd_ReadErrorCode( DdManager * dd ); 747 extern void Cudd_ClearErrorCode( DdManager * dd ); 748 extern FILE * Cudd_ReadStdout( DdManager * dd ); 749 extern void Cudd_SetStdout( DdManager * dd, FILE * fp ); 750 extern FILE * Cudd_ReadStderr( DdManager * dd ); 751 extern void Cudd_SetStderr( DdManager * dd, FILE * fp ); 752 extern unsigned int Cudd_ReadNextReordering( DdManager * dd ); 753 extern void Cudd_SetNextReordering( DdManager * dd, unsigned int next ); 754 extern double Cudd_ReadSwapSteps( DdManager * dd ); 755 extern unsigned int Cudd_ReadMaxLive( DdManager * dd ); 756 extern void Cudd_SetMaxLive( DdManager * dd, unsigned int maxLive ); 757 extern unsigned long Cudd_ReadMaxMemory( DdManager * dd ); 758 extern void Cudd_SetMaxMemory( DdManager * dd, unsigned long maxMemory ); 759 extern int Cudd_bddBindVar( DdManager * dd, int index ); 760 extern int Cudd_bddUnbindVar( DdManager * dd, int index ); 761 extern int Cudd_bddVarIsBound( DdManager * dd, int index ); 762 extern DdNode * Cudd_addExistAbstract( DdManager * manager, DdNode * f, DdNode * cube ); 763 extern DdNode * Cudd_addUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube ); 764 extern DdNode * Cudd_addOrAbstract( DdManager * manager, DdNode * f, DdNode * cube ); 765 extern DdNode * Cudd_addApply( DdManager * dd, DdNode * ( * )(DdManager * , DdNode ** , DdNode ** ), DdNode * f, DdNode * g ); 766 extern DdNode * Cudd_addPlus( DdManager * dd, DdNode ** f, DdNode ** g ); 767 extern DdNode * Cudd_addTimes( DdManager * dd, DdNode ** f, DdNode ** g ); 768 extern DdNode * Cudd_addThreshold( DdManager * dd, DdNode ** f, DdNode ** g ); 769 extern DdNode * Cudd_addSetNZ( DdManager * dd, DdNode ** f, DdNode ** g ); 770 extern DdNode * Cudd_addDivide( DdManager * dd, DdNode ** f, DdNode ** g ); 771 extern DdNode * Cudd_addMinus( DdManager * dd, DdNode ** f, DdNode ** g ); 772 extern DdNode * Cudd_addMinimum( DdManager * dd, DdNode ** f, DdNode ** g ); 773 extern DdNode * Cudd_addMaximum( DdManager * dd, DdNode ** f, DdNode ** g ); 774 extern DdNode * Cudd_addOneZeroMaximum( DdManager * dd, DdNode ** f, DdNode ** g ); 775 extern DdNode * Cudd_addDiff( DdManager * dd, DdNode ** f, DdNode ** g ); 776 extern DdNode * Cudd_addAgreement( DdManager * dd, DdNode ** f, DdNode ** g ); 777 extern DdNode * Cudd_addOr( DdManager * dd, DdNode ** f, DdNode ** g ); 778 extern DdNode * Cudd_addNand( DdManager * dd, DdNode ** f, DdNode ** g ); 779 extern DdNode * Cudd_addNor( DdManager * dd, DdNode ** f, DdNode ** g ); 780 extern DdNode * Cudd_addXor( DdManager * dd, DdNode ** f, DdNode ** g ); 781 extern DdNode * Cudd_addXnor( DdManager * dd, DdNode ** f, DdNode ** g ); 782 extern DdNode * Cudd_addMonadicApply( DdManager * dd, DdNode * ( * op)(DdManager * , DdNode * ), DdNode * f ); 783 extern DdNode * Cudd_addLog( DdManager * dd, DdNode * f ); 784 extern DdNode * Cudd_addFindMax( DdManager * dd, DdNode * f ); 785 extern DdNode * Cudd_addFindMin( DdManager * dd, DdNode * f ); 786 extern DdNode * Cudd_addIthBit( DdManager * dd, DdNode * f, int bit ); 787 extern DdNode * Cudd_addScalarInverse( DdManager * dd, DdNode * f, DdNode * epsilon ); 788 extern DdNode * Cudd_addIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); 789 extern DdNode * Cudd_addIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); 790 extern DdNode * Cudd_addEvalConst( DdManager * dd, DdNode * f, DdNode * g ); 791 extern int Cudd_addLeq( DdManager * dd, DdNode * f, DdNode * g ); 792 extern DdNode * Cudd_addCmpl( DdManager * dd, DdNode * f ); 793 extern DdNode * Cudd_addNegate( DdManager * dd, DdNode * f ); 794 extern DdNode * Cudd_addRoundOff( DdManager * dd, DdNode * f, int N ); 795 extern DdNode * Cudd_addWalsh( DdManager * dd, DdNode ** x, DdNode ** y, int n ); 796 extern DdNode * Cudd_addResidue( DdManager * dd, int n, int m, int options, int top ); 797 extern DdNode * Cudd_bddAndAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube ); 798 extern DdNode * Cudd_bddAndAbstractLimit( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, unsigned int limit ); 799 extern int Cudd_ApaNumberOfDigits( int binaryDigits ); 800 extern DdApaNumber Cudd_NewApaNumber( int digits ); 801 extern void Cudd_ApaCopy( int digits, DdApaNumber source, DdApaNumber dest ); 802 extern DdApaDigit Cudd_ApaAdd( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum ); 803 extern DdApaDigit Cudd_ApaSubtract( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff ); 804 extern DdApaDigit Cudd_ApaShortDivision( int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient ); 805 extern unsigned int Cudd_ApaIntDivision( int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient ); 806 extern void Cudd_ApaShiftRight( int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b ); 807 extern void Cudd_ApaSetToLiteral( int digits, DdApaNumber number, DdApaDigit literal ); 808 extern void Cudd_ApaPowerOfTwo( int digits, DdApaNumber number, int power ); 809 extern int Cudd_ApaCompare( int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second ); 810 extern int Cudd_ApaCompareRatios( int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen ); 811 extern int Cudd_ApaPrintHex( FILE * fp, int digits, DdApaNumber number ); 812 extern int Cudd_ApaPrintDecimal( FILE * fp, int digits, DdApaNumber number ); 813 extern int Cudd_ApaPrintExponential( FILE * fp, int digits, DdApaNumber number, int precision ); 814 extern DdApaNumber Cudd_ApaCountMinterm( DdManager * manager, DdNode * node, int nvars, int * digits ); 815 extern int Cudd_ApaPrintMinterm( FILE * fp, DdManager * dd, DdNode * node, int nvars ); 816 extern int Cudd_ApaPrintMintermExp( FILE * fp, DdManager * dd, DdNode * node, int nvars, int precision ); 817 extern int Cudd_ApaPrintDensity( FILE * fp, DdManager * dd, DdNode * node, int nvars ); 818 extern DdNode * Cudd_UnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality ); 819 extern DdNode * Cudd_OverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality ); 820 extern DdNode * Cudd_RemapUnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality ); 821 extern DdNode * Cudd_RemapOverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality ); 822 extern DdNode * Cudd_BiasedUnderApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 ); 823 extern DdNode * Cudd_BiasedOverApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 ); 824 extern DdNode * Cudd_bddExistAbstract( DdManager * manager, DdNode * f, DdNode * cube ); 825 extern DdNode * Cudd_bddXorExistAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube ); 826 extern DdNode * Cudd_bddUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube ); 827 extern DdNode * Cudd_bddBooleanDiff( DdManager * manager, DdNode * f, int x ); 828 extern int Cudd_bddVarIsDependent( DdManager * dd, DdNode * f, DdNode * var ); 829 extern double Cudd_bddCorrelation( DdManager * manager, DdNode * f, DdNode * g ); 830 extern double Cudd_bddCorrelationWeights( DdManager * manager, DdNode * f, DdNode * g, double * prob ); 831 extern DdNode * Cudd_bddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); 832 extern DdNode * Cudd_bddIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); 833 extern DdNode * Cudd_bddIntersect( DdManager * dd, DdNode * f, DdNode * g ); 834 extern DdNode * Cudd_bddAnd( DdManager * dd, DdNode * f, DdNode * g ); 835 extern DdNode * Cudd_bddAndLimit( DdManager * dd, DdNode * f, DdNode * g, unsigned int limit ); 836 extern DdNode * Cudd_bddOr( DdManager * dd, DdNode * f, DdNode * g ); 837 extern DdNode * Cudd_bddNand( DdManager * dd, DdNode * f, DdNode * g ); 838 extern DdNode * Cudd_bddNor( DdManager * dd, DdNode * f, DdNode * g ); 839 extern DdNode * Cudd_bddXor( DdManager * dd, DdNode * f, DdNode * g ); 840 extern DdNode * Cudd_bddXnor( DdManager * dd, DdNode * f, DdNode * g ); 841 extern int Cudd_bddLeq( DdManager * dd, DdNode * f, DdNode * g ); 842 extern DdNode * Cudd_addBddThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value ); 843 extern DdNode * Cudd_addBddStrictThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value ); 844 extern DdNode * Cudd_addBddInterval( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper ); 845 extern DdNode * Cudd_addBddIthBit( DdManager * dd, DdNode * f, int bit ); 846 extern DdNode * Cudd_BddToAdd( DdManager * dd, DdNode * B ); 847 extern DdNode * Cudd_addBddPattern( DdManager * dd, DdNode * f ); 848 extern DdNode * Cudd_bddTransfer( DdManager * ddSource, DdManager * ddDestination, DdNode * f ); 849 extern int Cudd_DebugCheck( DdManager * table ); 850 extern int Cudd_CheckKeys( DdManager * table ); 851 extern DdNode * Cudd_bddClippingAnd( DdManager * dd, DdNode * f, DdNode * g, int maxDepth, int direction ); 852 extern DdNode * Cudd_bddClippingAndAbstract( DdManager * dd, DdNode * f, DdNode * g, DdNode * cube, int maxDepth, int direction ); 853 extern DdNode * Cudd_Cofactor( DdManager * dd, DdNode * f, DdNode * g ); 854 extern DdNode * Cudd_bddCompose( DdManager * dd, DdNode * f, DdNode * g, int v ); 855 extern DdNode * Cudd_addCompose( DdManager * dd, DdNode * f, DdNode * g, int v ); 856 extern DdNode * Cudd_addPermute( DdManager * manager, DdNode * node, int * permut ); 857 extern DdNode * Cudd_addSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n ); 858 extern DdNode * Cudd_bddPermute( DdManager * manager, DdNode * node, int * permut ); 859 extern DdNode * Cudd_bddVarMap( DdManager * manager, DdNode * f ); 860 extern int Cudd_SetVarMap( DdManager * manager, DdNode ** x, DdNode ** y, int n ); 861 extern DdNode * Cudd_bddSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n ); 862 extern DdNode * Cudd_bddAdjPermuteX( DdManager * dd, DdNode * B, DdNode ** x, int n ); 863 extern DdNode * Cudd_addVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector ); 864 extern DdNode * Cudd_addGeneralVectorCompose( DdManager * dd, DdNode * f, DdNode ** vectorOn, DdNode ** vectorOff ); 865 extern DdNode * Cudd_addNonSimCompose( DdManager * dd, DdNode * f, DdNode ** vector ); 866 extern DdNode * Cudd_bddVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector ); 867 extern int Cudd_bddApproxConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts ); 868 extern int Cudd_bddApproxDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts ); 869 extern int Cudd_bddIterConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts ); 870 extern int Cudd_bddIterDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts ); 871 extern int Cudd_bddGenConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts ); 872 extern int Cudd_bddGenDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts ); 873 extern int Cudd_bddVarConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts ); 874 extern int Cudd_bddVarDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts ); 875 extern DdNode * Cudd_FindEssential( DdManager * dd, DdNode * f ); 876 extern int Cudd_bddIsVarEssential( DdManager * manager, DdNode * f, int id, int phase ); 877 extern DdTlcInfo * Cudd_FindTwoLiteralClauses( DdManager * dd, DdNode * f ); 878 extern int Cudd_PrintTwoLiteralClauses( DdManager * dd, DdNode * f, char ** names, FILE * fp ); 879 extern int Cudd_ReadIthClause( DdTlcInfo * tlc, int i, DdHalfWord * var1, DdHalfWord * var2, int * phase1, int * phase2 ); 880 extern void Cudd_tlcInfoFree( DdTlcInfo * t ); 881 extern int Cudd_DumpBlif( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, char * mname, FILE * fp, int mv ); 882 extern int Cudd_DumpBlifBody( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp, int mv ); 883 extern int Cudd_DumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp ); 884 extern int Cudd_DumpDaVinci( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp ); 885 extern int Cudd_DumpDDcal( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp ); 886 extern int Cudd_DumpFactoredForm( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp ); 887 extern DdNode * Cudd_bddConstrain( DdManager * dd, DdNode * f, DdNode * c ); 888 extern DdNode * Cudd_bddRestrict( DdManager * dd, DdNode * f, DdNode * c ); 889 extern DdNode * Cudd_bddNPAnd( DdManager * dd, DdNode * f, DdNode * c ); 890 extern DdNode * Cudd_addConstrain( DdManager * dd, DdNode * f, DdNode * c ); 891 extern DdNode ** Cudd_bddConstrainDecomp( DdManager * dd, DdNode * f ); 892 extern DdNode * Cudd_addRestrict( DdManager * dd, DdNode * f, DdNode * c ); 893 extern DdNode ** Cudd_bddCharToVect( DdManager * dd, DdNode * f ); 894 extern DdNode * Cudd_bddLICompaction( DdManager * dd, DdNode * f, DdNode * c ); 895 extern DdNode * Cudd_bddSqueeze( DdManager * dd, DdNode * l, DdNode * u ); 896 extern DdNode * Cudd_bddMinimize( DdManager * dd, DdNode * f, DdNode * c ); 897 extern DdNode * Cudd_SubsetCompress( DdManager * dd, DdNode * f, int nvars, int threshold ); 898 extern DdNode * Cudd_SupersetCompress( DdManager * dd, DdNode * f, int nvars, int threshold ); 899 extern MtrNode * Cudd_MakeTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type ); 900 extern int Cudd_addHarwell( FILE * fp, DdManager * dd, DdNode ** E, DdNode ** * x, DdNode ** * y, DdNode ** * xn, DdNode ** * yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy, int pr ); 901 extern DdManager * Cudd_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory ); 902 extern void Cudd_Quit( DdManager * unique ); 903 extern int Cudd_PrintLinear( DdManager * table ); 904 extern int Cudd_ReadLinear( DdManager * table, int x, int y ); 905 extern DdNode * Cudd_bddLiteralSetIntersection( DdManager * dd, DdNode * f, DdNode * g ); 906 extern DdNode * Cudd_addMatrixMultiply( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz ); 907 extern DdNode * Cudd_addTimesPlus( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz ); 908 extern DdNode * Cudd_addTriangle( DdManager * dd, DdNode * f, DdNode * g, DdNode ** z, int nz ); 909 extern DdNode * Cudd_addOuterSum( DdManager * dd, DdNode * M, DdNode * r, DdNode * c ); 910 extern DdNode * Cudd_PrioritySelect( DdManager * dd, DdNode * R, DdNode ** x, DdNode ** y, DdNode ** z, DdNode * Pi, int n, DdNode * ( * )(DdManager * , int, DdNode ** , DdNode ** , DdNode ** ) ); 911 extern DdNode * Cudd_Xgty( DdManager * dd, int N, DdNode ** z, DdNode ** x, DdNode ** y ); 912 extern DdNode * Cudd_Xeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y ); 913 extern DdNode * Cudd_addXeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y ); 914 extern DdNode * Cudd_Dxygtdxz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z ); 915 extern DdNode * Cudd_Dxygtdyz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z ); 916 extern DdNode * Cudd_Inequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y ); 917 extern DdNode * Cudd_Disequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y ); 918 extern DdNode * Cudd_bddInterval( DdManager * dd, int N, DdNode ** x, unsigned int lowerB, unsigned int upperB ); 919 extern DdNode * Cudd_CProjection( DdManager * dd, DdNode * R, DdNode * Y ); 920 extern DdNode * Cudd_addHamming( DdManager * dd, DdNode ** xVars, DdNode ** yVars, int nVars ); 921 extern int Cudd_MinHammingDist( DdManager * dd, DdNode * f, int * minterm, int upperBound ); 922 extern DdNode * Cudd_bddClosestCube( DdManager * dd, DdNode * f, DdNode * g, int * distance ); 923 extern int Cudd_addRead( FILE * fp, DdManager * dd, DdNode ** E, DdNode ** * x, DdNode ** * y, DdNode ** * xn, DdNode ** * yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy ); 924 extern int Cudd_bddRead( FILE * fp, DdManager * dd, DdNode ** E, DdNode ** * x, DdNode ** * y, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy ); 925 extern void Cudd_Ref( DdNode * n ); 926 extern void Cudd_RecursiveDeref( DdManager * table, DdNode * n ); 927 extern void Cudd_IterDerefBdd( DdManager * table, DdNode * n ); 928 extern void Cudd_DelayedDerefBdd( DdManager * table, DdNode * n ); 929 extern void Cudd_RecursiveDerefZdd( DdManager * table, DdNode * n ); 930 extern void Cudd_Deref( DdNode * node ); 931 extern int Cudd_CheckZeroRef( DdManager * manager ); 932 extern int Cudd_ReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize ); 933 extern int Cudd_ShuffleHeap( DdManager * table, int * permutation ); 934 extern DdNode * Cudd_Eval( DdManager * dd, DdNode * f, int * inputs ); 935 extern DdNode * Cudd_ShortestPath( DdManager * manager, DdNode * f, int * weight, int * support, int * length ); 936 extern DdNode * Cudd_LargestCube( DdManager * manager, DdNode * f, int * length ); 937 extern int Cudd_ShortestLength( DdManager * manager, DdNode * f, int * weight ); 938 extern DdNode * Cudd_Decreasing( DdManager * dd, DdNode * f, int i ); 939 extern DdNode * Cudd_Increasing( DdManager * dd, DdNode * f, int i ); 940 extern int Cudd_EquivDC( DdManager * dd, DdNode * F, DdNode * G, DdNode * D ); 941 extern int Cudd_bddLeqUnless( DdManager * dd, DdNode * f, DdNode * g, DdNode * D ); 942 extern int Cudd_EqualSupNorm( DdManager * dd, DdNode * f, DdNode * g, CUDD_VALUE_TYPE tolerance, int pr ); 943 extern DdNode * Cudd_bddMakePrime( DdManager * dd, DdNode * cube, DdNode * f ); 944 extern double * Cudd_CofMinterm( DdManager * dd, DdNode * node ); 945 extern DdNode * Cudd_SolveEqn( DdManager * bdd, DdNode * F, DdNode * Y, DdNode ** G, int ** yIndex, int n ); 946 extern DdNode * Cudd_VerifySol( DdManager * bdd, DdNode * F, DdNode ** G, int * yIndex, int n ); 947 extern DdNode * Cudd_SplitSet( DdManager * manager, DdNode * S, DdNode ** xVars, int n, double m ); 948 extern DdNode * Cudd_SubsetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold ); 949 extern DdNode * Cudd_SupersetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold ); 950 extern DdNode * Cudd_SubsetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit ); 951 extern DdNode * Cudd_SupersetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit ); 952 extern void Cudd_SymmProfile( DdManager * table, int lower, int upper ); 953 extern unsigned int Cudd_Prime( unsigned int p ); 954 extern int Cudd_PrintMinterm( DdManager * manager, DdNode * node ); 955 extern int Cudd_bddPrintCover( DdManager * dd, DdNode * l, DdNode * u ); 956 extern int Cudd_PrintDebug( DdManager * dd, DdNode * f, int n, int pr ); 957 extern int Cudd_DagSize( DdNode * node ); 958 extern int Cudd_EstimateCofactor( DdManager * dd, DdNode * node, int i, int phase ); 959 extern int Cudd_EstimateCofactorSimple( DdNode * node, int i ); 960 extern int Cudd_SharingSize( DdNode ** nodeArray, int n ); 961 extern double Cudd_CountMinterm( DdManager * manager, DdNode * node, int nvars ); 962 extern int Cudd_EpdCountMinterm( DdManager * manager, DdNode * node, int nvars, EpDouble * epd ); 963 extern double Cudd_CountPath( DdNode * node ); 964 extern double Cudd_CountPathsToNonZero( DdNode * node ); 965 extern DdNode * Cudd_Support( DdManager * dd, DdNode * f ); 966 extern int * Cudd_SupportIndex( DdManager * dd, DdNode * f ); 967 extern int Cudd_SupportSize( DdManager * dd, DdNode * f ); 968 extern DdNode * Cudd_VectorSupport( DdManager * dd, DdNode ** F, int n ); 969 extern int * Cudd_VectorSupportIndex( DdManager * dd, DdNode ** F, int n ); 970 extern int Cudd_VectorSupportSize( DdManager * dd, DdNode ** F, int n ); 971 extern int Cudd_ClassifySupport( DdManager * dd, DdNode * f, DdNode * g, DdNode ** common, DdNode ** onlyF, DdNode ** onlyG ); 972 extern int Cudd_CountLeaves( DdNode * node ); 973 extern int Cudd_bddPickOneCube( DdManager * ddm, DdNode * node, char * string ); 974 extern DdNode * Cudd_bddPickOneMinterm( DdManager * dd, DdNode * f, DdNode ** vars, int n ); 975 extern DdNode ** Cudd_bddPickArbitraryMinterms( DdManager * dd, DdNode * f, DdNode ** vars, int n, int k ); 976 extern DdNode * Cudd_SubsetWithMaskVars( DdManager * dd, DdNode * f, DdNode ** vars, int nvars, DdNode ** maskVars, int mvars ); 977 extern DdGen * Cudd_FirstCube( DdManager * dd, DdNode * f, int ** cube, CUDD_VALUE_TYPE * value ); 978 extern int Cudd_NextCube( DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value ); 979 extern DdGen * Cudd_FirstPrime(DdManager * dd, DdNode * l, DdNode * u, int ** cube ); 980 extern int Cudd_NextPrime(DdGen * gen, int ** cube ); 981 extern DdNode * Cudd_bddComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n ); 982 extern DdNode * Cudd_addComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n ); 983 extern DdNode * Cudd_CubeArrayToBdd( DdManager * dd, int * array ); 984 extern int Cudd_BddToCubeArray( DdManager * dd, DdNode * cube, int * array ); 985 extern DdGen * Cudd_FirstNode( DdManager * dd, DdNode * f, DdNode ** node ); 986 extern int Cudd_NextNode( DdGen * gen, DdNode ** node ); 987 extern int Cudd_GenFree( DdGen * gen ); 988 extern int Cudd_IsGenEmpty( DdGen * gen ); 989 extern DdNode * Cudd_IndicesToCube( DdManager * dd, int * array, int n ); 990 extern void Cudd_PrintVersion( FILE * fp ); 991 extern double Cudd_AverageDistance( DdManager * dd ); 992 extern long Cudd_Random( void ); 993 extern void Cudd_Srandom( long seed ); 994 extern double Cudd_Density( DdManager * dd, DdNode * f, int nvars ); 995 extern void Cudd_OutOfMem( long size ); 996 extern int Cudd_zddCount( DdManager * zdd, DdNode * P ); 997 extern double Cudd_zddCountDouble( DdManager * zdd, DdNode * P ); 998 extern DdNode * Cudd_zddProduct( DdManager * dd, DdNode * f, DdNode * g ); 999 extern DdNode * Cudd_zddUnateProduct( DdManager * dd, DdNode * f, DdNode * g ); 1000 extern DdNode * Cudd_zddWeakDiv( DdManager * dd, DdNode * f, DdNode * g ); 1001 extern DdNode * Cudd_zddDivide( DdManager * dd, DdNode * f, DdNode * g ); 1002 extern DdNode * Cudd_zddWeakDivF( DdManager * dd, DdNode * f, DdNode * g ); 1003 extern DdNode * Cudd_zddDivideF( DdManager * dd, DdNode * f, DdNode * g ); 1004 extern DdNode * Cudd_zddComplement( DdManager * dd, DdNode * node ); 1005 extern MtrNode * Cudd_MakeZddTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type ); 1006 extern DdNode * Cudd_zddIsop( DdManager * dd, DdNode * L, DdNode * U, DdNode ** zdd_I ); 1007 extern DdNode * Cudd_bddIsop( DdManager * dd, DdNode * L, DdNode * U ); 1008 extern DdNode * Cudd_MakeBddFromZddCover( DdManager * dd, DdNode * node ); 1009 extern int Cudd_zddDagSize( DdNode * p_node ); 1010 extern double Cudd_zddCountMinterm( DdManager * zdd, DdNode * node, int path ); 1011 extern void Cudd_zddPrintSubtable( DdManager * table ); 1012 extern DdNode * Cudd_zddPortFromBdd( DdManager * dd, DdNode * B ); 1013 extern DdNode * Cudd_zddPortToBdd( DdManager * dd, DdNode * f ); 1014 extern int Cudd_zddReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize ); 1015 extern int Cudd_zddShuffleHeap( DdManager * table, int * permutation ); 1016 extern DdNode * Cudd_zddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h ); 1017 extern DdNode * Cudd_zddUnion( DdManager * dd, DdNode * P, DdNode * Q ); 1018 extern DdNode * Cudd_zddIntersect( DdManager * dd, DdNode * P, DdNode * Q ); 1019 extern DdNode * Cudd_zddDiff( DdManager * dd, DdNode * P, DdNode * Q ); 1020 extern DdNode * Cudd_zddDiffConst( DdManager * zdd, DdNode * P, DdNode * Q ); 1021 extern DdNode * Cudd_zddSubset1( DdManager * dd, DdNode * P, int var ); 1022 extern DdNode * Cudd_zddSubset0( DdManager * dd, DdNode * P, int var ); 1023 extern DdNode * Cudd_zddChange( DdManager * dd, DdNode * P, int var ); 1024 extern void Cudd_zddSymmProfile( DdManager * table, int lower, int upper ); 1025 extern int Cudd_zddPrintMinterm( DdManager * zdd, DdNode * node ); 1026 extern int Cudd_zddPrintCover( DdManager * zdd, DdNode * node ); 1027 extern int Cudd_zddPrintDebug( DdManager * zdd, DdNode * f, int n, int pr ); 1028 extern DdGen * Cudd_zddFirstPath( DdManager * zdd, DdNode * f, int ** path ); 1029 extern int Cudd_zddNextPath( DdGen * gen, int ** path ); 1030 extern char * Cudd_zddCoverPathToString( DdManager * zdd, int * path, char * str ); 1031 extern int Cudd_zddDumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp ); 1032 extern int Cudd_bddSetPiVar( DdManager * dd, int index ); 1033 extern int Cudd_bddSetPsVar( DdManager * dd, int index ); 1034 extern int Cudd_bddSetNsVar( DdManager * dd, int index ); 1035 extern int Cudd_bddIsPiVar( DdManager * dd, int index ); 1036 extern int Cudd_bddIsPsVar( DdManager * dd, int index ); 1037 extern int Cudd_bddIsNsVar( DdManager * dd, int index ); 1038 extern int Cudd_bddSetPairIndex( DdManager * dd, int index, int pairIndex ); 1039 extern int Cudd_bddReadPairIndex( DdManager * dd, int index ); 1040 extern int Cudd_bddSetVarToBeGrouped( DdManager * dd, int index ); 1041 extern int Cudd_bddSetVarHardGroup( DdManager * dd, int index ); 1042 extern int Cudd_bddResetVarToBeGrouped( DdManager * dd, int index ); 1043 extern int Cudd_bddIsVarToBeGrouped( DdManager * dd, int index ); 1044 extern int Cudd_bddSetVarToBeUngrouped( DdManager * dd, int index ); 1045 extern int Cudd_bddIsVarToBeUngrouped( DdManager * dd, int index ); 1046 extern int Cudd_bddIsVarHardGroup( DdManager * dd, int index ); 1047 1048 /**AutomaticEnd***************************************************************/ 1049 1050 1051 1052 ABC_NAMESPACE_HEADER_END 1053 1054 #endif /* _CUDD */ 1055