distr/cudd/cudd.h

   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 _CUDD
  58 #define _CUDD
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Nested includes                                                           */
  62 /*---------------------------------------------------------------------------*/
  63
  64 #include "mtr.h"
  65 #include "epd.h"
  66
  67 #ifdef __cplusplus
  68 extern "C" {
  69 #endif
  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 };
 287
 288 #ifdef __osf__
 289 #pragma pointer_size restore
 290 #endif
 291
 292 typedef struct DdManager DdManager;
 293
 294 typedef struct DdGen DdGen;
 295
 296 /* These typedefs for arbitrary precision arithmetic should agree with
 297 ** the corresponding constant definitions above. */
 298 #if SIZEOF_LONG == 8
 299 typedef unsigned int DdApaDigit;
 300 typedef unsigned long int DdApaDoubleDigit;
 301 #else
 302 typedef unsigned short int DdApaDigit;
 303 typedef unsigned int DdApaDoubleDigit;
 304 #endif
 305 typedef DdApaDigit * DdApaNumber;
 306
 307 /* Return type for function computing two-literal clauses. */
 308 typedef struct DdTlcInfo DdTlcInfo;
 309
 310 /* Type of hook function. */
 311 typedef int (*DD_HFP)(DdManager *, const char *, void *);
 312 /* Type of priority function */
 313 typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **,
 314                             DdNode **);
 315 /* Type of apply operator. */
 316 typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
 317 /* Type of monadic apply operator. */
 318 typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
 319 /* Types of cache tag functions. */
 320 typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
 321 typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
 322 /* Type of memory-out function. */
 323 typedef void (*DD_OOMFP)(long);
 324 /* Type of comparison function for qsort. */
 325 typedef int (*DD_QSFP)(const void *, const void *);
 326
 327 /*---------------------------------------------------------------------------*/
 328 /* Variable declarations                                                     */
 329 /*---------------------------------------------------------------------------*/
 330
 331
 332 /*---------------------------------------------------------------------------*/
 333 /* Macro declarations                                                        */
 334 /*---------------------------------------------------------------------------*/
 335
 336
 337 /**Macro***********************************************************************
 338
 339   Synopsis     [Returns 1 if the node is a constant node.]
 340
 341   Description  [Returns 1 if the node is a constant node (rather than an
 342   internal node). All constant nodes have the same index
 343   (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either
 344   regular or complemented.]
 345
 346   SideEffects  [none]
 347
 348   SeeAlso      []
 349
 350 ******************************************************************************/
 351 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
 352
 353
 354 /**Macro***********************************************************************
 355
 356   Synopsis     [Complements a DD.]
 357
 358   Description  [Complements a DD by flipping the complement attribute of
 359   the pointer (the least significant bit).]
 360
 361   SideEffects  [none]
 362
 363   SeeAlso      [Cudd_NotCond]
 364
 365 ******************************************************************************/
 366 #define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
 367
 368
 369 /**Macro***********************************************************************
 370
 371   Synopsis     [Complements a DD if a condition is true.]
 372
 373   Description  [Complements a DD if condition c is true; c should be
 374   either 0 or 1, because it is used directly (for efficiency). If in
 375   doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]
 376
 377   SideEffects  [none]
 378
 379   SeeAlso      [Cudd_Not]
 380
 381 ******************************************************************************/
 382 #define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))
 383
 384
 385 /**Macro***********************************************************************
 386
 387   Synopsis     [Returns the regular version of a pointer.]
 388
 389   Description  []
 390
 391   SideEffects  [none]
 392
 393   SeeAlso      [Cudd_Complement Cudd_IsComplement]
 394
 395 ******************************************************************************/
 396 #define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
 397
 398
 399 /**Macro***********************************************************************
 400
 401   Synopsis     [Returns the complemented version of a pointer.]
 402
 403   Description  []
 404
 405   SideEffects  [none]
 406
 407   SeeAlso      [Cudd_Regular Cudd_IsComplement]
 408
 409 ******************************************************************************/
 410 #define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))
 411
 412
 413 /**Macro***********************************************************************
 414
 415   Synopsis     [Returns 1 if a pointer is complemented.]
 416
 417   Description  []
 418
 419   SideEffects  [none]
 420
 421   SeeAlso      [Cudd_Regular Cudd_Complement]
 422
 423 ******************************************************************************/
 424 #define Cudd_IsComplement(node) ((int) ((long) (node) & 01))
 425
 426
 427 /**Macro***********************************************************************
 428
 429   Synopsis     [Returns the then child of an internal node.]
 430
 431   Description  [Returns the then child of an internal node. If
 432   <code>node</code> is a constant node, the result is unpredictable.]
 433
 434   SideEffects  [none]
 435
 436   SeeAlso      [Cudd_E Cudd_V]
 437
 438 ******************************************************************************/
 439 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
 440
 441
 442 /**Macro***********************************************************************
 443
 444   Synopsis     [Returns the else child of an internal node.]
 445
 446   Description  [Returns the else child of an internal node. If
 447   <code>node</code> is a constant node, the result is unpredictable.]
 448
 449   SideEffects  [none]
 450
 451   SeeAlso      [Cudd_T Cudd_V]
 452
 453 ******************************************************************************/
 454 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
 455
 456
 457 /**Macro***********************************************************************
 458
 459   Synopsis     [Returns the value of a constant node.]
 460
 461   Description  [Returns the value of a constant node. If
 462   <code>node</code> is an internal node, the result is unpredictable.]
 463
 464   SideEffects  [none]
 465
 466   SeeAlso      [Cudd_T Cudd_E]
 467
 468 ******************************************************************************/
 469 #define Cudd_V(node) ((Cudd_Regular(node))->type.value)
 470
 471
 472 /**Macro***********************************************************************
 473
 474   Synopsis     [Returns the current position in the order of variable
 475   index.]
 476
 477   Description [Returns the current position in the order of variable
 478   index. This macro is obsolete and is kept for compatibility. New
 479   applications should use Cudd_ReadPerm instead.]
 480
 481   SideEffects  [none]
 482
 483   SeeAlso      [Cudd_ReadPerm]
 484
 485 ******************************************************************************/
 486 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
 487
 488
 489 /**Macro***********************************************************************
 490
 491   Synopsis     [Iterates over the cubes of a decision diagram.]
 492
 493   Description  [Iterates over the cubes of a decision diagram f.
 494   <ul>
 495   <li> DdManager *manager;
 496   <li> DdNode *f;
 497   <li> DdGen *gen;
 498   <li> int *cube;
 499   <li> CUDD_VALUE_TYPE value;
 500   </ul>
 501   Cudd_ForeachCube allocates and frees the generator. Therefore the
 502   application should not try to do that. Also, the cube is freed at the
 503   end of Cudd_ForeachCube and hence is not available outside of the loop.<p>
 504   CAUTION: It is assumed that dynamic reordering will not occur while
 505   there are open generators. It is the user's responsibility to make sure
 506   that dynamic reordering does not occur. As long as new nodes are not created
 507   during generation, and dynamic reordering is not called explicitly,
 508   dynamic reordering will not occur. Alternatively, it is sufficient to
 509   disable dynamic reordering. It is a mistake to dispose of a diagram
 510   on which generation is ongoing.]
 511
 512   SideEffects  [none]
 513
 514   SeeAlso      [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree
 515   Cudd_IsGenEmpty Cudd_AutodynDisable]
 516
 517 ******************************************************************************/
 518 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
 519     for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
 520         Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
 521         (void) Cudd_NextCube(gen, &cube, &value))
 522
 523
 524 /**Macro***********************************************************************
 525
 526   Synopsis     [Iterates over the primes of a Boolean function.]
 527
 528   Description  [Iterates over the primes of a Boolean function producing
 529   a prime and irredundant cover.
 530   <ul>
 531   <li> DdManager *manager;
 532   <li> DdNode *l;
 533   <li> DdNode *u;
 534   <li> DdGen *gen;
 535   <li> int *cube;
 536   </ul>
 537   The Boolean function is described by an upper bound and a lower bound.  If
 538   the function is completely specified, the two bounds coincide.
 539   Cudd_ForeachPrime allocates and frees the generator.  Therefore the
 540   application should not try to do that.  Also, the cube is freed at the
 541   end of Cudd_ForeachPrime and hence is not available outside of the loop.<p>
 542   CAUTION: It is a mistake to change a diagram on which generation is ongoing.]
 543
 544   SideEffects  [none]
 545
 546   SeeAlso      [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree
 547   Cudd_IsGenEmpty]
 548
 549 ******************************************************************************/
 550 #define Cudd_ForeachPrime(manager, l, u, gen, cube)\
 551     for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
 552         Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
 553         (void) Cudd_NextPrime(gen, &cube))
 554
 555
 556 /**Macro***********************************************************************
 557
 558   Synopsis     [Iterates over the nodes of a decision diagram.]
 559
 560   Description  [Iterates over the nodes of a decision diagram f.
 561   <ul>
 562   <li> DdManager *manager;
 563   <li> DdNode *f;
 564   <li> DdGen *gen;
 565   <li> DdNode *node;
 566   </ul>
 567   The nodes are returned in a seemingly random order.
 568   Cudd_ForeachNode allocates and frees the generator. Therefore the
 569   application should not try to do that.<p>
 570   CAUTION: It is assumed that dynamic reordering will not occur while
 571   there are open generators. It is the user's responsibility to make sure
 572   that dynamic reordering does not occur. As long as new nodes are not created
 573   during generation, and dynamic reordering is not called explicitly,
 574   dynamic reordering will not occur. Alternatively, it is sufficient to
 575   disable dynamic reordering. It is a mistake to dispose of a diagram
 576   on which generation is ongoing.]
 577
 578   SideEffects  [none]
 579
 580   SeeAlso      [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree
 581   Cudd_IsGenEmpty Cudd_AutodynDisable]
 582
 583 ******************************************************************************/
 584 #define Cudd_ForeachNode(manager, f, gen, node)\
 585     for((gen) = Cudd_FirstNode(manager, f, &node);\
 586         Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
 587         (void) Cudd_NextNode(gen, &node))
 588
 589
 590 /**Macro***********************************************************************
 591
 592   Synopsis     [Iterates over the paths of a ZDD.]
 593
 594   Description  [Iterates over the paths of a ZDD f.
 595   <ul>
 596   <li> DdManager *manager;
 597   <li> DdNode *f;
 598   <li> DdGen *gen;
 599   <li> int *path;
 600   </ul>
 601   Cudd_zddForeachPath allocates and frees the generator. Therefore the
 602   application should not try to do that. Also, the path is freed at the
 603   end of Cudd_zddForeachPath and hence is not available outside of the loop.<p>
 604   CAUTION: It is assumed that dynamic reordering will not occur while
 605   there are open generators.  It is the user's responsibility to make sure
 606   that dynamic reordering does not occur.  As long as new nodes are not created
 607   during generation, and dynamic reordering is not called explicitly,
 608   dynamic reordering will not occur.  Alternatively, it is sufficient to
 609   disable dynamic reordering.  It is a mistake to dispose of a diagram
 610   on which generation is ongoing.]
 611
 612   SideEffects  [none]
 613
 614   SeeAlso      [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree
 615   Cudd_IsGenEmpty Cudd_AutodynDisable]
 616
 617 ******************************************************************************/
 618 #define Cudd_zddForeachPath(manager, f, gen, path)\
 619     for((gen) = Cudd_zddFirstPath(manager, f, &path);\
 620         Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
 621         (void) Cudd_zddNextPath(gen, &path))
 622
 623
 624
 625 /**AutomaticStart*************************************************************/
 626
 627 /*---------------------------------------------------------------------------*/
 628 /* Function prototypes                                                       */
 629 /*---------------------------------------------------------------------------*/
 630
 631 extern DdNode * Cudd_addNewVar (DdManager *dd);
 632 extern DdNode * Cudd_addNewVarAtLevel (DdManager *dd, int level);
 633 extern DdNode * Cudd_bddNewVar (DdManager *dd);
 634 extern DdNode * Cudd_bddNewVarAtLevel (DdManager *dd, int level);
 635 extern DdNode * Cudd_addIthVar (DdManager *dd, int i);
 636 extern DdNode * Cudd_bddIthVar (DdManager *dd, int i);
 637 extern DdNode * Cudd_zddIthVar (DdManager *dd, int i);
 638 extern int Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity);
 639 extern DdNode * Cudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c);
 640 extern int Cudd_IsNonConstant (DdNode *f);
 641 extern void Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method);
 642 extern void Cudd_AutodynDisable (DdManager *unique);
 643 extern int Cudd_ReorderingStatus (DdManager *unique, Cudd_ReorderingType *method);
 644 extern void Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method);
 645 extern void Cudd_AutodynDisableZdd (DdManager *unique);
 646 extern int Cudd_ReorderingStatusZdd (DdManager *unique, Cudd_ReorderingType *method);
 647 extern int Cudd_zddRealignmentEnabled (DdManager *unique);
 648 extern void Cudd_zddRealignEnable (DdManager *unique);
 649 extern void Cudd_zddRealignDisable (DdManager *unique);
 650 extern int Cudd_bddRealignmentEnabled (DdManager *unique);
 651 extern void Cudd_bddRealignEnable (DdManager *unique);
 652 extern void Cudd_bddRealignDisable (DdManager *unique);
 653 extern DdNode * Cudd_ReadOne (DdManager *dd);
 654 extern DdNode * Cudd_ReadZddOne (DdManager *dd, int i);
 655 extern DdNode * Cudd_ReadZero (DdManager *dd);
 656 extern DdNode * Cudd_ReadLogicZero (DdManager *dd);
 657 extern DdNode * Cudd_ReadPlusInfinity (DdManager *dd);
 658 extern DdNode * Cudd_ReadMinusInfinity (DdManager *dd);
 659 extern DdNode * Cudd_ReadBackground (DdManager *dd);
 660 extern void Cudd_SetBackground (DdManager *dd, DdNode *bck);
 661 extern unsigned int Cudd_ReadCacheSlots (DdManager *dd);
 662 extern double Cudd_ReadCacheUsedSlots (DdManager * dd);
 663 extern double Cudd_ReadCacheLookUps (DdManager *dd);
 664 extern double Cudd_ReadCacheHits (DdManager *dd);
 665 extern double Cudd_ReadRecursiveCalls (DdManager * dd);
 666 extern unsigned int Cudd_ReadMinHit (DdManager *dd);
 667 extern void Cudd_SetMinHit (DdManager *dd, unsigned int hr);
 668 extern unsigned int Cudd_ReadLooseUpTo (DdManager *dd);
 669 extern void Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut);
 670 extern unsigned int Cudd_ReadMaxCache (DdManager *dd);
 671 extern unsigned int Cudd_ReadMaxCacheHard (DdManager *dd);
 672 extern void Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc);
 673 extern int Cudd_ReadSize (DdManager *dd);
 674 extern int Cudd_ReadZddSize (DdManager *dd);
 675 extern unsigned int Cudd_ReadSlots (DdManager *dd);
 676 extern double Cudd_ReadUsedSlots (DdManager * dd);
 677 extern double Cudd_ExpectedUsedSlots (DdManager * dd);
 678 extern unsigned int Cudd_ReadKeys (DdManager *dd);
 679 extern unsigned int Cudd_ReadDead (DdManager *dd);
 680 extern unsigned int Cudd_ReadMinDead (DdManager *dd);
 681 extern int Cudd_ReadReorderings (DdManager *dd);
 682 extern long Cudd_ReadReorderingTime (DdManager * dd);
 683 extern int Cudd_ReadGarbageCollections (DdManager * dd);
 684 extern long Cudd_ReadGarbageCollectionTime (DdManager * dd);
 685 extern double Cudd_ReadNodesFreed (DdManager * dd);
 686 extern double Cudd_ReadNodesDropped (DdManager * dd);
 687 extern double Cudd_ReadUniqueLookUps (DdManager * dd);
 688 extern double Cudd_ReadUniqueLinks (DdManager * dd);
 689 extern int Cudd_ReadSiftMaxVar (DdManager *dd);
 690 extern void Cudd_SetSiftMaxVar (DdManager *dd, int smv);
 691 extern int Cudd_ReadSiftMaxSwap (DdManager *dd);
 692 extern void Cudd_SetSiftMaxSwap (DdManager *dd, int sms);
 693 extern double Cudd_ReadMaxGrowth (DdManager *dd);
 694 extern void Cudd_SetMaxGrowth (DdManager *dd, double mg);
 695 extern double Cudd_ReadMaxGrowthAlternate (DdManager * dd);
 696 extern void Cudd_SetMaxGrowthAlternate (DdManager * dd, double mg);
 697 extern int Cudd_ReadReorderingCycle (DdManager * dd);
 698 extern void Cudd_SetReorderingCycle (DdManager * dd, int cycle);
 699 extern MtrNode * Cudd_ReadTree (DdManager *dd);
 700 extern void Cudd_SetTree (DdManager *dd, MtrNode *tree);
 701 extern void Cudd_FreeTree (DdManager *dd);
 702 extern MtrNode * Cudd_ReadZddTree (DdManager *dd);
 703 extern void Cudd_SetZddTree (DdManager *dd, MtrNode *tree);
 704 extern void Cudd_FreeZddTree (DdManager *dd);
 705 extern unsigned int Cudd_NodeReadIndex (DdNode *node);
 706 extern int Cudd_ReadPerm (DdManager *dd, int i);
 707 extern int Cudd_ReadPermZdd (DdManager *dd, int i);
 708 extern int Cudd_ReadInvPerm (DdManager *dd, int i);
 709 extern int Cudd_ReadInvPermZdd (DdManager *dd, int i);
 710 extern DdNode * Cudd_ReadVars (DdManager *dd, int i);
 711 extern CUDD_VALUE_TYPE Cudd_ReadEpsilon (DdManager *dd);
 712 extern void Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep);
 713 extern Cudd_AggregationType Cudd_ReadGroupcheck (DdManager *dd);
 714 extern void Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc);
 715 extern int Cudd_GarbageCollectionEnabled (DdManager *dd);
 716 extern void Cudd_EnableGarbageCollection (DdManager *dd);
 717 extern void Cudd_DisableGarbageCollection (DdManager *dd);
 718 extern int Cudd_DeadAreCounted (DdManager *dd);
 719 extern void Cudd_TurnOnCountDead (DdManager *dd);
 720 extern void Cudd_TurnOffCountDead (DdManager *dd);
 721 extern int Cudd_ReadRecomb (DdManager *dd);
 722 extern void Cudd_SetRecomb (DdManager *dd, int recomb);
 723 extern int Cudd_ReadSymmviolation (DdManager *dd);
 724 extern void Cudd_SetSymmviolation (DdManager *dd, int symmviolation);
 725 extern int Cudd_ReadArcviolation (DdManager *dd);
 726 extern void Cudd_SetArcviolation (DdManager *dd, int arcviolation);
 727 extern int Cudd_ReadPopulationSize (DdManager *dd);
 728 extern void Cudd_SetPopulationSize (DdManager *dd, int populationSize);
 729 extern int Cudd_ReadNumberXovers (DdManager *dd);
 730 extern void Cudd_SetNumberXovers (DdManager *dd, int numberXovers);
 731 extern unsigned long Cudd_ReadMemoryInUse (DdManager *dd);
 732 extern int Cudd_PrintInfo (DdManager *dd, FILE *fp);
 733 extern long Cudd_ReadPeakNodeCount (DdManager *dd);
 734 extern int Cudd_ReadPeakLiveNodeCount (DdManager * dd);
 735 extern long Cudd_ReadNodeCount (DdManager *dd);
 736 extern long Cudd_zddReadNodeCount (DdManager *dd);
 737 extern int Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
 738 extern int Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
 739 extern int Cudd_IsInHook (DdManager * dd, DD_HFP f, Cudd_HookType where);
 740 extern int Cudd_StdPreReordHook (DdManager *dd, const char *str, void *data);
 741 extern int Cudd_StdPostReordHook (DdManager *dd, const char *str, void *data);
 742 extern int Cudd_EnableReorderingReporting (DdManager *dd);
 743 extern int Cudd_DisableReorderingReporting (DdManager *dd);
 744 extern int Cudd_ReorderingReporting (DdManager *dd);
 745 extern Cudd_ErrorType Cudd_ReadErrorCode (DdManager *dd);
 746 extern void Cudd_ClearErrorCode (DdManager *dd);
 747 extern FILE * Cudd_ReadStdout (DdManager *dd);
 748 extern void Cudd_SetStdout (DdManager *dd, FILE *fp);
 749 extern FILE * Cudd_ReadStderr (DdManager *dd);
 750 extern void Cudd_SetStderr (DdManager *dd, FILE *fp);
 751 extern unsigned int Cudd_ReadNextReordering (DdManager *dd);
 752 extern void Cudd_SetNextReordering (DdManager *dd, unsigned int next);
 753 extern double Cudd_ReadSwapSteps (DdManager *dd);
 754 extern unsigned int Cudd_ReadMaxLive (DdManager *dd);
 755 extern void Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive);
 756 extern unsigned long Cudd_ReadMaxMemory (DdManager *dd);
 757 extern void Cudd_SetMaxMemory (DdManager *dd, unsigned long maxMemory);
 758 extern int Cudd_bddBindVar (DdManager *dd, int index);
 759 extern int Cudd_bddUnbindVar (DdManager *dd, int index);
 760 extern int Cudd_bddVarIsBound (DdManager *dd, int index);
 761 extern DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 762 extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 763 extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 764 extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
 765 extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g);
 766 extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g);
 767 extern DdNode * Cudd_addThreshold (DdManager *dd, DdNode **f, DdNode **g);
 768 extern DdNode * Cudd_addSetNZ (DdManager *dd, DdNode **f, DdNode **g);
 769 extern DdNode * Cudd_addDivide (DdManager *dd, DdNode **f, DdNode **g);
 770 extern DdNode * Cudd_addMinus (DdManager *dd, DdNode **f, DdNode **g);
 771 extern DdNode * Cudd_addMinimum (DdManager *dd, DdNode **f, DdNode **g);
 772 extern DdNode * Cudd_addMaximum (DdManager *dd, DdNode **f, DdNode **g);
 773 extern DdNode * Cudd_addOneZeroMaximum (DdManager *dd, DdNode **f, DdNode **g);
 774 extern DdNode * Cudd_addDiff (DdManager *dd, DdNode **f, DdNode **g);
 775 extern DdNode * Cudd_addAgreement (DdManager *dd, DdNode **f, DdNode **g);
 776 extern DdNode * Cudd_addOr (DdManager *dd, DdNode **f, DdNode **g);
 777 extern DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g);
 778 extern DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g);
 779 extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
 780 extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
 781 extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 782 extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
 783 extern DdNode * Cudd_addFindMax (DdManager *dd, DdNode *f);
 784 extern DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f);
 785 extern DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit);
 786 extern DdNode * Cudd_addScalarInverse (DdManager *dd, DdNode *f, DdNode *epsilon);
 787 extern DdNode * Cudd_addIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 788 extern DdNode * Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 789 extern DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g);
 790 extern int Cudd_addLeq (DdManager * dd, DdNode * f, DdNode * g);
 791 extern DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f);
 792 extern DdNode * Cudd_addNegate (DdManager *dd, DdNode *f);
 793 extern DdNode * Cudd_addRoundOff (DdManager *dd, DdNode *f, int N);
 794 extern DdNode * Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n);
 795 extern DdNode * Cudd_addResidue (DdManager *dd, int n, int m, int options, int top);
 796 extern DdNode * Cudd_bddAndAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
 797 extern DdNode * Cudd_bddAndAbstractLimit (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit);
 798 extern int Cudd_ApaNumberOfDigits (int binaryDigits);
 799 extern DdApaNumber Cudd_NewApaNumber (int digits);
 800 extern void Cudd_ApaCopy (int digits, DdApaNumber source, DdApaNumber dest);
 801 extern DdApaDigit Cudd_ApaAdd (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum);
 802 extern DdApaDigit Cudd_ApaSubtract (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff);
 803 extern DdApaDigit Cudd_ApaShortDivision (int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient);
 804 extern unsigned int Cudd_ApaIntDivision (int  digits, DdApaNumber dividend, unsigned int  divisor, DdApaNumber  quotient);
 805 extern void Cudd_ApaShiftRight (int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b);
 806 extern void Cudd_ApaSetToLiteral (int digits, DdApaNumber number, DdApaDigit literal);
 807 extern void Cudd_ApaPowerOfTwo (int digits, DdApaNumber number, int power);
 808 extern int Cudd_ApaCompare (int digitsFirst, DdApaNumber  first, int digitsSecond, DdApaNumber  second);
 809 extern int Cudd_ApaCompareRatios (int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen);
 810 extern int Cudd_ApaPrintHex (FILE *fp, int digits, DdApaNumber number);
 811 extern int Cudd_ApaPrintDecimal (FILE *fp, int digits, DdApaNumber number);
 812 extern int Cudd_ApaPrintExponential (FILE * fp, int  digits, DdApaNumber  number, int precision);
 813 extern DdApaNumber Cudd_ApaCountMinterm (DdManager *manager, DdNode *node, int nvars, int *digits);
 814 extern int Cudd_ApaPrintMinterm (FILE *fp, DdManager *dd, DdNode *node, int nvars);
 815 extern int Cudd_ApaPrintMintermExp (FILE * fp, DdManager * dd, DdNode * node, int  nvars, int precision);
 816 extern int Cudd_ApaPrintDensity (FILE * fp, DdManager * dd, DdNode * node, int  nvars);
 817 extern DdNode * Cudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
 818 extern DdNode * Cudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
 819 extern DdNode * Cudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
 820 extern DdNode * Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
 821 extern DdNode * Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
 822 extern DdNode * Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
 823 extern DdNode * Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 824 extern DdNode * Cudd_bddXorExistAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
 825 extern DdNode * Cudd_bddUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
 826 extern DdNode * Cudd_bddBooleanDiff (DdManager *manager, DdNode *f, int x);
 827 extern int Cudd_bddVarIsDependent (DdManager *dd, DdNode *f, DdNode *var);
 828 extern double Cudd_bddCorrelation (DdManager *manager, DdNode *f, DdNode *g);
 829 extern double Cudd_bddCorrelationWeights (DdManager *manager, DdNode *f, DdNode *g, double *prob);
 830 extern DdNode * Cudd_bddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 831 extern DdNode * Cudd_bddIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
 832 extern DdNode * Cudd_bddIntersect (DdManager *dd, DdNode *f, DdNode *g);
 833 extern DdNode * Cudd_bddAnd (DdManager *dd, DdNode *f, DdNode *g);
 834 extern DdNode * Cudd_bddAndLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
 835 extern DdNode * Cudd_bddOr (DdManager *dd, DdNode *f, DdNode *g);
 836 extern DdNode * Cudd_bddNand (DdManager *dd, DdNode *f, DdNode *g);
 837 extern DdNode * Cudd_bddNor (DdManager *dd, DdNode *f, DdNode *g);
 838 extern DdNode * Cudd_bddXor (DdManager *dd, DdNode *f, DdNode *g);
 839 extern DdNode * Cudd_bddXnor (DdManager *dd, DdNode *f, DdNode *g);
 840 extern int Cudd_bddLeq (DdManager *dd, DdNode *f, DdNode *g);
 841 extern DdNode * Cudd_addBddThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
 842 extern DdNode * Cudd_addBddStrictThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
 843 extern DdNode * Cudd_addBddInterval (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper);
 844 extern DdNode * Cudd_addBddIthBit (DdManager *dd, DdNode *f, int bit);
 845 extern DdNode * Cudd_BddToAdd (DdManager *dd, DdNode *B);
 846 extern DdNode * Cudd_addBddPattern (DdManager *dd, DdNode *f);
 847 extern DdNode * Cudd_bddTransfer (DdManager *ddSource, DdManager *ddDestination, DdNode *f);
 848 extern int Cudd_DebugCheck (DdManager *table);
 849 extern int Cudd_CheckKeys (DdManager *table);
 850 extern DdNode * Cudd_bddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
 851 extern DdNode * Cudd_bddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
 852 extern DdNode * Cudd_Cofactor (DdManager *dd, DdNode *f, DdNode *g);
 853 extern DdNode * Cudd_bddCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
 854 extern DdNode * Cudd_addCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
 855 extern DdNode * Cudd_addPermute (DdManager *manager, DdNode *node, int *permut);
 856 extern DdNode * Cudd_addSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
 857 extern DdNode * Cudd_bddPermute (DdManager *manager, DdNode *node, int *permut);
 858 extern DdNode * Cudd_bddVarMap (DdManager *manager, DdNode *f);
 859 extern int Cudd_SetVarMap (DdManager *manager, DdNode **x, DdNode **y, int n);
 860 extern DdNode * Cudd_bddSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
 861 extern DdNode * Cudd_bddAdjPermuteX (DdManager *dd, DdNode *B, DdNode **x, int n);
 862 extern DdNode * Cudd_addVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
 863 extern DdNode * Cudd_addGeneralVectorCompose (DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff);
 864 extern DdNode * Cudd_addNonSimCompose (DdManager *dd, DdNode *f, DdNode **vector);
 865 extern DdNode * Cudd_bddVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
 866 extern int Cudd_bddApproxConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
 867 extern int Cudd_bddApproxDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
 868 extern int Cudd_bddIterConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
 869 extern int Cudd_bddIterDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
 870 extern int Cudd_bddGenConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
 871 extern int Cudd_bddGenDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
 872 extern int Cudd_bddVarConjDecomp (DdManager *dd, DdNode * f, DdNode ***conjuncts);
 873 extern int Cudd_bddVarDisjDecomp (DdManager *dd, DdNode * f, DdNode ***disjuncts);
 874 extern DdNode * Cudd_FindEssential (DdManager *dd, DdNode *f);
 875 extern int Cudd_bddIsVarEssential (DdManager *manager, DdNode *f, int id, int phase);
 876 extern DdTlcInfo * Cudd_FindTwoLiteralClauses (DdManager * dd, DdNode * f);
 877 extern int Cudd_PrintTwoLiteralClauses (DdManager * dd, DdNode * f, char **names, FILE *fp);
 878 extern int Cudd_ReadIthClause (DdTlcInfo * tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2);
 879 extern void Cudd_tlcInfoFree (DdTlcInfo * t);
 880 extern int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv);
 881 extern int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp, int mv);
 882 extern int Cudd_DumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
 883 extern int Cudd_DumpDaVinci (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
 884 extern int Cudd_DumpDDcal (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
 885 extern int Cudd_DumpFactoredForm (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
 886 extern DdNode * Cudd_bddConstrain (DdManager *dd, DdNode *f, DdNode *c);
 887 extern DdNode * Cudd_bddRestrict (DdManager *dd, DdNode *f, DdNode *c);
 888 extern DdNode * Cudd_bddNPAnd (DdManager *dd, DdNode *f, DdNode *c);
 889 extern DdNode * Cudd_addConstrain (DdManager *dd, DdNode *f, DdNode *c);
 890 extern DdNode ** Cudd_bddConstrainDecomp (DdManager *dd, DdNode *f);
 891 extern DdNode * Cudd_addRestrict (DdManager *dd, DdNode *f, DdNode *c);
 892 extern DdNode ** Cudd_bddCharToVect (DdManager *dd, DdNode *f);
 893 extern DdNode * Cudd_bddLICompaction (DdManager *dd, DdNode *f, DdNode *c);
 894 extern DdNode * Cudd_bddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
 895 extern DdNode * Cudd_bddMinimize (DdManager *dd, DdNode *f, DdNode *c);
 896 extern DdNode * Cudd_SubsetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
 897 extern DdNode * Cudd_SupersetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
 898 extern MtrNode * Cudd_MakeTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
 899 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);
 900 extern DdManager * Cudd_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory);
 901 extern void Cudd_Quit (DdManager *unique);
 902 extern int Cudd_PrintLinear (DdManager *table);
 903 extern int Cudd_ReadLinear (DdManager *table, int x, int y);
 904 extern DdNode * Cudd_bddLiteralSetIntersection (DdManager *dd, DdNode *f, DdNode *g);
 905 extern DdNode * Cudd_addMatrixMultiply (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
 906 extern DdNode * Cudd_addTimesPlus (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
 907 extern DdNode * Cudd_addTriangle (DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz);
 908 extern DdNode * Cudd_addOuterSum (DdManager *dd, DdNode *M, DdNode *r, DdNode *c);
 909 extern DdNode * Cudd_PrioritySelect (DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pii, int n, DdNode * (*)(DdManager *, int, DdNode **, DdNode **, DdNode **));
 910 extern DdNode * Cudd_Xgty (DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y);
 911 extern DdNode * Cudd_Xeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
 912 extern DdNode * Cudd_addXeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
 913 extern DdNode * Cudd_Dxygtdxz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
 914 extern DdNode * Cudd_Dxygtdyz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
 915 extern DdNode * Cudd_Inequality (DdManager * dd, int  N, int c, DdNode ** x, DdNode ** y);
 916 extern DdNode * Cudd_Disequality (DdManager * dd, int  N, int c, DdNode ** x, DdNode ** y);
 917 extern DdNode * Cudd_bddInterval (DdManager * dd, int  N, DdNode ** x, unsigned int lowerB, unsigned int upperB);
 918 extern DdNode * Cudd_CProjection (DdManager *dd, DdNode *R, DdNode *Y);
 919 extern DdNode * Cudd_addHamming (DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars);
 920 extern int Cudd_MinHammingDist (DdManager *dd, DdNode *f, int *minterm, int upperBound);
 921 extern DdNode * Cudd_bddClosestCube (DdManager *dd, DdNode * f, DdNode *g, int *distance);
 922 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);
 923 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);
 924 extern void Cudd_Ref (DdNode *n);
 925 extern void Cudd_RecursiveDeref (DdManager *table, DdNode *n);
 926 extern void Cudd_IterDerefBdd (DdManager *table, DdNode *n);
 927 extern void Cudd_DelayedDerefBdd (DdManager * table, DdNode * n);
 928 extern void Cudd_RecursiveDerefZdd (DdManager *table, DdNode *n);
 929 extern void Cudd_Deref (DdNode *node);
 930 extern int Cudd_CheckZeroRef (DdManager *manager);
 931 extern int Cudd_ReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
 932 extern int Cudd_ShuffleHeap (DdManager *table, int *permutation);
 933 extern DdNode * Cudd_Eval (DdManager *dd, DdNode *f, int *inputs);
 934 extern DdNode * Cudd_ShortestPath (DdManager *manager, DdNode *f, int *weight, int *support, int *length);
 935 extern DdNode * Cudd_LargestCube (DdManager *manager, DdNode *f, int *length);
 936 extern int Cudd_ShortestLength (DdManager *manager, DdNode *f, int *weight);
 937 extern DdNode * Cudd_Decreasing (DdManager *dd, DdNode *f, int i);
 938 extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i);
 939 extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D);
 940 extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D);
 941 extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
 942 extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f);
 943 extern double * Cudd_CofMinterm (DdManager *dd, DdNode *node);
 944 extern DdNode * Cudd_SolveEqn (DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n);
 945 extern DdNode * Cudd_VerifySol (DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n);
 946 extern DdNode * Cudd_SplitSet (DdManager *manager, DdNode *S, DdNode **xVars, int n, double m);
 947 extern DdNode * Cudd_SubsetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
 948 extern DdNode * Cudd_SupersetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
 949 extern DdNode * Cudd_SubsetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
 950 extern DdNode * Cudd_SupersetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
 951 extern void Cudd_SymmProfile (DdManager *table, int lower, int upper);
 952 extern unsigned int Cudd_Prime (unsigned int p);
 953 extern int Cudd_PrintMinterm (DdManager *manager, DdNode *node);
 954 extern int Cudd_bddPrintCover (DdManager *dd, DdNode *l, DdNode *u);
 955 extern int Cudd_PrintDebug (DdManager *dd, DdNode *f, int n, int pr);
 956 extern int Cudd_DagSize (DdNode *node);
 957 extern int Cudd_EstimateCofactor (DdManager *dd, DdNode * node, int i, int phase);
 958 extern int Cudd_EstimateCofactorSimple (DdNode * node, int i);
 959 extern int Cudd_SharingSize (DdNode **nodeArray, int n);
 960 extern double Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars);
 961 extern int Cudd_EpdCountMinterm (DdManager *manager, DdNode *node, int nvars, EpDouble *epd);
 962 extern double Cudd_CountPath (DdNode *node);
 963 extern double Cudd_CountPathsToNonZero (DdNode *node);
 964 extern DdNode * Cudd_Support (DdManager *dd, DdNode *f);
 965 extern int * Cudd_SupportIndex (DdManager *dd, DdNode *f);
 966 extern int Cudd_SupportSize (DdManager *dd, DdNode *f);
 967 extern DdNode * Cudd_VectorSupport (DdManager *dd, DdNode **F, int n);
 968 extern int * Cudd_VectorSupportIndex (DdManager *dd, DdNode **F, int n);
 969 extern int Cudd_VectorSupportSize (DdManager *dd, DdNode **F, int n);
 970 extern int Cudd_ClassifySupport (DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG);
 971 extern int Cudd_CountLeaves (DdNode *node);
 972 extern int Cudd_bddPickOneCube (DdManager *ddm, DdNode *node, char *string);
 973 extern DdNode * Cudd_bddPickOneMinterm (DdManager *dd, DdNode *f, DdNode **vars, int n);
 974 extern DdNode ** Cudd_bddPickArbitraryMinterms (DdManager *dd, DdNode *f, DdNode **vars, int n, int k);
 975 extern DdNode * Cudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars);
 976 extern DdGen * Cudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value);
 977 extern int Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value);
 978 extern DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube);
 979 extern int Cudd_NextPrime(DdGen *gen, int **cube);
 980 extern DdNode * Cudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
 981 extern DdNode * Cudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
 982 extern DdNode * Cudd_CubeArrayToBdd (DdManager *dd, int *array);
 983 extern int Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array);
 984 extern DdGen * Cudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node);
 985 extern int Cudd_NextNode (DdGen *gen, DdNode **node);
 986 extern int Cudd_GenFree (DdGen *gen);
 987 extern int Cudd_IsGenEmpty (DdGen *gen);
 988 extern DdNode * Cudd_IndicesToCube (DdManager *dd, int *array, int n);
 989 extern void Cudd_PrintVersion (FILE *fp);
 990 extern double Cudd_AverageDistance (DdManager *dd);
 991 extern long Cudd_Random (void);
 992 extern void Cudd_Srandom (long seed);
 993 extern double Cudd_Density (DdManager *dd, DdNode *f, int nvars);
 994 extern void Cudd_OutOfMem (long size);
 995 extern int Cudd_zddCount (DdManager *zdd, DdNode *P);
 996 extern double Cudd_zddCountDouble (DdManager *zdd, DdNode *P);
 997 extern DdNode   * Cudd_zddProduct (DdManager *dd, DdNode *f, DdNode *g);
 998 extern DdNode   * Cudd_zddUnateProduct (DdManager *dd, DdNode *f, DdNode *g);
 999 extern DdNode   * Cudd_zddWeakDiv (DdManager *dd, DdNode *f, DdNode *g);
