source: vis_dev/glu-2.1/src/cuBdd/cudd.h @ 8

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

src glu
File size: 49.1 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [cudd.h]
4
5  PackageName [cudd]
6
7  Synopsis    [The University of Colorado decision diagram package.]
8
9  Description [External functions and data strucures of the CUDD package.
10  <ul>
11  <li> To turn on the gathering of statistics, define DD_STATS.
12  <li> To link with mis, define DD_MIS.
13  </ul>
14  Modified by Abelardo Pardo to interface it to VIS.
15  ]
16
17  SeeAlso     []
18
19  Author      [Fabio Somenzi]
20
21  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
22
23  All rights reserved.
24
25  Redistribution and use in source and binary forms, with or without
26  modification, are permitted provided that the following conditions
27  are met:
28
29  Redistributions of source code must retain the above copyright
30  notice, this list of conditions and the following disclaimer.
31
32  Redistributions in binary form must reproduce the above copyright
33  notice, this list of conditions and the following disclaimer in the
34  documentation and/or other materials provided with the distribution.
35
36  Neither the name of the University of Colorado nor the names of its
37  contributors may be used to endorse or promote products derived from
38  this software without specific prior written permission.
39
40  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
41  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
42  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
43  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
44  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
45  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
46  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
47  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
48  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
49  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
50  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
51  POSSIBILITY OF SUCH DAMAGE.]
52
53  Revision    [$Id: cudd.h,v 1.170 2005/05/18 06:07:41 fabio Exp $]
54
55******************************************************************************/
56
57#ifndef _CUDD
58#define _CUDD
59
60/*---------------------------------------------------------------------------*/
61/* Nested includes                                                           */
62/*---------------------------------------------------------------------------*/
63
64#include "mtr.h"
65#include "epd.h"
66
67#ifdef __cplusplus
68extern "C" {
69#endif
70
71/*---------------------------------------------------------------------------*/
72/* Constant declarations                                                     */
73/*---------------------------------------------------------------------------*/
74
75#define CUDD_VERSION "2.4.1"
76
77#ifndef SIZEOF_VOID_P
78#define SIZEOF_VOID_P 4
79#endif
80#ifndef SIZEOF_INT
81#define SIZEOF_INT 4
82#endif
83#ifndef SIZEOF_LONG
84#define SIZEOF_LONG 4
85#endif
86
87#ifndef TRUE
88#define TRUE 1
89#endif
90#ifndef FALSE
91#define FALSE 0
92#endif
93
94#define CUDD_VALUE_TYPE         double
95#define CUDD_OUT_OF_MEM         -1
96/* The sizes of the subtables and the cache must be powers of two. */
97#define CUDD_UNIQUE_SLOTS       256     /* initial size of subtables */
98#define CUDD_CACHE_SLOTS        262144  /* default size of the cache */
99
100/* Constants for residue functions. */
101#define CUDD_RESIDUE_DEFAULT    0
102#define CUDD_RESIDUE_MSB        1
103#define CUDD_RESIDUE_TC         2
104
105/* CUDD_MAXINDEX is defined in such a way that on 32-bit and 64-bit
106** machines one can cast an index to (int) without generating a negative
107** number.
108*/
109#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
110#define CUDD_MAXINDEX           (((DdHalfWord) ~0) >> 1)
111#else
112#define CUDD_MAXINDEX           ((DdHalfWord) ~0)
113#endif
114
115/* CUDD_CONST_INDEX is the index of constant nodes.  Currently this
116** is a synonim for CUDD_MAXINDEX. */
117#define CUDD_CONST_INDEX        CUDD_MAXINDEX
118
119/* These constants define the digits used in the representation of
120** arbitrary precision integers.  The two configurations tested use 8
121** and 16 bits for each digit.  The typedefs should be in agreement
122** with these definitions.
123*/
124#define DD_APA_BITS     16
125#define DD_APA_BASE     (1 << DD_APA_BITS)
126#define DD_APA_MASK     (DD_APA_BASE - 1)
127#define DD_APA_HEXPRINT "%04x"
128
129/*---------------------------------------------------------------------------*/
130/* Stucture declarations                                                     */
131/*---------------------------------------------------------------------------*/
132
133
134/*---------------------------------------------------------------------------*/
135/* Type declarations                                                         */
136/*---------------------------------------------------------------------------*/
137
138/**Enum************************************************************************
139
140  Synopsis    [Type of reordering algorithm.]
141
142  Description [Type of reordering algorithm.]
143
144******************************************************************************/
145typedef enum {
146    CUDD_REORDER_SAME,
147    CUDD_REORDER_NONE,
148    CUDD_REORDER_RANDOM,
149    CUDD_REORDER_RANDOM_PIVOT,
150    CUDD_REORDER_SIFT,
151    CUDD_REORDER_SIFT_CONVERGE,
152    CUDD_REORDER_SYMM_SIFT,
153    CUDD_REORDER_SYMM_SIFT_CONV,
154    CUDD_REORDER_WINDOW2,
155    CUDD_REORDER_WINDOW3,
156    CUDD_REORDER_WINDOW4,
157    CUDD_REORDER_WINDOW2_CONV,
158    CUDD_REORDER_WINDOW3_CONV,
159    CUDD_REORDER_WINDOW4_CONV,
160    CUDD_REORDER_GROUP_SIFT,
161    CUDD_REORDER_GROUP_SIFT_CONV,
162    CUDD_REORDER_ANNEALING,
163    CUDD_REORDER_GENETIC,
164    CUDD_REORDER_LINEAR,
165    CUDD_REORDER_LINEAR_CONVERGE,
166    CUDD_REORDER_LAZY_SIFT,
167    CUDD_REORDER_EXACT
168} Cudd_ReorderingType;
169
170
171/**Enum************************************************************************
172
173  Synopsis    [Type of aggregation methods.]
174
175  Description [Type of aggregation methods.]
176
177******************************************************************************/
178typedef enum {
179    CUDD_NO_CHECK,
180    CUDD_GROUP_CHECK,
181    CUDD_GROUP_CHECK2,
182    CUDD_GROUP_CHECK3,
183    CUDD_GROUP_CHECK4,
184    CUDD_GROUP_CHECK5,
185    CUDD_GROUP_CHECK6,
186    CUDD_GROUP_CHECK7,
187    CUDD_GROUP_CHECK8,
188    CUDD_GROUP_CHECK9
189} Cudd_AggregationType;
190
191
192/**Enum************************************************************************
193
194  Synopsis    [Type of hooks.]
195
196  Description [Type of hooks.]
197
198******************************************************************************/
199typedef enum {
200    CUDD_PRE_GC_HOOK,
201    CUDD_POST_GC_HOOK,
202    CUDD_PRE_REORDERING_HOOK,
203    CUDD_POST_REORDERING_HOOK
204} Cudd_HookType;
205
206
207/**Enum************************************************************************
208
209  Synopsis    [Type of error codes.]
210
211  Description [Type of  error codes.]
212
213******************************************************************************/
214typedef enum {
215    CUDD_NO_ERROR,
216    CUDD_MEMORY_OUT,
217    CUDD_TOO_MANY_NODES,
218    CUDD_MAX_MEM_EXCEEDED,
219    CUDD_INVALID_ARG,
220    CUDD_INTERNAL_ERROR
221} Cudd_ErrorType;
222
223
224/**Enum************************************************************************
225
226  Synopsis    [Group type for lazy sifting.]
227
228  Description [Group type for lazy sifting.]
229
230******************************************************************************/
231typedef enum {
232    CUDD_LAZY_NONE,
233    CUDD_LAZY_SOFT_GROUP,
234    CUDD_LAZY_HARD_GROUP,
235    CUDD_LAZY_UNGROUP
236} Cudd_LazyGroupType;
237
238
239/**Enum************************************************************************
240
241  Synopsis    [Variable type.]
242
243  Description [Variable type. Currently used only in lazy sifting.]
244
245******************************************************************************/
246typedef enum {
247    CUDD_VAR_PRIMARY_INPUT,
248    CUDD_VAR_PRESENT_STATE,
249    CUDD_VAR_NEXT_STATE
250} Cudd_VariableType;
251
252
253#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
254typedef unsigned int   DdHalfWord;
255#else
256typedef unsigned short DdHalfWord;
257#endif
258
259#ifdef __osf__
260#pragma pointer_size save
261#pragma pointer_size short
262#endif
263
264typedef struct DdNode DdNode;
265
266typedef struct DdChildren {
267    struct DdNode *T;
268    struct DdNode *E;
269} DdChildren;
270
271/* The DdNode structure is the only one exported out of the package */
272struct DdNode {
273    DdHalfWord index;
274    DdHalfWord ref;             /* reference count */
275    DdNode *next;               /* next pointer for unique table */
276    union {
277        CUDD_VALUE_TYPE value;  /* for constant nodes */
278        DdChildren kids;        /* for internal nodes */
279    } type;
280};
281
282#ifdef __osf__
283#pragma pointer_size restore
284#endif
285
286typedef struct DdManager DdManager;
287
288typedef struct DdGen DdGen;
289
290/* These typedefs for arbitrary precision arithmetic should agree with
291** the corresponding constant definitions above. */
292typedef unsigned short int DdApaDigit;
293typedef unsigned long int DdApaDoubleDigit;
294typedef DdApaDigit * DdApaNumber;
295
296/* Return type for function computing two-literal clauses. */
297typedef struct DdTlcInfo DdTlcInfo;
298
299/* Type of hook function. */
300typedef int (*DD_HFP)(DdManager *, const char *, void *);
301/* Type of priority function */
302typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **,
303                            DdNode **);
304/* Type of apply operator. */
305typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
306/* Type of monadic apply operator. */
307typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
308/* Types of cache tag functions. */
309typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
310typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
311/* Type of memory-out function. */
312typedef void (*DD_OOMFP)(long);
313/* Type of comparison function for qsort. */
314typedef int (*DD_QSFP)(const void *, const void *);
315
316/*---------------------------------------------------------------------------*/
317/* Variable declarations                                                     */
318/*---------------------------------------------------------------------------*/
319
320
321/*---------------------------------------------------------------------------*/
322/* Macro declarations                                                        */
323/*---------------------------------------------------------------------------*/
324
325
326/**Macro***********************************************************************
327
328  Synopsis     [Returns 1 if the node is a constant node.]
329
330  Description  [Returns 1 if the node is a constant node (rather than an
331  internal node). All constant nodes have the same index
332  (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either
333  regular or complemented.]
334
335  SideEffects  [none]
336
337  SeeAlso      []
338
339******************************************************************************/
340#define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
341
342
343/**Macro***********************************************************************
344
345  Synopsis     [Complements a DD.]
346
347  Description  [Complements a DD by flipping the complement attribute of
348  the pointer (the least significant bit).]
349
350  SideEffects  [none]
351
352  SeeAlso      [Cudd_NotCond]
353
354******************************************************************************/
355#define Cudd_Not(node) ((DdNode *)((long)(node) ^ 01))
356
357
358/**Macro***********************************************************************
359
360  Synopsis     [Complements a DD if a condition is true.]
361
362  Description  [Complements a DD if condition c is true; c should be
363  either 0 or 1, because it is used directly (for efficiency). If in
364  doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]
365
366  SideEffects  [none]
367
368  SeeAlso      [Cudd_Not]
369
370******************************************************************************/
371#define Cudd_NotCond(node,c) ((DdNode *)((long)(node) ^ (c)))
372
373
374/**Macro***********************************************************************
375
376  Synopsis     [Returns the regular version of a pointer.]
377
378  Description  []
379
380  SideEffects  [none]
381
382  SeeAlso      [Cudd_Complement Cudd_IsComplement]
383
384******************************************************************************/
385#define Cudd_Regular(node) ((DdNode *)((unsigned long)(node) & ~01))
386
387
388/**Macro***********************************************************************
389
390  Synopsis     [Returns the complemented version of a pointer.]
391
392  Description  []
393
394  SideEffects  [none]
395
396  SeeAlso      [Cudd_Regular Cudd_IsComplement]
397
398******************************************************************************/
399#define Cudd_Complement(node) ((DdNode *)((unsigned long)(node) | 01))
400
401
402/**Macro***********************************************************************
403
404  Synopsis     [Returns 1 if a pointer is complemented.]
405
406  Description  []
407
408  SideEffects  [none]
409
410  SeeAlso      [Cudd_Regular Cudd_Complement]
411
412******************************************************************************/
413#define Cudd_IsComplement(node) ((int) ((long) (node) & 01))
414
415
416/**Macro***********************************************************************
417
418  Synopsis     [Returns the then child of an internal node.]
419
420  Description  [Returns the then child of an internal node. If
421  <code>node</code> is a constant node, the result is unpredictable.]
422
423  SideEffects  [none]
424
425  SeeAlso      [Cudd_E Cudd_V]
426
427******************************************************************************/
428#define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
429
430
431/**Macro***********************************************************************
432
433  Synopsis     [Returns the else child of an internal node.]
434
435  Description  [Returns the else child of an internal node. If
436  <code>node</code> is a constant node, the result is unpredictable.]
437
438  SideEffects  [none]
439
440  SeeAlso      [Cudd_T Cudd_V]
441
442******************************************************************************/
443#define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
444
445
446/**Macro***********************************************************************
447
448  Synopsis     [Returns the value of a constant node.]
449
450  Description  [Returns the value of a constant node. If
451  <code>node</code> is an internal node, the result is unpredictable.]
452
453  SideEffects  [none]
454
455  SeeAlso      [Cudd_T Cudd_E]
456
457******************************************************************************/
458#define Cudd_V(node) ((Cudd_Regular(node))->type.value)
459
460
461/**Macro***********************************************************************
462
463  Synopsis     [Returns the current position in the order of variable
464  index.]
465
466  Description [Returns the current position in the order of variable
467  index. This macro is obsolete and is kept for compatibility. New
468  applications should use Cudd_ReadPerm instead.]
469
470  SideEffects  [none]
471
472  SeeAlso      [Cudd_ReadPerm]
473
474******************************************************************************/
475#define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
476
477
478/**Macro***********************************************************************
479
480  Synopsis     [Iterates over the cubes of a decision diagram.]
481
482  Description  [Iterates over the cubes of a decision diagram f.
483  <ul>
484  <li> DdManager *manager;
485  <li> DdNode *f;
486  <li> DdGen *gen;
487  <li> int *cube;
488  <li> CUDD_VALUE_TYPE value;
489  </ul>
490  Cudd_ForeachCube allocates and frees the generator. Therefore the
491  application should not try to do that. Also, the cube is freed at the
492  end of Cudd_ForeachCube and hence is not available outside of the loop.<p>
493  CAUTION: It is assumed that dynamic reordering will not occur while
494  there are open generators. It is the user's responsibility to make sure
495  that dynamic reordering does not occur. As long as new nodes are not created
496  during generation, and dynamic reordering is not called explicitly,
497  dynamic reordering will not occur. Alternatively, it is sufficient to
498  disable dynamic reordering. It is a mistake to dispose of a diagram
499  on which generation is ongoing.]
500
501  SideEffects  [none]
502
503  SeeAlso      [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree
504  Cudd_IsGenEmpty Cudd_AutodynDisable]
505
506******************************************************************************/
507#define Cudd_ForeachCube(manager, f, gen, cube, value)\
508    for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
509        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
510        (void) Cudd_NextCube(gen, &cube, &value))
511
512
513/**Macro***********************************************************************
514
515  Synopsis     [Iterates over the primes of a Boolean function.]
516
517  Description  [Iterates over the primes of a Boolean function producing
518  a prime and irredundant cover.
519  <ul>
520  <li> DdManager *manager;
521  <li> DdNode *l;
522  <li> DdNode *u;
523  <li> DdGen *gen;
524  <li> int *cube;
525  </ul>
526  The Boolean function is described by an upper bound and a lower bound.  If
527  the function is completely specified, the two bounds coincide.
528  Cudd_ForeachPrime allocates and frees the generator.  Therefore the
529  application should not try to do that.  Also, the cube is freed at the
530  end of Cudd_ForeachPrime and hence is not available outside of the loop.<p>
531  CAUTION: It is a mistake to change a diagram on which generation is ongoing.]
532
533  SideEffects  [none]
534
535  SeeAlso      [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree
536  Cudd_IsGenEmpty]
537
538******************************************************************************/
539#define Cudd_ForeachPrime(manager, l, u, gen, cube)\
540    for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
541        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
542        (void) Cudd_NextPrime(gen, &cube))
543
544
545/**Macro***********************************************************************
546
547  Synopsis     [Iterates over the nodes of a decision diagram.]
548
549  Description  [Iterates over the nodes of a decision diagram f.
550  <ul>
551  <li> DdManager *manager;
552  <li> DdNode *f;
553  <li> DdGen *gen;
554  <li> DdNode *node;
555  </ul>
556  The nodes are returned in a seemingly random order.
557  Cudd_ForeachNode allocates and frees the generator. Therefore the
558  application should not try to do that.<p>
559  CAUTION: It is assumed that dynamic reordering will not occur while
560  there are open generators. It is the user's responsibility to make sure
561  that dynamic reordering does not occur. As long as new nodes are not created
562  during generation, and dynamic reordering is not called explicitly,
563  dynamic reordering will not occur. Alternatively, it is sufficient to
564  disable dynamic reordering. It is a mistake to dispose of a diagram
565  on which generation is ongoing.]
566
567  SideEffects  [none]
568
569  SeeAlso      [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree
570  Cudd_IsGenEmpty Cudd_AutodynDisable]
571
572******************************************************************************/
573#define Cudd_ForeachNode(manager, f, gen, node)\
574    for((gen) = Cudd_FirstNode(manager, f, &node);\
575        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
576        (void) Cudd_NextNode(gen, &node))
577
578
579/**Macro***********************************************************************
580
581  Synopsis     [Iterates over the paths of a ZDD.]
582
583  Description  [Iterates over the paths of a ZDD f.
584  <ul>
585  <li> DdManager *manager;
586  <li> DdNode *f;
587  <li> DdGen *gen;
588  <li> int *path;
589  </ul>
590  Cudd_zddForeachPath allocates and frees the generator. Therefore the
591  application should not try to do that. Also, the path is freed at the
592  end of Cudd_zddForeachPath and hence is not available outside of the loop.<p>
593  CAUTION: It is assumed that dynamic reordering will not occur while
594  there are open generators.  It is the user's responsibility to make sure
595  that dynamic reordering does not occur.  As long as new nodes are not created
596  during generation, and dynamic reordering is not called explicitly,
597  dynamic reordering will not occur.  Alternatively, it is sufficient to
598  disable dynamic reordering.  It is a mistake to dispose of a diagram
599  on which generation is ongoing.]
600
601  SideEffects  [none]
602
603  SeeAlso      [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree
604  Cudd_IsGenEmpty Cudd_AutodynDisable]
605
606******************************************************************************/
607#define Cudd_zddForeachPath(manager, f, gen, path)\
608    for((gen) = Cudd_zddFirstPath(manager, f, &path);\
609        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
610        (void) Cudd_zddNextPath(gen, &path))
611
612
613
614/**AutomaticStart*************************************************************/
615
616/*---------------------------------------------------------------------------*/
617/* Function prototypes                                                       */
618/*---------------------------------------------------------------------------*/
619
620extern DdNode * Cudd_addNewVar (DdManager *dd);
621extern DdNode * Cudd_addNewVarAtLevel (DdManager *dd, int level);
622extern DdNode * Cudd_bddNewVar (DdManager *dd);
623extern DdNode * Cudd_bddNewVarAtLevel (DdManager *dd, int level);
624extern DdNode * Cudd_addIthVar (DdManager *dd, int i);
625extern DdNode * Cudd_bddIthVar (DdManager *dd, int i);
626extern DdNode * Cudd_zddIthVar (DdManager *dd, int i);
627extern int Cudd_zddVarsFromBddVars (DdManager *dd, int multiplicity);
628extern DdNode * Cudd_addConst (DdManager *dd, CUDD_VALUE_TYPE c);
629extern int Cudd_IsNonConstant (DdNode *f);
630extern void Cudd_AutodynEnable (DdManager *unique, Cudd_ReorderingType method);
631extern void Cudd_AutodynDisable (DdManager *unique);
632extern int Cudd_ReorderingStatus (DdManager *unique, Cudd_ReorderingType *method);
633extern void Cudd_AutodynEnableZdd (DdManager *unique, Cudd_ReorderingType method);
634extern void Cudd_AutodynDisableZdd (DdManager *unique);
635extern int Cudd_ReorderingStatusZdd (DdManager *unique, Cudd_ReorderingType *method);
636extern int Cudd_zddRealignmentEnabled (DdManager *unique);
637extern void Cudd_zddRealignEnable (DdManager *unique);
638extern void Cudd_zddRealignDisable (DdManager *unique);
639extern int Cudd_bddRealignmentEnabled (DdManager *unique);
640extern void Cudd_bddRealignEnable (DdManager *unique);
641extern void Cudd_bddRealignDisable (DdManager *unique);
642extern DdNode * Cudd_ReadOne (DdManager *dd);
643extern DdNode * Cudd_ReadZddOne (DdManager *dd, int i);
644extern DdNode * Cudd_ReadZero (DdManager *dd);
645extern DdNode * Cudd_ReadLogicZero (DdManager *dd);
646extern DdNode * Cudd_ReadPlusInfinity (DdManager *dd);
647extern DdNode * Cudd_ReadMinusInfinity (DdManager *dd);
648extern DdNode * Cudd_ReadBackground (DdManager *dd);
649extern void Cudd_SetBackground (DdManager *dd, DdNode *bck);
650extern unsigned int Cudd_ReadCacheSlots (DdManager *dd);
651extern double Cudd_ReadCacheUsedSlots (DdManager * dd);
652extern double Cudd_ReadCacheLookUps (DdManager *dd);
653extern double Cudd_ReadCacheHits (DdManager *dd);
654extern double Cudd_ReadRecursiveCalls (DdManager * dd);
655extern unsigned int Cudd_ReadMinHit (DdManager *dd);
656extern void Cudd_SetMinHit (DdManager *dd, unsigned int hr);
657extern unsigned int Cudd_ReadLooseUpTo (DdManager *dd);
658extern void Cudd_SetLooseUpTo (DdManager *dd, unsigned int lut);
659extern unsigned int Cudd_ReadMaxCache (DdManager *dd);
660extern unsigned int Cudd_ReadMaxCacheHard (DdManager *dd);
661extern void Cudd_SetMaxCacheHard (DdManager *dd, unsigned int mc);
662extern int Cudd_ReadSize (DdManager *dd);
663extern int Cudd_ReadZddSize (DdManager *dd);
664extern unsigned int Cudd_ReadSlots (DdManager *dd);
665extern double Cudd_ReadUsedSlots (DdManager * dd);
666extern double Cudd_ExpectedUsedSlots (DdManager * dd);
667extern unsigned int Cudd_ReadKeys (DdManager *dd);
668extern unsigned int Cudd_ReadDead (DdManager *dd);
669extern unsigned int Cudd_ReadMinDead (DdManager *dd);
670extern int Cudd_ReadReorderings (DdManager *dd);
671extern long Cudd_ReadReorderingTime (DdManager * dd);
672extern int Cudd_ReadGarbageCollections (DdManager * dd);
673extern long Cudd_ReadGarbageCollectionTime (DdManager * dd);
674extern double Cudd_ReadNodesFreed (DdManager * dd);
675extern double Cudd_ReadNodesDropped (DdManager * dd);
676extern double Cudd_ReadUniqueLookUps (DdManager * dd);
677extern double Cudd_ReadUniqueLinks (DdManager * dd);
678extern int Cudd_ReadSiftMaxVar (DdManager *dd);
679extern void Cudd_SetSiftMaxVar (DdManager *dd, int smv);
680extern int Cudd_ReadSiftMaxSwap (DdManager *dd);
681extern void Cudd_SetSiftMaxSwap (DdManager *dd, int sms);
682extern double Cudd_ReadMaxGrowth (DdManager *dd);
683extern void Cudd_SetMaxGrowth (DdManager *dd, double mg);
684extern double Cudd_ReadMaxGrowthAlternate (DdManager * dd);
685extern void Cudd_SetMaxGrowthAlternate (DdManager * dd, double mg);
686extern int Cudd_ReadReorderingCycle (DdManager * dd);
687extern void Cudd_SetReorderingCycle (DdManager * dd, int cycle);
688extern MtrNode * Cudd_ReadTree (DdManager *dd);
689extern void Cudd_SetTree (DdManager *dd, MtrNode *tree);
690extern void Cudd_FreeTree (DdManager *dd);
691extern MtrNode * Cudd_ReadZddTree (DdManager *dd);
692extern void Cudd_SetZddTree (DdManager *dd, MtrNode *tree);
693extern void Cudd_FreeZddTree (DdManager *dd);
694extern unsigned int Cudd_NodeReadIndex (DdNode *node);
695extern int Cudd_ReadPerm (DdManager *dd, int i);
696extern int Cudd_ReadPermZdd (DdManager *dd, int i);
697extern int Cudd_ReadInvPerm (DdManager *dd, int i);
698extern int Cudd_ReadInvPermZdd (DdManager *dd, int i);
699extern DdNode * Cudd_ReadVars (DdManager *dd, int i);
700extern CUDD_VALUE_TYPE Cudd_ReadEpsilon (DdManager *dd);
701extern void Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep);
702extern Cudd_AggregationType Cudd_ReadGroupcheck (DdManager *dd);
703extern void Cudd_SetGroupcheck (DdManager *dd, Cudd_AggregationType gc);
704extern int Cudd_GarbageCollectionEnabled (DdManager *dd);
705extern void Cudd_EnableGarbageCollection (DdManager *dd);
706extern void Cudd_DisableGarbageCollection (DdManager *dd);
707extern int Cudd_DeadAreCounted (DdManager *dd);
708extern void Cudd_TurnOnCountDead (DdManager *dd);
709extern void Cudd_TurnOffCountDead (DdManager *dd);
710extern int Cudd_ReadRecomb (DdManager *dd);
711extern void Cudd_SetRecomb (DdManager *dd, int recomb);
712extern int Cudd_ReadSymmviolation (DdManager *dd);
713extern void Cudd_SetSymmviolation (DdManager *dd, int symmviolation);
714extern int Cudd_ReadArcviolation (DdManager *dd);
715extern void Cudd_SetArcviolation (DdManager *dd, int arcviolation);
716extern int Cudd_ReadPopulationSize (DdManager *dd);
717extern void Cudd_SetPopulationSize (DdManager *dd, int populationSize);
718extern int Cudd_ReadNumberXovers (DdManager *dd);
719extern void Cudd_SetNumberXovers (DdManager *dd, int numberXovers);
720extern unsigned long Cudd_ReadMemoryInUse (DdManager *dd);
721extern int Cudd_PrintInfo (DdManager *dd, FILE *fp);
722extern long Cudd_ReadPeakNodeCount (DdManager *dd);
723extern int Cudd_ReadPeakLiveNodeCount (DdManager * dd);
724extern long Cudd_ReadNodeCount (DdManager *dd);
725extern long Cudd_zddReadNodeCount (DdManager *dd);
726extern int Cudd_AddHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
727extern int Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where);
728extern int Cudd_IsInHook (DdManager * dd, DD_HFP f, Cudd_HookType where);
729extern int Cudd_StdPreReordHook (DdManager *dd, const char *str, void *data);
730extern int Cudd_StdPostReordHook (DdManager *dd, const char *str, void *data);
731extern int Cudd_EnableReorderingReporting (DdManager *dd);
732extern int Cudd_DisableReorderingReporting (DdManager *dd);
733extern int Cudd_ReorderingReporting (DdManager *dd);
734extern Cudd_ErrorType Cudd_ReadErrorCode (DdManager *dd);
735extern void Cudd_ClearErrorCode (DdManager *dd);
736extern FILE * Cudd_ReadStdout (DdManager *dd);
737extern void Cudd_SetStdout (DdManager *dd, FILE *fp);
738extern FILE * Cudd_ReadStderr (DdManager *dd);
739extern void Cudd_SetStderr (DdManager *dd, FILE *fp);
740extern unsigned int Cudd_ReadNextReordering (DdManager *dd);
741extern void Cudd_SetNextReordering (DdManager *dd, unsigned int next);
742extern double Cudd_ReadSwapSteps (DdManager *dd);
743extern unsigned int Cudd_ReadMaxLive (DdManager *dd);
744extern void Cudd_SetMaxLive (DdManager *dd, unsigned int maxLive);
745extern unsigned long Cudd_ReadMaxMemory (DdManager *dd);
746extern void Cudd_SetMaxMemory (DdManager *dd, unsigned long maxMemory);
747extern int Cudd_bddBindVar (DdManager *dd, int index);
748extern int Cudd_bddUnbindVar (DdManager *dd, int index);
749extern int Cudd_bddVarIsBound (DdManager *dd, int index);
750extern DdNode * Cudd_addExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
751extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
752extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube);
753extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
754extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g);
755extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g);
756extern DdNode * Cudd_addThreshold (DdManager *dd, DdNode **f, DdNode **g);
757extern DdNode * Cudd_addSetNZ (DdManager *dd, DdNode **f, DdNode **g);
758extern DdNode * Cudd_addDivide (DdManager *dd, DdNode **f, DdNode **g);
759extern DdNode * Cudd_addMinus (DdManager *dd, DdNode **f, DdNode **g);
760extern DdNode * Cudd_addMinimum (DdManager *dd, DdNode **f, DdNode **g);
761extern DdNode * Cudd_addMaximum (DdManager *dd, DdNode **f, DdNode **g);
762extern DdNode * Cudd_addOneZeroMaximum (DdManager *dd, DdNode **f, DdNode **g);
763extern DdNode * Cudd_addDiff (DdManager *dd, DdNode **f, DdNode **g);
764extern DdNode * Cudd_addAgreement (DdManager *dd, DdNode **f, DdNode **g);
765extern DdNode * Cudd_addOr (DdManager *dd, DdNode **f, DdNode **g);
766extern DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g);
767extern DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g);
768extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
769extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
770extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
771extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
772extern DdNode * Cudd_addFindMax (DdManager *dd, DdNode *f);
773extern DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f);
774extern DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit);
775extern DdNode * Cudd_addScalarInverse (DdManager *dd, DdNode *f, DdNode *epsilon);
776extern DdNode * Cudd_addIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
777extern DdNode * Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
778extern DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g);
779extern int Cudd_addLeq (DdManager * dd, DdNode * f, DdNode * g);
780extern DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f);
781extern DdNode * Cudd_addNegate (DdManager *dd, DdNode *f);
782extern DdNode * Cudd_addRoundOff (DdManager *dd, DdNode *f, int N);
783extern DdNode * Cudd_addWalsh (DdManager *dd, DdNode **x, DdNode **y, int n);
784extern DdNode * Cudd_addResidue (DdManager *dd, int n, int m, int options, int top);
785extern DdNode * Cudd_bddAndAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
786extern DdNode * Cudd_bddAndAbstractLimit (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit);
787extern int Cudd_ApaNumberOfDigits (int binaryDigits);
788extern DdApaNumber Cudd_NewApaNumber (int digits);
789extern void Cudd_ApaCopy (int digits, DdApaNumber source, DdApaNumber dest);
790extern DdApaDigit Cudd_ApaAdd (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum);
791extern DdApaDigit Cudd_ApaSubtract (int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff);
792extern DdApaDigit Cudd_ApaShortDivision (int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient);
793extern unsigned int Cudd_ApaIntDivision (int  digits, DdApaNumber dividend, unsigned int  divisor, DdApaNumber  quotient);
794extern void Cudd_ApaShiftRight (int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b);
795extern void Cudd_ApaSetToLiteral (int digits, DdApaNumber number, DdApaDigit literal);
796extern void Cudd_ApaPowerOfTwo (int digits, DdApaNumber number, int power);
797extern int Cudd_ApaCompare (int digitsFirst, DdApaNumber  first, int digitsSecond, DdApaNumber  second);
798extern int Cudd_ApaCompareRatios (int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen);
799extern int Cudd_ApaPrintHex (FILE *fp, int digits, DdApaNumber number);
800extern int Cudd_ApaPrintDecimal (FILE *fp, int digits, DdApaNumber number);
801extern int Cudd_ApaPrintExponential (FILE * fp, int  digits, DdApaNumber  number, int precision);
802extern DdApaNumber Cudd_ApaCountMinterm (DdManager *manager, DdNode *node, int nvars, int *digits);
803extern int Cudd_ApaPrintMinterm (FILE *fp, DdManager *dd, DdNode *node, int nvars);
804extern int Cudd_ApaPrintMintermExp (FILE * fp, DdManager * dd, DdNode * node, int  nvars, int precision);
805extern int Cudd_ApaPrintDensity (FILE * fp, DdManager * dd, DdNode * node, int  nvars);
806extern DdNode * Cudd_UnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
807extern DdNode * Cudd_OverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
808extern DdNode * Cudd_RemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
809extern DdNode * Cudd_RemapOverApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
810extern DdNode * Cudd_BiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
811extern DdNode * Cudd_BiasedOverApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
812extern DdNode * Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube);
813extern DdNode * Cudd_bddXorExistAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
814extern DdNode * Cudd_bddUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube);
815extern DdNode * Cudd_bddBooleanDiff (DdManager *manager, DdNode *f, int x);
816extern int Cudd_bddVarIsDependent (DdManager *dd, DdNode *f, DdNode *var);
817extern double Cudd_bddCorrelation (DdManager *manager, DdNode *f, DdNode *g);
818extern double Cudd_bddCorrelationWeights (DdManager *manager, DdNode *f, DdNode *g, double *prob);
819extern DdNode * Cudd_bddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
820extern DdNode * Cudd_bddIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
821extern DdNode * Cudd_bddIntersect (DdManager *dd, DdNode *f, DdNode *g);
822extern DdNode * Cudd_bddAnd (DdManager *dd, DdNode *f, DdNode *g);
823extern DdNode * Cudd_bddAndLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
824extern DdNode * Cudd_bddOr (DdManager *dd, DdNode *f, DdNode *g);
825extern DdNode * Cudd_bddNand (DdManager *dd, DdNode *f, DdNode *g);
826extern DdNode * Cudd_bddNor (DdManager *dd, DdNode *f, DdNode *g);
827extern DdNode * Cudd_bddXor (DdManager *dd, DdNode *f, DdNode *g);
828extern DdNode * Cudd_bddXnor (DdManager *dd, DdNode *f, DdNode *g);
829extern int Cudd_bddLeq (DdManager *dd, DdNode *f, DdNode *g);
830extern DdNode * Cudd_addBddThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
831extern DdNode * Cudd_addBddStrictThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value);
832extern DdNode * Cudd_addBddInterval (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper);
833extern DdNode * Cudd_addBddIthBit (DdManager *dd, DdNode *f, int bit);
834extern DdNode * Cudd_BddToAdd (DdManager *dd, DdNode *B);
835extern DdNode * Cudd_addBddPattern (DdManager *dd, DdNode *f);
836extern DdNode * Cudd_bddTransfer (DdManager *ddSource, DdManager *ddDestination, DdNode *f);
837extern int Cudd_DebugCheck (DdManager *table);
838extern int Cudd_CheckKeys (DdManager *table);
839extern DdNode * Cudd_bddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
840extern DdNode * Cudd_bddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
841extern DdNode * Cudd_Cofactor (DdManager *dd, DdNode *f, DdNode *g);
842extern DdNode * Cudd_bddCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
843extern DdNode * Cudd_addCompose (DdManager *dd, DdNode *f, DdNode *g, int v);
844extern DdNode * Cudd_addPermute (DdManager *manager, DdNode *node, int *permut);
845extern DdNode * Cudd_addSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
846extern DdNode * Cudd_bddPermute (DdManager *manager, DdNode *node, int *permut);
847extern DdNode * Cudd_bddVarMap (DdManager *manager, DdNode *f);
848extern int Cudd_SetVarMap (DdManager *manager, DdNode **x, DdNode **y, int n);
849extern DdNode * Cudd_bddSwapVariables (DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n);
850extern DdNode * Cudd_bddAdjPermuteX (DdManager *dd, DdNode *B, DdNode **x, int n);
851extern DdNode * Cudd_addVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
852extern DdNode * Cudd_addGeneralVectorCompose (DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff);
853extern DdNode * Cudd_addNonSimCompose (DdManager *dd, DdNode *f, DdNode **vector);
854extern DdNode * Cudd_bddVectorCompose (DdManager *dd, DdNode *f, DdNode **vector);
855extern int Cudd_bddApproxConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
856extern int Cudd_bddApproxDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
857extern int Cudd_bddIterConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
858extern int Cudd_bddIterDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
859extern int Cudd_bddGenConjDecomp (DdManager *dd, DdNode *f, DdNode ***conjuncts);
860extern int Cudd_bddGenDisjDecomp (DdManager *dd, DdNode *f, DdNode ***disjuncts);
861extern int Cudd_bddVarConjDecomp (DdManager *dd, DdNode * f, DdNode ***conjuncts);
862extern int Cudd_bddVarDisjDecomp (DdManager *dd, DdNode * f, DdNode ***disjuncts);
863extern DdNode * Cudd_FindEssential (DdManager *dd, DdNode *f);
864extern int Cudd_bddIsVarEssential (DdManager *manager, DdNode *f, int id, int phase);
865extern DdTlcInfo * Cudd_FindTwoLiteralClauses (DdManager * dd, DdNode * f);
866extern int Cudd_PrintTwoLiteralClauses (DdManager * dd, DdNode * f, char **names, FILE *fp);
867extern int Cudd_ReadIthClause (DdTlcInfo * tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2);
868extern void Cudd_tlcInfoFree (DdTlcInfo * t);
869extern int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp);
870extern int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
871extern int Cudd_DumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
872extern int Cudd_DumpDaVinci (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
873extern int Cudd_DumpDDcal (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
874extern int Cudd_DumpFactoredForm (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
875extern DdNode * Cudd_bddConstrain (DdManager *dd, DdNode *f, DdNode *c);
876extern DdNode * Cudd_bddRestrict (DdManager *dd, DdNode *f, DdNode *c);
877extern DdNode * Cudd_bddNPAnd (DdManager *dd, DdNode *f, DdNode *c);
878extern DdNode * Cudd_addConstrain (DdManager *dd, DdNode *f, DdNode *c);
879extern DdNode ** Cudd_bddConstrainDecomp (DdManager *dd, DdNode *f);
880extern DdNode * Cudd_addRestrict (DdManager *dd, DdNode *f, DdNode *c);
881extern DdNode ** Cudd_bddCharToVect (DdManager *dd, DdNode *f);
882extern DdNode * Cudd_bddLICompaction (DdManager *dd, DdNode *f, DdNode *c);
883extern DdNode * Cudd_bddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
884extern DdNode * Cudd_bddMinimize (DdManager *dd, DdNode *f, DdNode *c);
885extern DdNode * Cudd_SubsetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
886extern DdNode * Cudd_SupersetCompress (DdManager *dd, DdNode *f, int nvars, int threshold);
887extern MtrNode * Cudd_MakeTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
888extern int Cudd_addHarwell (FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, DdNode ***xn, DdNode ***yn_, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy, int pr);
889extern DdManager * Cudd_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory);
890extern void Cudd_Quit (DdManager *unique);
891extern int Cudd_PrintLinear (DdManager *table);
892extern int Cudd_ReadLinear (DdManager *table, int x, int y);
893extern DdNode * Cudd_bddLiteralSetIntersection (DdManager *dd, DdNode *f, DdNode *g);
894extern DdNode * Cudd_addMatrixMultiply (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
895extern DdNode * Cudd_addTimesPlus (DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz);
896extern DdNode * Cudd_addTriangle (DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz);
897extern DdNode * Cudd_addOuterSum (DdManager *dd, DdNode *M, DdNode *r, DdNode *c);
898extern DdNode * Cudd_PrioritySelect (DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode * (*)(DdManager *, int, DdNode **, DdNode **, DdNode **));
899extern DdNode * Cudd_Xgty (DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y);
900extern DdNode * Cudd_Xeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
901extern DdNode * Cudd_addXeqy (DdManager *dd, int N, DdNode **x, DdNode **y);
902extern DdNode * Cudd_Dxygtdxz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
903extern DdNode * Cudd_Dxygtdyz (DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z);
904extern DdNode * Cudd_CProjection (DdManager *dd, DdNode *R, DdNode *Y);
905extern DdNode * Cudd_addHamming (DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars);
906extern int Cudd_MinHammingDist (DdManager *dd, DdNode *f, int *minterm, int upperBound);
907extern DdNode * Cudd_bddClosestCube (DdManager *dd, DdNode * f, DdNode *g, int *distance);
908extern int Cudd_addRead (FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, DdNode ***xn, DdNode ***yn_, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy);
909extern int Cudd_bddRead (FILE *fp, DdManager *dd, DdNode **E, DdNode ***x, DdNode ***y, int *nx, int *ny, int *m, int *n, int bx, int sx, int by, int sy);
910extern void Cudd_Ref (DdNode *n);
911extern void Cudd_RecursiveDeref (DdManager *table, DdNode *n);
912extern void Cudd_IterDerefBdd (DdManager *table, DdNode *n);
913extern void Cudd_DelayedDerefBdd (DdManager * table, DdNode * n);
914extern void Cudd_RecursiveDerefZdd (DdManager *table, DdNode *n);
915extern void Cudd_Deref (DdNode *node);
916extern int Cudd_CheckZeroRef (DdManager *manager);
917extern int Cudd_ReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
918extern int Cudd_ShuffleHeap (DdManager *table, int *permutation);
919extern DdNode * Cudd_Eval (DdManager *dd, DdNode *f, int *inputs);
920extern DdNode * Cudd_ShortestPath (DdManager *manager, DdNode *f, int *weight, int *support, int *length);
921extern DdNode * Cudd_LargestCube (DdManager *manager, DdNode *f, int *length);
922extern int Cudd_ShortestLength (DdManager *manager, DdNode *f, int *weight);
923extern DdNode * Cudd_Decreasing (DdManager *dd, DdNode *f, int i);
924extern DdNode * Cudd_Increasing (DdManager *dd, DdNode *f, int i);
925extern int Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D);
926extern int Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D);
927extern int Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
928extern DdNode * Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f);
929extern double * Cudd_CofMinterm (DdManager *dd, DdNode *node);
930extern DdNode * Cudd_SolveEqn (DdManager * bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n);
931extern DdNode * Cudd_VerifySol (DdManager * bdd, DdNode *F, DdNode **G, int *yIndex, int n);
932extern DdNode * Cudd_SplitSet (DdManager *manager, DdNode *S, DdNode **xVars, int n, double m);
933extern DdNode * Cudd_SubsetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
934extern DdNode * Cudd_SupersetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
935extern DdNode * Cudd_SubsetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
936extern DdNode * Cudd_SupersetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
937extern void Cudd_SymmProfile (DdManager *table, int lower, int upper);
938extern unsigned int Cudd_Prime (unsigned int p);
939extern int Cudd_PrintMinterm (DdManager *manager, DdNode *node);
940extern int Cudd_bddPrintCover (DdManager *dd, DdNode *l, DdNode *u);
941extern int Cudd_PrintDebug (DdManager *dd, DdNode *f, int n, int pr);
942extern int Cudd_DagSize (DdNode *node);
943extern int Cudd_EstimateCofactor (DdManager *dd, DdNode * node, int i, int phase);
944extern int Cudd_EstimateCofactorSimple (DdNode * node, int i);
945extern int Cudd_SharingSize (DdNode **nodeArray, int n);
946extern double Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars);
947extern int Cudd_EpdCountMinterm (DdManager *manager, DdNode *node, int nvars, EpDouble *epd);
948extern double Cudd_CountPath (DdNode *node);
949extern double Cudd_CountPathsToNonZero (DdNode *node);
950extern DdNode * Cudd_Support (DdManager *dd, DdNode *f);
951extern int * Cudd_SupportIndex (DdManager *dd, DdNode *f);
952extern int Cudd_SupportSize (DdManager *dd, DdNode *f);
953extern DdNode * Cudd_VectorSupport (DdManager *dd, DdNode **F, int n);
954extern int * Cudd_VectorSupportIndex (DdManager *dd, DdNode **F, int n);
955extern int Cudd_VectorSupportSize (DdManager *dd, DdNode **F, int n);
956extern int Cudd_ClassifySupport (DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG);
957extern int Cudd_CountLeaves (DdNode *node);
958extern int Cudd_bddPickOneCube (DdManager *ddm, DdNode *node, char *string);
959extern DdNode * Cudd_bddPickOneMinterm (DdManager *dd, DdNode *f, DdNode **vars, int n);
960extern DdNode ** Cudd_bddPickArbitraryMinterms (DdManager *dd, DdNode *f, DdNode **vars, int n, int k);
961extern DdNode * Cudd_SubsetWithMaskVars (DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars);
962extern DdGen * Cudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value);
963extern int Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value);
964extern DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube);
965extern int Cudd_NextPrime(DdGen *gen, int **cube);
966extern DdNode * Cudd_bddComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
967extern DdNode * Cudd_addComputeCube (DdManager *dd, DdNode **vars, int *phase, int n);
968extern DdNode * Cudd_CubeArrayToBdd (DdManager *dd, int *array);
969extern int Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array);
970extern DdGen * Cudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node);
971extern int Cudd_NextNode (DdGen *gen, DdNode **node);
972extern int Cudd_GenFree (DdGen *gen);
973extern int Cudd_IsGenEmpty (DdGen *gen);
974extern DdNode * Cudd_IndicesToCube (DdManager *dd, int *array, int n);
975extern void Cudd_PrintVersion (FILE *fp);
976extern double Cudd_AverageDistance (DdManager *dd);
977extern long Cudd_Random (void);
978extern void Cudd_Srandom (long seed);
979extern double Cudd_Density (DdManager *dd, DdNode *f, int nvars);
980extern void Cudd_OutOfMem (long size);
981extern int Cudd_zddCount (DdManager *zdd, DdNode *P);
982extern double Cudd_zddCountDouble (DdManager *zdd, DdNode *P);
983extern DdNode   * Cudd_zddProduct (DdManager *dd, DdNode *f, DdNode *g);
984extern DdNode   * Cudd_zddUnateProduct (DdManager *dd, DdNode *f, DdNode *g);
985extern DdNode   * Cudd_zddWeakDiv (DdManager *dd, DdNode *f, DdNode *g);
986extern DdNode   * Cudd_zddDivide (DdManager *dd, DdNode *f, DdNode *g);
987extern DdNode   * Cudd_zddWeakDivF (DdManager *dd, DdNode *f, DdNode *g);
988extern DdNode   * Cudd_zddDivideF (DdManager *dd, DdNode *f, DdNode *g);
989extern DdNode   * Cudd_zddComplement (DdManager *dd, DdNode *node);
990extern MtrNode * Cudd_MakeZddTreeNode (DdManager *dd, unsigned int low, unsigned int size, unsigned int type);
991extern DdNode   * Cudd_zddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
992extern DdNode   * Cudd_bddIsop (DdManager *dd, DdNode *L, DdNode *U);
993extern DdNode   * Cudd_MakeBddFromZddCover (DdManager *dd, DdNode *node);
994extern int Cudd_zddDagSize (DdNode *p_node);
995extern double Cudd_zddCountMinterm (DdManager *zdd, DdNode *node, int path);
996extern void Cudd_zddPrintSubtable (DdManager *table);
997extern DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B);
998extern DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f);
999extern int Cudd_zddReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize);
1000extern int Cudd_zddShuffleHeap (DdManager *table, int *permutation);
1001extern DdNode * Cudd_zddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
1002extern DdNode * Cudd_zddUnion (DdManager *dd, DdNode *P, DdNode *Q);
1003extern DdNode * Cudd_zddIntersect (DdManager *dd, DdNode *P, DdNode *Q);
1004extern DdNode * Cudd_zddDiff (DdManager *dd, DdNode *P, DdNode *Q);
1005extern DdNode * Cudd_zddDiffConst (DdManager *zdd, DdNode *P, DdNode *Q);
1006extern DdNode * Cudd_zddSubset1 (DdManager *dd, DdNode *P, int var);
1007extern DdNode * Cudd_zddSubset0 (DdManager *dd, DdNode *P, int var);
1008extern DdNode * Cudd_zddChange (DdManager *dd, DdNode *P, int var);
1009extern void Cudd_zddSymmProfile (DdManager *table, int lower, int upper);
1010extern int Cudd_zddPrintMinterm (DdManager *zdd, DdNode *node);
1011extern int Cudd_zddPrintCover (DdManager *zdd, DdNode *node);
1012extern int Cudd_zddPrintDebug (DdManager *zdd, DdNode *f, int n, int pr);
1013extern DdGen * Cudd_zddFirstPath (DdManager *zdd, DdNode *f, int **path);
1014extern int Cudd_zddNextPath (DdGen *gen, int **path);
1015extern char * Cudd_zddCoverPathToString (DdManager *zdd, int *path, char *str);
1016extern int Cudd_zddDumpDot (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
1017extern int Cudd_bddSetPiVar (DdManager *dd, int index);
1018extern int Cudd_bddSetPsVar (DdManager *dd, int index);
1019extern int Cudd_bddSetNsVar (DdManager *dd, int index);
1020extern int Cudd_bddIsPiVar (DdManager *dd, int index);
1021extern int Cudd_bddIsPsVar (DdManager *dd, int index);
1022extern int Cudd_bddIsNsVar (DdManager *dd, int index);
1023extern int Cudd_bddSetPairIndex (DdManager *dd, int index, int pairIndex);
1024extern int Cudd_bddReadPairIndex (DdManager *dd, int index);
1025extern int Cudd_bddSetVarToBeGrouped (DdManager *dd, int index);
1026extern int Cudd_bddSetVarHardGroup (DdManager *dd, int index);
1027extern int Cudd_bddResetVarToBeGrouped (DdManager *dd, int index);
1028extern int Cudd_bddIsVarToBeGrouped (DdManager *dd, int index);
1029extern int Cudd_bddSetVarToBeUngrouped (DdManager *dd, int index);
1030extern int Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index);
1031extern int Cudd_bddIsVarHardGroup (DdManager *dd, int index);
1032
1033/**AutomaticEnd***************************************************************/
1034
1035#ifdef __cplusplus
1036} /* end of extern "C" */
1037#endif
1038
1039#endif /* _CUDD */
Note: See TracBrowser for help on using the repository browser.