source: icGREP/icgrep-devel/cudd-2.5.1/cudd/cuddInt.h @ 4645

Last change on this file since 4645 was 4645, checked in by nmedfort, 4 years ago

Test for 64-bit pointers.

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