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

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

Upload of the CUDD library.

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