source: vis_dev/glu-2.3/src/cuBdd/cuddInt.h @ 50

Last change on this file since 50 was 13, checked in by cecile, 13 years ago

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