/**CHeaderFile*****************************************************************

  FileName    [cudd.h]

  PackageName [cudd]

  Synopsis    [The University of Colorado decision diagram package.]

  Description [External functions and data strucures of the CUDD package.
                <ul>
                <li> To turn on the gathering of statistics, define DD_STATS.
                <li> To link with mis, define DD_MIS.
                </ul>
               Modified by Abelardo Pardo to interface it to VIS.
  ]

  SeeAlso     []

  Author      [Fabio Somenzi]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

  Revision    [$Id: cudd.h,v 1.174 2009/02/21 05:55:18 fabio Exp $]

******************************************************************************/

#ifndef ABC__bdd__cudd__cudd_h
#define ABC__bdd__cudd__cudd_h


/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include "bdd/mtr/mtr.h"
#include "bdd/epd/epd.h"

ABC_NAMESPACE_HEADER_START


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define CUDD_VERSION "2.4.2"

#ifndef SIZEOF_VOID_P
#define SIZEOF_VOID_P 4
#endif
#ifndef SIZEOF_INT
#define SIZEOF_INT 4
#endif
#ifndef SIZEOF_LONG
#define SIZEOF_LONG 4
#endif

#ifndef TRUE
#define TRUE 1
#endif
#ifndef FALSE
#define FALSE 0
#endif

#define CUDD_VALUE_TYPE         double
#define CUDD_OUT_OF_MEM         -1
/* The sizes of the subtables and the cache must be powers of two. */
#define CUDD_UNIQUE_SLOTS       256     /* initial size of subtables */
#define CUDD_CACHE_SLOTS        262144  /* default size of the cache */

/* Constants for residue functions. */
#define CUDD_RESIDUE_DEFAULT    0
#define CUDD_RESIDUE_MSB        1
#define CUDD_RESIDUE_TC         2

/* CUDD_MAXINDEX is defined in such a way that on 32-bit and 64-bit
** machines one can cast an index to (int) without generating a negative
** number.
*/
#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
#define CUDD_MAXINDEX           (((DdHalfWord) ~0) >> 1)
#else
#define CUDD_MAXINDEX           ((DdHalfWord) ~0)
#endif

/* CUDD_CONST_INDEX is the index of constant nodes.  Currently this
** is a synonim for CUDD_MAXINDEX. */
#define CUDD_CONST_INDEX        CUDD_MAXINDEX

/* These constants define the digits used in the representation of
** arbitrary precision integers.  The configurations tested use 8, 16,
** and 32 bits for each digit.  The typedefs should be in agreement
** with these definitions.
*/
#if SIZEOF_LONG == 8
#define DD_APA_BITS     32
#define DD_APA_BASE     (1L << DD_APA_BITS)
#define DD_APA_HEXPRINT "%08x"
#else
#define DD_APA_BITS     16
#define DD_APA_BASE     (1 << DD_APA_BITS)
#define DD_APA_HEXPRINT "%04x"
#endif
#define DD_APA_MASK     (DD_APA_BASE - 1)

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/**Enum************************************************************************

  Synopsis    [Type of reordering algorithm.]

  Description [Type of reordering algorithm.]

******************************************************************************/
typedef enum {
    CUDD_REORDER_SAME,
    CUDD_REORDER_NONE,
    CUDD_REORDER_RANDOM,
    CUDD_REORDER_RANDOM_PIVOT,
    CUDD_REORDER_SIFT,
    CUDD_REORDER_SIFT_CONVERGE,
    CUDD_REORDER_SYMM_SIFT,
    CUDD_REORDER_SYMM_SIFT_CONV,
    CUDD_REORDER_WINDOW2,
    CUDD_REORDER_WINDOW3,
    CUDD_REORDER_WINDOW4,
    CUDD_REORDER_WINDOW2_CONV,
    CUDD_REORDER_WINDOW3_CONV,
    CUDD_REORDER_WINDOW4_CONV,
    CUDD_REORDER_GROUP_SIFT,
    CUDD_REORDER_GROUP_SIFT_CONV,
    CUDD_REORDER_ANNEALING,
    CUDD_REORDER_GENETIC,
    CUDD_REORDER_LINEAR,
    CUDD_REORDER_LINEAR_CONVERGE,
    CUDD_REORDER_LAZY_SIFT,
    CUDD_REORDER_EXACT
} Cudd_ReorderingType;


/**Enum************************************************************************

  Synopsis    [Type of aggregation methods.]

  Description [Type of aggregation methods.]

******************************************************************************/
typedef enum {
    CUDD_NO_CHECK,
    CUDD_GROUP_CHECK,
    CUDD_GROUP_CHECK2,
    CUDD_GROUP_CHECK3,
    CUDD_GROUP_CHECK4,
    CUDD_GROUP_CHECK5,
    CUDD_GROUP_CHECK6,
    CUDD_GROUP_CHECK7,
    CUDD_GROUP_CHECK8,
    CUDD_GROUP_CHECK9
} Cudd_AggregationType;


/**Enum************************************************************************

  Synopsis    [Type of hooks.]

  Description [Type of hooks.]

******************************************************************************/
typedef enum {
    CUDD_PRE_GC_HOOK,
    CUDD_POST_GC_HOOK,
    CUDD_PRE_REORDERING_HOOK,
    CUDD_POST_REORDERING_HOOK
} Cudd_HookType;


/**Enum************************************************************************

  Synopsis    [Type of error codes.]

  Description [Type of  error codes.]

******************************************************************************/
typedef enum {
    CUDD_NO_ERROR,
    CUDD_MEMORY_OUT,
    CUDD_TOO_MANY_NODES,
    CUDD_MAX_MEM_EXCEEDED,
    CUDD_INVALID_ARG,
    CUDD_INTERNAL_ERROR
} Cudd_ErrorType;


/**Enum************************************************************************

  Synopsis    [Group type for lazy sifting.]

  Description [Group type for lazy sifting.]

******************************************************************************/
typedef enum {
    CUDD_LAZY_NONE,
    CUDD_LAZY_SOFT_GROUP,
    CUDD_LAZY_HARD_GROUP,
    CUDD_LAZY_UNGROUP
} Cudd_LazyGroupType;


/**Enum************************************************************************

  Synopsis    [Variable type.]

  Description [Variable type. Currently used only in lazy sifting.]

******************************************************************************/
typedef enum {
    CUDD_VAR_PRIMARY_INPUT,
    CUDD_VAR_PRESENT_STATE,
    CUDD_VAR_NEXT_STATE
} Cudd_VariableType;


