source: vis_dev/glu-2.3/src/cuBdd/cudd.h @ 25

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

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