distr/cudd/cuddInt.h

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