#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
typedef unsigned int   DdHalfWord;
#else
typedef unsigned short DdHalfWord;
#endif

#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif

typedef struct DdNode DdNode;

typedef struct DdChildren {
    struct DdNode *T;
    struct DdNode *E;
} DdChildren;

/* The DdNode structure is the only one exported out of the package */
struct DdNode {
    DdHalfWord index;
    DdHalfWord ref;             /* reference count */
    DdNode *next;               /* next pointer for unique table */
    union {
        CUDD_VALUE_TYPE value;  /* for constant nodes */
        DdChildren kids;        /* for internal nodes */
    } type;
    ABC_INT64_T Id;
};

#ifdef __osf__
#pragma pointer_size restore
#endif

typedef struct DdManager DdManager;

typedef struct DdGen DdGen;

/* These typedefs for arbitrary precision arithmetic should agree with
** the corresponding constant definitions above. */
#if SIZEOF_LONG == 8
typedef unsigned int DdApaDigit;
typedef unsigned long int DdApaDoubleDigit;
#else
typedef unsigned short int DdApaDigit;
typedef unsigned int DdApaDoubleDigit;
#endif
typedef DdApaDigit * DdApaNumber;

/* Return type for function computing two-literal clauses. */
typedef struct DdTlcInfo DdTlcInfo;

/* Type of hook function. */
typedef int (*DD_HFP)(DdManager *, const char *, void *);
/* Type of priority function */
typedef DdNode * (*DD_PRFP)(DdManager * , int, DdNode **, DdNode **,
                            DdNode **);
/* Type of apply operator. */
typedef DdNode * (*DD_AOP)(DdManager *, DdNode **, DdNode **);
/* Type of monadic apply operator. */
typedef DdNode * (*DD_MAOP)(DdManager *, DdNode *);
/* Types of cache tag functions. */
typedef DdNode * (*DD_CTFP)(DdManager *, DdNode *, DdNode *);
typedef DdNode * (*DD_CTFP1)(DdManager *, DdNode *);
/* Type of memory-out function. */
typedef void (*DD_OOMFP)(long);
/* Type of comparison function for qsort. */
typedef int (*DD_QSFP)(const void *, const void *);

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**Macro***********************************************************************

  Synopsis     [Returns 1 if the node is a constant node.]

  Description  [Returns 1 if the node is a constant node (rather than an
  internal node). All constant nodes have the same index
  (CUDD_CONST_INDEX). The pointer passed to Cudd_IsConstant may be either
  regular or complemented.]

  SideEffects  [none]

  SeeAlso      []

******************************************************************************/
#define Cudd_IsConstant(node) ((Cudd_Regular(node))->index == CUDD_CONST_INDEX)


/**Macro***********************************************************************

  Synopsis     [Complements a DD.]

  Description  [Complements a DD by flipping the complement attribute of
  the pointer (the least significant bit).]

  SideEffects  [none]

  SeeAlso      [Cudd_NotCond]

******************************************************************************/
#define Cudd_Not(node) ((DdNode *)((ptrint)(node) ^ 01))


/**Macro***********************************************************************

  Synopsis     [Complements a DD if a condition is true.]

  Description  [Complements a DD if condition c is true; c should be
  either 0 or 1, because it is used directly (for efficiency). If in
  doubt on the values c may take, use "(c) ? Cudd_Not(node) : node".]

  SideEffects  [none]

  SeeAlso      [Cudd_Not]

******************************************************************************/
#define Cudd_NotCond(node,c) ((DdNode *)((ptrint)(node) ^ (c)))


/**Macro***********************************************************************

  Synopsis     [Returns the regular version of a pointer.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Complement Cudd_IsComplement]

******************************************************************************/
#define Cudd_Regular(node) ((DdNode *)((ptruint)(node) & ~01))


/**Macro***********************************************************************

  Synopsis     [Returns the complemented version of a pointer.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Regular Cudd_IsComplement]

******************************************************************************/
#define Cudd_Complement(node) ((DdNode *)((ptruint)(node) | 01))


/**Macro***********************************************************************

  Synopsis     [Returns 1 if a pointer is complemented.]

  Description  []

  SideEffects  [none]

  SeeAlso      [Cudd_Regular Cudd_Complement]

******************************************************************************/
#define Cudd_IsComplement(node) ((int) ((ptrint) (node) & 01))


/**Macro***********************************************************************

  Synopsis     [Returns the then child of an internal node.]

  Description  [Returns the then child of an internal node. If
  <code>node</code> is a constant node, the result is unpredictable.]

  SideEffects  [none]

  SeeAlso      [Cudd_E Cudd_V]

******************************************************************************/
#define Cudd_T(node) ((Cudd_Regular(node))->type.kids.T)


/**Macro***********************************************************************

  Synopsis     [Returns the else child of an internal node.]

  Description  [Returns the else child of an internal node. If
  <code>node</code> is a constant node, the result is unpredictable.]

  SideEffects  [none]

  SeeAlso      [Cudd_T Cudd_V]

******************************************************************************/
#define Cudd_E(node) ((Cudd_Regular(node))->type.kids.E)


/**Macro***********************************************************************

  Synopsis     [Returns the value of a constant node.]

  Description  [Returns the value of a constant node. If
  <code>node</code> is an internal node, the result is unpredictable.]

  SideEffects  [none]

  SeeAlso      [Cudd_T Cudd_E]

******************************************************************************/
#define Cudd_V(node) ((Cudd_Regular(node))->type.value)


/**Macro***********************************************************************

  Synopsis     [Returns the current position in the order of variable
  index.]

  Description [Returns the current position in the order of variable
  index. This macro is obsolete and is kept for compatibility. New
  applications should use Cudd_ReadPerm instead.]

  SideEffects  [none]

  SeeAlso      [Cudd_ReadPerm]

******************************************************************************/
#define Cudd_ReadIndex(dd,index) (Cudd_ReadPerm(dd,index))