1000 extern DdNode   * Cudd_zddDivide (DdManager *dd, DdNode *f, DdNode *g);
1001 extern DdNode   * Cudd_zddWeakDivF (DdManager *dd, DdNode *f, DdNode *g);
1002 extern DdNode   * Cudd_zddDivideF (DdManager *dd, DdNode *f, DdNode *g);
1003 extern DdNode   * Cudd_zddComplement (DdManager *dd, DdNode *node);
1004 extern MtrNode * Cudd_MakeZddTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
1005 extern DdNode   * Cudd_zddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
1006 extern DdNode   * Cudd_bddIsop (DdManager *dd, DdNode *L, DdNode *U);
1007 extern DdNode   * Cudd_MakeBddFromZddCover (DdManager *dd, DdNode *node);
1008 extern int Cudd_zddDagSize (DdNode *p_node);
1009 extern double Cudd_zddCountMinterm (DdManager *zdd, DdNode *node, int path);
1010 extern void Cudd_zddPrintSubtable (DdManager *table);
1011 extern DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B);
1012 extern DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f);
1013 extern int Cudd_zddReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
1014 extern int Cudd_zddShuffleHeap (DdManager *table, int *permutation);
1015 extern DdNode * Cudd_zddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
1016 extern DdNode * Cudd_zddUnion (DdManager *dd, DdNode *P, DdNode *Q);
1017 extern DdNode * Cudd_zddIntersect (DdManager *dd, DdNode *P, DdNode *Q);
1018 extern DdNode * Cudd_zddDiff (DdManager *dd, DdNode *P, DdNode *Q);
1019 extern DdNode * Cudd_zddDiffConst (DdManager *zdd, DdNode *P, DdNode *Q);
1020 extern DdNode * Cudd_zddSubset1 (DdManager *dd, DdNode *P, int var);
1021 extern DdNode * Cudd_zddSubset0 (DdManager *dd, DdNode *P, int var);
1022 extern DdNode * Cudd_zddChange (DdManager *dd, DdNode *P, int var);
1023 extern void Cudd_zddSymmProfile (DdManager *table, int lower, int upper);
1024 extern int Cudd_zddPrintMinterm (DdManager *zdd, DdNode *node);
1025 extern int Cudd_zddPrintCover (DdManager *zdd, DdNode *node);
1026 extern int Cudd_zddPrintDebug (DdManager *zdd, DdNode *f, int n, int pr);
1027 extern DdGen * Cudd_zddFirstPath (DdManager *zdd, DdNode *f, int **path);
1028 extern int Cudd_zddNextPath (DdGen *gen, int **path);
1029 extern char * Cudd_zddCoverPathToString (DdManager *zdd, int *path, char *str);
1030 extern int Cudd_zddDumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
1031 extern int Cudd_bddSetPiVar (DdManager *dd, int index);
1032 extern int Cudd_bddSetPsVar (DdManager *dd, int index);
1033 extern int Cudd_bddSetNsVar (DdManager *dd, int index);
1034 extern int Cudd_bddIsPiVar (DdManager *dd, int index);
1035 extern int Cudd_bddIsPsVar (DdManager *dd, int index);
1036 extern int Cudd_bddIsNsVar (DdManager *dd, int index);
1037 extern int Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex);
1038 extern int Cudd_bddReadPairIndex (DdManager *dd, int index);
1039 extern int Cudd_bddSetVarToBeGrouped (DdManager *dd, int index);
1040 extern int Cudd_bddSetVarHardGroup (DdManager *dd, int index);
1041 extern int Cudd_bddResetVarToBeGrouped (DdManager *dd, int index);
1042 extern int Cudd_bddIsVarToBeGrouped (DdManager *dd, int index);
1043 extern int Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index);
1044 extern int Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index);
1045 extern int Cudd_bddIsVarHardGroup (DdManager *dd, int index);
1046
1047 /**AutomaticEnd***************************************************************/
1048
1049 #ifdef __cplusplus
1050 } /* end of extern "C" */
1051 #endif
1052
1053 #endif /* _CUDD */