abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cudd.h
Go to the documentation of this file.
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 ABC__bdd__cudd__cudd_h
58 #define ABC__bdd__cudd__cudd_h
59 
60 
61 /*---------------------------------------------------------------------------*/
62 /* Nested includes */
63 /*---------------------------------------------------------------------------*/
64 
65 #include "bdd/mtr/mtr.h"
66 #include "bdd/epd/epd.h"
67 
68 ABC_NAMESPACE_HEADER_START
69 
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 ******************************************************************************/
151 typedef 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 ******************************************************************************/
184 typedef 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 ******************************************************************************/
205 typedef 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 ******************************************************************************/
220 typedef 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 ******************************************************************************/
237 typedef 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 ******************************************************************************/
252 typedef 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
260 typedef unsigned int DdHalfWord;
261 #else
262 typedef unsigned short DdHalfWord;
263 #endif
264 
265 #ifdef __osf__
266 #pragma pointer_size save
267 #pragma pointer_size short
268 #endif
269 
270 typedef struct DdNode DdNode;
271 
272 typedef 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 */
278 struct 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  ABC_INT64_T Id;
287 };
288 
289 #ifdef __osf__
290 #pragma pointer_size restore
291 #endif
292 
293 typedef struct DdManager DdManager;
294 
295 typedef struct DdGen DdGen;
296 
297 /* These typedefs for arbitrary precision arithmetic should agree with
298 ** the corresponding constant definitions above. */
299 #if SIZEOF_LONG == 8
300 typedef unsigned int DdApaDigit;
301 typedef unsigned long int DdApaDoubleDigit;
302 #else
303 typedef unsigned short int DdApaDigit;
304 typedef unsigned int DdApaDoubleDigit;
305 #endif
306 typedef DdApaDigit * DdApaNumber;
307 
308 /* Return type for function computing two-literal clauses. */
309 typedef struct DdTlcInfo DdTlcInfo;
310 
311 /* Type of hook function. */
312 typedef int (*DD_HFP)(DdManager *, const char *, void *);
313 /* Type of priority function */
314 typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **,
315  DdNode **);
316 /* Type of apply operator. */
317 typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
318 /* Type of monadic apply operator. */
319 typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
320 /* Types of cache tag functions. */
321 typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
322 typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
323 /* Type of memory-out function. */
324 typedef void (*DD_OOMFP)(long);
325 /* Type of comparison function for qsort. */
326 typedef int (*DD_QSFP)(const void *, const void *);
327 
328 /*---------------------------------------------------------------------------*/
329 /* Variable declarations */
330 /*---------------------------------------------------------------------------*/
331 
332 
333 /*---------------------------------------------------------------------------*/
334 /* Macro declarations */
335 /*---------------------------------------------------------------------------*/
336 
337 
338 /**Macro***********************************************************************
339 
340  Synopsis [Returns 1 if the node is a constant node.]
341 
342  Description [Returns 1 if the node is a constant node (rather than an
343  internal node). All constant nodes have the same index
344  (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either
345  regular or complemented.]
346 
347  SideEffects [none]
348 
349  SeeAlso []
350 
351 ******************************************************************************/
352 #define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)
353 
354 
355 /**Macro***********************************************************************
356 
357  Synopsis [Complements a DD.]
358 
359  Description [Complements a DD by flipping the complement attribute of
360  the pointer (the least significant bit).]
361 
362  SideEffects [none]
363 
364  SeeAlso [Cudd_NotCond]
365 
366 ******************************************************************************/
367 #define Cudd_Not(node) ((DdNode *)((ptrint)(node) ^ 01))
368 
369 
370 /**Macro***********************************************************************
371 
372  Synopsis [Complements a DD if a condition is true.]
373 
374  Description [Complements a DD if condition c is true; c should be
375  either 0 or 1, because it is used directly (for efficiency). If in
376  doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]
377 
378  SideEffects [none]
379 
380  SeeAlso [Cudd_Not]
381 
382 ******************************************************************************/
383 #define Cudd_NotCond(node,c) ((DdNode *)((ptrint)(node) ^ (c)))
384 
385 
386 /**Macro***********************************************************************
387 
388  Synopsis [Returns the regular version of a pointer.]
389 
390  Description []
391 
392  SideEffects [none]
393 
394  SeeAlso [Cudd_Complement Cudd_IsComplement]
395 
396 ******************************************************************************/
397 #define Cudd_Regular(node) ((DdNode *)((ptruint)(node) & ~01))
398 
399 
400 /**Macro***********************************************************************
401 
402  Synopsis [Returns the complemented version of a pointer.]
403 
404  Description []
405 
406  SideEffects [none]
407 
408  SeeAlso [Cudd_Regular Cudd_IsComplement]
409 
410 ******************************************************************************/
411 #define Cudd_Complement(node) ((DdNode *)((ptruint)(node) | 01))
412 
413 
414 /**Macro***********************************************************************
415 
416  Synopsis [Returns 1 if a pointer is complemented.]
417 
418  Description []
419 
420  SideEffects [none]
421 
422  SeeAlso [Cudd_Regular Cudd_Complement]
423 
424 ******************************************************************************/
425 #define Cudd_IsComplement(node) ((int) ((ptrint) (node) & 01))
426 
427 
428 /**Macro***********************************************************************
429 
430  Synopsis [Returns the then child of an internal node.]
431 
432  Description [Returns the then child of an internal node. If
433  <code>node</code> is a constant node, the result is unpredictable.]
434 
435  SideEffects [none]
436 
437  SeeAlso [Cudd_E Cudd_V]
438 
439 ******************************************************************************/
440 #define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)
441 
442 
443 /**Macro***********************************************************************
444 
445  Synopsis [Returns the else child of an internal node.]
446 
447  Description [Returns the else child of an internal node. If
448  <code>node</code> is a constant node, the result is unpredictable.]
449 
450  SideEffects [none]
451 
452  SeeAlso [Cudd_T Cudd_V]
453 
454 ******************************************************************************/
455 #define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)
456 
457 
458 /**Macro***********************************************************************
459 
460  Synopsis [Returns the value of a constant node.]
461 
462  Description [Returns the value of a constant node. If
463  <code>node</code> is an internal node, the result is unpredictable.]
464 
465  SideEffects [none]
466 
467  SeeAlso [Cudd_T Cudd_E]
468 
469 ******************************************************************************/
470 #define Cudd_V(node) ((Cudd_Regular(node))->type.value)
471 
472 
473 /**Macro***********************************************************************
474 
475  Synopsis [Returns the current position in the order of variable
476  index.]
477 
478  Description [Returns the current position in the order of variable
479  index. This macro is obsolete and is kept for compatibility. New
480  applications should use Cudd_ReadPerm instead.]
481 
482  SideEffects [none]
483 
484  SeeAlso [Cudd_ReadPerm]
485 
486 ******************************************************************************/
487 #define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))
488 
489 
490 /**Macro***********************************************************************
491 
492  Synopsis [Iterates over the cubes of a decision diagram.]
493 
494  Description [Iterates over the cubes of a decision diagram f.
495  <ul>
496  <li> DdManager *manager;
497  <li> DdNode *f;
498  <li> DdGen *gen;
499  <li> int *cube;
500  <li> CUDD_VALUE_TYPE value;
501  </ul>
502  Cudd_ForeachCube allocates and frees the generator. Therefore the
503  application should not try to do that. Also, the cube is freed at the
504  end of Cudd_ForeachCube and hence is not available outside of the loop.<p>
505  CAUTION: It is assumed that dynamic reordering will not occur while
506  there are open generators. It is the user's responsibility to make sure
507  that dynamic reordering does not occur. As long as new nodes are not created
508  during generation, and dynamic reordering is not called explicitly,
509  dynamic reordering will not occur. Alternatively, it is sufficient to
510  disable dynamic reordering. It is a mistake to dispose of a diagram
511  on which generation is ongoing.]
512 
513  SideEffects [none]
514 
515  SeeAlso [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree
516  Cudd_IsGenEmpty Cudd_AutodynDisable]
517 
518 ******************************************************************************/
519 #define Cudd_ForeachCube(manager, f, gen, cube, value)\
520  for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
521  Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
522  (void) Cudd_NextCube(gen, &cube, &value))
523 
524 
525 /**Macro***********************************************************************
526 
527  Synopsis [Iterates over the primes of a Boolean function.]
528 
529  Description [Iterates over the primes of a Boolean function producing
530  a prime and irredundant cover.
531  <ul>
532  <li> DdManager *manager;
533  <li> DdNode *l;
534  <li> DdNode *u;
535  <li> DdGen *gen;
536  <li> int *cube;
537  </ul>
538  The Boolean function is described by an upper bound and a lower bound. If
539  the function is completely specified, the two bounds coincide.
540  Cudd_ForeachPrime allocates and frees the generator. Therefore the
541  application should not try to do that. Also, the cube is freed at the
542  end of Cudd_ForeachPrime and hence is not available outside of the loop.<p>
543  CAUTION: It is a mistake to change a diagram on which generation is ongoing.]
544 
545  SideEffects [none]
546 
547  SeeAlso [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree
548  Cudd_IsGenEmpty]
549 
550 ******************************************************************************/
551 #define Cudd_ForeachPrime(manager, l, u, gen, cube)\
552  for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
553  Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
554  (void) Cudd_NextPrime(gen, &cube))
555 
556 
557 /**Macro***********************************************************************
558 
559  Synopsis [Iterates over the nodes of a decision diagram.]
560 
561  Description [Iterates over the nodes of a decision diagram f.
562  <ul>
563  <li> DdManager *manager;
564  <li> DdNode *f;
565  <li> DdGen *gen;
566  <li> DdNode *node;
567  </ul>
568  The nodes are returned in a seemingly random order.
569  Cudd_ForeachNode allocates and frees the generator. Therefore the
570  application should not try to do that.<p>
571  CAUTION: It is assumed that dynamic reordering will not occur while
572  there are open generators. It is the user's responsibility to make sure
573  that dynamic reordering does not occur. As long as new nodes are not created
574  during generation, and dynamic reordering is not called explicitly,
575  dynamic reordering will not occur. Alternatively, it is sufficient to
576  disable dynamic reordering. It is a mistake to dispose of a diagram
577  on which generation is ongoing.]
578 
579  SideEffects [none]
580 
581  SeeAlso [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree
582  Cudd_IsGenEmpty Cudd_AutodynDisable]
583 
584 ******************************************************************************/
585 #define Cudd_ForeachNode(manager, f, gen, node)\
586  for((gen) = Cudd_FirstNode(manager, f, &node);\
587  Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
588  (void) Cudd_NextNode(gen, &node))
589 
590 
591 /**Macro***********************************************************************
592 
593  Synopsis [Iterates over the paths of a ZDD.]
594 
595  Description [Iterates over the paths of a ZDD f.
596  <ul>
597  <li> DdManager *manager;
598  <li> DdNode *f;
599  <li> DdGen *gen;
600  <li> int *path;
601  </ul>
602  Cudd_zddForeachPath allocates and frees the generator. Therefore the
603  application should not try to do that. Also, the path is freed at the
604  end of Cudd_zddForeachPath and hence is not available outside of the loop.<p>
605  CAUTION: It is assumed that dynamic reordering will not occur while
606  there are open generators. It is the user's responsibility to make sure
607  that dynamic reordering does not occur. As long as new nodes are not created
608  during generation, and dynamic reordering is not called explicitly,
609  dynamic reordering will not occur. Alternatively, it is sufficient to
610  disable dynamic reordering. It is a mistake to dispose of a diagram
611  on which generation is ongoing.]
612 
613  SideEffects [none]
614 
615  SeeAlso [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree
616  Cudd_IsGenEmpty Cudd_AutodynDisable]
617 
618 ******************************************************************************/
619 #define Cudd_zddForeachPath(manager, f, gen, path)\
620  for((gen) = Cudd_zddFirstPath(manager, f, &path);\
621  Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
622  (void) Cudd_zddNextPath(gen, &path))
623 
624 
625 
626 /**AutomaticStart*************************************************************/
627 
628 /*---------------------------------------------------------------------------*/
629 /* Function prototypes */
630 /*---------------------------------------------------------------------------*/
631 
632 extern DdNode * Cudd_addNewVar( DdManager * dd );
633 extern DdNode * Cudd_addNewVarAtLevel( DdManager * dd, int level );
634 extern DdNode * Cudd_bddNewVar( DdManager * dd );
635 extern DdNode * Cudd_bddNewVarAtLevel( DdManager * dd, int level );
636 extern DdNode * Cudd_addIthVar( DdManager * dd, int i );
637 extern DdNode * Cudd_bddIthVar( DdManager * dd, int i );
638 extern DdNode * Cudd_zddIthVar( DdManager * dd, int i );
639 extern int Cudd_zddVarsFromBddVars( DdManager * dd, int multiplicity );
640 extern DdNode * Cudd_addConst( DdManager * dd, CUDD_VALUE_TYPE c );
641 extern int Cudd_IsNonConstant( DdNode * f );
642 extern void Cudd_AutodynEnable( DdManager * unique, Cudd_ReorderingType method );
643 extern void Cudd_AutodynDisable( DdManager * unique );
644 extern int Cudd_ReorderingStatus( DdManager * unique, Cudd_ReorderingType * method );
645 extern void Cudd_AutodynEnableZdd( DdManager * unique, Cudd_ReorderingType method );
646 extern void Cudd_AutodynDisableZdd( DdManager * unique );
647 extern int Cudd_ReorderingStatusZdd( DdManager * unique, Cudd_ReorderingType * method );
648 extern int Cudd_zddRealignmentEnabled( DdManager * unique );
649 extern void Cudd_zddRealignEnable( DdManager * unique );
650 extern void Cudd_zddRealignDisable( DdManager * unique );
651 extern int Cudd_bddRealignmentEnabled( DdManager * unique );
652 extern void Cudd_bddRealignEnable( DdManager * unique );
653 extern void Cudd_bddRealignDisable( DdManager * unique );
654 extern DdNode * Cudd_ReadOne( DdManager * dd );
655 extern DdNode * Cudd_ReadZddOne( DdManager * dd, int i );
656 extern DdNode * Cudd_ReadZero( DdManager * dd );
657 extern DdNode * Cudd_ReadLogicZero( DdManager * dd );
658 extern DdNode * Cudd_ReadPlusInfinity( DdManager * dd );
659 extern DdNode * Cudd_ReadMinusInfinity( DdManager * dd );
660 extern DdNode * Cudd_ReadBackground( DdManager * dd );
661 extern void Cudd_SetBackground( DdManager * dd, DdNode * bck );
662 extern unsigned int Cudd_ReadCacheSlots( DdManager * dd );
663 extern double Cudd_ReadCacheUsedSlots( DdManager * dd );
664 extern double Cudd_ReadCacheLookUps( DdManager * dd );
665 extern double Cudd_ReadCacheHits( DdManager * dd );
666 extern double Cudd_ReadRecursiveCalls( DdManager * dd );
667 extern unsigned int Cudd_ReadMinHit( DdManager * dd );
668 extern void Cudd_SetMinHit( DdManager * dd, unsigned int hr );
669 extern unsigned int Cudd_ReadLooseUpTo( DdManager * dd );
670 extern void Cudd_SetLooseUpTo( DdManager * dd, unsigned int lut );
671 extern unsigned int Cudd_ReadMaxCache( DdManager * dd );
672 extern unsigned int Cudd_ReadMaxCacheHard( DdManager * dd );
673 extern void Cudd_SetMaxCacheHard( DdManager * dd, unsigned int mc );
674 extern int Cudd_ReadSize( DdManager * dd );
675 extern int Cudd_ReadZddSize( DdManager * dd );
676 extern unsigned int Cudd_ReadSlots( DdManager * dd );
677 extern double Cudd_ReadUsedSlots( DdManager * dd );
678 extern double Cudd_ExpectedUsedSlots( DdManager * dd );
679 extern unsigned int Cudd_ReadKeys( DdManager * dd );
680 extern unsigned int Cudd_ReadDead( DdManager * dd );
681 extern unsigned int Cudd_ReadMinDead( DdManager * dd );
682 extern int Cudd_ReadReorderings( DdManager * dd );
683 extern long Cudd_ReadReorderingTime( DdManager * dd );
684 extern int Cudd_ReadGarbageCollections( DdManager * dd );
685 extern long Cudd_ReadGarbageCollectionTime( DdManager * dd );
686 extern double Cudd_ReadNodesFreed( DdManager * dd );
687 extern double Cudd_ReadNodesDropped( DdManager * dd );
688 extern double Cudd_ReadUniqueLookUps( DdManager * dd );
689 extern double Cudd_ReadUniqueLinks( DdManager * dd );
690 extern int Cudd_ReadSiftMaxVar( DdManager * dd );
691 extern void Cudd_SetSiftMaxVar( DdManager * dd, int smv );
692 extern int Cudd_ReadSiftMaxSwap( DdManager * dd );
693 extern void Cudd_SetSiftMaxSwap( DdManager * dd, int sms );
694 extern double Cudd_ReadMaxGrowth( DdManager * dd );
695 extern void Cudd_SetMaxGrowth( DdManager * dd, double mg );
696 extern double Cudd_ReadMaxGrowthAlternate( DdManager * dd );
697 extern void Cudd_SetMaxGrowthAlternate( DdManager * dd, double mg );
698 extern int Cudd_ReadReorderingCycle( DdManager * dd );
699 extern void Cudd_SetReorderingCycle( DdManager * dd, int cycle );
700 extern MtrNode * Cudd_ReadTree( DdManager * dd );
701 extern void Cudd_SetTree( DdManager * dd, MtrNode * tree );
702 extern void Cudd_FreeTree( DdManager * dd );
703 extern MtrNode * Cudd_ReadZddTree( DdManager * dd );
704 extern void Cudd_SetZddTree( DdManager * dd, MtrNode * tree );
705 extern void Cudd_FreeZddTree( DdManager * dd );
706 extern unsigned int Cudd_NodeReadIndex( DdNode * node );
707 extern int Cudd_ReadPerm( DdManager * dd, int i );
708 extern int Cudd_ReadPermZdd( DdManager * dd, int i );
709 extern int Cudd_ReadInvPerm( DdManager * dd, int i );
710 extern int Cudd_ReadInvPermZdd( DdManager * dd, int i );
711 extern DdNode * Cudd_ReadVars( DdManager * dd, int i );
712 extern CUDD_VALUE_TYPE Cudd_ReadEpsilon( DdManager * dd );
713 extern void Cudd_SetEpsilon( DdManager * dd, CUDD_VALUE_TYPE ep );
714 extern Cudd_AggregationType Cudd_ReadGroupcheck( DdManager * dd );
715 extern void Cudd_SetGroupcheck( DdManager * dd, Cudd_AggregationType gc );
716 extern int Cudd_GarbageCollectionEnabled( DdManager * dd );
717 extern void Cudd_EnableGarbageCollection( DdManager * dd );
718 extern void Cudd_DisableGarbageCollection( DdManager * dd );
719 extern int Cudd_DeadAreCounted( DdManager * dd );
720 extern void Cudd_TurnOnCountDead( DdManager * dd );
721 extern void Cudd_TurnOffCountDead( DdManager * dd );
722 extern int Cudd_ReadRecomb( DdManager * dd );
723 extern void Cudd_SetRecomb( DdManager * dd, int recomb );
724 extern int Cudd_ReadSymmviolation( DdManager * dd );
725 extern void Cudd_SetSymmviolation( DdManager * dd, int symmviolation );
726 extern int Cudd_ReadArcviolation( DdManager * dd );
727 extern void Cudd_SetArcviolation( DdManager * dd, int arcviolation );
728 extern int Cudd_ReadPopulationSize( DdManager * dd );
729 extern void Cudd_SetPopulationSize( DdManager * dd, int populationSize );
730 extern int Cudd_ReadNumberXovers( DdManager * dd );
731 extern void Cudd_SetNumberXovers( DdManager * dd, int numberXovers );
732 extern unsigned long Cudd_ReadMemoryInUse( DdManager * dd );
733 extern int Cudd_PrintInfo( DdManager * dd, FILE * fp );
734 extern long Cudd_ReadPeakNodeCount( DdManager * dd );
735 extern int Cudd_ReadPeakLiveNodeCount( DdManager * dd );
736 extern long Cudd_ReadNodeCount( DdManager * dd );
737 extern long Cudd_zddReadNodeCount( DdManager * dd );
738 extern int Cudd_AddHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
739 extern int Cudd_RemoveHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
740 extern int Cudd_IsInHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
741 extern int Cudd_StdPreReordHook( DdManager * dd, const char * str, void * data );
742 extern int Cudd_StdPostReordHook( DdManager * dd, const char * str, void * data );
743 extern int Cudd_EnableReorderingReporting( DdManager * dd );
744 extern int Cudd_DisableReorderingReporting( DdManager * dd );
745 extern int Cudd_ReorderingReporting( DdManager * dd );
746 extern Cudd_ErrorType Cudd_ReadErrorCode( DdManager * dd );
747 extern void Cudd_ClearErrorCode( DdManager * dd );
748 extern FILE * Cudd_ReadStdout( DdManager * dd );
749 extern void Cudd_SetStdout( DdManager * dd, FILE * fp );
750 extern FILE * Cudd_ReadStderr( DdManager * dd );
751 extern void Cudd_SetStderr( DdManager * dd, FILE * fp );
752 extern unsigned int Cudd_ReadNextReordering( DdManager * dd );
753 extern void Cudd_SetNextReordering( DdManager * dd, unsigned int next );
754 extern double Cudd_ReadSwapSteps( DdManager * dd );
755 extern unsigned int Cudd_ReadMaxLive( DdManager * dd );
756 extern void Cudd_SetMaxLive( DdManager * dd, unsigned int maxLive );
757 extern unsigned long Cudd_ReadMaxMemory( DdManager * dd );
758 extern void Cudd_SetMaxMemory( DdManager * dd, unsigned long maxMemory );
759 extern int Cudd_bddBindVar( DdManager * dd, int index );
760 extern int Cudd_bddUnbindVar( DdManager * dd, int index );
761 extern int Cudd_bddVarIsBound( DdManager * dd, int index );
762 extern DdNode * Cudd_addExistAbstract( DdManager * manager, DdNode * f, DdNode * cube );
763 extern DdNode * Cudd_addUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube );
764 extern DdNode * Cudd_addOrAbstract( DdManager * manager, DdNode * f, DdNode * cube );
765 extern DdNode * Cudd_addApply( DdManager * dd, DdNode * ( * )(DdManager * , DdNode ** , DdNode ** ), DdNode * f, DdNode * g );
766 extern DdNode * Cudd_addPlus( DdManager * dd, DdNode ** f, DdNode ** g );
767 extern DdNode * Cudd_addTimes( DdManager * dd, DdNode ** f, DdNode ** g );
768 extern DdNode * Cudd_addThreshold( DdManager * dd, DdNode ** f, DdNode ** g );
769 extern DdNode * Cudd_addSetNZ( DdManager * dd, DdNode ** f, DdNode ** g );
770 extern DdNode * Cudd_addDivide( DdManager * dd, DdNode ** f, DdNode ** g );
771 extern DdNode * Cudd_addMinus( DdManager * dd, DdNode ** f, DdNode ** g );
772 extern DdNode * Cudd_addMinimum( DdManager * dd, DdNode ** f, DdNode ** g );
773 extern DdNode * Cudd_addMaximum( DdManager * dd, DdNode ** f, DdNode ** g );
774 extern DdNode * Cudd_addOneZeroMaximum( DdManager * dd, DdNode ** f, DdNode ** g );
775 extern DdNode * Cudd_addDiff( DdManager * dd, DdNode ** f, DdNode ** g );
776 extern DdNode * Cudd_addAgreement( DdManager * dd, DdNode ** f, DdNode ** g );
777 extern DdNode * Cudd_addOr( DdManager * dd, DdNode ** f, DdNode ** g );
778 extern DdNode * Cudd_addNand( DdManager * dd, DdNode ** f, DdNode ** g );
779 extern DdNode * Cudd_addNor( DdManager * dd, DdNode ** f, DdNode ** g );
780 extern DdNode * Cudd_addXor( DdManager * dd, DdNode ** f, DdNode ** g );
781 extern DdNode * Cudd_addXnor( DdManager * dd, DdNode ** f, DdNode ** g );
782 extern DdNode * Cudd_addMonadicApply( DdManager * dd, DdNode * ( * op)(DdManager * , DdNode * ), DdNode * f );
783 extern DdNode * Cudd_addLog( DdManager * dd, DdNode * f );
784 extern DdNode * Cudd_addFindMax( DdManager * dd, DdNode * f );
785 extern DdNode * Cudd_addFindMin( DdManager * dd, DdNode * f );
786 extern DdNode * Cudd_addIthBit( DdManager * dd, DdNode * f, int bit );
787 extern DdNode * Cudd_addScalarInverse( DdManager * dd, DdNode * f, DdNode * epsilon );
788 extern DdNode * Cudd_addIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
789 extern DdNode * Cudd_addIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
790 extern DdNode * Cudd_addEvalConst( DdManager * dd, DdNode * f, DdNode * g );
791 extern int Cudd_addLeq( DdManager * dd, DdNode * f, DdNode * g );
792 extern DdNode * Cudd_addCmpl( DdManager * dd, DdNode * f );
793 extern DdNode * Cudd_addNegate( DdManager * dd, DdNode * f );
794 extern DdNode * Cudd_addRoundOff( DdManager * dd, DdNode * f, int N );
795 extern DdNode * Cudd_addWalsh( DdManager * dd, DdNode ** x, DdNode ** y, int n );
796 extern DdNode * Cudd_addResidue( DdManager * dd, int n, int m, int options, int top );
797 extern DdNode * Cudd_bddAndAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube );
798 extern DdNode * Cudd_bddAndAbstractLimit( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, unsigned int limit );
799 extern int Cudd_ApaNumberOfDigits( int binaryDigits );
800 extern DdApaNumber Cudd_NewApaNumber( int digits );
801 extern void Cudd_ApaCopy( int digits, DdApaNumber source, DdApaNumber dest );
802 extern DdApaDigit Cudd_ApaAdd( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum );
803 extern DdApaDigit Cudd_ApaSubtract( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff );
804 extern DdApaDigit Cudd_ApaShortDivision( int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient );
805 extern unsigned int Cudd_ApaIntDivision( int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient );
806 extern void Cudd_ApaShiftRight( int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b );
807 extern void Cudd_ApaSetToLiteral( int digits, DdApaNumber number, DdApaDigit literal );
808 extern void Cudd_ApaPowerOfTwo( int digits, DdApaNumber number, int power );
809 extern int Cudd_ApaCompare( int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second );
810 extern int Cudd_ApaCompareRatios( int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen );
811 extern int Cudd_ApaPrintHex( FILE * fp, int digits, DdApaNumber number );
812 extern int Cudd_ApaPrintDecimal( FILE * fp, int digits, DdApaNumber number );
813 extern int Cudd_ApaPrintExponential( FILE * fp, int digits, DdApaNumber number, int precision );
814 extern DdApaNumber Cudd_ApaCountMinterm( DdManager * manager, DdNode * node, int nvars, int * digits );
815 extern int Cudd_ApaPrintMinterm( FILE * fp, DdManager * dd, DdNode * node, int nvars );
816 extern int Cudd_ApaPrintMintermExp( FILE * fp, DdManager * dd, DdNode * node, int nvars, int precision );
817 extern int Cudd_ApaPrintDensity( FILE * fp, DdManager * dd, DdNode * node, int nvars );
818 extern DdNode * Cudd_UnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality );
819 extern DdNode * Cudd_OverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality );
820 extern DdNode * Cudd_RemapUnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality );
821 extern DdNode * Cudd_RemapOverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality );
822 extern DdNode * Cudd_BiasedUnderApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 );
823 extern DdNode * Cudd_BiasedOverApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 );
824 extern DdNode * Cudd_bddExistAbstract( DdManager * manager, DdNode * f, DdNode * cube );
825 extern DdNode * Cudd_bddXorExistAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube );
826 extern DdNode * Cudd_bddUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube );
827 extern DdNode * Cudd_bddBooleanDiff( DdManager * manager, DdNode * f, int x );
828 extern int Cudd_bddVarIsDependent( DdManager * dd, DdNode * f, DdNode * var );
829 extern double Cudd_bddCorrelation( DdManager * manager, DdNode * f, DdNode * g );
830 extern double Cudd_bddCorrelationWeights( DdManager * manager, DdNode * f, DdNode * g, double * prob );
831 extern DdNode * Cudd_bddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
832 extern DdNode * Cudd_bddIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
833 extern DdNode * Cudd_bddIntersect( DdManager * dd, DdNode * f, DdNode * g );
834 extern DdNode * Cudd_bddAnd( DdManager * dd, DdNode * f, DdNode * g );
835 extern DdNode * Cudd_bddAndLimit( DdManager * dd, DdNode * f, DdNode * g, unsigned int limit );
836 extern DdNode * Cudd_bddOr( DdManager * dd, DdNode * f, DdNode * g );
837 extern DdNode * Cudd_bddNand( DdManager * dd, DdNode * f, DdNode * g );
838 extern DdNode * Cudd_bddNor( DdManager * dd, DdNode * f, DdNode * g );
839 extern DdNode * Cudd_bddXor( DdManager * dd, DdNode * f, DdNode * g );
840 extern DdNode * Cudd_bddXnor( DdManager * dd, DdNode * f, DdNode * g );
841 extern int Cudd_bddLeq( DdManager * dd, DdNode * f, DdNode * g );
842 extern DdNode * Cudd_addBddThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value );
843 extern DdNode * Cudd_addBddStrictThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value );
844 extern DdNode * Cudd_addBddInterval( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper );
845 extern DdNode * Cudd_addBddIthBit( DdManager * dd, DdNode * f, int bit );
846 extern DdNode * Cudd_BddToAdd( DdManager * dd, DdNode * B );
847 extern DdNode * Cudd_addBddPattern( DdManager * dd, DdNode * f );
848 extern DdNode * Cudd_bddTransfer( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
849 extern int Cudd_DebugCheck( DdManager * table );
850 extern int Cudd_CheckKeys( DdManager * table );
851 extern DdNode * Cudd_bddClippingAnd( DdManager * dd, DdNode * f, DdNode * g, int maxDepth, int direction );
852 extern DdNode * Cudd_bddClippingAndAbstract( DdManager * dd, DdNode * f, DdNode * g, DdNode * cube, int maxDepth, int direction );
853 extern DdNode * Cudd_Cofactor( DdManager * dd, DdNode * f, DdNode * g );
854 extern DdNode * Cudd_bddCompose( DdManager * dd, DdNode * f, DdNode * g, int v );
855 extern DdNode * Cudd_addCompose( DdManager * dd, DdNode * f, DdNode * g, int v );
856 extern DdNode * Cudd_addPermute( DdManager * manager, DdNode * node, int * permut );
857 extern DdNode * Cudd_addSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n );
858 extern DdNode * Cudd_bddPermute( DdManager * manager, DdNode * node, int * permut );
859 extern DdNode * Cudd_bddVarMap( DdManager * manager, DdNode * f );
860 extern int Cudd_SetVarMap( DdManager * manager, DdNode ** x, DdNode ** y, int n );
861 extern DdNode * Cudd_bddSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n );
862 extern DdNode * Cudd_bddAdjPermuteX( DdManager * dd, DdNode * B, DdNode ** x, int n );
863 extern DdNode * Cudd_addVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector );
864 extern DdNode * Cudd_addGeneralVectorCompose( DdManager * dd, DdNode * f, DdNode ** vectorOn, DdNode ** vectorOff );
865 extern DdNode * Cudd_addNonSimCompose( DdManager * dd, DdNode * f, DdNode ** vector );
866 extern DdNode * Cudd_bddVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector );
867 extern int Cudd_bddApproxConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
868 extern int Cudd_bddApproxDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
869 extern int Cudd_bddIterConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
870 extern int Cudd_bddIterDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
871 extern int Cudd_bddGenConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
872 extern int Cudd_bddGenDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
873 extern int Cudd_bddVarConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
874 extern int Cudd_bddVarDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
875 extern DdNode * Cudd_FindEssential( DdManager * dd, DdNode * f );
876 extern int Cudd_bddIsVarEssential( DdManager * manager, DdNode * f, int id, int phase );
877 extern DdTlcInfo * Cudd_FindTwoLiteralClauses( DdManager * dd, DdNode * f );
878 extern int Cudd_PrintTwoLiteralClauses( DdManager * dd, DdNode * f, char ** names, FILE * fp );
879 extern int Cudd_ReadIthClause( DdTlcInfo * tlc, int i, DdHalfWord * var1, DdHalfWord * var2, int * phase1, int * phase2 );
880 extern void Cudd_tlcInfoFree( DdTlcInfo * t );
881 extern int Cudd_DumpBlif( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, char * mname, FILE * fp, int mv );
882 extern int Cudd_DumpBlifBody( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp, int mv );
883 extern int Cudd_DumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
884 extern int Cudd_DumpDaVinci( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
885 extern int Cudd_DumpDDcal( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
886 extern int Cudd_DumpFactoredForm( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
887 extern DdNode * Cudd_bddConstrain( DdManager * dd, DdNode * f, DdNode * c );
888 extern DdNode * Cudd_bddRestrict( DdManager * dd, DdNode * f, DdNode * c );
889 extern DdNode * Cudd_bddNPAnd( DdManager * dd, DdNode * f, DdNode * c );
890 extern DdNode * Cudd_addConstrain( DdManager * dd, DdNode * f, DdNode * c );
891 extern DdNode ** Cudd_bddConstrainDecomp( DdManager * dd, DdNode * f );
892 extern DdNode * Cudd_addRestrict( DdManager * dd, DdNode * f, DdNode * c );
893 extern DdNode ** Cudd_bddCharToVect( DdManager * dd, DdNode * f );
894 extern DdNode * Cudd_bddLICompaction( DdManager * dd, DdNode * f, DdNode * c );
895 extern DdNode * Cudd_bddSqueeze( DdManager * dd, DdNode * l, DdNode * u );
896 extern DdNode * Cudd_bddMinimize( DdManager * dd, DdNode * f, DdNode * c );
897 extern DdNode * Cudd_SubsetCompress( DdManager * dd, DdNode * f, int nvars, int threshold );
898 extern DdNode * Cudd_SupersetCompress( DdManager * dd, DdNode * f, int nvars, int threshold );
899 extern MtrNode * Cudd_MakeTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type );
900 extern 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 );
901 extern DdManager * Cudd_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory );
902 extern void Cudd_Quit( DdManager * unique );
903 extern int Cudd_PrintLinear( DdManager * table );
904 extern int Cudd_ReadLinear( DdManager * table, int x, int y );
905 extern DdNode * Cudd_bddLiteralSetIntersection( DdManager * dd, DdNode * f, DdNode * g );
906 extern DdNode * Cudd_addMatrixMultiply( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz );
907 extern DdNode * Cudd_addTimesPlus( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz );
908 extern DdNode * Cudd_addTriangle( DdManager * dd, DdNode * f, DdNode * g, DdNode ** z, int nz );
909 extern DdNode * Cudd_addOuterSum( DdManager * dd, DdNode * M, DdNode * r, DdNode * c );
910 extern DdNode * Cudd_PrioritySelect( DdManager * dd, DdNode * R, DdNode ** x, DdNode ** y, DdNode ** z, DdNode * Pi, int n, DdNode * ( * )(DdManager * , int, DdNode ** , DdNode ** , DdNode ** ) );
911 extern DdNode * Cudd_Xgty( DdManager * dd, int N, DdNode ** z, DdNode ** x, DdNode ** y );
912 extern DdNode * Cudd_Xeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y );
913 extern DdNode * Cudd_addXeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y );
914 extern DdNode * Cudd_Dxygtdxz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z );
915 extern DdNode * Cudd_Dxygtdyz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z );
916 extern DdNode * Cudd_Inequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y );
917 extern DdNode * Cudd_Disequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y );
918 extern DdNode * Cudd_bddInterval( DdManager * dd, int N, DdNode ** x, unsigned int lowerB, unsigned int upperB );
919 extern DdNode * Cudd_CProjection( DdManager * dd, DdNode * R, DdNode * Y );
920 extern DdNode * Cudd_addHamming( DdManager * dd, DdNode ** xVars, DdNode ** yVars, int nVars );
921 extern int Cudd_MinHammingDist( DdManager * dd, DdNode * f, int * minterm, int upperBound );
922 extern DdNode * Cudd_bddClosestCube( DdManager * dd, DdNode * f, DdNode * g, int * distance );
923 extern 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 );
924 extern 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 );
925 extern void Cudd_Ref( DdNode * n );
926 extern void Cudd_RecursiveDeref( DdManager * table, DdNode * n );
927 extern void Cudd_IterDerefBdd( DdManager * table, DdNode * n );
928 extern void Cudd_DelayedDerefBdd( DdManager * table, DdNode * n );
929 extern void Cudd_RecursiveDerefZdd( DdManager * table, DdNode * n );
930 extern void Cudd_Deref( DdNode * node );
931 extern int Cudd_CheckZeroRef( DdManager * manager );
932 extern int Cudd_ReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize );
933 extern int Cudd_ShuffleHeap( DdManager * table, int * permutation );
934 extern DdNode * Cudd_Eval( DdManager * dd, DdNode * f, int * inputs );
935 extern DdNode * Cudd_ShortestPath( DdManager * manager, DdNode * f, int * weight, int * support, int * length );
936 extern DdNode * Cudd_LargestCube( DdManager * manager, DdNode * f, int * length );
937 extern int Cudd_ShortestLength( DdManager * manager, DdNode * f, int * weight );
938 extern DdNode * Cudd_Decreasing( DdManager * dd, DdNode * f, int i );
939 extern DdNode * Cudd_Increasing( DdManager * dd, DdNode * f, int i );
940 extern int Cudd_EquivDC( DdManager * dd, DdNode * F, DdNode * G, DdNode * D );
941 extern int Cudd_bddLeqUnless( DdManager * dd, DdNode * f, DdNode * g, DdNode * D );
942 extern int Cudd_EqualSupNorm( DdManager * dd, DdNode * f, DdNode * g, CUDD_VALUE_TYPE tolerance, int pr );
943 extern DdNode * Cudd_bddMakePrime( DdManager * dd, DdNode * cube, DdNode * f );
944 extern double * Cudd_CofMinterm( DdManager * dd, DdNode * node );
945 extern DdNode * Cudd_SolveEqn( DdManager * bdd, DdNode * F, DdNode * Y, DdNode ** G, int ** yIndex, int n );
946 extern DdNode * Cudd_VerifySol( DdManager * bdd, DdNode * F, DdNode ** G, int * yIndex, int n );
947 extern DdNode * Cudd_SplitSet( DdManager * manager, DdNode * S, DdNode ** xVars, int n, double m );
948 extern DdNode * Cudd_SubsetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold );
949 extern DdNode * Cudd_SupersetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold );
950 extern DdNode * Cudd_SubsetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit );
951 extern DdNode * Cudd_SupersetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit );
952 extern void Cudd_SymmProfile( DdManager * table, int lower, int upper );
953 extern unsigned int Cudd_Prime( unsigned int p );
954 extern int Cudd_PrintMinterm( DdManager * manager, DdNode * node );
955 extern int Cudd_bddPrintCover( DdManager * dd, DdNode * l, DdNode * u );
956 extern int Cudd_PrintDebug( DdManager * dd, DdNode * f, int n, int pr );
957 extern int Cudd_DagSize( DdNode * node );
958 extern int Cudd_EstimateCofactor( DdManager * dd, DdNode * node, int i, int phase );
959 extern int Cudd_EstimateCofactorSimple( DdNode * node, int i );
960 extern int Cudd_SharingSize( DdNode ** nodeArray, int n );
961 extern double Cudd_CountMinterm( DdManager * manager, DdNode * node, int nvars );
962 extern int Cudd_EpdCountMinterm( DdManager * manager, DdNode * node, int nvars, EpDouble * epd );
963 extern double Cudd_CountPath( DdNode * node );
964 extern double Cudd_CountPathsToNonZero( DdNode * node );
965 extern DdNode * Cudd_Support( DdManager * dd, DdNode * f );
966 extern int * Cudd_SupportIndex( DdManager * dd, DdNode * f );
967 extern int Cudd_SupportSize( DdManager * dd, DdNode * f );
968 extern DdNode * Cudd_VectorSupport( DdManager * dd, DdNode ** F, int n );
969 extern int * Cudd_VectorSupportIndex( DdManager * dd, DdNode ** F, int n );
970 extern int Cudd_VectorSupportSize( DdManager * dd, DdNode ** F, int n );
971 extern int Cudd_ClassifySupport( DdManager * dd, DdNode * f, DdNode * g, DdNode ** common, DdNode ** onlyF, DdNode ** onlyG );
972 extern int Cudd_CountLeaves( DdNode * node );
973 extern int Cudd_bddPickOneCube( DdManager * ddm, DdNode * node, char * string );
974 extern DdNode * Cudd_bddPickOneMinterm( DdManager * dd, DdNode * f, DdNode ** vars, int n );
975 extern DdNode ** Cudd_bddPickArbitraryMinterms( DdManager * dd, DdNode * f, DdNode ** vars, int n, int k );
976 extern DdNode * Cudd_SubsetWithMaskVars( DdManager * dd, DdNode * f, DdNode ** vars, int nvars, DdNode ** maskVars, int mvars );
977 extern DdGen * Cudd_FirstCube( DdManager * dd, DdNode * f, int ** cube, CUDD_VALUE_TYPE * value );
978 extern int Cudd_NextCube( DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value );
979 extern DdGen * Cudd_FirstPrime(DdManager * dd, DdNode * l, DdNode * u, int ** cube );
980 extern int Cudd_NextPrime(DdGen * gen, int ** cube );
981 extern DdNode * Cudd_bddComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n );
982 extern DdNode * Cudd_addComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n );
983 extern DdNode * Cudd_CubeArrayToBdd( DdManager * dd, int * array );
984 extern int Cudd_BddToCubeArray( DdManager * dd, DdNode * cube, int * array );
985 extern DdGen * Cudd_FirstNode( DdManager * dd, DdNode * f, DdNode ** node );
986 extern int Cudd_NextNode( DdGen * gen, DdNode ** node );
987 extern int Cudd_GenFree( DdGen * gen );
988 extern int Cudd_IsGenEmpty( DdGen * gen );
989 extern DdNode * Cudd_IndicesToCube( DdManager * dd, int * array, int n );
990 extern void Cudd_PrintVersion( FILE * fp );
991 extern double Cudd_AverageDistance( DdManager * dd );
992 extern long Cudd_Random( void );
993 extern void Cudd_Srandom( long seed );
994 extern double Cudd_Density( DdManager * dd, DdNode * f, int nvars );
995 extern void Cudd_OutOfMem( long size );
996 extern int Cudd_zddCount( DdManager * zdd, DdNode * P );
997 extern double Cudd_zddCountDouble( DdManager * zdd, DdNode * P );
998 extern DdNode * Cudd_zddProduct( DdManager * dd, DdNode * f, DdNode * g );
999 extern DdNode * Cudd_zddUnateProduct( DdManager * dd, DdNode * f, DdNode * g );
1000 extern DdNode * Cudd_zddWeakDiv( DdManager * dd, DdNode * f, DdNode * g );
1001 extern DdNode * Cudd_zddDivide( DdManager * dd, DdNode * f, DdNode * g );
1002 extern DdNode * Cudd_zddWeakDivF( DdManager * dd, DdNode * f, DdNode * g );
1003 extern DdNode * Cudd_zddDivideF( DdManager * dd, DdNode * f, DdNode * g );
1004 extern DdNode * Cudd_zddComplement( DdManager * dd, DdNode * node );
1005 extern MtrNode * Cudd_MakeZddTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type );
1006 extern DdNode * Cudd_zddIsop( DdManager * dd, DdNode * L, DdNode * U, DdNode ** zdd_I );
1007 extern DdNode * Cudd_bddIsop( DdManager * dd, DdNode * L, DdNode * U );
1008 extern DdNode * Cudd_MakeBddFromZddCover( DdManager * dd, DdNode * node );
1009 extern int Cudd_zddDagSize( DdNode * p_node );
1010 extern double Cudd_zddCountMinterm( DdManager * zdd, DdNode * node, int path );
1011 extern void Cudd_zddPrintSubtable( DdManager * table );
1012 extern DdNode * Cudd_zddPortFromBdd( DdManager * dd, DdNode * B );
1013 extern DdNode * Cudd_zddPortToBdd( DdManager * dd, DdNode * f );
1014 extern int Cudd_zddReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize );
1015 extern int Cudd_zddShuffleHeap( DdManager * table, int * permutation );
1016 extern DdNode * Cudd_zddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
1017 extern DdNode * Cudd_zddUnion( DdManager * dd, DdNode * P, DdNode * Q );
1018 extern DdNode * Cudd_zddIntersect( DdManager * dd, DdNode * P, DdNode * Q );
1019 extern DdNode * Cudd_zddDiff( DdManager * dd, DdNode * P, DdNode * Q );
1020 extern DdNode * Cudd_zddDiffConst( DdManager * zdd, DdNode * P, DdNode * Q );
1021 extern DdNode * Cudd_zddSubset1( DdManager * dd, DdNode * P, int var );
1022 extern DdNode * Cudd_zddSubset0( DdManager * dd, DdNode * P, int var );
1023 extern DdNode * Cudd_zddChange( DdManager * dd, DdNode * P, int var );
1024 extern void Cudd_zddSymmProfile( DdManager * table, int lower, int upper );
1025 extern int Cudd_zddPrintMinterm( DdManager * zdd, DdNode * node );
1026 extern int Cudd_zddPrintCover( DdManager * zdd, DdNode * node );
1027 extern int Cudd_zddPrintDebug( DdManager * zdd, DdNode * f, int n, int pr );
1028 extern DdGen * Cudd_zddFirstPath( DdManager * zdd, DdNode * f, int ** path );
1029 extern int Cudd_zddNextPath( DdGen * gen, int ** path );
1030 extern char * Cudd_zddCoverPathToString( DdManager * zdd, int * path, char * str );
1031 extern int Cudd_zddDumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
1032 extern int Cudd_bddSetPiVar( DdManager * dd, int index );
1033 extern int Cudd_bddSetPsVar( DdManager * dd, int index );
1034 extern int Cudd_bddSetNsVar( DdManager * dd, int index );
1035 extern int Cudd_bddIsPiVar( DdManager * dd, int index );
1036 extern int Cudd_bddIsPsVar( DdManager * dd, int index );
1037 extern int Cudd_bddIsNsVar( DdManager * dd, int index );
1038 extern int Cudd_bddSetPairIndex( DdManager * dd, int index, int pairIndex );
1039 extern int Cudd_bddReadPairIndex( DdManager * dd, int index );
1040 extern int Cudd_bddSetVarToBeGrouped( DdManager * dd, int index );
1041 extern int Cudd_bddSetVarHardGroup( DdManager * dd, int index );
1042 extern int Cudd_bddResetVarToBeGrouped( DdManager * dd, int index );
1043 extern int Cudd_bddIsVarToBeGrouped( DdManager * dd, int index );
1044 extern int Cudd_bddSetVarToBeUngrouped( DdManager * dd, int index );
1045 extern int Cudd_bddIsVarToBeUngrouped( DdManager * dd, int index );
1046 extern int Cudd_bddIsVarHardGroup( DdManager * dd, int index );
1047 
1048 /**AutomaticEnd***************************************************************/
1049 
1050 
1051 
1052 ABC_NAMESPACE_HEADER_END
1053 
1054 #endif /* _CUDD */
Cudd_ReadLinear
int Cudd_ReadLinear(DdManager *table, int x, int y)
Definition: cuddLinear.c:191
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
Cudd_bddApproxDisjDecomp
int Cudd_bddApproxDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:273
Cudd_bddSetVarHardGroup
int Cudd_bddSetVarHardGroup(DdManager *dd, int index)
Definition: cuddAPI.c:4198
Cudd_SubsetHeavyBranch
DdNode * Cudd_SubsetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
Definition: cuddSubsetHB.c:209
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
Cudd_addBddThreshold
DdNode * Cudd_addBddThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
Definition: cuddBridge.c:154
Cudd_tlcInfoFree
void Cudd_tlcInfoFree(DdTlcInfo *t)
Definition: cuddEssent.c:455
Cudd_addOrAbstract
DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:216
Cudd_bddSetVarToBeUngrouped
int Cudd_bddSetVarToBeUngrouped(DdManager *dd, int index)
Definition: cuddAPI.c:4275
Cudd_ReadIthClause
int Cudd_ReadIthClause(DdTlcInfo *tlc, int i, DdHalfWord *var1, DdHalfWord *var2, int *phase1, int *phase2)
Definition: cuddEssent.c:359
Cudd_bddNPAnd
DdNode * Cudd_bddNPAnd(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:299
Cudd_NewApaNumber
DdApaNumber Cudd_NewApaNumber(int digits)
Definition: cuddApa.c:174
Cudd_AverageDistance
double Cudd_AverageDistance(DdManager *dd)
Definition: cuddUtil.c:2614
var1
static const int var1
Definition: satSolver.c:77
Cudd_SubsetWithMaskVars
DdNode * Cudd_SubsetWithMaskVars(DdManager *dd, DdNode *f, DdNode **vars, int nvars, DdNode **maskVars, int mvars)
Definition: cuddUtil.c:1602
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
DD_OOMFP
void(* DD_OOMFP)(long)
Definition: cudd.h:324
DdHalfWord
unsigned short DdHalfWord
Definition: cudd.h:262
Cudd_SetNumberXovers
void Cudd_SetNumberXovers(DdManager *dd, int numberXovers)
Definition: cuddAPI.c:2896
Cudd_bddNewVar
DdNode * Cudd_bddNewVar(DdManager *dd)
Definition: cuddAPI.c:323
Cudd_ReadMaxCache
unsigned int Cudd_ReadMaxCache(DdManager *dd)
Definition: cuddAPI.c:1371
Cudd_zddReadNodeCount
long Cudd_zddReadNodeCount(DdManager *dd)
Definition: cuddAPI.c:3221
Cudd_FindEssential
DdNode * Cudd_FindEssential(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:209
Cudd_bddSetPiVar
int Cudd_bddSetPiVar(DdManager *dd, int index)
Definition: cuddAPI.c:3977
Cudd_bddUnivAbstract
DdNode * Cudd_bddUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:207
Cudd_CProjection
DdNode * Cudd_CProjection(DdManager *dd, DdNode *R, DdNode *Y)
Definition: cuddPriority.c:1200
Cudd_Xeqy
DdNode * Cudd_Xeqy(DdManager *dd, int N, DdNode **x, DdNode **y)
Definition: cuddPriority.c:345
Cudd_bddVarConjDecomp
int Cudd_bddVarConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:615
Cudd_VerifySol
DdNode * Cudd_VerifySol(DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)
Definition: cuddSolve.c:169
DD_HFP
int(* DD_HFP)(DdManager *, const char *, void *)
Definition: cudd.h:312
Cudd_CofMinterm
double * Cudd_CofMinterm(DdManager *dd, DdNode *node)
Definition: cuddSign.c:131
DdNode::Id
ABC_INT64_T Id
Definition: cudd.h:286
Cudd_ReorderingStatusZdd
int Cudd_ReorderingStatusZdd(DdManager *unique, Cudd_ReorderingType *method)
Definition: cuddAPI.c:812
Cudd_addConstrain
DdNode * Cudd_addConstrain(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:336
Cudd_ReadCacheSlots
unsigned int Cudd_ReadCacheSlots(DdManager *dd)
Definition: cuddAPI.c:1152
Cudd_ApaCompare
int Cudd_ApaCompare(int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second)
Definition: cuddApa.c:449
Cudd_addScalarInverse
DdNode * Cudd_addScalarInverse(DdManager *dd, DdNode *f, DdNode *epsilon)
Definition: cuddAddInv.c:120
Cudd_OutOfMem
void Cudd_OutOfMem(long size)
Definition: cuddUtil.c:2837
Cudd_AggregationType
Cudd_AggregationType
Definition: cudd.h:184
Cudd_addSwapVariables
DdNode * Cudd_addSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:283
Cudd_bddPickOneMinterm
DdNode * Cudd_bddPickOneMinterm(DdManager *dd, DdNode *f, DdNode **vars, int n)
Definition: cuddUtil.c:1291
Cudd_zddDiffConst
DdNode * Cudd_zddDiffConst(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:266
Cudd_SetMaxCacheHard
void Cudd_SetMaxCacheHard(DdManager *dd, unsigned int mc)
Definition: cuddAPI.c:1415
Cudd_zddPortFromBdd
DdNode * Cudd_zddPortFromBdd(DdManager *dd, DdNode *B)
Definition: cuddZddPort.c:131
Cudd_bddComputeCube
DdNode * Cudd_bddComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Definition: cuddUtil.c:2196
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Cudd_bddIsVarHardGroup
int Cudd_bddIsVarHardGroup(DdManager *dd, int index)
Definition: cuddAPI.c:4326
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
DdNode
Definition: cudd.h:278
Cudd_SetMaxMemory
void Cudd_SetMaxMemory(DdManager *dd, unsigned long maxMemory)
Definition: cuddAPI.c:3876
Cudd_addLog
DdNode * Cudd_addLog(DdManager *dd, DdNode *f)
Definition: cuddAddApply.c:777
Cudd_Dxygtdyz
DdNode * Cudd_Dxygtdyz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
Definition: cuddPriority.c:621
Cudd_IsNonConstant
int Cudd_IsNonConstant(DdNode *f)
Definition: cuddAPI.c:645
Cudd_ReadSymmviolation
int Cudd_ReadSymmviolation(DdManager *dd)
Definition: cuddAPI.c:2710
Cudd_MakeZddTreeNode
MtrNode * Cudd_MakeZddTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
Definition: cuddZddGroup.c:163
Cudd_bddIterDisjDecomp
int Cudd_bddIterDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:456
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cudd_zddComplement
DdNode * Cudd_zddComplement(DdManager *dd, DdNode *node)
Definition: cuddZddFuncs.c:332
Cudd_ReadMinDead
unsigned int Cudd_ReadMinDead(DdManager *dd)
Definition: cuddAPI.c:1670
Cudd_addCmpl
DdNode * Cudd_addCmpl(DdManager *dd, DdNode *f)
Definition: cuddAddIte.c:347
Cudd_ShortestPath
DdNode * Cudd_ShortestPath(DdManager *manager, DdNode *f, int *weight, int *support, int *length)
Definition: cuddSat.c:201
Cudd_bddConstrainDecomp
DdNode ** Cudd_bddConstrainDecomp(DdManager *dd, DdNode *f)
Definition: cuddGenCof.c:371
Cudd_addOr
DdNode * Cudd_addOr(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:581
Cudd_bddPickOneCube
int Cudd_bddPickOneCube(DdManager *ddm, DdNode *node, char *string)
Definition: cuddUtil.c:1221
Cudd_zddSubset1
DdNode * Cudd_zddSubset1(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:330
Cudd_FirstNode
DdGen * Cudd_FirstNode(DdManager *dd, DdNode *f, DdNode **node)
Definition: cuddUtil.c:2400
Cudd_ReadMaxCacheHard
unsigned int Cudd_ReadMaxCacheHard(DdManager *dd)
Definition: cuddAPI.c:1391
Cudd_ApaPrintDensity
int Cudd_ApaPrintDensity(FILE *fp, DdManager *dd, DdNode *node, int nvars)
Definition: cuddApa.c:838
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
P
static byte P[256]
Definition: kitPerm.c:76
Cudd_Srandom
void Cudd_Srandom(long seed)
Definition: cuddUtil.c:2764
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_addNewVarAtLevel
DdNode * Cudd_addNewVarAtLevel(DdManager *dd, int level)
Definition: cuddAPI.c:290
Cudd_EquivDC
int Cudd_EquivDC(DdManager *dd, DdNode *F, DdNode *G, DdNode *D)
Definition: cuddSat.c:522
Cudd_ReadReorderings
int Cudd_ReadReorderings(DdManager *dd)
Definition: cuddAPI.c:1696
Cudd_Xgty
DdNode * Cudd_Xgty(DdManager *dd, int N, DdNode **z, DdNode **x, DdNode **y)
Definition: cuddPriority.c:280
Cudd_addComputeCube
DdNode * Cudd_addComputeCube(DdManager *dd, DdNode **vars, int *phase, int n)
Definition: cuddUtil.c:2246
DD_QSFP
int(* DD_QSFP)(const void *, const void *)
Definition: cudd.h:326
Cudd_NextPrime
int Cudd_NextPrime(DdGen *gen, int **cube)
Definition: cuddUtil.c:2130
Cudd_addConst
DdNode * Cudd_addConst(DdManager *dd, CUDD_VALUE_TYPE c)
Definition: cuddAPI.c:620
Cudd_SetStdout
void Cudd_SetStdout(DdManager *dd, FILE *fp)
Definition: cuddAPI.c:3674
Cudd_bddAdjPermuteX
DdNode * Cudd_bddAdjPermuteX(DdManager *dd, DdNode *B, DdNode **x, int n)
Definition: cuddCompose.c:512
Cudd_bddVarIsBound
int Cudd_bddVarIsBound(DdManager *dd, int index)
Definition: cuddAPI.c:3954
Cudd_addBddPattern
DdNode * Cudd_addBddPattern(DdManager *dd, DdNode *f)
Definition: cuddBridge.c:379
Cudd_PrintTwoLiteralClauses
int Cudd_PrintTwoLiteralClauses(DdManager *dd, DdNode *f, char **names, FILE *fp)
Definition: cuddEssent.c:393
Cudd_zddCountMinterm
double Cudd_zddCountMinterm(DdManager *zdd, DdNode *node, int path)
Definition: cuddZddMisc.c:158
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
Cudd_ReadNextReordering
unsigned int Cudd_ReadNextReordering(DdManager *dd)
Definition: cuddAPI.c:3742
Cudd_TurnOffCountDead
void Cudd_TurnOffCountDead(DdManager *dd)
Definition: cuddAPI.c:2633
Cudd_bddResetVarToBeGrouped
int Cudd_bddResetVarToBeGrouped(DdManager *dd, int index)
Definition: cuddAPI.c:4222
Cudd_RemapOverApprox
DdNode * Cudd_RemapOverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:366
Cudd_NextNode
int Cudd_NextNode(DdGen *gen, DdNode **node)
Definition: cuddUtil.c:2459
Cudd_ErrorType
Cudd_ErrorType
Definition: cudd.h:220
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
Cudd_zddDagSize
int Cudd_zddDagSize(DdNode *p_node)
Definition: cuddZddMisc.c:127
Cudd_addEvalConst
DdNode * Cudd_addEvalConst(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddAddIte.c:260
Cudd_bddPickArbitraryMinterms
DdNode ** Cudd_bddPickArbitraryMinterms(DdManager *dd, DdNode *f, DdNode **vars, int n, int k)
Definition: cuddUtil.c:1393
Cudd_ReadMaxMemory
unsigned long Cudd_ReadMaxMemory(DdManager *dd)
Definition: cuddAPI.c:3855
Cudd_bddExistAbstract
DdNode * Cudd_bddExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddBddAbs.c:130
Cudd_AutodynDisableZdd
void Cudd_AutodynDisableZdd(DdManager *unique)
Definition: cuddAPI.c:786
Cudd_addMonadicApply
DdNode * Cudd_addMonadicApply(DdManager *dd, DdNode *(*op)(DdManager *, DdNode *), DdNode *f)
Definition: cuddAddApply.c:747
Cudd_bddNor
DdNode * Cudd_bddNor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:445
Cudd_addNor
DdNode * Cudd_addNor(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:647
Cudd_ReadMinHit
unsigned int Cudd_ReadMinHit(DdManager *dd)
Definition: cuddAPI.c:1272
Cudd_zddWeakDivF
DdNode * Cudd_zddWeakDivF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:270
Cudd_SetRecomb
void Cudd_SetRecomb(DdManager *dd, int recomb)
Definition: cuddAPI.c:2682
Cudd_ReadPlusInfinity
DdNode * Cudd_ReadPlusInfinity(DdManager *dd)
Definition: cuddAPI.c:1076
Cudd_Decreasing
DdNode * Cudd_Decreasing(DdManager *dd, DdNode *f, int i)
Definition: cuddSat.c:417
Cudd_BiasedOverApprox
DdNode * Cudd_BiasedOverApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:463
Cudd_SetVarMap
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:416
Cudd_addFindMin
DdNode * Cudd_addFindMin(DdManager *dd, DdNode *f)
Definition: cuddAddFind.c:164
Cudd_OverApprox
DdNode * Cudd_OverApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:275
Cudd_SetBackground
void Cudd_SetBackground(DdManager *dd, DdNode *bck)
Definition: cuddAPI.c:1131
Cudd_SetMaxGrowthAlternate
void Cudd_SetMaxGrowthAlternate(DdManager *dd, double mg)
Definition: cuddAPI.c:2064
Cudd_ShortestLength
int Cudd_ShortestLength(DdManager *manager, DdNode *f, int *weight)
Definition: cuddSat.c:357
Cudd_CubeArrayToBdd
DdNode * Cudd_CubeArrayToBdd(DdManager *dd, int *array)
Definition: cuddUtil.c:2298
Cudd_bddSetVarToBeGrouped
int Cudd_bddSetVarToBeGrouped(DdManager *dd, int index)
Definition: cuddAPI.c:4171
Cudd_zddPortToBdd
DdNode * Cudd_zddPortToBdd(DdManager *dd, DdNode *f)
Definition: cuddZddPort.c:160
Cudd_zddRealignmentEnabled
int Cudd_zddRealignmentEnabled(DdManager *unique)
Definition: cuddAPI.c:837
Cudd_bddIsNsVar
int Cudd_bddIsNsVar(DdManager *dd, int index)
Definition: cuddAPI.c:4098
Cudd_ReadNodesDropped
double Cudd_ReadNodesDropped(DdManager *dd)
Definition: cuddAPI.c:1810
Cudd_ReadGroupcheck
Cudd_AggregationType Cudd_ReadGroupcheck(DdManager *dd)
Definition: cuddAPI.c:2474
Cudd_bddAndAbstractLimit
DdNode * Cudd_bddAndAbstractLimit(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, unsigned int limit)
Definition: cuddAndAbs.c:158
Cudd_addIteConstant
DdNode * Cudd_addIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:163
Cudd_SupersetShortPaths
DdNode * Cudd_SupersetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
Definition: cuddSubsetSP.c:272
Cudd_ReorderingReporting
int Cudd_ReorderingReporting(DdManager *dd)
Definition: cuddAPI.c:3591
Cudd_addApply
DdNode * Cudd_addApply(DdManager *dd, DdNode *(*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g)
Cudd_zddDiff
DdNode * Cudd_zddDiff(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:236
Cudd_addHarwell
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)
Definition: cuddHarwell.c:124
Cudd_bddAndLimit
DdNode * Cudd_bddAndLimit(DdManager *dd, DdNode *f, DdNode *g, unsigned int limit)
Definition: cuddBddIte.c:346
Cudd_bddSwapVariables
DdNode * Cudd_bddSwapVariables(DdManager *dd, DdNode *f, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:464
Cudd_addMaximum
DdNode * Cudd_addMaximum(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:430
DdGen
Definition: cuddInt.h:204
Cudd_ReadZero
DdNode * Cudd_ReadZero(DdManager *dd)
Definition: cuddAPI.c:1036
DdApaDigit
unsigned short int DdApaDigit
Definition: cudd.h:303
DdTlcInfo::vars
DdHalfWord * vars
Definition: cuddEssent.c:123
Cudd_IsGenEmpty
int Cudd_IsGenEmpty(DdGen *gen)
Definition: cuddUtil.c:2531
Cudd_bddLICompaction
DdNode * Cudd_bddLICompaction(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:570
Cudd_bddClosestCube
DdNode * Cudd_bddClosestCube(DdManager *dd, DdNode *f, DdNode *g, int *distance)
Definition: cuddPriority.c:1359
Cudd_bddGenConjDecomp
int Cudd_bddGenConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:496
Cudd_bddIte
DdNode * Cudd_bddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:143
Cudd_addResidue
DdNode * Cudd_addResidue(DdManager *dd, int n, int m, int options, int top)
Definition: cuddAddWalsh.c:161
Cudd_ApaAdd
DdApaDigit Cudd_ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum)
Definition: cuddApa.c:221
Cudd_addXor
DdNode * Cudd_addXor(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:679
Cudd_zddDivide
DdNode * Cudd_zddDivide(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:241
Cudd_CountLeaves
int Cudd_CountLeaves(DdNode *node)
Definition: cuddUtil.c:1194
Cudd_SolveEqn
DdNode * Cudd_SolveEqn(DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n)
Definition: cuddSolve.c:126
Cudd_MakeBddFromZddCover
DdNode * Cudd_MakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:203
Cudd_zddChange
DdNode * Cudd_zddChange(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:392
Cudd_BiasedUnderApprox
DdNode * Cudd_BiasedUnderApprox(DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0)
Definition: cuddApprox.c:413
Cudd_ReadPeakLiveNodeCount
int Cudd_ReadPeakLiveNodeCount(DdManager *dd)
Definition: cuddAPI.c:3151
Cudd_zddNextPath
int Cudd_zddNextPath(DdGen *gen, int **path)
Definition: cuddZddUtil.c:387
Cudd_ApaPrintHex
int Cudd_ApaPrintHex(FILE *fp, int digits, DdApaNumber number)
Definition: cuddApa.c:532
Cudd_DeadAreCounted
int Cudd_DeadAreCounted(DdManager *dd)
Definition: cuddAPI.c:2585
Cudd_SetLooseUpTo
void Cudd_SetLooseUpTo(DdManager *dd, unsigned int lut)
Definition: cuddAPI.c:1345
Cudd_zddIntersect
DdNode * Cudd_zddIntersect(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:207
Cudd_SetSiftMaxVar
void Cudd_SetSiftMaxVar(DdManager *dd, int smv)
Definition: cuddAPI.c:1913
M
word M(word f1, word f2, int n)
Definition: kitPerm.c:240
Cudd_ReadVars
DdNode * Cudd_ReadVars(DdManager *dd, int i)
Definition: cuddAPI.c:2407
Cudd_ReadGarbageCollectionTime
long Cudd_ReadGarbageCollectionTime(DdManager *dd)
Definition: cuddAPI.c:1762
Cudd_SubsetCompress
DdNode * Cudd_SubsetCompress(DdManager *dd, DdNode *f, int nvars, int threshold)
Definition: cuddGenCof.c:700
Cudd_bddRead
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)
Definition: cuddRead.c:369
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Cudd_addDivide
DdNode * Cudd_addDivide(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:312
Cudd_PrioritySelect
DdNode * Cudd_PrioritySelect(DdManager *dd, DdNode *R, DdNode **x, DdNode **y, DdNode **z, DdNode *Pi, int n, DdNode *(*)(DdManager *, int, DdNode **, DdNode **, DdNode **))
Cudd_bddInterval
DdNode * Cudd_bddInterval(DdManager *dd, int N, DdNode **x, unsigned int lowerB, unsigned int upperB)
Definition: cuddPriority.c:1121
Cudd_addAgreement
DdNode * Cudd_addAgreement(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:551
Cudd_NextCube
int Cudd_NextCube(DdGen *gen, int **cube, CUDD_VALUE_TYPE *value)
Definition: cuddUtil.c:1917
Cudd_VariableType
Cudd_VariableType
Definition: cudd.h:252
Cudd_ReadInvPerm
int Cudd_ReadInvPerm(DdManager *dd, int i)
Definition: cuddAPI.c:2354
Cudd_bddIsVarEssential
int Cudd_bddIsVarEssential(DdManager *manager, DdNode *f, int id, int phase)
Definition: cuddEssent.c:239
Cudd_zddIte
DdNode * Cudd_zddIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddZddSetop.c:148
Cudd_zddFirstPath
DdGen * Cudd_zddFirstPath(DdManager *zdd, DdNode *f, int **path)
Definition: cuddZddUtil.c:275
Cudd_bddTransfer
DdNode * Cudd_bddTransfer(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition: cuddBridge.c:409
Cudd_FreeTree
void Cudd_FreeTree(DdManager *dd)
Definition: cuddAPI.c:2180
Cudd_zddProduct
DdNode * Cudd_zddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:145
Cudd_bddVectorCompose
DdNode * Cudd_bddVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:791
Cudd_ReadReorderingTime
long Cudd_ReadReorderingTime(DdManager *dd)
Definition: cuddAPI.c:1718
Cudd_SetZddTree
void Cudd_SetZddTree(DdManager *dd, MtrNode *tree)
Definition: cuddAPI.c:2224
Cudd_addNonSimCompose
DdNode * Cudd_addNonSimCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:682
Cudd_LargestCube
DdNode * Cudd_LargestCube(DdManager *manager, DdNode *f, int *length)
Definition: cuddSat.c:285
Cudd_bddNand
DdNode * Cudd_bddNand(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:413
onames
static const char * onames[]
Definition: testcudd.c:71
Cudd_ReadBackground
DdNode * Cudd_ReadBackground(DdManager *dd)
Definition: cuddAPI.c:1112
Cudd_ApaPrintMintermExp
int Cudd_ApaPrintMintermExp(FILE *fp, DdManager *dd, DdNode *node, int nvars, int precision)
Definition: cuddApa.c:800
Cudd_addCompose
DdNode * Cudd_addCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Definition: cuddCompose.c:204
Cudd_addLeq
int Cudd_addLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddAddIte.c:376
Cudd_bddIteConstant
DdNode * Cudd_bddIteConstant(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:174
Cudd_ClearErrorCode
void Cudd_ClearErrorCode(DdManager *dd)
Definition: cuddAPI.c:3632
Cudd_bddMinimize
DdNode * Cudd_bddMinimize(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:653
Cudd_zddUnion
DdNode * Cudd_zddUnion(DdManager *dd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:178
Cudd_addBddIthBit
DdNode * Cudd_addBddIthBit(DdManager *dd, DdNode *f, int bit)
Definition: cuddBridge.c:306
Cudd_addRoundOff
DdNode * Cudd_addRoundOff(DdManager *dd, DdNode *f, int N)
Definition: cuddAddNeg.c:148
Cudd_ApaPrintExponential
int Cudd_ApaPrintExponential(FILE *fp, int digits, DdApaNumber number, int precision)
Definition: cuddApa.c:619
Cudd_ReadNodesFreed
double Cudd_ReadNodesFreed(DdManager *dd)
Definition: cuddAPI.c:1784
Cudd_SetReorderingCycle
void Cudd_SetReorderingCycle(DdManager *dd, int cycle)
Definition: cuddAPI.c:2111
Cudd_ReadZddTree
MtrNode * Cudd_ReadZddTree(DdManager *dd)
Definition: cuddAPI.c:2204
Cudd_DumpDDcal
int Cudd_DumpDDcal(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:729
Cudd_ReadNumberXovers
int Cudd_ReadNumberXovers(DdManager *dd)
Definition: cuddAPI.c:2870
Cudd_Eval
DdNode * Cudd_Eval(DdManager *dd, DdNode *f, int *inputs)
Definition: cuddSat.c:157
Cudd_bddIsPiVar
int Cudd_bddIsPiVar(DdManager *dd, int index)
Definition: cuddAPI.c:4050
Cudd_bddVarMap
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:373
Cudd_addThreshold
DdNode * Cudd_addThreshold(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:248
Cudd_bddLiteralSetIntersection
DdNode * Cudd_bddLiteralSetIntersection(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddLiteral.c:118
Cudd_Random
long Cudd_Random(void)
Definition: cuddUtil.c:2702
Cudd_bddBindVar
int Cudd_bddBindVar(DdManager *dd, int index)
Definition: cuddAPI.c:3899
Cudd_IndicesToCube
DdNode * Cudd_IndicesToCube(DdManager *dd, int *array, int n)
Definition: cuddUtil.c:2553
Cudd_EnableGarbageCollection
void Cudd_EnableGarbageCollection(DdManager *dd)
Definition: cuddAPI.c:2539
Cudd_addPermute
DdNode * Cudd_addPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:242
Cudd_EstimateCofactorSimple
int Cudd_EstimateCofactorSimple(DdNode *node, int i)
Definition: cuddUtil.c:517
Cudd_FirstPrime
DdGen * Cudd_FirstPrime(DdManager *dd, DdNode *l, DdNode *u, int **cube)
Definition: cuddUtil.c:2028
Cudd_SetEpsilon
void Cudd_SetEpsilon(DdManager *dd, CUDD_VALUE_TYPE ep)
Definition: cuddAPI.c:2451
DdNode::value
CUDD_VALUE_TYPE value
Definition: cudd.h:283
DdApaDoubleDigit
unsigned int DdApaDoubleDigit
Definition: cudd.h:304
Cudd_addIthVar
DdNode * Cudd_addIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:384
Cudd_bddMakePrime
DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f)
Definition: cuddSat.c:864
Cudd_zddShuffleHeap
int Cudd_zddShuffleHeap(DdManager *table, int *permutation)
Definition: cuddZddReord.c:304
Cudd_SupersetHeavyBranch
DdNode * Cudd_SupersetHeavyBranch(DdManager *dd, DdNode *f, int numVars, int threshold)
Definition: cuddSubsetHB.c:259
Cudd_HookType
Cudd_HookType
Definition: cudd.h:205
Cudd_addXnor
DdNode * Cudd_addXnor(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:713
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
Cudd_ReadPerm
int Cudd_ReadPerm(DdManager *dd, int i)
Definition: cuddAPI.c:2301
Cudd_PrintLinear
int Cudd_PrintLinear(DdManager *table)
Definition: cuddLinear.c:153
Cudd_bddNewVarAtLevel
DdNode * Cudd_bddNewVarAtLevel(DdManager *dd, int level)
Definition: cuddAPI.c:351
Cudd_ShuffleHeap
int Cudd_ShuffleHeap(DdManager *table, int *permutation)
Definition: cuddReorder.c:338
Cudd_ReorderingStatus
int Cudd_ReorderingStatus(DdManager *unique, Cudd_ReorderingType *method)
Definition: cuddAPI.c:735
Cudd_PrintInfo
int Cudd_PrintInfo(DdManager *dd, FILE *fp)
Definition: cuddAPI.c:2937
Cudd_bddConstrain
DdNode * Cudd_bddConstrain(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:180
Cudd_zddSubset0
DdNode * Cudd_zddSubset0(DdManager *dd, DdNode *P, int var)
Definition: cuddZddSetop.c:362
Cudd_bddCorrelation
double Cudd_bddCorrelation(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddCorr.c:147
Cudd_bddPermute
DdNode * Cudd_bddPermute(DdManager *manager, DdNode *node, int *permut)
Definition: cuddCompose.c:332
Cudd_bddGenDisjDecomp
int Cudd_bddGenDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:575
Cudd_ReadTree
MtrNode * Cudd_ReadTree(DdManager *dd)
Definition: cuddAPI.c:2132
Cudd_bddCompose
DdNode * Cudd_bddCompose(DdManager *dd, DdNode *f, DdNode *g, int v)
Definition: cuddCompose.c:167
DdChildren
struct DdChildren DdChildren
DdNode::next
DdNode * next
Definition: cudd.h:281
Cudd_ApaSetToLiteral
void Cudd_ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
Definition: cuddApa.c:389
Cudd_addVectorCompose
DdNode * Cudd_addVectorCompose(DdManager *dd, DdNode *f, DdNode **vector)
Definition: cuddCompose.c:563
Cudd_bddRealignEnable
void Cudd_bddRealignEnable(DdManager *unique)
Definition: cuddAPI.c:943
Cudd_ReadCacheHits
double Cudd_ReadCacheHits(DdManager *dd)
Definition: cuddAPI.c:1225
Cudd_bddLeqUnless
int Cudd_bddLeqUnless(DdManager *dd, DdNode *f, DdNode *g, DdNode *D)
Definition: cuddSat.c:622
Cudd_ReadInvPermZdd
int Cudd_ReadInvPermZdd(DdManager *dd, int i)
Definition: cuddAPI.c:2380
Cudd_CountPath
double Cudd_CountPath(DdNode *node)
Definition: cuddUtil.c:623
Cudd_FindTwoLiteralClauses
DdTlcInfo * Cudd_FindTwoLiteralClauses(DdManager *dd, DdNode *f)
Definition: cuddEssent.c:277
Cudd_zddPrintDebug
int Cudd_zddPrintDebug(DdManager *zdd, DdNode *f, int n, int pr)
Definition: cuddZddUtil.c:215
Cudd_SetNextReordering
void Cudd_SetNextReordering(DdManager *dd, unsigned int next)
Definition: cuddAPI.c:3766
Cudd_PrintMinterm
int Cudd_PrintMinterm(DdManager *manager, DdNode *node)
Definition: cuddUtil.c:216
Cudd_ReadUsedSlots
double Cudd_ReadUsedSlots(DdManager *dd)
Definition: cuddAPI.c:1503
Cudd_addPlus
DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:168
Cudd_SymmProfile
void Cudd_SymmProfile(DdManager *table, int lower, int upper)
Definition: cuddSymmetry.c:142
Cudd_ReadCacheUsedSlots
double Cudd_ReadCacheUsedSlots(DdManager *dd)
Definition: cuddAPI.c:1175
Cudd_addBddInterval
DdNode * Cudd_addBddInterval(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper)
Definition: cuddBridge.c:244
Cudd_ReadZddSize
int Cudd_ReadZddSize(DdManager *dd)
Definition: cuddAPI.c:1461
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
Cudd_RemapUnderApprox
DdNode * Cudd_RemapUnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, double quality)
Definition: cuddApprox.c:320
Cudd_bddIsPsVar
int Cudd_bddIsPsVar(DdManager *dd, int index)
Definition: cuddAPI.c:4074
Cudd_addIthBit
DdNode * Cudd_addIthBit(DdManager *dd, DdNode *f, int bit)
Definition: cuddAddFind.c:213
Cudd_zddRealignEnable
void Cudd_zddRealignEnable(DdManager *unique)
Definition: cuddAPI.c:867
Cudd_bddSetNsVar
int Cudd_bddSetNsVar(DdManager *dd, int index)
Definition: cuddAPI.c:4025
Cudd_ReadRecomb
int Cudd_ReadRecomb(DdManager *dd)
Definition: cuddAPI.c:2657
DdNode::kids
DdChildren kids
Definition: cudd.h:284
Cudd_BddToAdd
DdNode * Cudd_BddToAdd(DdManager *dd, DdNode *B)
Definition: cuddBridge.c:349
Cudd_ReadErrorCode
Cudd_ErrorType Cudd_ReadErrorCode(DdManager *dd)
Definition: cuddAPI.c:3612
Cudd_zddWeakDiv
DdNode * Cudd_zddWeakDiv(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:210
Cudd_bddXorExistAbstract
DdNode * Cudd_bddXorExistAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddBddAbs.c:169
DdChildren::E
struct DdNode * E
Definition: cudd.h:274
Cudd_StdPreReordHook
int Cudd_StdPreReordHook(DdManager *dd, const char *str, void *data)
Definition: cuddAPI.c:3408
Cudd_zddCount
int Cudd_zddCount(DdManager *zdd, DdNode *P)
Definition: cuddZddCount.c:137
Cudd_ClassifySupport
int Cudd_ClassifySupport(DdManager *dd, DdNode *f, DdNode *g, DdNode **common, DdNode **onlyF, DdNode **onlyG)
Definition: cuddUtil.c:1085
Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
Cudd_bddVarDisjDecomp
int Cudd_bddVarDisjDecomp(DdManager *dd, DdNode *f, DdNode ***disjuncts)
Definition: cuddDecomp.c:733
size
static int size
Definition: cuddSign.c:86
Cudd_zddIsop
DdNode * Cudd_zddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:136
Cudd_addSetNZ
DdNode * Cudd_addSetNZ(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:282
Cudd_ApaPowerOfTwo
void Cudd_ApaPowerOfTwo(int digits, DdApaNumber number, int power)
Definition: cuddApa.c:417
Cudd_bddAndAbstract
DdNode * Cudd_bddAndAbstract(DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
Definition: cuddAndAbs.c:124
Cudd_addRead
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)
Definition: cuddRead.c:146
Cudd_bddClippingAnd
DdNode * Cudd_bddClippingAnd(DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
Definition: cuddClip.c:129
Cudd_ReadSwapSteps
double Cudd_ReadSwapSteps(DdManager *dd)
Definition: cuddAPI.c:3787
ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
Cudd_bddRestrict
DdNode * Cudd_bddRestrict(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:212
Cudd_bddBooleanDiff
DdNode * Cudd_bddBooleanDiff(DdManager *manager, DdNode *f, int x)
Definition: cuddBddAbs.c:246
Cudd_MakeTreeNode
MtrNode * Cudd_MakeTreeNode(DdManager *dd, unsigned int low, unsigned int size, unsigned int type)
Definition: cuddGroup.c:206
Cudd_SetMinHit
void Cudd_SetMinHit(DdManager *dd, unsigned int hr)
Definition: cuddAPI.c:1298
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Cudd_AutodynEnableZdd
void Cudd_AutodynEnableZdd(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:760
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Cudd_SetPopulationSize
void Cudd_SetPopulationSize(DdManager *dd, int populationSize)
Definition: cuddAPI.c:2843
Cudd_bddIsVarToBeUngrouped
int Cudd_bddIsVarToBeUngrouped(DdManager *dd, int index)
Definition: cuddAPI.c:4301
Cudd_addNegate
DdNode * Cudd_addNegate(DdManager *dd, DdNode *f)
Definition: cuddAddNeg.c:120
Cudd_SetArcviolation
void Cudd_SetArcviolation(DdManager *dd, int arcviolation)
Definition: cuddAPI.c:2790
Cudd_SetSymmviolation
void Cudd_SetSymmviolation(DdManager *dd, int symmviolation)
Definition: cuddAPI.c:2737
Cudd_ApaSubtract
DdApaDigit Cudd_ApaSubtract(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff)
Definition: cuddApa.c:253
MtrNode
Definition: mtr.h:131
Cudd_EqualSupNorm
int Cudd_EqualSupNorm(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr)
Definition: cuddSat.c:796
Cudd_EstimateCofactor
int Cudd_EstimateCofactor(DdManager *dd, DdNode *node, int i, int phase)
Definition: cuddUtil.c:477
ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
Cudd_Increasing
DdNode * Cudd_Increasing(DdManager *dd, DdNode *f, int i)
Definition: cuddSat.c:497
Cudd_bddVarIsDependent
int Cudd_bddVarIsDependent(DdManager *dd, DdNode *f, DdNode *var)
Definition: cuddBddAbs.c:284
Cudd_zddPrintSubtable
void Cudd_zddPrintSubtable(DdManager *table)
Definition: cuddZddMisc.c:184
Cudd_ApaPrintDecimal
int Cudd_ApaPrintDecimal(FILE *fp, int digits, DdApaNumber number)
Definition: cuddApa.c:562
Cudd_PrintDebug
int Cudd_PrintDebug(DdManager *dd, DdNode *f, int n, int pr)
Definition: cuddUtil.c:382
DdApaNumber
DdApaDigit * DdApaNumber
Definition: cudd.h:306
Cudd_SetTree
void Cudd_SetTree(DdManager *dd, MtrNode *tree)
Definition: cuddAPI.c:2152
Cudd_RemoveHook
int Cudd_RemoveHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Definition: cuddAPI.c:3306
Cudd_bddClippingAndAbstract
DdNode * Cudd_bddClippingAndAbstract(DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)
Definition: cuddClip.c:163
Cudd_bddPrintCover
int Cudd_bddPrintCover(DdManager *dd, DdNode *l, DdNode *u)
Definition: cuddUtil.c:253
Cudd_CheckZeroRef
int Cudd_CheckZeroRef(DdManager *manager)
Definition: cuddRef.c:466
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
Cudd_zddUnateProduct
DdNode * Cudd_zddUnateProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:176
DdNode::type
union DdNode::@29 type
Cudd_bddCharToVect
DdNode ** Cudd_bddCharToVect(DdManager *dd, DdNode *f)
Definition: cuddGenCof.c:510
Cudd_ReadZddOne
DdNode * Cudd_ReadZddOne(DdManager *dd, int i)
Definition: cuddAPI.c:1010
Cudd_addGeneralVectorCompose
DdNode * Cudd_addGeneralVectorCompose(DdManager *dd, DdNode *f, DdNode **vectorOn, DdNode **vectorOff)
Definition: cuddCompose.c:621
Cudd_ReadLooseUpTo
unsigned int Cudd_ReadLooseUpTo(DdManager *dd)
Definition: cuddAPI.c:1321
Cudd_bddIsop
DdNode * Cudd_bddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:174
Cudd_zddReduceHeap
int Cudd_zddReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddZddReord.c:171
Cudd_Dxygtdxz
DdNode * Cudd_Dxygtdxz(DdManager *dd, int N, DdNode **x, DdNode **y, DdNode **z)
Definition: cuddPriority.c:494
phase
static pcube phase
Definition: cvrm.c:405
Cudd_EnableReorderingReporting
int Cudd_EnableReorderingReporting(DdManager *dd)
Definition: cuddAPI.c:3536
Cudd_bddIsVarToBeGrouped
int Cudd_bddIsVarToBeGrouped(DdManager *dd, int index)
Definition: cuddAPI.c:4249
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Cudd_ReadNodeCount
long Cudd_ReadNodeCount(DdManager *dd)
Definition: cuddAPI.c:3179
Cudd_ReadUniqueLinks
double Cudd_ReadUniqueLinks(DdManager *dd)
Definition: cuddAPI.c:1865
Cudd_ReadMinusInfinity
DdNode * Cudd_ReadMinusInfinity(DdManager *dd)
Definition: cuddAPI.c:1094
Cudd_CountPathsToNonZero
double Cudd_CountPathsToNonZero(DdNode *node)
Definition: cuddUtil.c:707
Cudd_addIte
DdNode * Cudd_addIte(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddAddIte.c:129
Cudd_Inequality
DdNode * Cudd_Inequality(DdManager *dd, int N, int c, DdNode **x, DdNode **y)
Definition: cuddPriority.c:744
Cudd_addFindMax
DdNode * Cudd_addFindMax(DdManager *dd, DdNode *f)
Definition: cuddAddFind.c:124
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
Cudd_DisableGarbageCollection
void Cudd_DisableGarbageCollection(DdManager *dd)
Definition: cuddAPI.c:2563
Cudd_zddDivideF
DdNode * Cudd_zddDivideF(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:299
Cudd_ReadCacheLookUps
double Cudd_ReadCacheLookUps(DdManager *dd)
Definition: cuddAPI.c:1204
Cudd_bddApproxConjDecomp
int Cudd_bddApproxConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:175
Cudd_ReadStderr
FILE * Cudd_ReadStderr(DdManager *dd)
Definition: cuddAPI.c:3697
Cudd_addRestrict
DdNode * Cudd_addRestrict(DdManager *dd, DdNode *f, DdNode *c)
Definition: cuddGenCof.c:431
Cudd_addTriangle
DdNode * Cudd_addTriangle(DdManager *dd, DdNode *f, DdNode *g, DdNode **z, int nz)
Definition: cuddMatMult.c:243
Cudd_DumpBlif
int Cudd_DumpBlif(DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv)
Definition: cuddExport.c:136
Cudd_SubsetShortPaths
DdNode * Cudd_SubsetShortPaths(DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit)
Definition: cuddSubsetSP.c:220
Cudd_addMinus
DdNode * Cudd_addMinus(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:349
Cudd_bddSetPsVar
int Cudd_bddSetPsVar(DdManager *dd, int index)
Definition: cuddAPI.c:4001
Cudd_Density
double Cudd_Density(DdManager *dd, DdNode *f, int nvars)
Definition: cuddUtil.c:2802
Cudd_ReadMaxLive
unsigned int Cudd_ReadMaxLive(DdManager *dd)
Definition: cuddAPI.c:3812
Cudd_ApaCompareRatios
int Cudd_ApaCompareRatios(int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen)
Definition: cuddApa.c:489
Cudd_UnderApprox
DdNode * Cudd_UnderApprox(DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality)
Definition: cuddApprox.c:228
Cudd_ApaCopy
void Cudd_ApaCopy(int digits, DdApaNumber source, DdApaNumber dest)
Definition: cuddApa.c:194
DdNode::index
DdHalfWord index
Definition: cudd.h:279
Cudd_NodeReadIndex
unsigned int Cudd_NodeReadIndex(DdNode *node)
Definition: cuddAPI.c:2277
Cudd_Prime
unsigned int Cudd_Prime(unsigned int p)
Definition: cuddTable.c:188
Cudd_zddPrintMinterm
int Cudd_zddPrintMinterm(DdManager *zdd, DdNode *node)
Definition: cuddZddUtil.c:135
Cudd_AddHook
int Cudd_AddHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Definition: cuddAPI.c:3244
Cudd_ReadReorderingCycle
int Cudd_ReadReorderingCycle(DdManager *dd)
Definition: cuddAPI.c:2088
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_bddSetPairIndex
int Cudd_bddSetPairIndex(DdManager *dd, int index, int pairIndex)
Definition: cuddAPI.c:4122
Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
Cudd_bddXor
DdNode * Cudd_bddXor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:476
Cudd_addOuterSum
DdNode * Cudd_addOuterSum(DdManager *dd, DdNode *M, DdNode *r, DdNode *c)
Definition: cuddMatMult.c:296
Cudd_SetGroupcheck
void Cudd_SetGroupcheck(DdManager *dd, Cudd_AggregationType gc)
Definition: cuddAPI.c:2496
Cudd_GenFree
int Cudd_GenFree(DdGen *gen)
Definition: cuddUtil.c:2491
Cudd_addTimesPlus
DdNode * Cudd_addTimesPlus(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
Definition: cuddMatMult.c:185
Cudd_bddRealignDisable
void Cudd_bddRealignDisable(DdManager *unique)
Definition: cuddAPI.c:965
Cudd_FirstCube
DdGen * Cudd_FirstCube(DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value)
Definition: cuddUtil.c:1798
Cudd_SupportIndex
int * Cudd_SupportIndex(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:815
Cudd_VectorSupportSize
int Cudd_VectorSupportSize(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:1028
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
Cudd_SetMaxGrowth
void Cudd_SetMaxGrowth(DdManager *dd, double mg)
Definition: cuddAPI.c:2013
Cudd_IsInHook
int Cudd_IsInHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Definition: cuddAPI.c:3359
Cudd_bddUnbindVar
int Cudd_bddUnbindVar(DdManager *dd, int index)
Definition: cuddAPI.c:3927
Cudd_bddReadPairIndex
int Cudd_bddReadPairIndex(DdManager *dd, int index)
Definition: cuddAPI.c:4148
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Cudd_ReadMemoryInUse
unsigned long Cudd_ReadMemoryInUse(DdManager *dd)
Definition: cuddAPI.c:2916
Cudd_bddRealignmentEnabled
int Cudd_bddRealignmentEnabled(DdManager *unique)
Definition: cuddAPI.c:913
Cudd_DelayedDerefBdd
void Cudd_DelayedDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:274
Cudd_zddIthVar
DdNode * Cudd_zddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:448
Cudd_ReadPopulationSize
int Cudd_ReadPopulationSize(DdManager *dd)
Definition: cuddAPI.c:2817
value
int value
Definition: misc/espresso/main.h:90
Cudd_DumpBlifBody
int Cudd_DumpBlifBody(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp, int mv)
Definition: cuddExport.c:252
Cudd_ApaIntDivision
unsigned int Cudd_ApaIntDivision(int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient)
Definition: cuddApa.c:324
Cudd_addDiff
DdNode * Cudd_addDiff(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:511
Cudd_zddSymmProfile
void Cudd_zddSymmProfile(DdManager *table, int lower, int upper)
Definition: cuddZddSymm.c:145
Cudd_SupersetCompress
DdNode * Cudd_SupersetCompress(DdManager *dd, DdNode *f, int nvars, int threshold)
Definition: cuddGenCof.c:750
Cudd_DumpDot
int Cudd_DumpDot(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:344
Cudd_zddVarsFromBddVars
int Cudd_zddVarsFromBddVars(DdManager *dd, int multiplicity)
Definition: cuddAPI.c:519
Cudd_ApaPrintMinterm
int Cudd_ApaPrintMinterm(FILE *fp, DdManager *dd, DdNode *node, int nvars)
Definition: cuddApa.c:761
Cudd_zddPrintCover
int Cudd_zddPrintCover(DdManager *zdd, DdNode *node)
Definition: cuddZddUtil.c:169
Cudd_VectorSupportIndex
int * Cudd_VectorSupportIndex(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:980
Cudd_ReadPermZdd
int Cudd_ReadPermZdd(DdManager *dd, int i)
Definition: cuddAPI.c:2328
Cudd_FreeZddTree
void Cudd_FreeZddTree(DdManager *dd)
Definition: cuddAPI.c:2252
Cudd_zddCountDouble
double Cudd_zddCountDouble(DdManager *zdd, DdNode *P)
Definition: cuddZddCount.c:176
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
DdChildren::T
struct DdNode * T
Definition: cudd.h:273
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Cudd_ReadMaxGrowthAlternate
double Cudd_ReadMaxGrowthAlternate(DdManager *dd)
Definition: cuddAPI.c:2039
Cudd_addExistAbstract
DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:129
Cudd_ApaNumberOfDigits
int Cudd_ApaNumberOfDigits(int binaryDigits)
Definition: cuddApa.c:147
Cudd_addUnivAbstract
DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube)
Definition: cuddAddAbs.c:178
Cudd_TurnOnCountDead
void Cudd_TurnOnCountDead(DdManager *dd)
Definition: cuddAPI.c:2608
Cudd_bddCorrelationWeights
double Cudd_bddCorrelationWeights(DdManager *manager, DdNode *f, DdNode *g, double *prob)
Definition: cuddBddCorr.c:189
Cudd_addHamming
DdNode * Cudd_addHamming(DdManager *dd, DdNode **xVars, DdNode **yVars, int nVars)
Definition: cuddPriority.c:1255
Cudd_ApaCountMinterm
DdApaNumber Cudd_ApaCountMinterm(DdManager *manager, DdNode *node, int nvars, int *digits)
Definition: cuddApa.c:684
Cudd_ReadPeakNodeCount
long Cudd_ReadPeakNodeCount(DdManager *dd)
Definition: cuddAPI.c:3122
Cudd_ApaShortDivision
DdApaDigit Cudd_ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient)
Definition: cuddApa.c:283
Cudd_DumpFactoredForm
int Cudd_DumpFactoredForm(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:889
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_addMatrixMultiply
DdNode * Cudd_addMatrixMultiply(DdManager *dd, DdNode *A, DdNode *B, DdNode **z, int nz)
Definition: cuddMatMult.c:132
Cudd_ReadSiftMaxSwap
int Cudd_ReadSiftMaxSwap(DdManager *dd)
Definition: cuddAPI.c:1938
Cudd_addNand
DdNode * Cudd_addNand(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:615
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
Cudd_ApaShiftRight
void Cudd_ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b)
Definition: cuddApa.c:361
Cudd_addTimes
DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:208
Cudd_StdPostReordHook
int Cudd_StdPostReordHook(DdManager *dd, const char *str, void *data)
Definition: cuddAPI.c:3501
Cudd_addNewVar
DdNode * Cudd_addNewVar(DdManager *dd)
Definition: cuddAPI.c:259
Cudd_ReadSiftMaxVar
int Cudd_ReadSiftMaxVar(DdManager *dd)
Definition: cuddAPI.c:1891
Cudd_ReadMaxGrowth
double Cudd_ReadMaxGrowth(DdManager *dd)
Definition: cuddAPI.c:1988
Cudd_GarbageCollectionEnabled
int Cudd_GarbageCollectionEnabled(DdManager *dd)
Definition: cuddAPI.c:2517
Cudd_ReorderingType
Cudd_ReorderingType
Definition: cudd.h:151
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Cudd_SetSiftMaxSwap
void Cudd_SetSiftMaxSwap(DdManager *dd, int sms)
Definition: cuddAPI.c:1962
Cudd_ReadSlots
unsigned int Cudd_ReadSlots(DdManager *dd)
Definition: cuddAPI.c:1480
Cudd_MinHammingDist
int Cudd_MinHammingDist(DdManager *dd, DdNode *f, int *minterm, int upperBound)
Definition: cuddPriority.c:1318
Cudd_ReadStdout
FILE * Cudd_ReadStdout(DdManager *dd)
Definition: cuddAPI.c:3654
Cudd_DumpDaVinci
int Cudd_DumpDaVinci(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:615
Cudd_SplitSet
DdNode * Cudd_SplitSet(DdManager *manager, DdNode *S, DdNode **xVars, int n, double m)
Definition: cuddSplit.c:128
Cudd_bddIntersect
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:282
Cudd_addWalsh
DdNode * Cudd_addWalsh(DdManager *dd, DdNode **x, DdNode **y, int n)
Definition: cuddAddWalsh.c:120
Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
Cudd_Disequality
DdNode * Cudd_Disequality(DdManager *dd, int N, int c, DdNode **x, DdNode **y)
Definition: cuddPriority.c:932
Cudd_addMinimum
DdNode * Cudd_addMinimum(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:385
Cudd_LazyGroupType
Cudd_LazyGroupType
Definition: cudd.h:237
Cudd_SetMaxLive
void Cudd_SetMaxLive(DdManager *dd, unsigned int maxLive)
Definition: cuddAPI.c:3833
Cudd_EpdCountMinterm
int Cudd_EpdCountMinterm(DdManager *manager, DdNode *node, int nvars, EpDouble *epd)
Definition: cuddUtil.c:657
Cudd_SetStderr
void Cudd_SetStderr(DdManager *dd, FILE *fp)
Definition: cuddAPI.c:3717
Cudd_ReadGarbageCollections
int Cudd_ReadGarbageCollections(DdManager *dd)
Definition: cuddAPI.c:1741
Cudd_ReadEpsilon
CUDD_VALUE_TYPE Cudd_ReadEpsilon(DdManager *dd)
Definition: cuddAPI.c:2430
S
static shot S[256]
Definition: kitPerm.c:40
Cudd_addOneZeroMaximum
DdNode * Cudd_addOneZeroMaximum(DdManager *dd, DdNode **f, DdNode **g)
Definition: cuddAddApply.c:476
Cudd_addBddStrictThreshold
DdNode * Cudd_addBddStrictThreshold(DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
Definition: cuddBridge.c:199
Cudd_zddRealignDisable
void Cudd_zddRealignDisable(DdManager *unique)
Definition: cuddAPI.c:889
Cudd_VectorSupport
DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:908
Cudd_DisableReorderingReporting
int Cudd_DisableReorderingReporting(DdManager *dd)
Definition: cuddAPI.c:3564
Cudd_ExpectedUsedSlots
double Cudd_ExpectedUsedSlots(DdManager *dd)
Definition: cuddAPI.c:1572
Cudd_bddSqueeze
DdNode * Cudd_bddSqueeze(DdManager *dd, DdNode *l, DdNode *u)
Definition: cuddGenCof.c:602
Cudd_BddToCubeArray
int Cudd_BddToCubeArray(DdManager *dd, DdNode *cube, int *array)
Definition: cuddUtil.c:2346
Cudd_bddIterConjDecomp
int Cudd_bddIterConjDecomp(DdManager *dd, DdNode *f, DdNode ***conjuncts)
Definition: cuddDecomp.c:313
Cudd_addXeqy
DdNode * Cudd_addXeqy(DdManager *dd, int N, DdNode **x, DdNode **y)
Definition: cuddPriority.c:408
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Cudd_zddCoverPathToString
char * Cudd_zddCoverPathToString(DdManager *zdd, int *path, char *str)
Definition: cuddZddUtil.c:475
Cudd_ReadUniqueLookUps
double Cudd_ReadUniqueLookUps(DdManager *dd)
Definition: cuddAPI.c:1836
Cudd_zddDumpDot
int Cudd_zddDumpDot(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddZddUtil.c:549
Cudd_PrintVersion
void Cudd_PrintVersion(FILE *fp)
Definition: cuddUtil.c:2592
Cudd_ReadRecursiveCalls
double Cudd_ReadRecursiveCalls(DdManager *dd)
Definition: cuddAPI.c:1246
Cudd_ReadArcviolation
int Cudd_ReadArcviolation(DdManager *dd)
Definition: cuddAPI.c:2764