/**Macro***********************************************************************

  Synopsis     [Iterates over the cubes of a decision diagram.]

  Description  [Iterates over the cubes of a decision diagram f.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *f;
  <li> DdGen *gen;
  <li> int *cube;
  <li> CUDD_VALUE_TYPE value;
  </ul>
  Cudd_ForeachCube allocates and frees the generator. Therefore the
  application should not try to do that. Also, the cube is freed at the
  end of Cudd_ForeachCube and hence is not available outside of the loop.<p>
  CAUTION: It is assumed that dynamic reordering will not occur while
  there are open generators. It is the user's responsibility to make sure
  that dynamic reordering does not occur. As long as new nodes are not created
  during generation, and dynamic reordering is not called explicitly,
  dynamic reordering will not occur. Alternatively, it is sufficient to
  disable dynamic reordering. It is a mistake to dispose of a diagram
  on which generation is ongoing.]

  SideEffects  [none]

  SeeAlso      [Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_GenFree
  Cudd_IsGenEmpty Cudd_AutodynDisable]

******************************************************************************/
#define Cudd_ForeachCube(manager, f, gen, cube, value)\
    for((gen) = Cudd_FirstCube(manager, f, &cube, &value);\
        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
        (void) Cudd_NextCube(gen, &cube, &value))


/**Macro***********************************************************************

  Synopsis     [Iterates over the primes of a Boolean function.]

  Description  [Iterates over the primes of a Boolean function producing
  a prime and irredundant cover.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *l;
  <li> DdNode *u;
  <li> DdGen *gen;
  <li> int *cube;
  </ul>
  The Boolean function is described by an upper bound and a lower bound.  If
  the function is completely specified, the two bounds coincide.
  Cudd_ForeachPrime allocates and frees the generator.  Therefore the
  application should not try to do that.  Also, the cube is freed at the
  end of Cudd_ForeachPrime and hence is not available outside of the loop.<p>
  CAUTION: It is a mistake to change a diagram on which generation is ongoing.]

  SideEffects  [none]

  SeeAlso      [Cudd_ForeachCube Cudd_FirstPrime Cudd_NextPrime Cudd_GenFree
  Cudd_IsGenEmpty]

******************************************************************************/
#define Cudd_ForeachPrime(manager, l, u, gen, cube)\
    for((gen) = Cudd_FirstPrime(manager, l, u, &cube);\
        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
        (void) Cudd_NextPrime(gen, &cube))


/**Macro***********************************************************************

  Synopsis     [Iterates over the nodes of a decision diagram.]

  Description  [Iterates over the nodes of a decision diagram f.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *f;
  <li> DdGen *gen;
  <li> DdNode *node;
  </ul>
  The nodes are returned in a seemingly random order.
  Cudd_ForeachNode allocates and frees the generator. Therefore the
  application should not try to do that.<p>
  CAUTION: It is assumed that dynamic reordering will not occur while
  there are open generators. It is the user's responsibility to make sure
  that dynamic reordering does not occur. As long as new nodes are not created
  during generation, and dynamic reordering is not called explicitly,
  dynamic reordering will not occur. Alternatively, it is sufficient to
  disable dynamic reordering. It is a mistake to dispose of a diagram
  on which generation is ongoing.]

  SideEffects  [none]

  SeeAlso      [Cudd_ForeachCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree
  Cudd_IsGenEmpty Cudd_AutodynDisable]

******************************************************************************/
#define Cudd_ForeachNode(manager, f, gen, node)\
    for((gen) = Cudd_FirstNode(manager, f, &node);\
        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
        (void) Cudd_NextNode(gen, &node))


/**Macro***********************************************************************

  Synopsis     [Iterates over the paths of a ZDD.]

  Description  [Iterates over the paths of a ZDD f.
  <ul>
  <li> DdManager *manager;
  <li> DdNode *f;
  <li> DdGen *gen;
  <li> int *path;
  </ul>
  Cudd_zddForeachPath allocates and frees the generator. Therefore the
  application should not try to do that. Also, the path is freed at the
  end of Cudd_zddForeachPath and hence is not available outside of the loop.<p>
  CAUTION: It is assumed that dynamic reordering will not occur while
  there are open generators.  It is the user's responsibility to make sure
  that dynamic reordering does not occur.  As long as new nodes are not created
  during generation, and dynamic reordering is not called explicitly,
  dynamic reordering will not occur.  Alternatively, it is sufficient to
  disable dynamic reordering.  It is a mistake to dispose of a diagram
  on which generation is ongoing.]

  SideEffects  [none]

  SeeAlso      [Cudd_zddFirstPath Cudd_zddNextPath Cudd_GenFree
  Cudd_IsGenEmpty Cudd_AutodynDisable]

******************************************************************************/
#define Cudd_zddForeachPath(manager, f, gen, path)\
    for((gen) = Cudd_zddFirstPath(manager, f, &path);\
        Cudd_IsGenEmpty(gen) ? Cudd_GenFree(gen) : TRUE;\
        (void) Cudd_zddNextPath(gen, &path))



/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

extern DdNode *        Cudd_addNewVar( DdManager * dd );
extern DdNode *        Cudd_addNewVarAtLevel( DdManager * dd, int level );
extern DdNode *        Cudd_bddNewVar( DdManager * dd );
extern DdNode *        Cudd_bddNewVarAtLevel( DdManager * dd, int level );
extern DdNode *        Cudd_addIthVar( DdManager * dd, int i );
extern DdNode *        Cudd_bddIthVar( DdManager * dd, int i );
extern DdNode *        Cudd_zddIthVar( DdManager * dd, int i );
extern int             Cudd_zddVarsFromBddVars( DdManager * dd, int multiplicity );
extern DdNode *        Cudd_addConst( DdManager * dd, CUDD_VALUE_TYPE c );
extern int             Cudd_IsNonConstant( DdNode * f );
extern void            Cudd_AutodynEnable( DdManager * unique, Cudd_ReorderingType method );
extern void            Cudd_AutodynDisable( DdManager * unique );
extern int             Cudd_ReorderingStatus( DdManager * unique, Cudd_ReorderingType * method );
extern void            Cudd_AutodynEnableZdd( DdManager * unique, Cudd_ReorderingType method );
extern void            Cudd_AutodynDisableZdd( DdManager * unique );
extern int             Cudd_ReorderingStatusZdd( DdManager * unique, Cudd_ReorderingType * method );
extern int             Cudd_zddRealignmentEnabled( DdManager * unique );
extern void            Cudd_zddRealignEnable( DdManager * unique );
extern void            Cudd_zddRealignDisable( DdManager * unique );
extern int             Cudd_bddRealignmentEnabled( DdManager * unique );
extern void            Cudd_bddRealignEnable( DdManager * unique );
extern void            Cudd_bddRealignDisable( DdManager * unique );
extern DdNode *        Cudd_ReadOne( DdManager * dd );
extern DdNode *        Cudd_ReadZddOne( DdManager * dd, int i );
extern DdNode *        Cudd_ReadZero( DdManager * dd );
extern DdNode *        Cudd_ReadLogicZero( DdManager * dd );
extern DdNode *        Cudd_ReadPlusInfinity( DdManager * dd );
extern DdNode *        Cudd_ReadMinusInfinity( DdManager * dd );
extern DdNode *        Cudd_ReadBackground( DdManager * dd );
extern void            Cudd_SetBackground( DdManager * dd, DdNode * bck );
extern unsigned int    Cudd_ReadCacheSlots( DdManager * dd );
extern double          Cudd_ReadCacheUsedSlots( DdManager * dd );
extern double          Cudd_ReadCacheLookUps( DdManager * dd );
extern double          Cudd_ReadCacheHits( DdManager * dd );
extern double          Cudd_ReadRecursiveCalls( DdManager * dd );
extern unsigned int    Cudd_ReadMinHit( DdManager * dd );
extern void            Cudd_SetMinHit( DdManager * dd, unsigned int hr );
extern unsigned int    Cudd_ReadLooseUpTo( DdManager * dd );
extern void            Cudd_SetLooseUpTo( DdManager * dd, unsigned int lut );
extern unsigned int    Cudd_ReadMaxCache( DdManager * dd );
extern unsigned int    Cudd_ReadMaxCacheHard( DdManager * dd );
extern void            Cudd_SetMaxCacheHard( DdManager * dd, unsigned int mc );
extern int             Cudd_ReadSize( DdManager * dd );
extern int             Cudd_ReadZddSize( DdManager * dd );
extern unsigned int    Cudd_ReadSlots( DdManager * dd );
extern double          Cudd_ReadUsedSlots( DdManager * dd );
extern double          Cudd_ExpectedUsedSlots( DdManager * dd );
extern unsigned int    Cudd_ReadKeys( DdManager * dd );
extern unsigned int    Cudd_ReadDead( DdManager * dd );
extern unsigned int    Cudd_ReadMinDead( DdManager * dd );
extern int             Cudd_ReadReorderings( DdManager * dd );
extern long            Cudd_ReadReorderingTime( DdManager * dd );
extern int             Cudd_ReadGarbageCollections( DdManager * dd );
extern long            Cudd_ReadGarbageCollectionTime( DdManager * dd );
extern double          Cudd_ReadNodesFreed( DdManager * dd );
extern double          Cudd_ReadNodesDropped( DdManager * dd );
extern double          Cudd_ReadUniqueLookUps( DdManager * dd );
extern double          Cudd_ReadUniqueLinks( DdManager * dd );
extern int             Cudd_ReadSiftMaxVar( DdManager * dd );
extern void            Cudd_SetSiftMaxVar( DdManager * dd, int smv );
extern int             Cudd_ReadSiftMaxSwap( DdManager * dd );
extern void            Cudd_SetSiftMaxSwap( DdManager * dd, int sms );
extern double          Cudd_ReadMaxGrowth( DdManager * dd );
extern void            Cudd_SetMaxGrowth( DdManager * dd, double mg );
extern double          Cudd_ReadMaxGrowthAlternate( DdManager * dd );
extern void            Cudd_SetMaxGrowthAlternate( DdManager * dd, double mg );
extern int             Cudd_ReadReorderingCycle( DdManager * dd );
extern void            Cudd_SetReorderingCycle( DdManager * dd, int cycle );
extern MtrNode *       Cudd_ReadTree( DdManager * dd );
extern void            Cudd_SetTree( DdManager * dd, MtrNode * tree );
extern void            Cudd_FreeTree( DdManager * dd );
extern MtrNode *       Cudd_ReadZddTree( DdManager * dd );
extern void            Cudd_SetZddTree( DdManager * dd, MtrNode * tree );
extern void            Cudd_FreeZddTree( DdManager * dd );
extern unsigned int    Cudd_NodeReadIndex( DdNode * node );
extern int             Cudd_ReadPerm( DdManager * dd, int i );
extern int             Cudd_ReadPermZdd( DdManager * dd, int i );
extern int             Cudd_ReadInvPerm( DdManager * dd, int i );
extern int             Cudd_ReadInvPermZdd( DdManager * dd, int i );
extern DdNode *        Cudd_ReadVars( DdManager * dd, int i );
extern CUDD_VALUE_TYPE Cudd_ReadEpsilon( DdManager * dd );
extern void            Cudd_SetEpsilon( DdManager * dd, CUDD_VALUE_TYPE ep );
extern Cudd_AggregationType Cudd_ReadGroupcheck( DdManager * dd );
extern void            Cudd_SetGroupcheck( DdManager * dd, Cudd_AggregationType gc );
extern int             Cudd_GarbageCollectionEnabled( DdManager * dd );
extern void            Cudd_EnableGarbageCollection( DdManager * dd );
extern void            Cudd_DisableGarbageCollection( DdManager * dd );
extern int             Cudd_DeadAreCounted( DdManager * dd );
extern void            Cudd_TurnOnCountDead( DdManager * dd );
extern void            Cudd_TurnOffCountDead( DdManager * dd );
extern int             Cudd_ReadRecomb( DdManager * dd );
extern void            Cudd_SetRecomb( DdManager * dd, int recomb );
extern int             Cudd_ReadSymmviolation( DdManager * dd );
extern void            Cudd_SetSymmviolation( DdManager * dd, int symmviolation );
extern int             Cudd_ReadArcviolation( DdManager * dd );
extern void            Cudd_SetArcviolation( DdManager * dd, int arcviolation );
extern int             Cudd_ReadPopulationSize( DdManager * dd );
extern void            Cudd_SetPopulationSize( DdManager * dd, int populationSize );
extern int             Cudd_ReadNumberXovers( DdManager * dd );
extern void            Cudd_SetNumberXovers( DdManager * dd, int numberXovers );
extern unsigned long   Cudd_ReadMemoryInUse( DdManager * dd );
extern int             Cudd_PrintInfo( DdManager * dd, FILE * fp );
extern long            Cudd_ReadPeakNodeCount( DdManager * dd );
extern int             Cudd_ReadPeakLiveNodeCount( DdManager * dd );
extern long            Cudd_ReadNodeCount( DdManager * dd );
extern long            Cudd_zddReadNodeCount( DdManager * dd );
extern int             Cudd_AddHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
extern int             Cudd_RemoveHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
extern int             Cudd_IsInHook( DdManager * dd, DD_HFP f, Cudd_HookType where );
extern int             Cudd_StdPreReordHook( DdManager * dd, const char * str, void * data );
extern int             Cudd_StdPostReordHook( DdManager * dd, const char * str, void * data );
extern int             Cudd_EnableReorderingReporting( DdManager * dd );
extern int             Cudd_DisableReorderingReporting( DdManager * dd );
extern int             Cudd_ReorderingReporting( DdManager * dd );
extern Cudd_ErrorType  Cudd_ReadErrorCode( DdManager * dd );
extern void            Cudd_ClearErrorCode( DdManager * dd );
extern FILE *          Cudd_ReadStdout( DdManager * dd );
extern void            Cudd_SetStdout( DdManager * dd, FILE * fp );
extern FILE *          Cudd_ReadStderr( DdManager * dd );
extern void            Cudd_SetStderr( DdManager * dd, FILE * fp );
extern unsigned int    Cudd_ReadNextReordering( DdManager * dd );
extern void            Cudd_SetNextReordering( DdManager * dd, unsigned int next );
extern double          Cudd_ReadSwapSteps( DdManager * dd );
extern unsigned int    Cudd_ReadMaxLive( DdManager * dd );
extern void            Cudd_SetMaxLive( DdManager * dd, unsigned int maxLive );
extern unsigned long   Cudd_ReadMaxMemory( DdManager * dd );
extern void            Cudd_SetMaxMemory( DdManager * dd, unsigned long maxMemory );
extern int             Cudd_bddBindVar( DdManager * dd, int index );
extern int             Cudd_bddUnbindVar( DdManager * dd, int index );
extern int             Cudd_bddVarIsBound( DdManager * dd, int index );
extern DdNode *        Cudd_addExistAbstract( DdManager * manager, DdNode * f, DdNode * cube );
extern DdNode *        Cudd_addUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube );
extern DdNode *        Cudd_addOrAbstract( DdManager * manager, DdNode * f, DdNode * cube );
extern DdNode *        Cudd_addApply( DdManager * dd, DdNode * ( * )(DdManager * , DdNode ** , DdNode ** ), DdNode * f, DdNode * g );
extern DdNode *        Cudd_addPlus( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addTimes( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addThreshold( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addSetNZ( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addDivide( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addMinus( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addMinimum( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addMaximum( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addOneZeroMaximum( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addDiff( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addAgreement( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addOr( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addNand( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addNor( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addXor( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addXnor( DdManager * dd, DdNode ** f, DdNode ** g );
extern DdNode *        Cudd_addMonadicApply( DdManager * dd, DdNode * ( * op)(DdManager * , DdNode * ), DdNode * f );
extern DdNode *        Cudd_addLog( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addFindMax( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addFindMin( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addIthBit( DdManager * dd, DdNode * f, int bit );
extern DdNode *        Cudd_addScalarInverse( DdManager * dd, DdNode * f, DdNode * epsilon );
extern DdNode *        Cudd_addIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
extern DdNode *        Cudd_addIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
extern DdNode *        Cudd_addEvalConst( DdManager * dd, DdNode * f, DdNode * g );
extern int             Cudd_addLeq( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_addCmpl( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addNegate( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addRoundOff( DdManager * dd, DdNode * f, int N );
extern DdNode *        Cudd_addWalsh( DdManager * dd, DdNode ** x, DdNode ** y, int n );
extern DdNode *        Cudd_addResidue( DdManager * dd, int n, int m, int options, int top );
extern DdNode *        Cudd_bddAndAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube );
extern DdNode *        Cudd_bddAndAbstractLimit( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, unsigned int limit );
extern int             Cudd_ApaNumberOfDigits( int binaryDigits );
extern DdApaNumber     Cudd_NewApaNumber( int digits );
extern void            Cudd_ApaCopy( int digits, DdApaNumber source, DdApaNumber dest );
extern DdApaDigit      Cudd_ApaAdd( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber sum );
extern DdApaDigit      Cudd_ApaSubtract( int digits, DdApaNumber a, DdApaNumber b, DdApaNumber diff );
extern DdApaDigit      Cudd_ApaShortDivision( int digits, DdApaNumber dividend, DdApaDigit divisor, DdApaNumber quotient );
extern unsigned int    Cudd_ApaIntDivision( int digits, DdApaNumber dividend, unsigned int divisor, DdApaNumber quotient );
extern void            Cudd_ApaShiftRight( int digits, DdApaDigit in, DdApaNumber a, DdApaNumber b );
extern void            Cudd_ApaSetToLiteral( int digits, DdApaNumber number, DdApaDigit literal );
extern void            Cudd_ApaPowerOfTwo( int digits, DdApaNumber number, int power );
extern int             Cudd_ApaCompare( int digitsFirst, DdApaNumber first, int digitsSecond, DdApaNumber second );
extern int             Cudd_ApaCompareRatios( int digitsFirst, DdApaNumber firstNum, unsigned int firstDen, int digitsSecond, DdApaNumber secondNum, unsigned int secondDen );
extern int             Cudd_ApaPrintHex( FILE * fp, int digits, DdApaNumber number );
extern int             Cudd_ApaPrintDecimal( FILE * fp, int digits, DdApaNumber number );
extern int             Cudd_ApaPrintExponential( FILE * fp, int digits, DdApaNumber number, int precision );
extern DdApaNumber     Cudd_ApaCountMinterm( DdManager * manager, DdNode * node, int nvars, int * digits );
extern int             Cudd_ApaPrintMinterm( FILE * fp, DdManager * dd, DdNode * node, int nvars );
extern int             Cudd_ApaPrintMintermExp( FILE * fp, DdManager * dd, DdNode * node, int nvars, int precision );
extern int             Cudd_ApaPrintDensity( FILE * fp, DdManager * dd, DdNode * node, int nvars );
extern DdNode *        Cudd_UnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality );
extern DdNode *        Cudd_OverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, int safe, double quality );
extern DdNode *        Cudd_RemapUnderApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality );
extern DdNode *        Cudd_RemapOverApprox( DdManager * dd, DdNode * f, int numVars, int threshold, double quality );
extern DdNode *        Cudd_BiasedUnderApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 );
extern DdNode *        Cudd_BiasedOverApprox( DdManager * dd, DdNode * f, DdNode * b, int numVars, int threshold, double quality1, double quality0 );
extern DdNode *        Cudd_bddExistAbstract( DdManager * manager, DdNode * f, DdNode * cube );
extern DdNode *        Cudd_bddXorExistAbstract( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube );
extern DdNode *        Cudd_bddUnivAbstract( DdManager * manager, DdNode * f, DdNode * cube );
extern DdNode *        Cudd_bddBooleanDiff( DdManager * manager, DdNode * f, int x );
extern int             Cudd_bddVarIsDependent( DdManager * dd, DdNode * f, DdNode * var );
extern double          Cudd_bddCorrelation( DdManager * manager, DdNode * f, DdNode * g );
extern double          Cudd_bddCorrelationWeights( DdManager * manager, DdNode * f, DdNode * g, double * prob );
extern DdNode *        Cudd_bddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
extern DdNode *        Cudd_bddIteConstant( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
extern DdNode *        Cudd_bddIntersect( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddAnd( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddAndLimit( DdManager * dd, DdNode * f, DdNode * g, unsigned int limit );
extern DdNode *        Cudd_bddOr( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddNand( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddNor( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddXor( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddXnor( DdManager * dd, DdNode * f, DdNode * g );
extern int             Cudd_bddLeq( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_addBddThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value );
extern DdNode *        Cudd_addBddStrictThreshold( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE value );
extern DdNode *        Cudd_addBddInterval( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper );
extern DdNode *        Cudd_addBddIthBit( DdManager * dd, DdNode * f, int bit );
extern DdNode *        Cudd_BddToAdd( DdManager * dd, DdNode * B );
extern DdNode *        Cudd_addBddPattern( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_bddTransfer( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
extern int             Cudd_DebugCheck( DdManager * table );
extern int             Cudd_CheckKeys( DdManager * table );
extern DdNode *        Cudd_bddClippingAnd( DdManager * dd, DdNode * f, DdNode * g, int maxDepth, int direction );
extern DdNode *        Cudd_bddClippingAndAbstract( DdManager * dd, DdNode * f, DdNode * g, DdNode * cube, int maxDepth, int direction );
extern DdNode *        Cudd_Cofactor( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_bddCompose( DdManager * dd, DdNode * f, DdNode * g, int v );
extern DdNode *        Cudd_addCompose( DdManager * dd, DdNode * f, DdNode * g, int v );
extern DdNode *        Cudd_addPermute( DdManager * manager, DdNode * node, int * permut );
extern DdNode *        Cudd_addSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n );
extern DdNode *        Cudd_bddPermute( DdManager * manager, DdNode * node, int * permut );
extern DdNode *        Cudd_bddVarMap( DdManager * manager, DdNode * f );
extern int             Cudd_SetVarMap( DdManager * manager, DdNode ** x, DdNode ** y, int n );
extern DdNode *        Cudd_bddSwapVariables( DdManager * dd, DdNode * f, DdNode ** x, DdNode ** y, int n );
extern DdNode *        Cudd_bddAdjPermuteX( DdManager * dd, DdNode * B, DdNode ** x, int n );
extern DdNode *        Cudd_addVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector );
extern DdNode *        Cudd_addGeneralVectorCompose( DdManager * dd, DdNode * f, DdNode ** vectorOn, DdNode ** vectorOff );
extern DdNode *        Cudd_addNonSimCompose( DdManager * dd, DdNode * f, DdNode ** vector );
extern DdNode *        Cudd_bddVectorCompose( DdManager * dd, DdNode * f, DdNode ** vector );
extern int             Cudd_bddApproxConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
extern int             Cudd_bddApproxDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
extern int             Cudd_bddIterConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
extern int             Cudd_bddIterDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
extern int             Cudd_bddGenConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
extern int             Cudd_bddGenDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
extern int             Cudd_bddVarConjDecomp( DdManager * dd, DdNode * f, DdNode ** * conjuncts );
extern int             Cudd_bddVarDisjDecomp( DdManager * dd, DdNode * f, DdNode ** * disjuncts );
extern DdNode *        Cudd_FindEssential( DdManager * dd, DdNode * f );
extern int             Cudd_bddIsVarEssential( DdManager * manager, DdNode * f, int id, int phase );
extern DdTlcInfo *     Cudd_FindTwoLiteralClauses( DdManager * dd, DdNode * f );
extern int             Cudd_PrintTwoLiteralClauses( DdManager * dd, DdNode * f, char ** names, FILE * fp );
extern int             Cudd_ReadIthClause( DdTlcInfo * tlc, int i, DdHalfWord * var1, DdHalfWord * var2, int * phase1, int * phase2 );
extern void            Cudd_tlcInfoFree( DdTlcInfo * t );
extern int             Cudd_DumpBlif( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, char * mname, FILE * fp, int mv );
extern int             Cudd_DumpBlifBody( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp, int mv );
extern int             Cudd_DumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
extern int             Cudd_DumpDaVinci( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
extern int             Cudd_DumpDDcal( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
extern int             Cudd_DumpFactoredForm( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
extern DdNode *        Cudd_bddConstrain( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode *        Cudd_bddRestrict( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode *        Cudd_bddNPAnd( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode *        Cudd_addConstrain( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode **       Cudd_bddConstrainDecomp( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_addRestrict( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode **       Cudd_bddCharToVect( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_bddLICompaction( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode *        Cudd_bddSqueeze( DdManager * dd, DdNode * l, DdNode * u );
extern DdNode *        Cudd_bddMinimize( DdManager * dd, DdNode * f, DdNode * c );
extern DdNode *        Cudd_SubsetCompress( DdManager * dd, DdNode * f, int nvars, int threshold );
extern DdNode *        Cudd_SupersetCompress( DdManager * dd, DdNode * f, int nvars, int threshold );
extern MtrNode *       Cudd_MakeTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type );
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 );
extern DdManager *     Cudd_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory );
extern void            Cudd_Quit( DdManager * unique );
extern int             Cudd_PrintLinear( DdManager * table );
extern int             Cudd_ReadLinear( DdManager * table, int x, int y );
extern DdNode *        Cudd_bddLiteralSetIntersection( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_addMatrixMultiply( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz );
extern DdNode *        Cudd_addTimesPlus( DdManager * dd, DdNode * A, DdNode * B, DdNode ** z, int nz );
extern DdNode *        Cudd_addTriangle( DdManager * dd, DdNode * f, DdNode * g, DdNode ** z, int nz );
extern DdNode *        Cudd_addOuterSum( DdManager * dd, DdNode * M, DdNode * r, DdNode * c );
extern DdNode *        Cudd_PrioritySelect( DdManager * dd, DdNode * R, DdNode ** x, DdNode ** y, DdNode ** z, DdNode * Pi, int n, DdNode * ( * )(DdManager * , int, DdNode ** , DdNode ** , DdNode ** ) );
extern DdNode *        Cudd_Xgty( DdManager * dd, int N, DdNode ** z, DdNode ** x, DdNode ** y );
extern DdNode *        Cudd_Xeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y );
extern DdNode *        Cudd_addXeqy( DdManager * dd, int N, DdNode ** x, DdNode ** y );
extern DdNode *        Cudd_Dxygtdxz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z );
extern DdNode *        Cudd_Dxygtdyz( DdManager * dd, int N, DdNode ** x, DdNode ** y, DdNode ** z );
extern DdNode *        Cudd_Inequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y );
extern DdNode *        Cudd_Disequality( DdManager * dd, int N, int c, DdNode ** x, DdNode ** y );
extern DdNode *        Cudd_bddInterval( DdManager * dd, int N, DdNode ** x, unsigned int lowerB, unsigned int upperB );
extern DdNode *        Cudd_CProjection( DdManager * dd, DdNode * R, DdNode * Y );
extern DdNode *        Cudd_addHamming( DdManager * dd, DdNode ** xVars, DdNode ** yVars, int nVars );
extern int             Cudd_MinHammingDist( DdManager * dd, DdNode * f, int * minterm, int upperBound );
extern DdNode *        Cudd_bddClosestCube( DdManager * dd, DdNode * f, DdNode * g, int * distance );
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 );
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 );
extern void            Cudd_Ref( DdNode * n );
extern void            Cudd_RecursiveDeref( DdManager * table, DdNode * n );
extern void            Cudd_IterDerefBdd( DdManager * table, DdNode * n );
extern void            Cudd_DelayedDerefBdd( DdManager * table, DdNode * n );
extern void            Cudd_RecursiveDerefZdd( DdManager * table, DdNode * n );
extern void            Cudd_Deref( DdNode * node );
extern int             Cudd_CheckZeroRef( DdManager * manager );
extern int             Cudd_ReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize );
extern int             Cudd_ShuffleHeap( DdManager * table, int * permutation );
extern DdNode *        Cudd_Eval( DdManager * dd, DdNode * f, int * inputs );
extern DdNode *        Cudd_ShortestPath( DdManager * manager, DdNode * f, int * weight, int * support, int * length );
extern DdNode *        Cudd_LargestCube( DdManager * manager, DdNode * f, int * length );
extern int             Cudd_ShortestLength( DdManager * manager, DdNode * f, int * weight );
extern DdNode *        Cudd_Decreasing( DdManager * dd, DdNode * f, int i );
extern DdNode *        Cudd_Increasing( DdManager * dd, DdNode * f, int i );
extern int             Cudd_EquivDC( DdManager * dd, DdNode * F, DdNode * G, DdNode * D );
extern int             Cudd_bddLeqUnless( DdManager * dd, DdNode * f, DdNode * g, DdNode * D );
extern int             Cudd_EqualSupNorm( DdManager * dd, DdNode * f, DdNode * g, CUDD_VALUE_TYPE tolerance, int pr );
extern DdNode *        Cudd_bddMakePrime( DdManager * dd, DdNode * cube, DdNode * f );
extern double *        Cudd_CofMinterm( DdManager * dd, DdNode * node );
extern DdNode *        Cudd_SolveEqn( DdManager * bdd, DdNode * F, DdNode * Y, DdNode ** G, int ** yIndex, int n );
extern DdNode *        Cudd_VerifySol( DdManager * bdd, DdNode * F, DdNode ** G, int * yIndex, int n );
extern DdNode *        Cudd_SplitSet( DdManager * manager, DdNode * S, DdNode ** xVars, int n, double m );
extern DdNode *        Cudd_SubsetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold );
extern DdNode *        Cudd_SupersetHeavyBranch( DdManager * dd, DdNode * f, int numVars, int threshold );
extern DdNode *        Cudd_SubsetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit );
extern DdNode *        Cudd_SupersetShortPaths( DdManager * dd, DdNode * f, int numVars, int threshold, int hardlimit );
extern void            Cudd_SymmProfile( DdManager * table, int lower, int upper );
extern unsigned int    Cudd_Prime( unsigned int p );
extern int             Cudd_PrintMinterm( DdManager * manager, DdNode * node );
extern int             Cudd_bddPrintCover( DdManager * dd, DdNode * l, DdNode * u );
extern int             Cudd_PrintDebug( DdManager * dd, DdNode * f, int n, int pr );
extern int             Cudd_DagSize( DdNode * node );
extern int             Cudd_EstimateCofactor( DdManager * dd, DdNode * node, int i, int phase );
extern int             Cudd_EstimateCofactorSimple( DdNode * node, int i );
extern int             Cudd_SharingSize( DdNode ** nodeArray, int n );
extern double          Cudd_CountMinterm( DdManager * manager, DdNode * node, int nvars );
extern int             Cudd_EpdCountMinterm( DdManager * manager, DdNode * node, int nvars, EpDouble * epd );
extern double          Cudd_CountPath( DdNode * node );
extern double          Cudd_CountPathsToNonZero( DdNode * node );
extern DdNode *        Cudd_Support( DdManager * dd, DdNode * f );
extern int *           Cudd_SupportIndex( DdManager * dd, DdNode * f );
extern int             Cudd_SupportSize( DdManager * dd, DdNode * f );
extern DdNode *        Cudd_VectorSupport( DdManager * dd, DdNode ** F, int n );
extern int *           Cudd_VectorSupportIndex( DdManager * dd, DdNode ** F, int n );
extern int             Cudd_VectorSupportSize( DdManager * dd, DdNode ** F, int n );
extern int             Cudd_ClassifySupport( DdManager * dd, DdNode * f, DdNode * g, DdNode ** common, DdNode ** onlyF, DdNode ** onlyG );
extern int             Cudd_CountLeaves( DdNode * node );
extern int             Cudd_bddPickOneCube( DdManager * ddm, DdNode * node, char * string );
extern DdNode *        Cudd_bddPickOneMinterm( DdManager * dd, DdNode * f, DdNode ** vars, int n );
extern DdNode **       Cudd_bddPickArbitraryMinterms( DdManager * dd, DdNode * f, DdNode ** vars, int n, int k );
extern DdNode *        Cudd_SubsetWithMaskVars( DdManager * dd, DdNode * f, DdNode ** vars, int nvars, DdNode ** maskVars, int mvars );
extern DdGen *         Cudd_FirstCube( DdManager * dd, DdNode * f, int ** cube, CUDD_VALUE_TYPE * value );
extern int             Cudd_NextCube( DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value );
extern DdGen *         Cudd_FirstPrime(DdManager * dd, DdNode * l, DdNode * u, int ** cube );
extern int             Cudd_NextPrime(DdGen * gen, int ** cube );
extern DdNode *        Cudd_bddComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n );
extern DdNode *        Cudd_addComputeCube( DdManager * dd, DdNode ** vars, int * phase, int n );
extern DdNode *        Cudd_CubeArrayToBdd( DdManager * dd, int * array );
extern int             Cudd_BddToCubeArray( DdManager * dd, DdNode * cube, int * array );
extern DdGen *         Cudd_FirstNode( DdManager * dd, DdNode * f, DdNode ** node );
extern int             Cudd_NextNode( DdGen * gen, DdNode ** node );
extern int             Cudd_GenFree( DdGen * gen );
extern int             Cudd_IsGenEmpty( DdGen * gen );
extern DdNode *        Cudd_IndicesToCube( DdManager * dd, int * array, int n );
extern void            Cudd_PrintVersion( FILE * fp );
extern double          Cudd_AverageDistance( DdManager * dd );
extern long            Cudd_Random( void );
extern void            Cudd_Srandom( long seed );
extern double          Cudd_Density( DdManager * dd, DdNode * f, int nvars );
extern void            Cudd_OutOfMem( long size );
extern int             Cudd_zddCount( DdManager * zdd, DdNode * P );
extern double          Cudd_zddCountDouble( DdManager * zdd, DdNode * P );
extern DdNode *        Cudd_zddProduct( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddUnateProduct( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddWeakDiv( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddDivide( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddWeakDivF( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddDivideF( DdManager * dd, DdNode * f, DdNode * g );
extern DdNode *        Cudd_zddComplement( DdManager * dd, DdNode * node );
extern MtrNode *       Cudd_MakeZddTreeNode( DdManager * dd, unsigned int low, unsigned int size, unsigned int type );
extern DdNode *        Cudd_zddIsop( DdManager * dd, DdNode * L, DdNode * U, DdNode ** zdd_I );
extern DdNode *        Cudd_bddIsop( DdManager * dd, DdNode * L, DdNode * U );
extern DdNode *        Cudd_MakeBddFromZddCover( DdManager * dd, DdNode * node );
extern int             Cudd_zddDagSize( DdNode * p_node );
extern double          Cudd_zddCountMinterm( DdManager * zdd, DdNode * node, int path );
extern void            Cudd_zddPrintSubtable( DdManager * table );
extern DdNode *        Cudd_zddPortFromBdd( DdManager * dd, DdNode * B );
extern DdNode *        Cudd_zddPortToBdd( DdManager * dd, DdNode * f );
extern int             Cudd_zddReduceHeap( DdManager * table, Cudd_ReorderingType heuristic, int minsize );
extern int             Cudd_zddShuffleHeap( DdManager * table, int * permutation );
extern DdNode *        Cudd_zddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h );
extern DdNode *        Cudd_zddUnion( DdManager * dd, DdNode * P, DdNode * Q );
extern DdNode *        Cudd_zddIntersect( DdManager * dd, DdNode * P, DdNode * Q );
extern DdNode *        Cudd_zddDiff( DdManager * dd, DdNode * P, DdNode * Q );
extern DdNode *        Cudd_zddDiffConst( DdManager * zdd, DdNode * P, DdNode * Q );
extern DdNode *        Cudd_zddSubset1( DdManager * dd, DdNode * P, int var );
extern DdNode *        Cudd_zddSubset0( DdManager * dd, DdNode * P, int var );
extern DdNode *        Cudd_zddChange( DdManager * dd, DdNode * P, int var );
extern void            Cudd_zddSymmProfile( DdManager * table, int lower, int upper );
extern int             Cudd_zddPrintMinterm( DdManager * zdd, DdNode * node );
extern int             Cudd_zddPrintCover( DdManager * zdd, DdNode * node );
extern int             Cudd_zddPrintDebug( DdManager * zdd, DdNode * f, int n, int pr );
extern DdGen *         Cudd_zddFirstPath( DdManager * zdd, DdNode * f, int ** path );
extern int             Cudd_zddNextPath( DdGen * gen, int ** path );
extern char *          Cudd_zddCoverPathToString( DdManager * zdd, int * path, char * str );
extern int             Cudd_zddDumpDot( DdManager * dd, int n, DdNode ** f, char ** inames, char ** onames, FILE * fp );
extern int             Cudd_bddSetPiVar( DdManager * dd, int index );
extern int             Cudd_bddSetPsVar( DdManager * dd, int index );
extern int             Cudd_bddSetNsVar( DdManager * dd, int index );
extern int             Cudd_bddIsPiVar( DdManager * dd, int index );
extern int             Cudd_bddIsPsVar( DdManager * dd, int index );
extern int             Cudd_bddIsNsVar( DdManager * dd, int index );
extern int             Cudd_bddSetPairIndex( DdManager * dd, int index, int pairIndex );
extern int             Cudd_bddReadPairIndex( DdManager * dd, int index );
extern int             Cudd_bddSetVarToBeGrouped( DdManager * dd, int index );
extern int             Cudd_bddSetVarHardGroup( DdManager * dd, int index );
extern int             Cudd_bddResetVarToBeGrouped( DdManager * dd, int index );
extern int             Cudd_bddIsVarToBeGrouped( DdManager * dd, int index );
extern int             Cudd_bddSetVarToBeUngrouped( DdManager * dd, int index );
extern int             Cudd_bddIsVarToBeUngrouped( DdManager * dd, int index );
extern int             Cudd_bddIsVarHardGroup( DdManager * dd, int index );

/**AutomaticEnd***************************************************************/



ABC_NAMESPACE_HEADER_END

#endif /* _CUDD */