extraBdd.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/st/st.h"
#include "bdd/cudd/cuddInt.h"
#include "misc/extra/extra.h"

Include dependency graph for extraBdd.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Extra_SymmInfo_t_
struct	Extra_UnateVar_t_
struct	Extra_UnateInfo_t_

Macros
#define	b0   Cudd_Not((dd)->one)
#define	b1   (dd)->one
#define	z0   (dd)->zero
#define	z1   (dd)->one
#define	a0   (dd)->zero
#define	a1   (dd)->one
#define	hashKey1(a, TSIZE)
#define	hashKey2(a, b, TSIZE)
#define	hashKey3(a, b, c, TSIZE)
#define	hashKey4(a, b, c, d, TSIZE)
#define	hashKey5(a, b, c, d, e, TSIZE)
#define	ABC_PRB(dd, f)

Typedefs
typedef struct Extra_ImageTree_t_	Extra_ImageTree_t
typedef struct Extra_ImageTree2_t_	Extra_ImageTree2_t
typedef struct Extra_SymmInfo_t_	Extra_SymmInfo_t
typedef struct Extra_UnateVar_t_	Extra_UnateVar_t
typedef struct Extra_UnateInfo_t_	Extra_UnateInfo_t

Functions
DdNode *	Extra_bddSpaceFromFunctionFast (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceFromFunction (DdManager *dd, DdNode *bF, DdNode *bG)
DdNode *	extraBddSpaceFromFunction (DdManager *dd, DdNode *bF, DdNode *bG)
DdNode *	Extra_bddSpaceFromFunctionPos (DdManager *dd, DdNode *bFunc)
DdNode *	extraBddSpaceFromFunctionPos (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceFromFunctionNeg (DdManager *dd, DdNode *bFunc)
DdNode *	extraBddSpaceFromFunctionNeg (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddSpaceCanonVars (DdManager *dd, DdNode *bSpace)
DdNode *	extraBddSpaceCanonVars (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceEquations (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceEquationsNeg (DdManager *dd, DdNode *bSpace)
DdNode *	extraBddSpaceEquationsNeg (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceEquationsPos (DdManager *dd, DdNode *bSpace)
DdNode *	extraBddSpaceEquationsPos (DdManager *dd, DdNode *bSpace)
DdNode *	Extra_bddSpaceFromMatrixPos (DdManager *dd, DdNode *zA)
DdNode *	extraBddSpaceFromMatrixPos (DdManager *dd, DdNode *zA)
DdNode *	Extra_bddSpaceFromMatrixNeg (DdManager *dd, DdNode *zA)
DdNode *	extraBddSpaceFromMatrixNeg (DdManager *dd, DdNode *zA)
DdNode *	Extra_bddSpaceReduce (DdManager *dd, DdNode *bFunc, DdNode *bCanonVars)
DdNode **	Extra_bddSpaceExorGates (DdManager *dd, DdNode *bFuncRed, DdNode *zEquations)
DdNode *	Extra_bddEncodingBinary (DdManager *dd, DdNode **pbFuncs, int nFuncs, DdNode **pbVars, int nVars)
DdNode *	Extra_bddEncodingNonStrict (DdManager *dd, DdNode **pbColumns, int nColumns, DdNode *bVarsCol, DdNode **pCVars, int nMulti, int *pSimple)
st__table *	Extra_bddNodePathsUnderCut (DdManager *dd, DdNode *bFunc, int CutLevel)
int	Extra_bddNodePathsUnderCutArray (DdManager *dd, DdNode **paNodes, DdNode **pbCubes, int nNodes, DdNode **paNodesRes, DdNode **pbCubesRes, int CutLevel)
int	Extra_ProfileWidth (DdManager *dd, DdNode *F, int *Profile, int CutLevel)
Extra_ImageTree_t *	Extra_bddImageStart (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Extra_bddImageCompute (Extra_ImageTree_t *pTree, DdNode *bCare)
void	Extra_bddImageTreeDelete (Extra_ImageTree_t *pTree)
DdNode *	Extra_bddImageRead (Extra_ImageTree_t *pTree)
Extra_ImageTree2_t *	Extra_bddImageStart2 (DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
DdNode *	Extra_bddImageCompute2 (Extra_ImageTree2_t *pTree, DdNode *bCare)
void	Extra_bddImageTreeDelete2 (Extra_ImageTree2_t *pTree)
DdNode *	Extra_bddImageRead2 (Extra_ImageTree2_t *pTree)
DdNode *	Extra_TransferPermute (DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
DdNode *	Extra_TransferLevelByLevel (DdManager *ddSource, DdManager *ddDestination, DdNode *f)
DdNode *	Extra_bddRemapUp (DdManager *dd, DdNode *bF)
DdNode *	Extra_bddMove (DdManager *dd, DdNode *bF, int nVars)
DdNode *	extraBddMove (DdManager *dd, DdNode *bF, DdNode *bFlag)
void	Extra_StopManager (DdManager *dd)
void	Extra_bddPrint (DdManager *dd, DdNode *F)
void	Extra_bddPrintSupport (DdManager *dd, DdNode *F)
void	extraDecomposeCover (DdManager *dd, DdNode *zC, DdNode **zC0, DdNode **zC1, DdNode **zC2)
int	Extra_bddSuppSize (DdManager *dd, DdNode *bSupp)
int	Extra_bddSuppContainVar (DdManager *dd, DdNode *bS, DdNode *bVar)
int	Extra_bddSuppOverlapping (DdManager *dd, DdNode *S1, DdNode *S2)
int	Extra_bddSuppDifferentVars (DdManager *dd, DdNode *S1, DdNode *S2, int DiffMax)
int	Extra_bddSuppCheckContainment (DdManager *dd, DdNode *bL, DdNode *bH, DdNode **bLarge, DdNode **bSmall)
int *	Extra_SupportArray (DdManager *dd, DdNode *F, int *support)
int *	Extra_VectorSupportArray (DdManager *dd, DdNode **F, int n, int *support)
DdNode *	Extra_bddFindOneCube (DdManager *dd, DdNode *bF)
DdNode *	Extra_bddGetOneCube (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_bddComputeRangeCube (DdManager *dd, int iStart, int iStop)
DdNode *	Extra_bddBitsToCube (DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
DdNode *	Extra_bddSupportNegativeCube (DdManager *dd, DdNode *f)
int	Extra_bddIsVar (DdNode *bFunc)
DdNode *	Extra_bddCreateAnd (DdManager *dd, int nVars)
DdNode *	Extra_bddCreateOr (DdManager *dd, int nVars)
DdNode *	Extra_bddCreateExor (DdManager *dd, int nVars)
DdNode *	Extra_zddPrimes (DdManager *dd, DdNode *F)
void	Extra_bddPermuteArray (DdManager *dd, DdNode **bNodesIn, DdNode **bNodesOut, int nNodes, int *permut)
DdNode *	Extra_bddComputeCube (DdManager *dd, DdNode **bXVars, int nVars)
DdNode *	Extra_bddChangePolarity (DdManager *dd, DdNode *bFunc, DdNode *bVars)
DdNode *	extraBddChangePolarity (DdManager *dd, DdNode *bFunc, DdNode *bVars)
int	Extra_bddVarIsInCube (DdNode *bCube, int iVar)
DdNode *	Extra_bddAndPermute (DdManager *ddF, DdNode *bF, DdManager *ddG, DdNode *bG, int *pPermute)
int	Extra_bddCountCubes (DdManager *dd, DdNode **pFuncs, int nFuncs, int fMode, int nLimit, int *pGuide)
void	Extra_zddDumpPla (DdManager *dd, DdNode *zCover, int nVars, char *pFileName)
DdNode *	Extra_bddTuples (DdManager *dd, int K, DdNode *bVarsN)
DdNode *	extraBddTuples (DdManager *dd, DdNode *bVarsK, DdNode *bVarsN)
DdNode *	Extra_zddMaximal (DdManager *dd, DdNode *S)
DdNode *	extraZddMaximal (DdManager *dd, DdNode *S)
DdNode *	Extra_zddMinimal (DdManager *dd, DdNode *S)
DdNode *	extraZddMinimal (DdManager *dd, DdNode *S)
DdNode *	Extra_zddMaxUnion (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	extraZddMaxUnion (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	Extra_zddMinUnion (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	extraZddMinUnion (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	Extra_zddDotProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	extraZddDotProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	Extra_zddCrossProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	extraZddCrossProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	Extra_zddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	extraZddMaxDotProduct (DdManager *dd, DdNode *S, DdNode *T)
DdNode *	Extra_zddSubSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	extraZddSubSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	Extra_zddSupSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	extraZddSupSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	Extra_zddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	extraZddNotSubSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	Extra_zddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	extraZddNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	Extra_zddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
DdNode *	extraZddMaxNotSupSet (DdManager *dd, DdNode *X, DdNode *Y)
int	Extra_zddEmptyBelongs (DdManager *dd, DdNode *zS)
int	Extra_zddIsOneSubset (DdManager *dd, DdNode *zS)
void	Extra_PrintKMap (FILE *pFile, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nVars, DdNode **XVars, int fSuppType, char **pVarNames)
void	Extra_PrintKMapRelation (FILE *pFile, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nXVars, int nYVars, DdNode **XVars, DdNode **YVars)
Extra_SymmInfo_t *	Extra_SymmPairsCompute (DdManager *dd, DdNode *bFunc)
Extra_SymmInfo_t *	Extra_SymmPairsComputeNaive (DdManager *dd, DdNode *bFunc)
int	Extra_bddCheckVarsSymmetricNaive (DdManager *dd, DdNode *bF, int iVar1, int iVar2)
Extra_SymmInfo_t *	Extra_SymmPairsAllocate (int nVars)
void	Extra_SymmPairsDissolve (Extra_SymmInfo_t *)
void	Extra_SymmPairsPrint (Extra_SymmInfo_t *)
Extra_SymmInfo_t *	Extra_SymmPairsCreateFromZdd (DdManager *dd, DdNode *zPairs, DdNode *bVars)
DdNode *	Extra_zddSymmPairsCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	extraZddSymmPairsCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	Extra_zddGetSymmetricVars (DdManager *dd, DdNode *bF, DdNode *bG, DdNode *bVars)
DdNode *	extraZddGetSymmetricVars (DdManager *dd, DdNode *bF, DdNode *bG, DdNode *bVars)
DdNode *	Extra_zddGetSingletons (DdManager *dd, DdNode *bVars)
DdNode *	extraZddGetSingletons (DdManager *dd, DdNode *bVars)
DdNode *	Extra_bddReduceVarSet (DdManager *dd, DdNode *bVars, DdNode *bF)
DdNode *	extraBddReduceVarSet (DdManager *dd, DdNode *bVars, DdNode *bF)
int	Extra_bddCheckVarsSymmetric (DdManager *dd, DdNode *bF, int iVar1, int iVar2)
DdNode *	extraBddCheckVarsSymmetric (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	Extra_zddTuplesFromBdd (DdManager *dd, int K, DdNode *bVarsN)
DdNode *	extraZddTuplesFromBdd (DdManager *dd, DdNode *bVarsK, DdNode *bVarsN)
DdNode *	Extra_zddSelectOneSubset (DdManager *dd, DdNode *zS)
DdNode *	extraZddSelectOneSubset (DdManager *dd, DdNode *zS)
DdNode *	Extra_bddAndTime (DdManager *dd, DdNode *f, DdNode *g, int TimeOut)
DdNode *	Extra_bddAndAbstractTime (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int TimeOut)
DdNode *	Extra_TransferPermuteTime (DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute, int TimeOut)
Extra_UnateInfo_t *	Extra_UnateInfoAllocate (int nVars)
void	Extra_UnateInfoDissolve (Extra_UnateInfo_t *)
void	Extra_UnateInfoPrint (Extra_UnateInfo_t *)
Extra_UnateInfo_t *	Extra_UnateInfoCreateFromZdd (DdManager *dd, DdNode *zUnate, DdNode *bVars)
int	Extra_bddCheckUnateNaive (DdManager *dd, DdNode *bF, int iVar)
Extra_UnateInfo_t *	Extra_UnateComputeFast (DdManager *dd, DdNode *bFunc)
Extra_UnateInfo_t *	Extra_UnateComputeSlow (DdManager *dd, DdNode *bFunc)
DdNode *	Extra_zddUnateInfoCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	extraZddUnateInfoCompute (DdManager *dd, DdNode *bF, DdNode *bVars)
DdNode *	Extra_zddGetSingletonsBoth (DdManager *dd, DdNode *bVars)
DdNode *	extraZddGetSingletonsBoth (DdManager *dd, DdNode *bVars)

Macro Definition Documentation

a0

#define a0   (dd)->zero

Definition at line 79 of file extraBdd.h.

a1

#define a1   (dd)->one

Definition at line 80 of file extraBdd.h.

ABC_PRB

#define ABC_PRB	(		dd,
			f )

Value:

printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")

Definition at line 206 of file extraBdd.h.

b0

#define b0   Cudd_Not((dd)->one)

CFile****************************************************************

FileName [extraBdd.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [Various reusable software utilities.]

Description [This library contains a number of operators and traversal routines developed to extend the functionality of CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/) To compile your code with the library, #include "extra.h" in your source files and link your project to CUDD and this library. Use the library at your own risk and with caution. Note that debugging of some operators still continues.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

extraBdd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 75 of file extraBdd.h.

b1

#define b1   (dd)->one

Definition at line 76 of file extraBdd.h.

hashKey1

#define hashKey1	(		a,
			TSIZE )

Value:

((ABC_PTRUINT_T)(a) % TSIZE)

Definition at line 83 of file extraBdd.h.

#define hashKey1(a,TSIZE) \
((ABC_PTRUINT_T)(a) % TSIZE)

hashKey2

#define hashKey2	(		a,
			b,
			TSIZE )

Value:

(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)

Definition at line 86 of file extraBdd.h.

#define hashKey2(a,b,TSIZE) \
(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)

hashKey3

#define hashKey3	(		a,
			b,
			c,
			TSIZE )

Value:

(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)

Definition at line 89 of file extraBdd.h.

#define hashKey3(a,b,c,TSIZE) \
(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)

hashKey4

#define hashKey4	(		a,
			b,
			c,
			d,
			TSIZE )

Value:

((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)

Definition at line 92 of file extraBdd.h.

#define hashKey4(a,b,c,d,TSIZE) \
((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)

hashKey5

#define hashKey5	(		a,
			b,
			c,
			d,
			e,
			TSIZE )

Value:

(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)

Definition at line 96 of file extraBdd.h.

#define hashKey5(a,b,c,d,e,TSIZE) \
(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)

z0

#define z0   (dd)->zero

Definition at line 77 of file extraBdd.h.

z1

#define z1   (dd)->one

Definition at line 78 of file extraBdd.h.

Typedef Documentation

Extra_ImageTree2_t

typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t

Definition at line 155 of file extraBdd.h.

Extra_ImageTree_t

typedef struct Extra_ImageTree_t_ Extra_ImageTree_t

Definition at line 146 of file extraBdd.h.

Extra_SymmInfo_t

typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t

Definition at line 256 of file extraBdd.h.

Extra_UnateInfo_t

typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t

Definition at line 320 of file extraBdd.h.

Extra_UnateVar_t

typedef struct Extra_UnateVar_t_ Extra_UnateVar_t

Definition at line 313 of file extraBdd.h.

Function Documentation

Extra_bddAndAbstractTime()

DdNode * Extra_bddAndAbstractTime ( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int TimeOut )

extern

Function********************************************************************

Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise. Cudd_bddAndAbstract implements the semiring matrix multiplication algorithm for the boolean semiring.]

SideEffects [None]

SeeAlso [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]

Definition at line 117 of file extraBddTime.c.

{
    DdNode *res;
    int Counter = 0;
 
    do {
    manager->reordered = 0;
    res = cuddBddAndAbstractRecurTime(manager, f, g, cube, &Counter, TimeOut);
    } while (manager->reordered == 1);
    return(res);
 
} /* end of Extra_bddAndAbstractTime */

Extra_bddAndPermute()

DdNode * Extra_bddAndPermute ( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute )

extern

Function*************************************************************

Synopsis [Computes the AND of two BDD with different orders.]

Description [Derives the result of Boolean AND of bF and bG in ddF. The array pPermute gives the mapping of variables of ddG into that of ddF.]

SideEffects []

SeeAlso []

Definition at line 1090 of file extraBddMisc.c.

{
    DdHashTable * table;
    DdNode * bRes;
    do
    {
        ddF->reordered = 0;
        table = cuddHashTableInit( ddF, 2, 256 );
        if (table == NULL) return NULL;
        bRes = extraBddAndPermute( table, ddF, bF, ddG, bG, pPermute );  
        if ( bRes ) cuddRef( bRes );
        cuddHashTableQuit( table );
        if ( bRes ) cuddDeref( bRes );
//if ( ddF->reordered == 1 )
//printf( "Reordering happened\n" );
    }
    while ( ddF->reordered == 1 );
//printf( "|F| =%6d  |G| =%6d  |H| =%6d  |F|*|G| =%9d\n", 
//       Cudd_DagSize(bF), Cudd_DagSize(bG), Cudd_DagSize(bRes), 
//       Cudd_DagSize(bF) * Cudd_DagSize(bG) );
    return ( bRes );
}

Here is the caller graph for this function:

Extra_bddAndTime()

DdNode * Extra_bddAndTime ( DdManager * dd, DdNode * f, DdNode * g, int TimeOut )

extern

AutomaticEnd Function********************************************************************

Synopsis [Computes the conjunction of two BDDs f and g.]

Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]

Definition at line 83 of file extraBddTime.c.

{
    DdNode *res;
    int Counter = 0;
 
    do {
    dd->reordered = 0;
    res = cuddBddAndRecurTime(dd,f,g, &Counter, TimeOut);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_bddAndTime */

Extra_bddBitsToCube()

DdNode * Extra_bddBitsToCube ( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst )

extern

Function********************************************************************

Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code]

Description [Returns a bdd composed of elementary bdds found in array BddVars[] such that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, the most significant bit is encoded with the first bdd variable). If the variables BddVars are not specified, takes the first CodeWidth variables of the manager]

SideEffects []

SeeAlso []

Definition at line 730 of file extraBddMisc.c.

{
    int z;
    DdNode * bTemp, * bVar, * bVarBdd, * bResult;
 
    bResult = b1;   Cudd_Ref( bResult );
    for ( z = 0; z < CodeWidth; z++ )
    {
        bVarBdd = (pbVars)? pbVars[z]: dd->vars[z];
        if ( fMsbFirst )
            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 );
        else
            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 );
        bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar );     Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bResult );
 
    return bResult;
}  /* end of Extra_bddBitsToCube */

Here is the caller graph for this function:

Extra_bddChangePolarity()

DdNode * Extra_bddChangePolarity ( DdManager * dd, DdNode * bFunc, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Changes the polarity of vars listed in the cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 1029 of file extraBddMisc.c.

{
    DdNode  *res;
    do {
        dd->reordered = 0;
        res = extraBddChangePolarity( dd, bFunc, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_bddChangePolarity */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddCheckUnateNaive()

int Extra_bddCheckUnateNaive ( DdManager * dd, DdNode * bF, int iVar )

extern

Function********************************************************************

Synopsis [Checks if the two variables are symmetric.]

Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.]

SideEffects []

SeeAlso []

Definition at line 338 of file extraBddUnate.c.

{
    DdNode * bCof0, * bCof1;
    int Res;
 
    assert( iVar < dd->size );
 
    bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) );  Cudd_Ref( bCof0 );
    bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) );            Cudd_Ref( bCof1 );
 
    if ( Cudd_bddLeq( dd, bCof0, bCof1 ) )
        Res = 1;
    else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) )
        Res =-1;
    else
        Res = 0;
 
    Cudd_RecursiveDeref( dd, bCof0 );
    Cudd_RecursiveDeref( dd, bCof1 );
    return Res;
} /* end of Extra_bddCheckUnateNaive */

Here is the caller graph for this function:

Extra_bddCheckVarsSymmetric()

int Extra_bddCheckVarsSymmetric ( DdManager * dd, DdNode * bF, int iVar1, int iVar2 )

extern

Function********************************************************************

Synopsis [Checks the possibility of two variables being symmetric.]

Description [Returns 0 if vars are not symmetric. Return 1 if vars can be symmetric.]

SideEffects []

SeeAlso []

Definition at line 360 of file extraBddSymm.c.

{
    DdNode * bVars;
    int Res;
 
//  return 1;
 
    assert( iVar1 != iVar2 );
    assert( iVar1 < dd->size );
    assert( iVar2 < dd->size );
 
    bVars = Cudd_bddAnd( dd, dd->vars[iVar1], dd->vars[iVar2] );   Cudd_Ref( bVars );
 
    Res = (int)( extraBddCheckVarsSymmetric( dd, bF, bVars ) == b1 );
 
    Cudd_RecursiveDeref( dd, bVars );
 
    return Res;
} /* end of Extra_bddCheckVarsSymmetric */

Here is the call graph for this function:

Extra_bddCheckVarsSymmetricNaive()

int Extra_bddCheckVarsSymmetricNaive ( DdManager * dd, DdNode * bF, int iVar1, int iVar2 )

extern

Function********************************************************************

Synopsis [Checks if the two variables are symmetric.]

Description [Returns 0 if vars are not symmetric. Return 1 if vars are symmetric.]

SideEffects []

SeeAlso []

Definition at line 443 of file extraBddSymm.c.

{
    DdNode * bCube1, * bCube2;
    DdNode * bCof01, * bCof10;
    int Res;
 
    assert( iVar1 != iVar2 );
    assert( iVar1 < dd->size );
    assert( iVar2 < dd->size );
 
    bCube1 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar1] ), dd->vars[iVar2] );   Cudd_Ref( bCube1 );
    bCube2 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar2] ), dd->vars[iVar1] );   Cudd_Ref( bCube2 );
 
    bCof01 = Cudd_Cofactor( dd, bF, bCube1 );  Cudd_Ref( bCof01 );
    bCof10 = Cudd_Cofactor( dd, bF, bCube2 );  Cudd_Ref( bCof10 );
 
    Res = (int)( bCof10 == bCof01 );
 
    Cudd_RecursiveDeref( dd, bCof01 );
    Cudd_RecursiveDeref( dd, bCof10 );
    Cudd_RecursiveDeref( dd, bCube1 );
    Cudd_RecursiveDeref( dd, bCube2 );
 
    return Res;
} /* end of Extra_bddCheckVarsSymmetricNaive */

Here is the caller graph for this function:

Extra_bddComputeCube()

DdNode * Extra_bddComputeCube ( DdManager * dd, DdNode ** bXVars, int nVars )

extern

Function********************************************************************

Synopsis [Computes the positive polarty cube composed of the first vars in the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 1001 of file extraBddMisc.c.

{
    DdNode * bRes;
    DdNode * bTemp;
    int i;
 
    bRes = b1; Cudd_Ref( bRes );
    for ( i = 0; i < nVars; i++ )
    {
        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
    }
 
    Cudd_Deref( bRes );
    return bRes;
}

Here is the caller graph for this function:

Extra_bddComputeRangeCube()

DdNode * Extra_bddComputeRangeCube ( DdManager * dd, int iStart, int iStop )

extern

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file extraBddMisc.c.

{
    DdNode * bTemp, * bProd;
    int i;
    assert( iStart <= iStop );
    assert( iStart >= 0 && iStart <= dd->size );
    assert( iStop >= 0  && iStop  <= dd->size );
    bProd = b1;         Cudd_Ref( bProd );
    for ( i = iStart; i < iStop; i++ )
    {
        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bTemp ); 
    }
    Cudd_Deref( bProd );
    return bProd;
}

Extra_bddCountCubes()

int Extra_bddCountCubes ( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide )

extern

Definition at line 1485 of file extraBddMisc.c.

{
    DdNode * pF0, * pF1; 
    int i, Count, Count0, Count1, CounterAll = 0;
    st__table *table = st__init_table( st__ptrcmp, st__ptrhash );
    unsigned int saveLimit = dd->maxLive;
    dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes
    for ( i = 0; i < nFuncs; i++ )
    {
        if ( !pFuncs[i] )
            continue;
        pF1 = pF0 = NULL;
        Count0 = Count1 = nLimit;
        if ( fMode == -1 || fMode == 1 ) // both or pos
            pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit );
        pFuncs[i] = Cudd_Not( pFuncs[i] );
        if ( fMode == -1 || fMode == 0 ) // both or neg
            pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 );
        pFuncs[i] = Cudd_Not( pFuncs[i] );
        if ( !pF1 && !pF0 )
            break;
        if ( !pF0 )                  pGuide[i] = 1, Count = Count1; // use pos
        else if ( !pF1 )             pGuide[i] = 0, Count = Count0; // use neg
        else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos
        else                         pGuide[i] = 0, Count = Count0; // use neg
        CounterAll += Count;
        //printf( "Output %5d has %5d cubes (%d)  (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 );
    }
    dd->maxLive = saveLimit;
    st__free_table( table );
    return i == nFuncs ? CounterAll : -1;
}   /* end of Extra_bddCountCubes */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddCreateAnd()

DdNode * Extra_bddCreateAnd ( DdManager * dd, int nVars )

extern

Function********************************************************************

Synopsis [Creates AND composed of the first nVars of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 858 of file extraBddMisc.c.

{
    DdNode * bFunc, * bTemp;
    int i;
    bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc );
    for ( i = 0; i < nVars; i++ )
    {
        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bFunc );
    return bFunc;
}

Here is the caller graph for this function:

Extra_bddCreateExor()

DdNode * Extra_bddCreateExor ( DdManager * dd, int nVars )

extern

Function********************************************************************

Synopsis [Creates EXOR composed of the first nVars of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 908 of file extraBddMisc.c.

{
    DdNode * bFunc, * bTemp;
    int i;
    bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
    for ( i = 0; i < nVars; i++ )
    {
        bFunc = Cudd_bddXor( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bFunc );
    return bFunc;
}

Here is the caller graph for this function:

Extra_bddCreateOr()

DdNode * Extra_bddCreateOr ( DdManager * dd, int nVars )

extern

Function********************************************************************

Synopsis [Creates OR composed of the first nVars of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 883 of file extraBddMisc.c.

{
    DdNode * bFunc, * bTemp;
    int i;
    bFunc = Cudd_ReadLogicZero(dd); Cudd_Ref( bFunc );
    for ( i = 0; i < nVars; i++ )
    {
        bFunc = Cudd_bddOr( dd, bTemp = bFunc, Cudd_bddIthVar(dd,i) );  Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Cudd_Deref( bFunc );
    return bFunc;
}

Here is the caller graph for this function:

Extra_bddEncodingBinary()

DdNode * Extra_bddEncodingBinary ( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars )

extern

AutomaticEnd Function********************************************************************

Synopsis [Performs the binary encoding of the set of function using the given vars.]

Description [Performs a straight binary encoding of the set of functions using the variable cubes formed from the given set of variables. ]

SideEffects []

SeeAlso []

Definition at line 138 of file extraBddCas.c.

{
    int i;
    DdNode * bResult;
    DdNode * bCube, * bTemp, * bProd;
 
    assert( nVars >= Abc_Base2Log(nFuncs) );
 
    bResult = b0;   Cudd_Ref( bResult );
    for ( i = 0; i < nFuncs; i++ )
    {
        bCube   = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );   Cudd_Ref( bCube );
        bProd   = Cudd_bddAnd( dd, bCube, pbFuncs[i] );         Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bCube );
 
        bResult = Cudd_bddOr( dd, bProd, bTemp = bResult );     Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }
 
    Cudd_Deref( bResult );
    return bResult;
} /* end of Extra_bddEncodingBinary */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddEncodingNonStrict()

DdNode * Extra_bddEncodingNonStrict ( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple )

extern

Function********************************************************************

Synopsis [Solves the column encoding problem using a sophisticated method.]

Description [The encoding is based on the idea of deriving functions which depend on only one variable, which corresponds to the case of non-disjoint decompostion. It is assumed that the variables pCVars are ordered below the variables representing the solumns, and the first variable pCVars[0] is the topmost one.]

SideEffects []

SeeAlso [Extra_bddEncodingBinary]

Definition at line 184 of file extraBddCas.c.

{
    DdNode * bEncoded, * bResult;
    int nVarsCol = Cudd_SupportSize(dd,bVarsCol);
    abctime clk;
 
    // cannot work with more that 32-bit codes
    assert( nMulti < 32 );
 
    // perform the preliminary encoding using the straight binary code
    bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti );   Cudd_Ref( bEncoded );
    //printf( "Node count = %d", Cudd_DagSize(bEncoded) );
 
    // set the backgroup value for counting minterms
    s_Terminal = b0;
    // set the level of the encoding variables
    s_EncodingVarsLevel = dd->invperm[pCVars[0]->index];
 
    // the current number of backtracks
    s_BackTracks = 0;
    // the variables that are cofactored on the topmost level where everything starts (no vars)
    s_Field[0][0] = b1;   
    // the size of the best set of "simple" encoding variables found so far
    s_nVarsBest   = 0;
 
    // set the relation to be accessible to traversal procedures
    s_Encoded = bEncoded;
    // the set of all vars to be accessible to traversal procedures
    s_VarAll  = bVarsCol;
    // the column multiplicity
    s_MultiStart  = nMulti;
 
 
    clk = Abc_Clock();
    // find the simplest encoding
    if ( nColumns > 2 )
    EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 );
//  printf( "The number of backtracks = %d\n", s_BackTracks );
//  s_EncSearchTime += Abc_Clock() - clk;
 
    // allocate the temporary storage for the columns
    s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) );
 
//  clk = Abc_Clock();
    bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
//  s_EncComputeTime += Abc_Clock() - clk;
    
    // delocate the preliminarily encoded set
    Cudd_RecursiveDeref( dd, bEncoded );
//  Cudd_RecursiveDeref( dd, aEncoded );
 
    ABC_FREE( s_pbTemp );
 
    *pSimple = s_nVarsBest;
    Cudd_Deref( bResult );
    return bResult;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddFindOneCube()

DdNode * Extra_bddFindOneCube ( DdManager * dd, DdNode * bF )

extern

Function********************************************************************

Synopsis [Find any cube belonging to the on-set of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 605 of file extraBddMisc.c.

{
    char * s_Temp;
    DdNode * bCube, * bTemp;
    int v;
 
    // get the vector of variables in the cube
    s_Temp = ABC_ALLOC( char, dd->size );
    Cudd_bddPickOneCube( dd, bF, s_Temp );
 
    // start the cube
    bCube = b1; Cudd_Ref( bCube );
    for ( v = 0; v < dd->size; v++ )
        if ( s_Temp[v] == 0 )
        {
//          Cube &= !s_XVars[v];
            bCube = Cudd_bddAnd( dd, bTemp = bCube, Cudd_Not(dd->vars[v]) ); Cudd_Ref( bCube );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        else if ( s_Temp[v] == 1 )
        {
//          Cube &=  s_XVars[v];
            bCube = Cudd_bddAnd( dd, bTemp = bCube,          dd->vars[v]  ); Cudd_Ref( bCube );
            Cudd_RecursiveDeref( dd, bTemp );
        }
    Cudd_Deref(bCube);
    ABC_FREE( s_Temp );
    return bCube;
}

Here is the caller graph for this function:

Extra_bddGetOneCube()

DdNode * Extra_bddGetOneCube ( DdManager * dd, DdNode * bFunc )

extern

Function********************************************************************

Synopsis [Returns one cube contained in the given BDD.]

Description [This function returns the cube with the smallest bits-to-integer value.]

SideEffects []

Definition at line 645 of file extraBddMisc.c.

{
    DdNode * bFuncR, * bFunc0, * bFunc1;
    DdNode * bRes0,  * bRes1,  * bRes;
 
    bFuncR = Cudd_Regular(bFunc);
    if ( cuddIsConstant(bFuncR) )
        return bFunc;
 
    // cofactor
    if ( Cudd_IsComplement(bFunc) )
    {
        bFunc0 = Cudd_Not( cuddE(bFuncR) );
        bFunc1 = Cudd_Not( cuddT(bFuncR) );
    }
    else
    {
        bFunc0 = cuddE(bFuncR);
        bFunc1 = cuddT(bFuncR);
    }
 
    // try to find the cube with the negative literal
    bRes0 = Extra_bddGetOneCube( dd, bFunc0 );  Cudd_Ref( bRes0 );
 
    if ( bRes0 != b0 )
    {
        bRes = Cudd_bddAnd( dd, bRes0, Cudd_Not(dd->vars[bFuncR->index]) ); Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bRes0 );
    }
    else
    {
        Cudd_RecursiveDeref( dd, bRes0 );
        // try to find the cube with the positive literal
        bRes1 = Extra_bddGetOneCube( dd, bFunc1 );  Cudd_Ref( bRes1 );
        assert( bRes1 != b0 );
        bRes = Cudd_bddAnd( dd, bRes1, dd->vars[bFuncR->index] ); Cudd_Ref( bRes );
        Cudd_RecursiveDeref( dd, bRes1 );
    }
 
    Cudd_Deref( bRes );
    return bRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddImageCompute()

DdNode * Extra_bddImageCompute ( Extra_ImageTree_t * pTree, DdNode * bCare )

extern

Function*************************************************************

Synopsis [Compute the image.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file extraBddImage.c.

{
    DdManager * dd = pTree->pCare->dd;
    DdNode * bSupp, * bRem;
 
    pTree->nIter++;
 
    // make sure the supports are okay
    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
    if ( bSupp != pTree->bCareSupp )
    {
        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
        if ( bRem != b1 )
        {
printf( "Original care set support: " );
ABC_PRB( dd, pTree->bCareSupp );
printf( "Current care set support: " );
ABC_PRB( dd, bSupp );
            Cudd_RecursiveDeref( dd, bSupp );
            Cudd_RecursiveDeref( dd, bRem );
            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
            return NULL;
        }
        Cudd_RecursiveDeref( dd, bRem );
    }
    Cudd_RecursiveDeref( dd, bSupp );
 
    // remove the previous image
    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
 
    // compute the image
    pTree->nNodesMax = 0;
    Extra_bddImageCompute_rec( pTree, pTree->pRoot );
    if ( pTree->nNodesMaxT < pTree->nNodesMax )
        pTree->nNodesMaxT = pTree->nNodesMax;
 
//    if ( pTree->fVerbose )
//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
    return pTree->pRoot->bImage;
}

Extra_bddImageCompute2()

DdNode * Extra_bddImageCompute2 ( Extra_ImageTree2_t * pTree, DdNode * bCare )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file extraBddImage.c.

{
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
    Cudd_Ref( pTree->bImage );
    return pTree->bImage;
}

Here is the caller graph for this function:

Extra_bddImageRead()

DdNode * Extra_bddImageRead ( Extra_ImageTree_t * pTree )

extern

Function*************************************************************

Synopsis [Reads the image from the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file extraBddImage.c.

{
    return pTree->pRoot->bImage;
}

Extra_bddImageRead2()

DdNode * Extra_bddImageRead2 ( Extra_ImageTree2_t * pTree )

extern

Function*************************************************************

Synopsis [Returns the previously computed image.]

Description []

SideEffects []

SeeAlso []

Definition at line 1150 of file extraBddImage.c.

{
    return pTree->bImage;
}

Extra_bddImageStart()

Extra_ImageTree_t * Extra_bddImageStart ( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars, int fVerbose )

extern

AutomaticEnd Function*************************************************************

Synopsis [Starts the image computation using tree-based scheduling.]

Description [This procedure starts the image computation. It uses the given care set to test-run the image computation and creates the quantification tree by scheduling variable quantifications. The tree can be used to compute images for other care sets without rescheduling. In this case, Extra_bddImageCompute() should be called.]

SideEffects []

SeeAlso []

Definition at line 156 of file extraBddImage.c.

{
    Extra_ImageTree_t * pTree;
    Extra_ImagePart_t ** pParts;
    Extra_ImageVar_t ** pVars;
    Extra_ImageNode_t ** pNodes;
    int v;
 
    if ( fVerbose && dd->size <= 80 )
        Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
 
    // create variables, partitions and leaf nodes
    pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
    pVars  = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
    pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
    
    // create the tree
    pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
    memset( pTree, 0, sizeof(Extra_ImageTree_t) );
    pTree->pCare = pNodes[nParts];
    pTree->fVerbose = fVerbose;
 
    // process the nodes
    while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
 
    // make sure the variables are gone
    for ( v = 0; v < dd->size; v++ )
        assert( pVars[v] == NULL );
    ABC_FREE( pVars );
 
    // merge the topmost nodes
    while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
 
    // make sure the nodes are gone
    for ( v = 0; v < nParts + 1; v++ )
        assert( pNodes[v] == NULL );
    ABC_FREE( pNodes );
 
//    if ( fVerbose )
//        Extra_bddImagePrintTree( pTree );
 
    // set the support of the care set
    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
 
    // clean the partitions
    Extra_DeleteParts_rec( pTree->pRoot );
    ABC_FREE( pParts );
    return pTree;
}

Here is the call graph for this function:

Extra_bddImageStart2()

Extra_ImageTree2_t * Extra_bddImageStart2 ( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, int nVars, DdNode ** pbVars, int fVerbose )

extern

Function*************************************************************

Synopsis [Starts the monolithic image computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1066 of file extraBddImage.c.

{
    Extra_ImageTree2_t * pTree;
    DdNode * bCubeAll, * bCubeNot, * bTemp;
    int i;
 
    pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
    pTree->dd = dd;
    pTree->bImage = NULL;
 
    bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
    bCubeNot = Extra_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
    Cudd_RecursiveDeref( dd, bCubeAll );
    Cudd_RecursiveDeref( dd, bCubeNot );
 
    // derive the monolithic relation
    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
    for ( i = 0; i < nParts; i++ )
    {
        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
        Cudd_RecursiveDeref( dd, bTemp );
    }
    Extra_bddImageCompute2( pTree, bCare );
    return pTree;
}

Here is the call graph for this function:

Extra_bddImageTreeDelete()

void Extra_bddImageTreeDelete ( Extra_ImageTree_t * pTree )

extern

Function*************************************************************

Synopsis [Delete the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file extraBddImage.c.

{
    if ( pTree->bCareSupp )
        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
    Extra_bddImageTreeDelete_rec( pTree->pRoot );
    ABC_FREE( pTree );
}

Extra_bddImageTreeDelete2()

void Extra_bddImageTreeDelete2 ( Extra_ImageTree2_t * pTree )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1128 of file extraBddImage.c.

{
    if ( pTree->bRel )
        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
    if ( pTree->bCube )
        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
    if ( pTree->bImage )
        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
    ABC_FREE( pTree );
}

Extra_bddIsVar()

int Extra_bddIsVar ( DdNode * bFunc )

extern

Function********************************************************************

Synopsis [Returns 1 if the BDD is the BDD of elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file extraBddMisc.c.

{
    bFunc = Cudd_Regular( bFunc );
    if ( cuddIsConstant(bFunc) )
        return 0;
    return cuddIsConstant( cuddT(bFunc) ) && cuddIsConstant( Cudd_Regular(cuddE(bFunc)) );
}

Extra_bddMove()

DdNode * Extra_bddMove ( DdManager * dd, DdNode * bF, int nVars )

extern

Function********************************************************************

Synopsis [Moves the BDD by the given number of variables up or down.]

Description []

SideEffects []

SeeAlso [Extra_bddShift]

Definition at line 187 of file extraBddMisc.c.

{
    DdNode * res;
    DdNode * bVars;
    if ( nVars == 0 )
        return bF;
    if ( Cudd_IsConstant(bF) )
        return bF;
    assert( nVars <= dd->size );
    if ( nVars > 0 )
        bVars = dd->vars[nVars];
    else
        bVars = Cudd_Not(dd->vars[-nVars]);
 
    do {
        dd->reordered = 0;
        res = extraBddMove( dd, bF, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_bddMove */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddNodePathsUnderCut()

st__table * Extra_bddNodePathsUnderCut ( DdManager * dd, DdNode * bFunc, int CutLevel )

extern

Function********************************************************************

Synopsis [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.]

Description [The table returned contains the set of BDD nodes pointed to under the cut and, for each node, the BDD of the sum of paths leading to this node from the root The sums of paths in the table are referenced. CutLevel is the first DD level considered to be under the cut.]

SideEffects []

SeeAlso [Extra_bddNodePaths]

Definition at line 263 of file extraBddCas.c.

{
    st__table * Visited;  // temporary table to remember the visited nodes
    st__table * CutNodes; // the result goes here
    st__table * Result; // the result goes here
    DdNode * aFunc;
 
    s_CutLevel = CutLevel;
 
    Result  = st__init_table( st__ptrcmp, st__ptrhash);;
    // the terminal cases
    if ( Cudd_IsConstant( bFunc ) )
    {
        if ( bFunc == b1 )
        {
            st__insert( Result, (char*)b1, (char*)b1 );
            Cudd_Ref( b1 );
            Cudd_Ref( b1 );
        }
        else
        {
            st__insert( Result, (char*)b0, (char*)b0 );
            Cudd_Ref( b0 );
            Cudd_Ref( b0 );
        }
        return Result;
    }
 
    // create the ADD to simplify processing (no complemented edges)
    aFunc = Cudd_BddToAdd( dd, bFunc );   Cudd_Ref( aFunc );
 
    // Step 1: Start the tables and collect information about the nodes above the cut 
    // this information tells how many edges point to each node
    Visited  = st__init_table( st__ptrcmp, st__ptrhash);;
    CutNodes = st__init_table( st__ptrcmp, st__ptrhash);;
 
    CountNodeVisits_rec( dd, aFunc, Visited );
 
    // Step 2: Traverse the BDD using the visited table and compute the sum of paths
    CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes );
 
    // at this point the table of cut nodes is ready and the table of visited is useless
    {
        st__generator * gen;
        DdNode * aNode;
        traventry * p;
        st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p )
        {
            Cudd_RecursiveDeref( dd, p->bSum );
            ABC_FREE( p );
        }
        st__free_table( Visited );
    }
 
    // go through the table CutNodes and create the BDD and the path to be returned
    {
        st__generator * gen;
        DdNode * aNode, * bNode, * bSum;
        st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum)
        {
            // aNode is not referenced, because aFunc is holding it
            bNode = Cudd_addBddPattern( dd, aNode );  Cudd_Ref( bNode ); 
            st__insert( Result, (char*)bNode, (char*)bSum );
            // the new table takes both refs
        }
        st__free_table( CutNodes );
    }
 
    // dereference the ADD
    Cudd_RecursiveDeref( dd, aFunc );
 
    // return the table
    return Result;
 
} /* end of Extra_bddNodePathsUnderCut */

Here is the call graph for this function:

Extra_bddNodePathsUnderCutArray()

int Extra_bddNodePathsUnderCutArray ( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel )

extern

Function********************************************************************

Synopsis [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.]

Description [Takes the array, paNodes, of ADD nodes to start the traversal, the array, pbCubes, of BDD cubes to start the traversal with in each node, and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes. Returns the number of columns found. Fills in paNodesRes (pbCubesRes) with the set of ADD columns (BDD paths). These arrays should be allocated by the user.]

SideEffects []

SeeAlso [Extra_bddNodePaths]

Definition at line 355 of file extraBddCas.c.

{
    st__table * Visited;  // temporary table to remember the visited nodes
    st__table * CutNodes; // the nodes under the cut go here
    int i, Counter;
 
    s_CutLevel = CutLevel;
 
    // there should be some nodes
    assert( nNodes > 0 );
    if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) )
    {
        if ( paNodes[0] == a1 )
        {
            paNodesRes[0] = a1;          Cudd_Ref( a1 );
            pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
        }
        else
        {
            paNodesRes[0] = a0;          Cudd_Ref( a0 );
            pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
        }
        return 1;
    }
 
    // Step 1: Start the table and collect information about the nodes above the cut 
    // this information tells how many edges point to each node
    CutNodes = st__init_table( st__ptrcmp, st__ptrhash);;
    Visited  = st__init_table( st__ptrcmp, st__ptrhash);;
 
    for ( i = 0; i < nNodes; i++ )
        CountNodeVisits_rec( dd, paNodes[i], Visited );
 
    // Step 2: Traverse the BDD using the visited table and compute the sum of paths
    for ( i = 0; i < nNodes; i++ )
        CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes );
 
    // at this point, the table of cut nodes is ready and the table of visited is useless
    {
        st__generator * gen;
        DdNode * aNode;
        traventry * p;
        st__foreach_item( Visited, gen, (const char**)&aNode, (char**)&p )
        {
            Cudd_RecursiveDeref( dd, p->bSum );
            ABC_FREE( p );
        }
        st__free_table( Visited );
    }
 
    // go through the table CutNodes and create the BDD and the path to be returned
    {
        st__generator * gen;
        DdNode * aNode, * bSum;
        Counter = 0;
        st__foreach_item( CutNodes, gen, (const char**)&aNode, (char**)&bSum)
        {
            paNodesRes[Counter] = aNode;   Cudd_Ref( aNode ); 
            pbCubesRes[Counter] = bSum;
            Counter++;
        }
        st__free_table( CutNodes );
    }
 
    // return the number of cofactors found
    return Counter;
 
} /* end of Extra_bddNodePathsUnderCutArray */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddPermuteArray()

void Extra_bddPermuteArray ( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int * permut )

extern

Function********************************************************************

Synopsis [Permutes the variables of the array of BDDs.]

Description [Given a permutation in array permut, creates a new BDD with permuted variables. There should be an entry in array permut for each variable in the manager. The i-th entry of permut holds the index of the variable that is to substitute the i-th variable. The DDs in the resulting array are already referenced.]

SideEffects [None]

SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]

Definition at line 961 of file extraBddMisc.c.

{
    DdHashTable *table;
    int i, k;
    do
    {
        manager->reordered = 0;
        table = cuddHashTableInit( manager, 1, 2 );
 
        /* permute the output functions one-by-one */
        for ( i = 0; i < nNodes; i++ )
        {
            bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut );
            if ( bNodesOut[i] == NULL )
            {
                /* deref the array of the already computed outputs */
                for ( k = 0; k < i; k++ )
                    Cudd_RecursiveDeref( manager, bNodesOut[k] );
                break;
            }
            cuddRef( bNodesOut[i] );
        }
        /* Dispose of local cache. */
        cuddHashTableQuit( table );
    }
    while ( manager->reordered == 1 );
}    /* end of Extra_bddPermuteArray */

Here is the caller graph for this function:

Extra_bddPrint()

void Extra_bddPrint ( DdManager * dd, DdNode * F )

extern

Function********************************************************************

Synopsis [Outputs the BDD in a readable format.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 246 of file extraBddMisc.c.

{
    DdGen * Gen;
    int * Cube;
    CUDD_VALUE_TYPE Value;
    int nVars = dd->size;
    int fFirstCube = 1;
    int i;
 
    if ( F == NULL )
    {
        printf("NULL");
        return;
    }
    if ( F == b0 )
    {
        printf("Constant 0");
        return;
    }
    if ( F == b1 )
    {
        printf("Constant 1");
        return;
    }
 
    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
    {
        if ( fFirstCube )
            fFirstCube = 0;
        else
//          Output << " + ";
            printf( " + " );
 
        for ( i = 0; i < nVars; i++ )
            if ( Cube[i] == 0 )
                printf( "[%d]'", i );
//              printf( "%c'", (char)('a'+i) );
            else if ( Cube[i] == 1 )
                printf( "[%d]", i );
//              printf( "%c", (char)('a'+i) );
    }
 
//  printf("\n");
}

Here is the caller graph for this function:

Extra_bddPrintSupport()

void Extra_bddPrintSupport ( DdManager * dd, DdNode * F )

extern

Function********************************************************************

Synopsis [Outputs the BDD in a readable format.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 302 of file extraBddMisc.c.

{
    DdNode * bSupp;
    bSupp = Cudd_Support( dd, F );   Cudd_Ref( bSupp );
    Extra_bddPrint( dd, bSupp );
    Cudd_RecursiveDeref( dd, bSupp );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddReduceVarSet()

DdNode * Extra_bddReduceVarSet ( DdManager * dd, DdNode * bVars, DdNode * bF )

extern

Function********************************************************************

Synopsis [Filters the set of variables using the support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file extraBddSymm.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraBddReduceVarSet( dd, bVars, bF );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_bddReduceVarSet */

Here is the call graph for this function:

Extra_bddRemapUp()

DdNode * Extra_bddRemapUp ( DdManager * dd, DdNode * bF )

extern

Function********************************************************************

Synopsis [Remaps the function to depend on the topmost variables on the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file extraBddMisc.c.

{
    int * pPermute;
    DdNode * bSupp, * bTemp, * bRes;
    int Counter;
 
    pPermute = ABC_ALLOC( int, dd->size );
 
    // get support
    bSupp = Cudd_Support( dd, bF );    Cudd_Ref( bSupp );
 
    // create the variable map
    // to remap the DD into the upper part of the manager
    Counter = 0;
    for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
        pPermute[bTemp->index] = dd->invperm[Counter++];
 
    // transfer the BDD and remap it
    bRes = Cudd_bddPermute( dd, bF, pPermute );  Cudd_Ref( bRes );
 
    // remove support
    Cudd_RecursiveDeref( dd, bSupp );
 
    // return
    Cudd_Deref( bRes );
    ABC_FREE( pPermute );
    return bRes;
}

Here is the caller graph for this function:

Extra_bddSpaceCanonVars()

DdNode * Extra_bddSpaceCanonVars ( DdManager * dd, DdNode * bSpace )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceCanonVars( dd, bSpace );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceEquations()

DdNode * Extra_bddSpaceEquations ( DdManager * dd, DdNode * bSpace )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 361 of file extraBddAuto.c.

{
    DdNode * zRes;
    DdNode * zEquPos;
    DdNode * zEquNeg;
    zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace );  Cudd_Ref( zEquPos );
    zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace );  Cudd_Ref( zEquNeg );
    zRes    = Cudd_zddUnion( dd, zEquPos, zEquNeg );     Cudd_Ref( zRes );
    Cudd_RecursiveDerefZdd( dd, zEquPos );
    Cudd_RecursiveDerefZdd( dd, zEquNeg );
    Cudd_Deref( zRes );
    return zRes;
}

Here is the call graph for this function:

Extra_bddSpaceEquationsNeg()

DdNode * Extra_bddSpaceEquationsNeg ( DdManager * dd, DdNode * bSpace )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file extraBddAuto.c.

{
    DdNode * zRes;
    do {
        dd->reordered = 0;
        zRes = extraBddSpaceEquationsNeg( dd, bSpace );
    } while (dd->reordered == 1);
    return zRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddSpaceEquationsPos()

DdNode * Extra_bddSpaceEquationsPos ( DdManager * dd, DdNode * bSpace )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file extraBddAuto.c.

{
    DdNode * zRes;
    do {
        dd->reordered = 0;
        zRes = extraBddSpaceEquationsPos( dd, bSpace );
    } while (dd->reordered == 1);
    return zRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddSpaceExorGates()

DdNode ** Extra_bddSpaceExorGates ( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )

extern

Function*************************************************************

Synopsis []

Description [Returns the array of ZDDs with the number equal to the number of vars in the DD manager. If the given var is non-canonical, this array contains the referenced ZDD representing literals in the corresponding EXOR equation.]

SideEffects []

SeeAlso []

Definition at line 497 of file extraBddAuto.c.

{
    DdNode ** pzRes;
    int * pVarsNonCan;
    DdNode * zEquRem;
    int iVarNonCan;
    DdNode * zExor, * zTemp;
 
    // get the set of non-canonical variables
    pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
    Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
 
    // allocate storage for the EXOR sets
    pzRes = ABC_ALLOC( DdNode *, dd->size );
    memset( pzRes, 0, sizeof(DdNode *) * dd->size );
 
    // go through all the equations
    zEquRem = zEquations;  Cudd_Ref( zEquRem );
    while ( zEquRem != z0 )
    {
        // extract one product
        zExor = Extra_zddSelectOneSubset( dd, zEquRem );   Cudd_Ref( zExor );
        // remove it from the set
        zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor );  Cudd_Ref( zEquRem );
        Cudd_RecursiveDerefZdd( dd, zTemp );
 
        // locate the non-canonical variable
        iVarNonCan = -1;
        for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) )
        {
            if ( pVarsNonCan[zTemp->index/2] == 1 )
            {
                assert( iVarNonCan == -1 );
                iVarNonCan = zTemp->index/2;
            }
        }
        assert( iVarNonCan != -1 );
 
        if ( Extra_zddLitCountComb( dd, zExor ) > 1 )
            pzRes[ iVarNonCan ] = zExor; // takes ref
        else
            Cudd_RecursiveDerefZdd( dd, zExor );
    }
    Cudd_RecursiveDerefZdd( dd, zEquRem );
 
    ABC_FREE( pVarsNonCan );
    return pzRes;
}

Here is the call graph for this function:

Extra_bddSpaceFromFunction()

DdNode * Extra_bddSpaceFromFunction ( DdManager * dd, DdNode * bF, DdNode * bG )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunction( dd, bF, bG );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceFromFunctionFast()

DdNode * Extra_bddSpaceFromFunctionFast ( DdManager * dd, DdNode * bFunc )

extern

CFile****************************************************************

FileName [extraBddAuto.c]

PackageName [extra]

Synopsis [Computation of autosymmetries.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id

extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp

] AutomaticStart AutomaticEnd Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file extraBddAuto.c.

{
    int * pSupport;
    int * pPermute;
    int * pPermuteBack;
    DdNode ** pCompose;
    DdNode * bCube, * bTemp;
    DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift;
    int nSupp, Counter;
    int i, lev;
 
    // get the support
    pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
    Extra_SupportArray( dd, bFunc, pSupport );
    nSupp = 0;
    for ( i = 0; i < dd->size; i++ )
        if ( pSupport[i] )
            nSupp++;
 
    // make sure the manager has enough variables
    if ( 2*nSupp > dd->size )
    {
        printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
        fflush( stdout );
        ABC_FREE( pSupport );
        return NULL;
    }
 
    // create the permutation arrays
    pPermute     = ABC_ALLOC( int, dd->size );
    pPermuteBack = ABC_ALLOC( int, dd->size );
    pCompose     = ABC_ALLOC( DdNode *, dd->size );
    for ( i = 0; i < dd->size; i++ )
    {
        pPermute[i]     = i;
        pPermuteBack[i] = i;
        pCompose[i]     = dd->vars[i];   Cudd_Ref( pCompose[i] );
    }
 
    // remap the function in such a way that the variables are interleaved
    Counter = 0;
    bCube = b1;  Cudd_Ref( bCube );
    for ( lev = 0; lev < dd->size; lev++ )
        if ( pSupport[ dd->invperm[lev] ] )
        {   // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter;
            pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter];
            // var from level 2*Counter+1 should go back to the place of this var
            pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev];
            // the permutation should be defined in such a way that variable
            // on level 2*Counter is replaced by an EXOR of itself and var on the next level
            Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] );
            pCompose[ dd->invperm[2*Counter] ] = 
                Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] );  
            Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] );
            // add this variable to the cube
            bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] );  Cudd_Ref( bCube );
            Cudd_RecursiveDeref( dd, bTemp );
            // increment the counter
            Counter ++;
        }
 
    // permute the functions
    bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute );         Cudd_Ref( bFunc1 );
    // compose to gate the function depending on both vars
    bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose );  Cudd_Ref( bFunc2 );
    // gate the vector space
    // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] )
    bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube );  Cudd_Ref( bSpaceShift );
    bSpaceShift = Cudd_Not( bSpaceShift );
    // permute the space back into the original mapping
    bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace );
    Cudd_RecursiveDeref( dd, bFunc1 );
    Cudd_RecursiveDeref( dd, bFunc2 );
    Cudd_RecursiveDeref( dd, bSpaceShift );
    Cudd_RecursiveDeref( dd, bCube );
 
    for ( i = 0; i < dd->size; i++ )
        Cudd_RecursiveDeref( dd, pCompose[i] );
    ABC_FREE( pPermute );
    ABC_FREE( pPermuteBack );
    ABC_FREE( pCompose );
    ABC_FREE( pSupport );
 
    Cudd_Deref( bSpace );
    return bSpace;
}

Here is the call graph for this function:

Extra_bddSpaceFromFunctionNeg()

DdNode * Extra_bddSpaceFromFunctionNeg ( DdManager * dd, DdNode * bFunc )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunctionNeg( dd, bFunc );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceFromFunctionPos()

DdNode * Extra_bddSpaceFromFunctionPos ( DdManager * dd, DdNode * bFunc )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromFunctionPos( dd, bFunc );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceFromMatrixNeg()

DdNode * Extra_bddSpaceFromMatrixNeg ( DdManager * dd, DdNode * zA )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromMatrixNeg( dd, zA );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceFromMatrixPos()

DdNode * Extra_bddSpaceFromMatrixPos ( DdManager * dd, DdNode * zA )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file extraBddAuto.c.

{
    DdNode * bRes;
    do {
        dd->reordered = 0;
        bRes = extraBddSpaceFromMatrixPos( dd, zA );
    } while (dd->reordered == 1);
    return bRes;
}

Here is the call graph for this function:

Extra_bddSpaceReduce()

DdNode * Extra_bddSpaceReduce ( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file extraBddAuto.c.

{
    DdNode * bNegCube;
    DdNode * bResult;
    bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars );  Cudd_Ref( bNegCube );
    bResult  = Cudd_Cofactor( dd, bFunc, bNegCube );            Cudd_Ref( bResult );
    Cudd_RecursiveDeref( dd, bNegCube );
    Cudd_Deref( bResult );
    return bResult;
}

Here is the call graph for this function:

Extra_bddSuppCheckContainment()

int Extra_bddSuppCheckContainment ( DdManager * dd, DdNode * bL, DdNode * bH, DdNode ** bLarge, DdNode ** bSmall )

extern

Function********************************************************************

Synopsis [Checks the support containment.]

Description [This function returns 1 if one support is contained in another. In this case, bLarge (bSmall) is assigned to point to the larger (smaller) support. If the supports are identical, return 0 and does not assign the supports!]

SideEffects []

SeeAlso []

Definition at line 443 of file extraBddMisc.c.

{
    DdNode * bSL = bL;
    DdNode * bSH = bH;
    int fLcontainsH = 1;
    int fHcontainsL = 1;
    int TopVar;
    
    if ( bSL == bSH )
        return 0;
 
    while ( bSL != b1 || bSH != b1 )
    {
        if ( bSL == b1 )
        { // Low component has no vars; High components has some vars
            fLcontainsH = 0;
            if ( fHcontainsL == 0 )
                return 0;
            else
                break;
        }
 
        if ( bSH == b1 )
        { // similarly
            fHcontainsL = 0;
            if ( fLcontainsH == 0 )
                return 0;
            else
                break;
        }
 
        // determine the topmost var of the supports by comparing their levels
        if ( dd->perm[bSL->index] < dd->perm[bSH->index] )
            TopVar = bSL->index;
        else
            TopVar = bSH->index;
 
        if ( TopVar == bSL->index && TopVar == bSH->index ) 
        { // they are on the same level
            // it does not tell us anything about their containment
            // skip this var
            bSL = cuddT(bSL);
            bSH = cuddT(bSH);
        }
        else if ( TopVar == bSL->index ) // and TopVar != bSH->index
        { // Low components is higher and contains more vars
            // it is not possible that High component contains Low
            fHcontainsL = 0;
            // skip this var
            bSL = cuddT(bSL);
        }
        else // if ( TopVar == bSH->index ) // and TopVar != bSL->index
        { // similarly
            fLcontainsH = 0;
            // skip this var
            bSH = cuddT(bSH);
        }
 
        // check the stopping condition
        if ( !fHcontainsL && !fLcontainsH )
            return 0;
    }
    // only one of them can be true at the same time
    assert( !fHcontainsL || !fLcontainsH );
    if ( fHcontainsL )
    {
        *bLarge = bH;
        *bSmall = bL;
    }
    else // fLcontainsH
    {
        *bLarge = bL;
        *bSmall = bH;
    }
    return 1;
}

Extra_bddSuppContainVar()

int Extra_bddSuppContainVar ( DdManager * dd, DdNode * bS, DdNode * bVar )

extern

Function********************************************************************

Synopsis [Returns 1 if the support contains the given BDD variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file extraBddMisc.c.

{ 
    for( ; bS != b1; bS = cuddT(bS) )
        if ( bS->index == bVar->index )
            return 1;
    return 0;
}

Extra_bddSuppDifferentVars()

int Extra_bddSuppDifferentVars ( DdManager * dd, DdNode * S1, DdNode * S2, int DiffMax )

extern

Function********************************************************************

Synopsis [Returns the number of different vars in two supports.]

Description [Counts the number of variables that appear in one support and does not appear in other support. If the number exceeds DiffMax, returns DiffMax.]

SideEffects []

SeeAlso []

Definition at line 393 of file extraBddMisc.c.

{
    int Result = 0;
    while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
    {
        // if the top vars are the same, this var is the same
        if ( S1->index == S2->index )
        {
            S1 = cuddT(S1);
            S2 = cuddT(S2);
            continue;
        }
        // the top var is different
        Result++;
 
        if ( Result >= DiffMax )
            return DiffMax;
 
        // if the top vars are different, skip the one, which is higher
        if ( dd->perm[S1->index] < dd->perm[S2->index] )
            S1 = cuddT(S1);
        else
            S2 = cuddT(S2);
    }
 
    // consider the remaining variables
    if ( S1->index != CUDD_CONST_INDEX )
        Result += Extra_bddSuppSize(dd,S1);
    else if ( S2->index != CUDD_CONST_INDEX )
        Result += Extra_bddSuppSize(dd,S2);
 
    if ( Result >= DiffMax )
        return DiffMax;
    return Result;
}

Here is the call graph for this function:

Extra_bddSupportNegativeCube()

DdNode * Extra_bddSupportNegativeCube ( DdManager * dd, DdNode * f )

extern

Function********************************************************************

Synopsis [Finds the support as a negative polarity cube.]

Description [Finds the variables on which a DD depends. Returns a BDD consisting of the product of the variables in the negative polarity if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_VectorSupport Cudd_Support]

Definition at line 764 of file extraBddMisc.c.

{
    int *support;
    DdNode *res, *tmp, *var;
    int i, j;
    int size;
 
    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax( dd->size, dd->sizeZ );
    support = ABC_ALLOC( int, size );
    if ( support == NULL )
    {
        dd->errorCode = CUDD_MEMORY_OUT;
        return ( NULL );
    }
    for ( i = 0; i < size; i++ )
    {
        support[i] = 0;
    }
 
    /* Compute support and clean up markers. */
    ddSupportStep2( Cudd_Regular( f ), support );
    ddClearFlag2( Cudd_Regular( f ) );
 
    /* Transform support from array to cube. */
    do
    {
        dd->reordered = 0;
        res = DD_ONE( dd );
        cuddRef( res );
        for ( j = size - 1; j >= 0; j-- )
        {                        /* for each level bottom-up */
            i = ( j >= dd->size ) ? j : dd->invperm[j];
            if ( support[i] == 1 )
            {
                var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) );
                var = Cudd_Not(var);
                cuddRef( var );
                tmp = cuddBddAndRecur( dd, res, var );
                if ( tmp == NULL )
                {
                    Cudd_RecursiveDeref( dd, res );
                    Cudd_RecursiveDeref( dd, var );
                    res = NULL;
                    break;
                }
                cuddRef( tmp );
                Cudd_RecursiveDeref( dd, res );
                Cudd_RecursiveDeref( dd, var );
                res = tmp;
            }
        }
    }
    while ( dd->reordered == 1 );
 
    ABC_FREE( support );
    if ( res != NULL )
        cuddDeref( res );
    return ( res );
 
}                                /* end of Extra_SupportNeg */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_bddSuppOverlapping()

int Extra_bddSuppOverlapping ( DdManager * dd, DdNode * S1, DdNode * S2 )

extern

Function********************************************************************

Synopsis [Returns 1 if two supports represented as BDD cubes are overlapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file extraBddMisc.c.

{
    while ( S1->index != CUDD_CONST_INDEX && S2->index != CUDD_CONST_INDEX )
    {
        // if the top vars are the same, they intersect
        if ( S1->index == S2->index )
            return 1;
        // if the top vars are different, skip the one, which is higher
        if ( dd->perm[S1->index] < dd->perm[S2->index] )
            S1 = cuddT(S1);
        else
            S2 = cuddT(S2);
    }
    return 0;
}

Extra_bddSuppSize()

int Extra_bddSuppSize ( DdManager * dd, DdNode * bSupp )

extern

Function********************************************************************

Synopsis [Returns the size of the support.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file extraBddMisc.c.

{
    int Counter = 0;
    while ( bSupp != b1 )
    {
        assert( !Cudd_IsComplement(bSupp) );
        assert( cuddE(bSupp) == b0 );
 
        bSupp = cuddT(bSupp);
        Counter++;
    }
    return Counter;
}

Here is the caller graph for this function:

Extra_bddTuples()

DdNode * Extra_bddTuples ( DdManager * dd, int K, DdNode * VarsN )

extern

Function********************************************************************

Synopsis [Builds BDD representing the set of fixed-size variable tuples.]

Description [Creates BDD of all combinations of variables in Support that have k vars in them.]

SideEffects []

SeeAlso []

Definition at line 2691 of file extraBddMisc.c.

{
    DdNode  *res;
    int     autoDyn;
 
    /* it is important that reordering does not happen, 
       otherwise, this methods will not work */
 
    autoDyn = dd->autoDyn;
    dd->autoDyn = 0;
 
    do {
        /* transform the numeric arguments (K) into a DdNode * argument;
         * this allows us to use the standard internal CUDD cache */
        DdNode *VarSet = VarsN, *VarsK = VarsN;
        int     nVars = 0, i;
 
        /* determine the number of variables in VarSet */
        while ( VarSet != b1 )
        {
            nVars++;
            /* make sure that the VarSet is a cube */
            if ( cuddE( VarSet ) != b0 )
                return NULL;
            VarSet = cuddT( VarSet );
        }
        /* make sure that the number of variables in VarSet is less or equal 
           that the number of variables that should be present in the tuples
        */
        if ( K > nVars )
            return NULL;
 
        /* the second argument in the recursive call stands for <n>;
         * create the first argument, which stands for <k> 
         * as when we are talking about the tuple of <k> out of <n> */
        for ( i = 0; i < nVars-K; i++ )
            VarsK = cuddT( VarsK );
 
        dd->reordered = 0;
        res = extraBddTuples(dd, VarsK, VarsN );
 
    } while (dd->reordered == 1);
    dd->autoDyn = autoDyn;
    return(res);
 
} /* end of Extra_bddTuples */

Here is the call graph for this function:

Extra_bddVarIsInCube()

int Extra_bddVarIsInCube ( DdNode * bCube, int iVar )

extern

Function*************************************************************

Synopsis [Checks if the given variable belongs to the cube.]

Description [Return -1 if the var does not appear in the cube. Otherwise, returns polarity (0 or 1) of the var in the cube.]

SideEffects []

SeeAlso []

Definition at line 1056 of file extraBddMisc.c.

{
    DdNode * bCube0, * bCube1;
    while ( Cudd_Regular(bCube)->index != CUDD_CONST_INDEX )
    {
        bCube0 = Cudd_NotCond( cuddE(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
        bCube1 = Cudd_NotCond( cuddT(Cudd_Regular(bCube)), Cudd_IsComplement(bCube) );
        // make sure it is a cube
        assert( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) || // bCube0 == 0
                (Cudd_IsComplement(bCube1) && Cudd_Regular(bCube1)->index == CUDD_CONST_INDEX) ); // bCube1 == 0
        // quit if it is the last one
        if ( Cudd_Regular(bCube)->index == iVar )
            return (int)(Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX);
        // get the next cube
        if ( (Cudd_IsComplement(bCube0) && Cudd_Regular(bCube0)->index == CUDD_CONST_INDEX) )
            bCube = bCube1;
        else
            bCube = bCube0;
    }
    return -1;
}

Extra_PrintKMap()

void Extra_PrintKMap ( FILE * Output, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames )

extern

AutomaticEnd Function********************************************************************

Synopsis [Prints the K-map of the function.]

Description [If the pointer to the array of variables XVars is NULL, fSuppType determines how the support will be determined. fSuppType == 0 – takes the first nVars of the manager fSuppType == 1 – takes the topmost nVars of the manager fSuppType == 2 – determines support from the on-set and the offset ]

SideEffects []

SeeAlso []

Definition at line 201 of file extraBddKmap.c.

{
    int fPrintTruth = 1;
    int d, p, n, s, v, h, w;
    int nVarsVer;
    int nVarsHor;
    int nCellsVer;
    int nCellsHor;
    int nSkipSpaces;
 
    // make sure that on-set and off-set do not overlap
    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
    {
        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
        return;
    }
    if ( nVars == 0 )
        { printf( "Function is constant %d.\n", !Cudd_IsComplement(OnSet) ); return; }
 
    // print truth table for debugging
    if ( fPrintTruth )
    {
        DdNode * bCube, * bPart;
        printf( "Truth table: " );
        if ( nVars == 0 )
            printf( "Constant" );
        else if ( nVars == 1 )
            printf( "1-var function" );
        else
        {
//            printf( "0x" );
            for ( d = (1<<(nVars-2)) - 1; d >= 0; d-- )
            {
                int Value = 0;
                for ( s = 0; s < 4; s++ )
                {
                    bCube = Extra_bddBitsToCube( dd, 4*d+s, nVars, dd->vars, 0 );   Cudd_Ref( bCube );
                    bPart = Cudd_Cofactor( dd, OnSet, bCube );                      Cudd_Ref( bPart );
                    Value |= ((int)(bPart == b1) << s);
                    Cudd_RecursiveDeref( dd, bPart );
                    Cudd_RecursiveDeref( dd, bCube );
                }
                if ( Value < 10 )
                    fprintf( stdout, "%d", Value );
                else
                    fprintf( stdout, "%c", 'a' + Value-10 );
            }
        }
        printf( "\n" );
    }
 
 
/*
    if ( OnSet == b1 )
    {
        fprintf( Output, "PrintKMap(): Constant 1\n" );
        return;
    }
    if ( OffSet == b1 )
    {
        fprintf( Output, "PrintKMap(): Constant 0\n" );
        return;
    }
*/
    if ( nVars < 0 || nVars > MAXVARS )
    {
        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
        return;
    }
 
    // determine the support if it is not given
    if ( XVars == NULL )
    {
        if ( fSuppType == 0 )
        {   // assume that the support includes the first nVars of the manager
            assert( nVars );
            for ( v = 0; v < nVars; v++ )
                s_XVars[v] = Cudd_bddIthVar( dd, v );
        }
        else if ( fSuppType == 1 )
        {   // assume that the support includes the topmost nVars of the manager
            assert( nVars );
            for ( v = 0; v < nVars; v++ )
                s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
        }
        else // determine the support
        {
            DdNode * SuppOn, * SuppOff, * Supp;
            int cVars = 0;
            DdNode * TempSupp;
 
            // determine support
            SuppOn = Cudd_Support( dd, OnSet );         Cudd_Ref( SuppOn );
            SuppOff = Cudd_Support( dd, OffSet );       Cudd_Ref( SuppOff );
            Supp = Cudd_bddAnd( dd, SuppOn, SuppOff );  Cudd_Ref( Supp );
            Cudd_RecursiveDeref( dd, SuppOn );
            Cudd_RecursiveDeref( dd, SuppOff );
 
            nVars = Cudd_SupportSize( dd, Supp );
            if ( nVars > MAXVARS )
            {
                fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
                Cudd_RecursiveDeref( dd, Supp );
                return;
            }
 
            // assign variables
            for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
                s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );
 
            Cudd_RecursiveDeref( dd, TempSupp );
        }
    }
    else
    {
        // copy variables
        assert( XVars );
        for ( v = 0; v < nVars; v++ )
            s_XVars[v] = XVars[v];
    }

    // determine the Karnaugh map parameters
    nVarsVer = nVars/2;
    nVarsHor = nVars - nVarsVer;
 
    nCellsVer = (1<<nVarsVer);
    nCellsHor = (1<<nVarsHor);
    nSkipSpaces = nVarsVer + 1;

    // print variable names
    fprintf( Output, "\n" );
    for ( w = 0; w < nVarsVer; w++ )
        if ( pVarNames == NULL )
            fprintf( Output, "%c", 'a'+nVarsHor+w );
        else
            fprintf( Output, " %s", pVarNames[nVarsHor+w] );
 
    if ( fHorizontalVarNamesPrintedAbove )
    {
        fprintf( Output, " \\ " );
        for ( w = 0; w < nVarsHor; w++ )
            if ( pVarNames == NULL )
                fprintf( Output, "%c", 'a'+w );
            else
                fprintf( Output, "%s ", pVarNames[w] );
    }
    fprintf( Output, "\n" );
 
    if ( fHorizontalVarNamesPrintedAbove )
    {
        // print horizontal digits
        for ( d = 0; d < nVarsHor; d++ )
        {
            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
            for ( n = 0; n < nCellsHor; n++ )
                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
                    fprintf( Output, "1   " );
                else
                    fprintf( Output, "0   " );
            fprintf( Output, "\n" );
        }
    }

    // print the upper line
    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
    for ( s = 0; s < nCellsHor; s++ )
    {
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        if ( s != nCellsHor-1 )
        {
            if ( s&1 )
                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
            else
                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
        }
    }
    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
    fprintf( Output, "\n" );

    // print the map
    for ( v = 0; v < nCellsVer; v++ )
    {
        DdNode * CubeVerBDD;
 
        // print horizontal digits
//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
        for ( n = 0; n < nVarsVer; n++ )
            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
                fprintf( Output, "1" );
            else
                fprintf( Output, "0" );
        fprintf( Output, " " );
 
        // find vertical cube
        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 );    Cudd_Ref( CubeVerBDD );
 
        // print text line
        fprintf( Output, "%c", DOUBLE_VERTICAL );
        for ( h = 0; h < nCellsHor; h++ )
        {
            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
 
            fprintf( Output, " " );
//          fprintf( Output, "x" );
            // determine what should be printed
            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 );    Cudd_Ref( CubeHorBDD );
            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                   Cudd_Ref( Prod );
            Cudd_RecursiveDeref( dd, CubeHorBDD );
 
            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
            Cudd_RecursiveDeref( dd, Prod );
 
#ifdef WIN32
            {
            HANDLE hConsole = GetStdHandle(STD_OUTPUT_HANDLE);
            char Symb = 0, Color = 0;
            if ( ValueOnSet == b1 && ValueOffSet == b0 )
                Symb = SYMBOL_ONE,     Color = 14;  // yellow
            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
                Symb = SYMBOL_ZERO,    Color = 11;  // blue
            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
                Symb = SYMBOL_DC,      Color = 10;  // green
            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
                Symb = SYMBOL_OVERLAP, Color = 12;  // red
            else
                assert(0);
            SetConsoleTextAttribute( hConsole, Color );
            fprintf( Output, "%c", Symb );
            SetConsoleTextAttribute( hConsole, 7 );
            }
#else
            {
            if ( ValueOnSet == b1 && ValueOffSet == b0 )
                fprintf( Output, "%c", SYMBOL_ONE );
            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
                fprintf( Output, "%c", SYMBOL_ZERO );
            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
                fprintf( Output, "%c", SYMBOL_DC );
            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
                fprintf( Output, "%c", SYMBOL_OVERLAP );
            else
                assert(0);
            }
#endif
 
            Cudd_RecursiveDeref( dd, ValueOnSet );
            Cudd_RecursiveDeref( dd, ValueOffSet );
            fprintf( Output, " " );
 
            if ( h != nCellsHor-1 )
            {
                if ( h&1 )
                    fprintf( Output, "%c", DOUBLE_VERTICAL );
                else
                    fprintf( Output, "%c", SINGLE_VERTICAL );
            }
        }
        fprintf( Output, "%c", DOUBLE_VERTICAL );
        fprintf( Output, "\n" );
 
        Cudd_RecursiveDeref( dd, CubeVerBDD );
 
        if ( v != nCellsVer-1 )
        // print separator line
        {
            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
            if ( v&1 )
            {
                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
                for ( s = 0; s < nCellsHor; s++ )
                {
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    if ( s != nCellsHor-1 )
                    {
                        if ( s&1 )
                            fprintf( Output, "%c", DOUBLES_CROSS );
                        else
                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
                    }
                }
                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
            }
            else
            {
                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
                for ( s = 0; s < nCellsHor; s++ )
                {
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    if ( s != nCellsHor-1 )
                    {
                        if ( s&1 )
                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
                        else
                            fprintf( Output, "%c", SINGLES_CROSS );
                    }
                }
                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
            }
            fprintf( Output, "\n" );
        }
    }
    
    // print the lower line
    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
    for ( s = 0; s < nCellsHor; s++ )
    {
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        if ( s != nCellsHor-1 )
        {
            if ( s&1 )
                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
            else
                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
        }
    }
    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
    fprintf( Output, "\n" );
 
    if ( !fHorizontalVarNamesPrintedAbove )
    {
        // print horizontal digits
        for ( d = 0; d < nVarsHor; d++ )
        {
            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
            for ( n = 0; n < nCellsHor; n++ )
                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
                    fprintf( Output, "1   " );
                else
                    fprintf( Output, "0   " );

            fprintf( Output, "%c", (char)('a'+d) );
            fprintf( Output, "\n" );
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_PrintKMapRelation()

void Extra_PrintKMapRelation ( FILE * Output, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars )

extern

Function********************************************************************

Synopsis [Prints the K-map of the relation.]

Description [Assumes that the relation depends the first nXVars of XVars and the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.]

SideEffects []

SeeAlso []

Definition at line 581 of file extraBddKmap.c.

{
    int d, p, n, s, v, h, w;
    int nVars;
    int nVarsVer;
    int nVarsHor;
    int nCellsVer;
    int nCellsHor;
    int nSkipSpaces;
 
    // make sure that on-set and off-set do not overlap
    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
    {
        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
        return;
    }
 
    if ( OnSet == b1 )
    {
        fprintf( Output, "PrintKMap(): Constant 1\n" );
        return;
    }
    if ( OffSet == b1 )
    {
        fprintf( Output, "PrintKMap(): Constant 0\n" );
        return;
    }
 
    nVars = nXVars + nYVars;
    if ( nVars < 0 || nVars > MAXVARS )
    {
        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
        return;
    }
 

    // determine the Karnaugh map parameters
    nVarsVer = nXVars;
    nVarsHor = nYVars;
    nCellsVer = (1<<nVarsVer);
    nCellsHor = (1<<nVarsHor);
    nSkipSpaces = nVarsVer + 1;

    // print variable names
    fprintf( Output, "\n" );
    for ( w = 0; w < nVarsVer; w++ )
        fprintf( Output, "%c", 'a'+nVarsHor+w );
    if ( fHorizontalVarNamesPrintedAbove )
    {
        fprintf( Output, " \\ " );
        for ( w = 0; w < nVarsHor; w++ )
            fprintf( Output, "%c", 'a'+w );
    }
    fprintf( Output, "\n" );
 
    if ( fHorizontalVarNamesPrintedAbove )
    {
        // print horizontal digits
        for ( d = 0; d < nVarsHor; d++ )
        {
            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
            for ( n = 0; n < nCellsHor; n++ )
                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
                    fprintf( Output, "1   " );
                else
                    fprintf( Output, "0   " );
            fprintf( Output, "\n" );
        }
    }

    // print the upper line
    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
    for ( s = 0; s < nCellsHor; s++ )
    {
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        if ( s != nCellsHor-1 )
        {
            if ( s&1 )
                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
            else
                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
        }
    }
    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
    fprintf( Output, "\n" );

    // print the map
    for ( v = 0; v < nCellsVer; v++ )
    {
        DdNode * CubeVerBDD;
 
        // print horizontal digits
//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
        for ( n = 0; n < nVarsVer; n++ )
            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
                fprintf( Output, "1" );
            else
                fprintf( Output, "0" );
        fprintf( Output, " " );
 
        // find vertical cube
//      CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor );    Cudd_Ref( CubeVerBDD );
        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 );                 Cudd_Ref( CubeVerBDD );
 
        // print text line
        fprintf( Output, "%c", DOUBLE_VERTICAL );
        for ( h = 0; h < nCellsHor; h++ )
        {
            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
 
            fprintf( Output, " " );
//          fprintf( Output, "x" );
            // determine what should be printed
//          CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars );    Cudd_Ref( CubeHorBDD );
            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 );        Cudd_Ref( CubeHorBDD );
            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                           Cudd_Ref( Prod );
            Cudd_RecursiveDeref( dd, CubeHorBDD );
 
            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
            Cudd_RecursiveDeref( dd, Prod );
 
            if ( ValueOnSet == b1 && ValueOffSet == b0 )
                fprintf( Output, "%c", SYMBOL_ONE );
            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
                fprintf( Output, "%c", SYMBOL_ZERO );
            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
                fprintf( Output, "%c", SYMBOL_DC );
            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
                fprintf( Output, "%c", SYMBOL_OVERLAP );
            else
                assert(0);
 
            Cudd_RecursiveDeref( dd, ValueOnSet );
            Cudd_RecursiveDeref( dd, ValueOffSet );
            fprintf( Output, " " );
 
            if ( h != nCellsHor-1 )
            {
                if ( h&1 )
                    fprintf( Output, "%c", DOUBLE_VERTICAL );
                else
                    fprintf( Output, "%c", SINGLE_VERTICAL );
            }
        }
        fprintf( Output, "%c", DOUBLE_VERTICAL );
        fprintf( Output, "\n" );
 
        Cudd_RecursiveDeref( dd, CubeVerBDD );
 
        if ( v != nCellsVer-1 )
        // print separator line
        {
            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
            if ( v&1 )
            {
                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
                for ( s = 0; s < nCellsHor; s++ )
                {
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
                    if ( s != nCellsHor-1 )
                    {
                        if ( s&1 )
                            fprintf( Output, "%c", DOUBLES_CROSS );
                        else
                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
                    }
                }
                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
            }
            else
            {
                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
                for ( s = 0; s < nCellsHor; s++ )
                {
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
                    if ( s != nCellsHor-1 )
                    {
                        if ( s&1 )
                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
                        else
                            fprintf( Output, "%c", SINGLES_CROSS );
                    }
                }
                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
            }
            fprintf( Output, "\n" );
        }
    }
    
    // print the lower line
    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
    for ( s = 0; s < nCellsHor; s++ )
    {
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
        if ( s != nCellsHor-1 )
        {
            if ( s&1 )
                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
            else
                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
        }
    }
    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
    fprintf( Output, "\n" );
 
    if ( !fHorizontalVarNamesPrintedAbove )
    {
        // print horizontal digits
        for ( d = 0; d < nVarsHor; d++ )
        {
            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
            for ( n = 0; n < nCellsHor; n++ )
                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
                    fprintf( Output, "1   " );
                else
                    fprintf( Output, "0   " );

            fprintf( Output, "%c", (char)('a'+d) );
            fprintf( Output, "\n" );
        }
    }
}

Here is the call graph for this function:

Extra_ProfileWidth()

int Extra_ProfileWidth ( DdManager * dd, DdNode * Func, int * pProfile, int CutLevel )

extern

Function*************************************************************

Synopsis [Fast computation of the BDD profile.]

Description [The array to store the profile is given by the user and should contain at least as many entries as there is the maximum of the BDD/ZDD size of the manager PLUS ONE. When we say that the widths of the DD on level L is W, we mean the following. Let us create the cut between the level L-1 and the level L and count the number of different DD nodes pointed to across the cut. This number is the width W. From this it follows the on level 0, the width is equal to the number of external pointers to the considered DDs. If there is only one DD, then the profile on level 0 is always 1. If this DD is rooted in the topmost variable, then the width on level 1 is always 2, etc. The width at the level equal to dd->size is the number of terminal nodes in the DD. (Because we consider the first level #0 and the last level #dd->size, the profile array should contain dd->size+1 entries.) ]

SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs]

SeeAlso []

Definition at line 519 of file extraBddCas.c.

{
    st__generator * gen;
    st__table * tNodeTopRef; // this table stores the top level from which this node is pointed to
    st__table * tNodes;
    DdNode * node;
    DdNode * nodeR;
    int LevelStart, Limit;
    int i, size;
    int WidthMax;
  
    // start the mapping table
    tNodeTopRef = st__init_table( st__ptrcmp, st__ptrhash);;
    // add the topmost node to the profile
    extraProfileUpdateTopLevel( tNodeTopRef, 0, Func );
 
    // collect all nodes
    tNodes = Extra_CollectNodes( Func );
    // go though all the nodes and set the top level the cofactors are pointed from
//  Cudd_ForeachNode( dd, Func, genDD, node )
    st__foreach_item( tNodes, gen, (const char**)&node, NULL )
    {
//      assert( Cudd_Regular(node) );  // this procedure works only with ADD/ZDD (not BDD w/ compl.edges)
        nodeR = Cudd_Regular(node);
        if ( cuddIsConstant(nodeR) )
            continue;
        // this node is not a constant - consider its cofactors
        extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) );
        extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) );
    }
    st__free_table( tNodes );
 
    // clean the profile
    size = ddMax(dd->size, dd->sizeZ) + 1;
    for ( i = 0; i < size; i++ ) 
        pProfile[i] = 0;
 
    // create the profile
    st__foreach_item( tNodeTopRef, gen, (const char**)&node, (char**)&LevelStart )
    {
        nodeR = Cudd_Regular(node);
        Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index];
        for ( i = LevelStart; i <= Limit; i++ )
            pProfile[i]++;
    }
 
    if ( CutLevel != -1 && CutLevel != 0  )
        size = CutLevel;
 
    // get the max width
    WidthMax = 0;
    for ( i = 0; i < size; i++ ) 
        if ( WidthMax < pProfile[i] )
            WidthMax = pProfile[i];
 
    // deref the table
    st__free_table( tNodeTopRef );
 
    return WidthMax;
} /* end of Extra_ProfileWidth */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_StopManager()

void Extra_StopManager ( DdManager * dd )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file extraBddMisc.c.

{
    int RetValue;
    // check for remaining references in the package
    RetValue = Cudd_CheckZeroRef( dd );
    if ( RetValue > 10 )
//    if ( RetValue )
        printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
//  Cudd_PrintInfo( dd, stdout );
    Cudd_Quit( dd );
}

Here is the caller graph for this function:

Extra_SupportArray()

int * Extra_SupportArray ( DdManager * dd, DdNode * f, int * support )

extern

Function********************************************************************

Synopsis [Finds variables on which the DD depends and returns them as am array.]

Description [Finds the variables on which the DD depends. Returns an array with entries set to 1 for those variables that belong to the support; NULL otherwise. The array is allocated by the user and should have at least as many entries as the maximum number of variables in BDD and ZDD parts of the manager.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport]

Definition at line 537 of file extraBddMisc.c.

{
    int i, size;
 
    /* Initialize support array for ddSupportStep. */
    size = ddMax(dd->size, dd->sizeZ);
    for (i = 0; i < size; i++) 
        support[i] = 0;
    
    /* Compute support and clean up markers. */
    ddSupportStep2(Cudd_Regular(f),support);
    ddClearFlag2(Cudd_Regular(f));
 
    return(support);
 
} /* end of Extra_SupportArray */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_SymmPairsAllocate()

Extra_SymmInfo_t * Extra_SymmPairsAllocate ( int nVars )

extern

Function********************************************************************

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file extraBddSymm.c.

{
    int i;
    Extra_SymmInfo_t * p;
 
    // allocate and clean the storage for symmetry info
    p = ABC_ALLOC( Extra_SymmInfo_t, 1 );
    memset( p, 0, sizeof(Extra_SymmInfo_t) );
    p->nVars     = nVars;
    p->pVars     = ABC_ALLOC( int, nVars );  
    p->pSymms    = ABC_ALLOC( char *, nVars );  
    p->pSymms[0] = ABC_ALLOC( char  , nVars * nVars );
    memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) );
 
    for ( i = 1; i < nVars; i++ )
        p->pSymms[i] = p->pSymms[i-1] + nVars;
 
    return p;
} /* end of Extra_SymmPairsAllocate */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_SymmPairsCompute()

Extra_SymmInfo_t * Extra_SymmPairsCompute ( DdManager * dd, DdNode * bFunc )

extern

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes the classical symmetry information for the function.]

Description [Returns the symmetry information in the form of Extra_SymmInfo_t structure.]

SideEffects [If the ZDD variables are not derived from BDD variables with multiplicity 2, this function may derive them in a wrong way.]

SeeAlso []

Definition at line 73 of file extraBddSymm.c.

{
    DdNode * bSupp;
    DdNode * zRes;
    Extra_SymmInfo_t * p;
 
    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
    zRes  = Extra_zddSymmPairsCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );
 
    p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp );
 
    Cudd_RecursiveDeref( dd, bSupp );
    Cudd_RecursiveDerefZdd( dd, zRes );
 
    return p;
 
} /* end of Extra_SymmPairsCompute */

Here is the call graph for this function:

Extra_SymmPairsComputeNaive()

Extra_SymmInfo_t * Extra_SymmPairsComputeNaive ( DdManager * dd, DdNode * bFunc )

extern

Function********************************************************************

Synopsis [Computes the classical symmetry information for the function.]

Description [Uses the naive way of comparing cofactors.]

SideEffects []

SeeAlso []

Definition at line 396 of file extraBddSymm.c.

{
    DdNode * bSupp, * bTemp;
    int nSuppSize;
    Extra_SymmInfo_t * p;
    int i, k;
 
    // compute the support
    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
//printf( "Support = %d. ", nSuppSize );
//Extra_bddPrint( dd, bSupp );
//printf( "%d ", nSuppSize );
 
    // allocate the storage for symmetry info
    p = Extra_SymmPairsAllocate( nSuppSize );
 
    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
        p->pVars[i] = bTemp->index;
 
    // go through the candidate pairs and check using Idea1
    for ( i = 0; i < nSuppSize; i++ )
    for ( k = i+1; k < nSuppSize; k++ )
    {
        p->pSymms[k][i] = p->pSymms[i][k] = Extra_bddCheckVarsSymmetricNaive( dd, bFunc, p->pVars[i], p->pVars[k] );
        if ( p->pSymms[i][k] )
             p->nSymms++;
    }
 
    Cudd_RecursiveDeref( dd, bSupp );
    return p;
 
} /* end of Extra_SymmPairsComputeNaive */

Here is the call graph for this function:

Extra_SymmPairsCreateFromZdd()

Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd ( DdManager * dd, DdNode * zPairs, DdNode * bSupp )

extern

Function********************************************************************

Synopsis [Creates the symmetry information structure from ZDD.]

Description [ZDD representation of symmetries is the set of cubes, each of which has two variables in the positive polarity. These variables correspond to the symmetric variable pair.]

SideEffects []

SeeAlso []

Definition at line 288 of file extraBddSymm.c.

{
    int i;
    int nSuppSize;
    Extra_SymmInfo_t * p;
    int * pMapVars2Nums;
    DdNode * bTemp;
    DdNode * zSet, * zCube, * zTemp;
    int iVar1, iVar2;
 
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
 
    // allocate and clean the storage for symmetry info
    p = Extra_SymmPairsAllocate( nSuppSize );
 
    // allocate the storage for the temporary map
    pMapVars2Nums = ABC_ALLOC( int, dd->size );
    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
    // assign the variables
    p->nVarsMax = dd->size;
//  p->nNodes   = Cudd_DagSize( zPairs );
    p->nNodes   = 0;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        p->pVars[i] = bTemp->index;
        pMapVars2Nums[bTemp->index] = i;
    }
 
    // write the symmetry info into the structure
    zSet = zPairs;   Cudd_Ref( zSet );
    while ( zSet != z0 )
    {
        // get the next cube
        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );
 
        // add these two variables to the data structure
        assert( cuddT( cuddT(zCube) ) == z1 );
        iVar1 = zCube->index/2;
        iVar2 = cuddT(zCube)->index/2;
        if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] )
            p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1;
        else
            p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1;
        // count the symmetric pairs
        p->nSymms ++;
 
        // update the cuver and deref the cube
        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zCube );
 
    } // for each cube 
    Cudd_RecursiveDerefZdd( dd, zSet );
 
    ABC_FREE( pMapVars2Nums );
    return p;
 
} /* end of Extra_SymmPairsCreateFromZdd */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_SymmPairsDissolve()

void Extra_SymmPairsDissolve ( Extra_SymmInfo_t * p )

extern

Function********************************************************************

Synopsis [Deallocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file extraBddSymm.c.

{
    ABC_FREE( p->pVars );
    ABC_FREE( p->pSymms[0] );
    ABC_FREE( p->pSymms    );
    ABC_FREE( p );
} /* end of Extra_SymmPairsDissolve */

Extra_SymmPairsPrint()

void Extra_SymmPairsPrint ( Extra_SymmInfo_t * p )

extern

Function********************************************************************

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file extraBddSymm.c.

{
    int i, k;
    printf( "\n" );
    for ( i = 0; i < p->nVars; i++ )
    {
        for ( k = 0; k <= i; k++ )
            printf( " " );
        for ( k = i+1; k < p->nVars; k++ )
            if ( p->pSymms[i][k] )
                printf( "1" );
            else
                printf( "." );
        printf( "\n" );
    }
} /* end of Extra_SymmPairsPrint */

Extra_TransferLevelByLevel()

DdNode * Extra_TransferLevelByLevel ( DdManager * ddSource, DdManager * ddDestination, DdNode * f )

extern

Function********************************************************************

Synopsis [Transfers the BDD from one manager into another level by level.]

Description [Transfers the BDD from one manager into another while preserving the correspondence between variables level by level.]

SideEffects [None]

SeeAlso []

Definition at line 112 of file extraBddMisc.c.

{
    DdNode * bRes;
    int * pPermute;
    int nMin, nMax, i;
 
    nMin = ddMin(ddSource->size, ddDestination->size);
    nMax = ddMax(ddSource->size, ddDestination->size);
    pPermute = ABC_ALLOC( int, nMax );
    // set up the variable permutation
    for ( i = 0; i < nMin; i++ )
        pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i];
    if ( ddSource->size > ddDestination->size )
    {
        for (      ; i < nMax; i++ )
            pPermute[ ddSource->invperm[i] ] = -1;
    }
    bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute );
    ABC_FREE( pPermute );
    return bRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_TransferPermute()

DdNode * Extra_TransferPermute ( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute )

extern

AutomaticEnd Function********************************************************************

Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.]

Description [Convert a {A,B}DD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the {A,B}DD in the destination manager if successful; NULL otherwise. The i-th entry in the array Permute tells what is the index of the i-th variable from the old manager in the new manager.]

SideEffects [None]

SeeAlso []

Definition at line 87 of file extraBddMisc.c.

{
    DdNode * bRes;
    do
    {
        ddDestination->reordered = 0;
        bRes = extraTransferPermute( ddSource, ddDestination, f, Permute );
    }
    while ( ddDestination->reordered == 1 );
    return ( bRes );
 
}                               /* end of Extra_TransferPermute */

Here is the caller graph for this function:

Extra_TransferPermuteTime()

DdNode * Extra_TransferPermuteTime ( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute, int TimeOut )

extern

Function********************************************************************

Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.]

Description [Convert a {A,B}DD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the {A,B}DD in the destination manager if successful; NULL otherwise. The i-th entry in the array Permute tells what is the index of the i-th variable from the old manager in the new manager.]

SideEffects [None]

SeeAlso []

Definition at line 150 of file extraBddTime.c.

{
    DdNode * bRes;
    do
    {
        ddDestination->reordered = 0;
        bRes = extraTransferPermuteTime( ddSource, ddDestination, f, Permute, TimeOut );
    }
    while ( ddDestination->reordered == 1 );
    return ( bRes );
 
} /* end of Extra_TransferPermuteTime */

Extra_UnateComputeFast()

Extra_UnateInfo_t * Extra_UnateComputeFast ( DdManager * dd, DdNode * bFunc )

extern

CFile****************************************************************

FileName [extraBddUnate.c]

PackageName [extra]

Synopsis [Efficient methods to compute the information about unate variables using an algorithm that is conceptually similar to the algorithm for two-variable symmetry computation presented in: A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. Transactions on CAD, Nov. 2003.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id

extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp

] AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes the classical symmetry information for the function.]

Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.]

SideEffects [If the ZDD variables are not derived from BDD variables with multiplicity 2, this function may derive them in a wrong way.]

SeeAlso []

Definition at line 73 of file extraBddUnate.c.

{
    DdNode * bSupp;
    DdNode * zRes;
    Extra_UnateInfo_t * p;
 
    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
    zRes  = Extra_zddUnateInfoCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );
 
    p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp );
 
    Cudd_RecursiveDeref( dd, bSupp );
    Cudd_RecursiveDerefZdd( dd, zRes );
 
    return p;
 
} /* end of Extra_UnateInfoCompute */

Here is the call graph for this function:

Extra_UnateComputeSlow()

Extra_UnateInfo_t * Extra_UnateComputeSlow ( DdManager * dd, DdNode * bFunc )

extern

Function********************************************************************

Synopsis [Computes the classical unateness information for the function.]

Description [Uses the naive way of comparing cofactors.]

SideEffects []

SeeAlso []

Definition at line 293 of file extraBddUnate.c.

{
    int nSuppSize;
    DdNode * bSupp, * bTemp;
    Extra_UnateInfo_t * p;
    int i, Res;
 
    // compute the support
    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
//printf( "Support = %d. ", nSuppSize );
//Extra_bddPrint( dd, bSupp );
//printf( "%d ", nSuppSize );
 
    // allocate the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );
 
    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index );
        p->pVars[i].iVar = bTemp->index;
        if ( Res == -1 )
            p->pVars[i].Neg = 1;
        else if ( Res == 1 )
            p->pVars[i].Pos = 1;
        p->nUnate += (Res != 0);
    }
    Cudd_RecursiveDeref( dd, bSupp );
    return p;
 
} /* end of Extra_UnateComputeSlow */

Here is the call graph for this function:

Extra_UnateInfoAllocate()

Extra_UnateInfo_t * Extra_UnateInfoAllocate ( int nVars )

extern

Function********************************************************************

Synopsis [Allocates unateness information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file extraBddUnate.c.

{
    Extra_UnateInfo_t * p;
    // allocate and clean the storage for unateness info
    p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
    memset( p, 0, sizeof(Extra_UnateInfo_t) );
    p->nVars     = nVars;
    p->pVars     = ABC_ALLOC( Extra_UnateVar_t, nVars );  
    memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
    return p;
} /* end of Extra_UnateInfoAllocate */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_UnateInfoCreateFromZdd()

Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd ( DdManager * dd, DdNode * zPairs, DdNode * bSupp )

extern

Function********************************************************************

Synopsis [Creates the symmetry information structure from ZDD.]

Description [ZDD representation of symmetries is the set of cubes, each of which has two variables in the positive polarity. These variables correspond to the symmetric variable pair.]

SideEffects []

SeeAlso []

Definition at line 227 of file extraBddUnate.c.

{
    Extra_UnateInfo_t * p;
    DdNode * bTemp, * zSet, * zCube, * zTemp;
    int * pMapVars2Nums;
    int i, nSuppSize;
 
    nSuppSize = Extra_bddSuppSize( dd, bSupp );
 
    // allocate and clean the storage for symmetry info
    p = Extra_UnateInfoAllocate( nSuppSize );
 
    // allocate the storage for the temporary map
    pMapVars2Nums = ABC_ALLOC( int, dd->size );
    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
    // assign the variables
    p->nVarsMax = dd->size;
    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
    {
        p->pVars[i].iVar = bTemp->index;
        pMapVars2Nums[bTemp->index] = i;
    }
 
    // write the symmetry info into the structure
    zSet = zPairs;   Cudd_Ref( zSet );
//    Cudd_zddPrintCover( dd, zPairs );    printf( "\n" );
    while ( zSet != z0 )
    {
        // get the next cube
        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );
 
        // add this var to the data structure
        assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 );
        if ( zCube->index & 1 ) // neg
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1;
        else
            p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1;
        // count the unate vars
        p->nUnate++;
 
        // update the cuver and deref the cube
        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zCube );
 
    } // for each cube 
    Cudd_RecursiveDerefZdd( dd, zSet );
    ABC_FREE( pMapVars2Nums );
    return p;
 
} /* end of Extra_UnateInfoCreateFromZdd */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_UnateInfoDissolve()

void Extra_UnateInfoDissolve ( Extra_UnateInfo_t * p )

extern

Function********************************************************************

Synopsis [Deallocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file extraBddUnate.c.

{
    ABC_FREE( p->pVars );
    ABC_FREE( p );
} /* end of Extra_UnateInfoDissolve */

Extra_UnateInfoPrint()

void Extra_UnateInfoPrint ( Extra_UnateInfo_t * p )

extern

Function********************************************************************

Synopsis [Allocates symmetry information structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file extraBddUnate.c.

{
    char * pBuffer;
    int i;
    pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
    memset( pBuffer, ' ', (size_t)p->nVarsMax );
    pBuffer[p->nVarsMax] = 0;
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pVars[i].Neg )
            pBuffer[ p->pVars[i].iVar ] = 'n';
        else if ( p->pVars[i].Pos )
            pBuffer[ p->pVars[i].iVar ] = 'p';
        else
            pBuffer[ p->pVars[i].iVar ] = '.';
    printf( "%s\n", pBuffer );
    ABC_FREE( pBuffer );
} /* end of Extra_UnateInfoPrint */

Here is the call graph for this function:

Extra_VectorSupportArray()

int * Extra_VectorSupportArray ( DdManager * dd, DdNode ** F, int n, int * support )

extern

Function********************************************************************

Synopsis [Finds the variables on which a set of DDs depends.]

Description [Finds the variables on which a set of DDs depends. The set must contain either BDDs and ADDs, or ZDDs. Returns a BDD consisting of the product of the variables if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_Support Cudd_ClassifySupport]

Definition at line 572 of file extraBddMisc.c.

{
    int i, size;
 
    /* Allocate and initialize support array for ddSupportStep. */
    size = ddMax( dd->size, dd->sizeZ );
    for ( i = 0; i < size; i++ )
        support[i] = 0;
 
    /* Compute support and clean up markers. */
    for ( i = 0; i < n; i++ )
        ddSupportStep2( Cudd_Regular(F[i]), support );
    for ( i = 0; i < n; i++ )
        ddClearFlag2( Cudd_Regular(F[i]) );
 
    return support;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_zddCrossProduct()

DdNode * Extra_zddCrossProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Computes the cross product of two sets of subsets represented by ZDDs.]

Description [The cross product is defined as a set of pair-wise intersections of subsets belonging to the arguments.]

SideEffects []

SeeAlso [Extra_zddDotProduct]

Definition at line 236 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddCrossProduct(dd, S, T);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddCrossProduct */

Here is the call graph for this function:

Extra_zddDotProduct()

DdNode * Extra_zddDotProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Computes the dot product of two sets of subsets represented by ZDDs.]

Description [The dot product is defined as a set of pair-wise unions of subsets belonging to the arguments.]

SideEffects []

SeeAlso [Extra_zddCrossProduct]

Definition at line 208 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddDotProduct(dd, S, T);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddDotProduct */

Here is the call graph for this function:

Extra_zddDumpPla()

void Extra_zddDumpPla ( DdManager * dd, DdNode * F, int nVars, char * pFileName )

extern

Function*************************************************************

Synopsis [Writes ZDD into a PLA file.]

Description []

SideEffects []

SeeAlso []

Definition at line 2307 of file extraBddMisc.c.

{
    DdGen *gen;
    char * pCube;
    int * pPath, i;
    FILE * pFile = fopen( pFileName, "wb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
        return;
    }
    fprintf( pFile, "# PLA file dumped by Extra_zddDumpPla() in ABC\n" );
    fprintf( pFile, ".i %d\n", nVars );
    fprintf( pFile, ".o 1\n" );
    pCube = ABC_CALLOC( char, dd->sizeZ );
    Cudd_zddForeachPath( dd, F, gen, pPath )
    {
        for ( i = 0; i < nVars; i++ )
            pCube[i] = '-';
        for ( i = 0; i < nVars; i++ )
            if ( pPath[2*i] == 1 || pPath[2*i+1] == 1 )
                pCube[i] = '0' + (pPath[2*i] == 1);
        fprintf( pFile, "%s 1\n", pCube );           
    }
    fprintf( pFile, ".e\n\n" );
    fclose( pFile );
    ABC_FREE( pCube );
}

Extra_zddEmptyBelongs()

int Extra_zddEmptyBelongs ( DdManager * dd, DdNode * zS )

extern

Function********************************************************************

Synopsis [Returns 1 if ZDD contains the empty combination; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file extraBddSet.c.

{
    while ( zS->index != CUDD_MAXINDEX )
        zS = cuddE( zS );
    return (int)( zS == z1 );
 
} /* end of Extra_zddEmptyBelongs */

Here is the caller graph for this function:

Extra_zddGetSingletons()

DdNode * Extra_zddGetSingletons ( DdManager * dd, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Converts a set of variables into a set of singleton subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file extraBddSymm.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddGetSingletons( dd, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddGetSingletons */

Here is the call graph for this function:

Extra_zddGetSingletonsBoth()

DdNode * Extra_zddGetSingletonsBoth ( DdManager * dd, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Converts a set of variables into a set of singleton subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file extraBddUnate.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddGetSingletonsBoth( dd, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddGetSingletonsBoth */

Here is the call graph for this function:

Extra_zddGetSymmetricVars()

DdNode * Extra_zddGetSymmetricVars ( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Returns a singleton-set ZDD containing all variables that are symmetric with the given one.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file extraBddSymm.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddGetSymmetricVars( dd, bF, bG, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddGetSymmetricVars */

Here is the call graph for this function:

Extra_zddIsOneSubset()

int Extra_zddIsOneSubset ( DdManager * dd, DdNode * zS )

extern

Function********************************************************************

Synopsis [Returns 1 if the set is empty or consists of one subset only.]

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file extraBddSet.c.

{
    while ( zS->index != CUDD_MAXINDEX )
    {
        assert( cuddT(zS) != z0 );
        if ( cuddE(zS) != z0 )
            return 0;
        zS = cuddT( zS );
    }
    return (int)( zS == z1 );
 
} /* end of Extra_zddEmptyBelongs */

Extra_zddMaxDotProduct()

DdNode * Extra_zddMaxDotProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Computes the maximal of the DotProduct of the union of two sets represented by ZDDs.]

Description []

SideEffects []

SeeAlso [Extra_zddDotProduct Extra_zddMaximal Extra_zddMinCrossProduct]

Definition at line 263 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddMaxDotProduct(dd, S, T);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddMaxDotProduct */

Here is the call graph for this function:

Extra_zddMaximal()

DdNode * Extra_zddMaximal ( DdManager * dd, DdNode * S )

extern

CFile***********************************************************************

FileName [zMaxMin.c]

PackageName [extra]

Synopsis [Experimental version of some ZDD operators.]

Description [External procedures included in this module:

• Extra_zddMaximal();
• Extra_zddMinimal();
• Extra_zddMaxUnion();
• Extra_zddMinUnion();
• Extra_zddDotProduct();
• Extra_zddCrossProduct();
• Extra_zddMaxDotProduct();

Internal procedures included in this module:

• extraZddMaximal();
• extraZddMinimal();
• extraZddMaxUnion();
• extraZddMinUnion();
• extraZddDotProduct();
• extraZddCrossProduct();
• extraZddMaxDotProduct();

StaTc procedures included in this module:

DotProduct and MaxDotProduct were introduced by O.Coudert to solve problems arising in two-level planar routing See O. Coudert, C.-J. R. Shi. Exact Multi-Layer Topological Planar Routing. Proc. of IEEE Custom Integrated Circuit Conference '96, pp. 179-182. ]

SeeAlso []

Author [Alan Mishchenko]

Copyright []

ReviSon [$zMaxMin.c, v.1.2, November 26, 2000, alanmi $] AutomaTcStart AutomaTcEnd Function********************************************************************

Synopsis [Computes the maximal of a set represented by its ZDD.]

Description []

SideEffects []

SeeAlso [Extra_zddMinimal]

Definition at line 101 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddMaximal(dd, S);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddMaximal */

Here is the call graph for this function:

Extra_zddMaxNotSupSet()

DdNode * Extra_zddMaxNotSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Computes the maximal of subsets in X not contained in any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddSubSet, Extra_zddNotSupSet]

Definition at line 232 of file extraBddSet.c.

{
    DdNode  *res;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
    dd->reordered = 0;
    res = extraZddMaxNotSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);
 
} /* end of Extra_zddMaxNotSupSet */

Here is the call graph for this function:

Extra_zddMaxUnion()

DdNode * Extra_zddMaxUnion ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Computes the maximal of the union of two sets represented by ZDDs.]

Description []

SideEffects []

SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMinUnion]

Definition at line 153 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddMaxUnion(dd, S, T);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddMaxUnion */

Here is the call graph for this function:

Extra_zddMinimal()

DdNode * Extra_zddMinimal ( DdManager * dd, DdNode * S )

extern

Function********************************************************************

Synopsis [Computes the minimal of a set represented by its ZDD.]

Description []

SideEffects []

SeeAlso [Extra_zddMaximal]

Definition at line 127 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddMinimal(dd, S);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddMinimal */

Here is the call graph for this function:

Extra_zddMinUnion()

DdNode * Extra_zddMinUnion ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Computes the minimal of the union of two sets represented by ZDDs.]

Description []

SideEffects []

SeeAlso [Extra_zddMaximal Extra_zddMimimal Extra_zddMaxUnion]

Definition at line 180 of file extraBddMaxMin.c.

{
    DdNode  *res;
    do {
    dd->reordered = 0;
    res = extraZddMinUnion(dd, S, T);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddMinUnion */

Here is the call graph for this function:

Extra_zddNotSubSet()

DdNode * Extra_zddNotSubSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Computes subsets in X that are not contained in any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

Definition at line 165 of file extraBddSet.c.

{
    DdNode  *res;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
    dd->reordered = 0;
    res = extraZddNotSubSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);
 
} /* end of Extra_zddNotSubSet */

Here is the call graph for this function:

Extra_zddNotSupSet()

DdNode * Extra_zddNotSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Computes subsets in X that do not contain any of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddSupSet, Extra_zddNotSubSet]

Definition at line 198 of file extraBddSet.c.

{
    DdNode  *res;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
    dd->reordered = 0;
    res = extraZddNotSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);
 
} /* end of Extra_zddNotSupSet */

Here is the call graph for this function:

Extra_zddPrimes()

DdNode * Extra_zddPrimes ( DdManager * dd, DdNode * F )

extern

Function********************************************************************

Synopsis [Computes the set of primes as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 933 of file extraBddMisc.c.

{
    DdNode    *res;
    do {
        dd->reordered = 0;
        res = extraZddPrimes(dd, F);
        if ( dd->reordered == 1 )
            printf("\nReordering in Extra_zddPrimes()\n");
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddPrimes */

Extra_zddSelectOneSubset()

DdNode * Extra_zddSelectOneSubset ( DdManager * dd, DdNode * zS )

extern

Function********************************************************************

Synopsis [Selects one subset from the set of subsets represented by a ZDD.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 546 of file extraBddSymm.c.

{
    DdNode  *res;
    do {
        dd->reordered = 0;
        res = extraZddSelectOneSubset(dd, zS);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddSelectOneSubset */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_zddSubSet()

DdNode * Extra_zddSubSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

CFile***********************************************************************

FileName [zSubSet.c]

PackageName [extra]

Synopsis [Experimental version of some ZDD operators.]

Description [External procedures included in this module:

• Extra_zddSubSet();
• Extra_zddSupSet();
• Extra_zddNotSubSet();
• Extra_zddNotSupSet();
• Extra_zddMaxNotSupSet();
• Extra_zddEmptyBelongs();
• Extra_zddIsOneSubset();

Internal procedures included in this module:

• extraZddSubSet();
• extraZddSupSet();
• extraZddNotSubSet();
• extraZddNotSupSet();
• extraZddMaxNotSupSet();

Static procedures included in this module:

SubSet, SupSet, NotSubSet, NotSupSet were introduced by O.Coudert to solve problems arising in two-level SOP minimization. See O. Coudert, "Two-Level Logic Minimization: An Overview", Integration. Vol. 17, No. 2, pp. 97-140, Oct 1994. ]

SeeAlso []

Author [Alan Mishchenko]

Copyright []

Revision [$zSubSet.c, v.1.2, November 16, 2000, alanmi $] AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes subsets in X that are contained in some of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddNotSubSet, Extra_zddSupSet, Extra_zddNotSupSet]

Definition at line 100 of file extraBddSet.c.

{
    DdNode  *res;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
    dd->reordered = 0;
    res = extraZddSubSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);
 
} /* end of Extra_zddSubSet */

Here is the call graph for this function:

Extra_zddSupSet()

DdNode * Extra_zddSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Computes subsets in X that contain some of the subsets of Y.]

Description []

SideEffects []

SeeAlso [Extra_zddSubSet, Extra_zddNotSubSet, Extra_zddNotSupSet]

Definition at line 133 of file extraBddSet.c.

{
    DdNode  *res;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
    dd->reordered = 0;
    res = extraZddSupSet(dd, X, Y);
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return(res);
 
} /* end of Extra_zddSupSet */

Here is the call graph for this function:

Extra_zddSymmPairsCompute()

DdNode * Extra_zddSymmPairsCompute ( DdManager * dd, DdNode * bF, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Computes the classical symmetry information as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file extraBddSymm.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddSymmPairsCompute( dd, bF, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddSymmPairsCompute */

Here is the call graph for this function:

Here is the caller graph for this function:

Extra_zddTuplesFromBdd()

DdNode * Extra_zddTuplesFromBdd ( DdManager * dd, int K, DdNode * bVarsN )

extern

Function********************************************************************

Synopsis [Builds ZDD representing the set of fixed-size variable tuples.]

Description [Creates ZDD of all combinations of variables in Support that is represented by a BDD.]

SideEffects [New ZDD variables are created if indices of the variables present in the combination are larger than the currently allocated number of ZDD variables.]

SeeAlso []

Definition at line 488 of file extraBddSymm.c.

{
    DdNode  *zRes;
    int     autoDynZ;
 
    autoDynZ = dd->autoDynZ;
    dd->autoDynZ = 0;
 
    do {
        /* transform the numeric arguments (K) into a DdNode* argument;
         * this allows us to use the standard internal CUDD cache */
        DdNode *bVarSet = bVarsN, *bVarsK = bVarsN;
        int     nVars = 0, i;
 
        /* determine the number of variables in VarSet */
        while ( bVarSet != b1 )
        {
            nVars++;
            /* make sure that the VarSet is a cube */
            if ( cuddE( bVarSet ) != b0 )
                return NULL;
            bVarSet = cuddT( bVarSet );
        }
        /* make sure that the number of variables in VarSet is less or equal 
           that the number of variables that should be present in the tuples
        */
        if ( K > nVars )
            return NULL;
 
        /* the second argument in the recursive call stannds for <n>;
         * reate the first argument, which stands for <k>
         * as when we are talking about the tuple of <k> out of <n> */
        for ( i = 0; i < nVars-K; i++ )
            bVarsK = cuddT( bVarsK );
 
        dd->reordered = 0;
        zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN );
 
    } while (dd->reordered == 1);
    dd->autoDynZ = autoDynZ;
    return zRes;
 
} /* end of Extra_zddTuplesFromBdd */

Here is the call graph for this function:

Extra_zddUnateInfoCompute()

DdNode * Extra_zddUnateInfoCompute ( DdManager * dd, DdNode * bF, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Computes the classical symmetry information as a ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file extraBddUnate.c.

{
    DdNode * res;
    do {
        dd->reordered = 0;
        res = extraZddUnateInfoCompute( dd, bF, bVars );
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_zddUnateInfoCompute */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddChangePolarity()

DdNode * extraBddChangePolarity ( DdManager * dd, DdNode * bFunc, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().]

Description []

SideEffects []

SeeAlso []

Definition at line 2041 of file extraBddMisc.c.

{
    DdNode * bRes;
 
    if ( bVars == b1 )
        return bFunc;
    if ( Cudd_IsConstant(bFunc) )
        return bFunc;
 
    if ( (bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars)) )
        return bRes;
    else
    {
        DdNode * bFR = Cudd_Regular(bFunc); 
        int LevelF   = dd->perm[bFR->index];
        int LevelV   = dd->perm[bVars->index];
 
        if ( LevelV < LevelF )
            bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
        else // if ( LevelF <= LevelV )
        {
            DdNode * bRes0, * bRes1;             
            DdNode * bF0, * bF1;             
            DdNode * bVarsNext;
 
            // cofactor the functions
            if ( bFR != bFunc ) // bFunc is complemented 
            {
                bF0 = Cudd_Not( cuddE(bFR) );
                bF1 = Cudd_Not( cuddT(bFR) );
            }
            else
            {
                bF0 = cuddE(bFR);
                bF1 = cuddT(bFR);
            }
 
            if ( LevelF == LevelV )
                bVarsNext = cuddT(bVars);
            else
                bVarsNext = bVars;
 
            bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
            if ( bRes0 == NULL ) 
                return NULL;
            cuddRef( bRes0 );
 
            bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
            if ( bRes1 == NULL ) 
            {
                Cudd_RecursiveDeref( dd, bRes0 );
                return NULL;
            }
            cuddRef( bRes1 );
 
            if ( LevelF == LevelV )
            { // swap the cofactors
                DdNode * bTemp;
                bTemp = bRes0;
                bRes0 = bRes1;
                bRes1 = bTemp;
            }
 
            /* only aRes0 and aRes1 are referenced at this point */
 
            /* consider the case when Res0 and Res1 are the same node */
            if ( bRes0 == bRes1 )
                bRes = bRes1;
            /* consider the case when Res1 is complemented */
            else if ( Cudd_IsComplement(bRes1) ) 
            {
                bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
                if ( bRes == NULL ) 
                {
                    Cudd_RecursiveDeref(dd,bRes0);
                    Cudd_RecursiveDeref(dd,bRes1);
                    return NULL;
                }
                bRes = Cudd_Not(bRes);
            } 
            else 
            {
                bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
                if ( bRes == NULL ) 
                {
                    Cudd_RecursiveDeref(dd,bRes0);
                    Cudd_RecursiveDeref(dd,bRes1);
                    return NULL;
                }
            }
            cuddDeref( bRes0 );
            cuddDeref( bRes1 );
        }
            
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
        return bRes;
    }
} /* end of extraBddChangePolarity */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddCheckVarsSymmetric()

DdNode * extraBddCheckVarsSymmetric ( DdManager * dd, DdNode * bF, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_bddCheckVarsSymmetric().]

Description [Returns b0 if the variables are not symmetric. Returns b1 if the variables can be symmetric. The variables are represented in the form of a two-variable cube. In case the cube contains one variable (below Var1 level), the cube's pointer is complemented if the variable Var1 occurred on the current path; otherwise, the cube's pointer is regular. Uses additional complemented bit (Hash_Not) to mark the result if in the BDD rooted that this node there is a branch passing though the node labeled with Var2.]

SideEffects []

SeeAlso []

Definition at line 1169 of file extraBddSymm.c.

{
    DdNode * bRes;
 
    if ( bF == b0 )
        return b1;
 
    assert( bVars != b1 );
    
    if ( (bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars)) )
        return bRes;
    else
    {
        DdNode * bRes0, * bRes1;
        DdNode * bF0, * bF1;             
        DdNode * bFR = Cudd_Regular(bF);
        int LevelF = cuddI(dd,bFR->index);
 
        DdNode * bVarsR = Cudd_Regular(bVars);
        int fVar1Pres;
        int iLev1;
        int iLev2;
 
        if ( bVarsR != bVars ) // cube's pointer is complemented
        {
            assert( cuddT(bVarsR) == b1 );
            fVar1Pres = 1;                    // the first var is present on the path
            iLev1 = -1;                       // we are already below the first var level
            iLev2 = dd->perm[bVarsR->index];  // the level of the second var
        }
        else  // cube's pointer is NOT complemented
        {
            fVar1Pres = 0;                    // the first var is absent on the path
            if ( cuddT(bVars) == b1 )
            {
                iLev1 = -1;                             // we are already below the first var level 
                iLev2 = dd->perm[bVars->index];         // the level of the second var
            }
            else
            {
                assert( cuddT(cuddT(bVars)) == b1 );
                iLev1 = dd->perm[bVars->index];         // the level of the first var 
                iLev2 = dd->perm[cuddT(bVars)->index];  // the level of the second var
            }
        }
 
        // cofactor the function
        // the cofactors are needed only if we are above the second level
        if ( LevelF < iLev2 )
        {
            if ( bFR != bF ) // bFunc is complemented 
            {
                bF0 = Cudd_Not( cuddE(bFR) );
                bF1 = Cudd_Not( cuddT(bFR) );
            }
            else
            {
                bF0 = cuddE(bFR);
                bF1 = cuddT(bFR);
            }
        }
        else
            bF0 = bF1 = NULL;
 
        // consider five cases:
        // (1) F is above iLev1
        // (2) F is on the level iLev1
        // (3) F is between iLev1 and iLev2
        // (4) F is on the level iLev2
        // (5) F is below iLev2
 
        // (1) F is above iLev1
        if ( LevelF < iLev1 )
        {
            // the returned result cannot have the hash attribute
            // because we still did not reach the level of Var1;
            // the attribute never travels above the level of Var1
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
//          assert( !Hash_IsComplement( bRes0 ) );
            assert( bRes0 != z0 );
            if ( bRes0 == b0 )
                bRes = b0;
            else
                bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars );
//          assert( !Hash_IsComplement( bRes ) );
            assert( bRes != z0 );
        }
        // (2) F is on the level iLev1
        else if ( LevelF == iLev1 )
        {
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) );
            if ( bRes0 == b0 )
                bRes = b0;
            else
            {
                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) );
                if ( bRes1 == b0 )
                    bRes = b0;
                else
                {
//                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
                    if ( bRes0 == z0 || bRes1 == z0 )
                        bRes = b1;
                    else
                        bRes = b0;
                }
            }
        }
        // (3) F is between iLev1 and iLev2
        else if ( LevelF < iLev2 )
        {
            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
            if ( bRes0 == b0 )
                bRes = b0;
            else
            {
                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars );
                if ( bRes1 == b0 )
                    bRes = b0;
                else
                {
//                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
//                      bRes = Hash_Not( b1 );
                    if ( bRes0 == z0 || bRes1 == z0 )
                        bRes = z0;
                    else
                        bRes = b1;
                }
            }
        }
        // (4) F is on the level iLev2
        else if ( LevelF == iLev2 )
        {
            // this is the only place where the hash attribute (Hash_Not) can be added 
            // to the result; it can be added only if the path came through the node
            // lebeled with Var1; therefore, the hash attribute cannot be returned
            // to the caller function
            if ( fVar1Pres )
//              bRes = Hash_Not( b1 );
                bRes = z0;
            else 
                bRes = b0;
        }
        // (5) F is below iLev2
        else // if ( LevelF > iLev2 )
        {
            // it is possible that the path goes through the node labeled by Var1
            // and still everything is okay; we do not label with Hash_Not here
            // because the path does not go through node labeled by Var2
            bRes = b1;
        }
 
        cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes);
        return bRes;
    }
} /* end of extraBddCheckVarsSymmetric */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddMove()

DdNode * extraBddMove ( DdManager * dd, DdNode * bF, DdNode * bDist )

extern

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]

Description []

SideEffects []

SeeAlso []

Definition at line 1128 of file extraBddMisc.c.

{
    DdNode * bRes;
 
    if ( Cudd_IsConstant(bF) )
        return bF;
 
    if ( (bRes = cuddCacheLookup2(dd, extraBddMove, bF, bDist)) )
        return bRes;
    else
    {
        DdNode * bRes0, * bRes1;             
        DdNode * bF0, * bF1;             
        DdNode * bFR = Cudd_Regular(bF); 
        int VarNew;
        
        if ( Cudd_IsComplement(bDist) )
            VarNew = bFR->index - Cudd_Not(bDist)->index;
        else
            VarNew = bFR->index + bDist->index;
        assert( VarNew < dd->size );
 
        // cofactor the functions
        if ( bFR != bF ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        bRes0 = extraBddMove( dd, bF0, bDist );
        if ( bRes0 == NULL ) 
            return NULL;
        cuddRef( bRes0 );
 
        bRes1 = extraBddMove( dd, bF1, bDist );
        if ( bRes1 == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bRes1 );
 
        /* only bRes0 and bRes1 are referenced at this point */
        bRes = cuddBddIteRecur( dd, dd->vars[VarNew], bRes1, bRes0 );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bRes1 );
            return NULL;
        }
        cuddRef( bRes );
        Cudd_RecursiveDeref( dd, bRes0 );
        Cudd_RecursiveDeref( dd, bRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert2( dd, extraBddMove, bF, bDist, bRes );
        cuddDeref( bRes );
        return bRes;
    }
} /* end of extraBddMove */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddReduceVarSet()

DdNode * extraBddReduceVarSet ( DdManager * dd, DdNode * bVars, DdNode * bF )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_bddReduceVarSet.]

Description [Returns the set of all variables in the given set that are not in the support of the given function.]

SideEffects []

SeeAlso []

Definition at line 1062 of file extraBddSymm.c.

{
    DdNode * bRes;
    DdNode * bFR = Cudd_Regular(bF);
 
    if ( cuddIsConstant(bFR) || bVars == b1 )
        return bVars;
 
    if ( (bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF)) )
        return bRes;
    else
    {
        DdNode * bF0, * bF1;             
        DdNode * bVarsThis, * bVarsLower, * bTemp;
        int LevelF;
 
        // if LevelF is below LevelV, scroll through the vars in bVars 
        LevelF = dd->perm[bFR->index];
        for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );
        // scroll also through the current var, because it should be not be added
        if ( LevelF == cuddI(dd,bVarsThis->index) )
            bVarsLower = cuddT(bVarsThis);
        else
            bVarsLower = bVarsThis;
 
        // cofactor the function
        if ( bFR != bF ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        // solve subproblems
        bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );
        if ( bRes == NULL ) 
            return NULL;
        cuddRef( bRes );
 
        bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bTemp );
            return NULL;
        }
        cuddRef( bRes );
        Cudd_RecursiveDeref( dd, bTemp );
 
        // the current var should not be added
        // add the skipped vars
        if ( bVarsThis != bVars )
        {
            DdNode * bVarsExtra;
 
            // extract the skipped variables
            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDeref( dd, bRes );
                return NULL;
            }
            cuddRef( bVarsExtra );
 
            // add these variables
            bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref( dd, bTemp );
                Cudd_RecursiveDeref( dd, bVarsExtra );
                return NULL;
            }
            cuddRef( bRes );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bVarsExtra );
        }
        cuddDeref( bRes );
 
        cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );
        return bRes;
    }
}   /* end of extraBddReduceVarSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceCanonVars()

DdNode * extraBddSpaceCanonVars ( DdManager * dd, DdNode * bF )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]

Description []

SideEffects []

SeeAlso []

Definition at line 1000 of file extraBddAuto.c.

{
    DdNode * bRes, * bFR;
    statLine( dd );
 
    bFR = Cudd_Regular(bF);
    if ( cuddIsConstant(bFR) )
        return bF;
 
    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )
        return bRes;
    else
    {
        DdNode * bF0,  * bF1;
        DdNode * bRes, * bRes0; 
 
        if ( bFR != bF ) // bF is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        if ( bF0 == b0 )
        {
            bRes = extraBddSpaceCanonVars( dd, bF1 );
            if ( bRes == NULL )
                return NULL;
        }
        else if ( bF1 == b0 )
        {
            bRes = extraBddSpaceCanonVars( dd, bF0 );
            if ( bRes == NULL )
                return NULL;
        }
        else
        {
            bRes0 = extraBddSpaceCanonVars( dd, bF0 );
            if ( bRes0 == NULL )
                return NULL;
            cuddRef( bRes0 );
 
            bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref( dd,bRes0 );
                return NULL;
            }
            cuddDeref( bRes0 );
        }
 
        cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
        return bRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceEquationsNeg()

DdNode * extraBddSpaceEquationsNeg ( DdManager * dd, DdNode * bF )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().]

Description []

SideEffects []

SeeAlso []

Definition at line 1201 of file extraBddAuto.c.

{
    DdNode * zRes;
    statLine( dd );
 
    if ( bF == b0 )
        return z1;
    if ( bF == b1 )
        return z0;
    
    if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF)) )
        return zRes;
    else
    {
        DdNode * bFR, * bF0,  * bF1;
        DdNode * zPos0, * zPos1, * zNeg1; 
        DdNode * zRes, * zRes0, * zRes1;
 
        bFR = Cudd_Regular(bF);
        if ( bFR != bF ) // bF is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        if ( bF0 == b0 )
        {
            zRes = extraBddSpaceEquationsNeg( dd, bF1 );
            if ( zRes == NULL )
                return NULL;
        }
        else if ( bF1 == b0 )
        {
            zRes0 = extraBddSpaceEquationsNeg( dd, bF0 );
            if ( zRes0 == NULL )
                return NULL;
            cuddRef( zRes0 );
 
            // add the current element to the set
            zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                return NULL;
            }
            cuddDeref( zRes0 );
        }
        else
        {
            zPos0 = extraBddSpaceEquationsNeg( dd, bF0 );
            if ( zPos0 == NULL )
                return NULL;
            cuddRef( zPos0 );
 
            zPos1 = extraBddSpaceEquationsNeg( dd, bF1 );
            if ( zPos1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zPos0);
                return NULL;
            }
            cuddRef( zPos1 );
 
            zNeg1 = extraBddSpaceEquationsPos( dd, bF1 );
            if ( zNeg1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zNeg1 );
 
 
            zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zNeg1);
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zRes0 );
 
            zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                Cudd_RecursiveDerefZdd(dd, zNeg1);
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd(dd, zNeg1);
            Cudd_RecursiveDerefZdd(dd, zPos0);
            Cudd_RecursiveDerefZdd(dd, zPos1);
            // only zRes0 and zRes1 are refed at this point
 
            zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
 
        cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes );
        return zRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceEquationsPos()

DdNode * extraBddSpaceEquationsPos ( DdManager * dd, DdNode * bF )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1071 of file extraBddAuto.c.

{
    DdNode * zRes;
    statLine( dd );
 
    if ( bF == b0 )
        return z1;
    if ( bF == b1 )
        return z0;
    
    if ( (zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF)) )
        return zRes;
    else
    {
        DdNode * bFR, * bF0,  * bF1;
        DdNode * zPos0, * zPos1, * zNeg1; 
        DdNode * zRes, * zRes0, * zRes1;
 
        bFR = Cudd_Regular(bF);
        if ( bFR != bF ) // bF is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        if ( bF0 == b0 )
        {
            zRes1 = extraBddSpaceEquationsPos( dd, bF1 );
            if ( zRes1 == NULL )
                return NULL;
            cuddRef( zRes1 );
 
            // add the current element to the set
            zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddDeref( zRes1 );
        }
        else if ( bF1 == b0 )
        {
            zRes = extraBddSpaceEquationsPos( dd, bF0 );
            if ( zRes == NULL )
                return NULL;
        }
        else
        {
            zPos0 = extraBddSpaceEquationsPos( dd, bF0 );
            if ( zPos0 == NULL )
                return NULL;
            cuddRef( zPos0 );
 
            zPos1 = extraBddSpaceEquationsPos( dd, bF1 );
            if ( zPos1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zPos0);
                return NULL;
            }
            cuddRef( zPos1 );
 
            zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 );
            if ( zNeg1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zNeg1 );
 
 
            zRes0 = cuddZddIntersect( dd, zPos0, zPos1 );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zNeg1);
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zRes0 );
 
            zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                Cudd_RecursiveDerefZdd(dd, zNeg1);
                Cudd_RecursiveDerefZdd(dd, zPos0);
                Cudd_RecursiveDerefZdd(dd, zPos1);
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd(dd, zNeg1);
            Cudd_RecursiveDerefZdd(dd, zPos0);
            Cudd_RecursiveDerefZdd(dd, zPos1);
            // only zRes0 and zRes1 are refed at this point
 
            zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
 
        cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes );
        return zRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceFromFunction()

DdNode * extraBddSpaceFromFunction ( DdManager * dd, DdNode * bF, DdNode * bG )

extern

Function********************************************************************

Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.]

Description []

SideEffects []

SeeAlso []

Definition at line 562 of file extraBddAuto.c.

{
    DdNode * bRes;
    DdNode * bFR, * bGR;
 
    bFR = Cudd_Regular( bF ); 
    bGR = Cudd_Regular( bG ); 
    if ( cuddIsConstant(bFR) )
    {
        if ( bF == bG )
            return b1;
        else 
            return b0;
    }
    if ( cuddIsConstant(bGR) )
        return b0;
    // both bFunc and bCore are not constants
 
    // the operation is commutative - normalize the problem
    if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG )
        return extraBddSpaceFromFunction(dd, bG, bF);
 
 
    if ( (bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG)) )
        return bRes;
    else
    {
        DdNode * bF0, * bF1;
        DdNode * bG0, * bG1;
        DdNode * bTemp1, * bTemp2;
        DdNode * bRes0, * bRes1;
        int LevelF, LevelG;
        int index;
 
        LevelF = dd->perm[bFR->index];
        LevelG = dd->perm[bGR->index];
        if ( LevelF <= LevelG )
        {
            index = dd->invperm[LevelF];
            if ( bFR != bF )
            {
                bF0 = Cudd_Not( cuddE(bFR) );
                bF1 = Cudd_Not( cuddT(bFR) );
            }
            else
            {
                bF0 = cuddE(bFR);
                bF1 = cuddT(bFR);
            }
        }
        else
        {
            index = dd->invperm[LevelG];
            bF0 = bF1 = bF;
        }
 
        if ( LevelG <= LevelF )
        {
            if ( bGR != bG )
            {
                bG0 = Cudd_Not( cuddE(bGR) );
                bG1 = Cudd_Not( cuddT(bGR) );
            }
            else
            {
                bG0 = cuddE(bGR);
                bG1 = cuddT(bGR);
            }
        }
        else
            bG0 = bG1 = bG;
 
        bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 );
        if ( bTemp1 == NULL ) 
            return NULL;
        cuddRef( bTemp1 );
 
        bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 );
        if ( bTemp2 == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bTemp1 );
            return NULL;
        }
        cuddRef( bTemp2 );
 
 
        bRes0  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
        if ( bRes0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bTemp1 );
            Cudd_RecursiveDeref( dd, bTemp2 );
            return NULL;
        }
        cuddRef( bRes0 );
        Cudd_RecursiveDeref( dd, bTemp1 );
        Cudd_RecursiveDeref( dd, bTemp2 );
 
 
        bTemp1  = extraBddSpaceFromFunction( dd, bF0, bG1 );
        if ( bTemp1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bTemp1 );
 
        bTemp2  = extraBddSpaceFromFunction( dd, bF1, bG0 );
        if ( bTemp2 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bTemp1 );
            return NULL;
        }
        cuddRef( bTemp2 );
 
        bRes1  = cuddBddAndRecur( dd, bTemp1, bTemp2 );
        if ( bRes1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bTemp1 );
            Cudd_RecursiveDeref( dd, bTemp2 );
            return NULL;
        }
        cuddRef( bRes1 );
        Cudd_RecursiveDeref( dd, bTemp1 );
        Cudd_RecursiveDeref( dd, bTemp2 );
 
 
 
        // consider the case when Res0 and Res1 are the same node 
        if ( bRes0 == bRes1 )
            bRes = bRes1;
        // consider the case when Res1 is complemented 
        else if ( Cudd_IsComplement(bRes1) ) 
        {
            bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0));
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
            bRes = Cudd_Not(bRes);
        } 
        else 
        {
            bRes = cuddUniqueInter( dd, index, bRes1, bRes0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
        }
        cuddDeref( bRes0 );
        cuddDeref( bRes1 );
            
        // insert the result into cache 
        cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes);
        return bRes;
    }
}  /* end of extraBddSpaceFromFunction */

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceFromFunctionNeg()

DdNode * extraBddSpaceFromFunctionNeg ( DdManager * dd, DdNode * bF )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 869 of file extraBddAuto.c.

{
    DdNode * bRes, * bFR;
    statLine( dd );
 
    bFR = Cudd_Regular(bF);
    if ( cuddIsConstant(bFR) )
        return b0;
 
    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF)) )
        return bRes;
    else
    {
        DdNode * bF0,   * bF1;
        DdNode * bPos0, * bPos1;
        DdNode * bNeg0, * bNeg1;
        DdNode * bRes0, * bRes1; 
 
        if ( bFR != bF ) // bF is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
 
        bPos0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
        if ( bPos0 == NULL )
            return NULL;
        cuddRef( bPos0 );
 
        bPos1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
        if ( bPos1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bPos0 );
            return NULL;
        }
        cuddRef( bPos1 );
 
        bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
        if ( bRes0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bPos0 );
            Cudd_RecursiveDeref( dd, bPos1 );
            return NULL;
        }
        cuddRef( bRes0 );
        Cudd_RecursiveDeref( dd, bPos0 );
        Cudd_RecursiveDeref( dd, bPos1 );
 
 
        bNeg0  = extraBddSpaceFromFunctionPos( dd, bF0 );
        if ( bNeg0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bNeg0 );
 
        bNeg1  = extraBddSpaceFromFunctionPos( dd, bF1 );
        if ( bNeg1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bNeg0 );
            return NULL;
        }
        cuddRef( bNeg1 );
 
        bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
        if ( bRes1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bNeg0 );
            Cudd_RecursiveDeref( dd, bNeg1 );
            return NULL;
        }
        cuddRef( bRes1 );
        Cudd_RecursiveDeref( dd, bNeg0 );
        Cudd_RecursiveDeref( dd, bNeg1 );
 
 
        // consider the case when Res0 and Res1 are the same node 
        if ( bRes0 == bRes1 )
            bRes = bRes1;
        // consider the case when Res1 is complemented 
        else if ( Cudd_IsComplement(bRes1) ) 
        {
            bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
            bRes = Cudd_Not(bRes);
        } 
        else 
        {
            bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
        }
        cuddDeref( bRes0 );
        cuddDeref( bRes1 );
 
        cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes );
        return bRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceFromFunctionPos()

DdNode * extraBddSpaceFromFunctionPos ( DdManager * dd, DdNode * bF )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file extraBddAuto.c.

{
    DdNode * bRes, * bFR;
    statLine( dd );
 
    bFR = Cudd_Regular(bF);
    if ( cuddIsConstant(bFR) )
        return b1;
 
    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF)) )
        return bRes;
    else
    {
        DdNode * bF0,   * bF1;
        DdNode * bPos0, * bPos1;
        DdNode * bNeg0, * bNeg1;
        DdNode * bRes0, * bRes1; 
 
        if ( bFR != bF ) // bF is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
 
        bPos0  = extraBddSpaceFromFunctionPos( dd, bF0 );
        if ( bPos0 == NULL )
            return NULL;
        cuddRef( bPos0 );
 
        bPos1  = extraBddSpaceFromFunctionPos( dd, bF1 );
        if ( bPos1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bPos0 );
            return NULL;
        }
        cuddRef( bPos1 );
 
        bRes0  = cuddBddAndRecur( dd, bPos0, bPos1 );
        if ( bRes0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bPos0 );
            Cudd_RecursiveDeref( dd, bPos1 );
            return NULL;
        }
        cuddRef( bRes0 );
        Cudd_RecursiveDeref( dd, bPos0 );
        Cudd_RecursiveDeref( dd, bPos1 );
 
 
        bNeg0  = extraBddSpaceFromFunctionNeg( dd, bF0 );
        if ( bNeg0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bNeg0 );
 
        bNeg1  = extraBddSpaceFromFunctionNeg( dd, bF1 );
        if ( bNeg1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bNeg0 );
            return NULL;
        }
        cuddRef( bNeg1 );
 
        bRes1  = cuddBddAndRecur( dd, bNeg0, bNeg1 );
        if ( bRes1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bNeg0 );
            Cudd_RecursiveDeref( dd, bNeg1 );
            return NULL;
        }
        cuddRef( bRes1 );
        Cudd_RecursiveDeref( dd, bNeg0 );
        Cudd_RecursiveDeref( dd, bNeg1 );
 
 
        // consider the case when Res0 and Res1 are the same node 
        if ( bRes0 == bRes1 )
            bRes = bRes1;
        // consider the case when Res1 is complemented 
        else if ( Cudd_IsComplement(bRes1) ) 
        {
            bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
            bRes = Cudd_Not(bRes);
        } 
        else 
        {
            bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
        }
        cuddDeref( bRes0 );
        cuddDeref( bRes1 );
 
        cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes );
        return bRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceFromMatrixNeg()

DdNode * extraBddSpaceFromMatrixNeg ( DdManager * dd, DdNode * zA )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1451 of file extraBddAuto.c.

{
    DdNode * bRes;
    statLine( dd );
 
    if ( zA == z0 )
        return b1;
    if ( zA == z1 )
        return b0;
 
    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA)) )
        return bRes;
    else
    {
        DdNode * bP0, * bP1;
        DdNode * bN0, * bN1;
        DdNode * bRes0, * bRes1; 
 
        bP0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
        if ( bP0 == NULL )
            return NULL;
        cuddRef( bP0 );
 
        bP1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
        if ( bP1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bP0 );
            return NULL;
        }
        cuddRef( bP1 );
 
        bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
        if ( bRes0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bP0 );
            Cudd_RecursiveDeref( dd, bP1 );
            return NULL;
        }
        cuddRef( bRes0 );
        Cudd_RecursiveDeref( dd, bP0 );
        Cudd_RecursiveDeref( dd, bP1 );
 
 
        bN0  = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) );
        if ( bN0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bN0 );
 
        bN1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
        if ( bN1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bN0 );
            return NULL;
        }
        cuddRef( bN1 );
 
        bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
        if ( bRes1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bN0 );
            Cudd_RecursiveDeref( dd, bN1 );
            return NULL;
        }
        cuddRef( bRes1 );
        Cudd_RecursiveDeref( dd, bN0 );
        Cudd_RecursiveDeref( dd, bN1 );
 
 
        // consider the case when Res0 and Res1 are the same node 
        if ( bRes0 == bRes1 )
            bRes = bRes1;
        // consider the case when Res1 is complemented 
        else if ( Cudd_IsComplement(bRes1) ) 
        {
            bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
            bRes = Cudd_Not(bRes);
        } 
        else 
        {
            bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
        }
        cuddDeref( bRes0 );
        cuddDeref( bRes1 );
 
        cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes );
        return bRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddSpaceFromMatrixPos()

DdNode * extraBddSpaceFromMatrixPos ( DdManager * dd, DdNode * zA )

extern

Function*************************************************************

Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]

Description []

SideEffects []

SeeAlso []

Definition at line 1333 of file extraBddAuto.c.

{
    DdNode * bRes;
    statLine( dd );
 
    if ( zA == z0 )
        return b1;
    if ( zA == z1 )
        return b1;
 
    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA)) )
        return bRes;
    else
    {
        DdNode * bP0, * bP1;
        DdNode * bN0, * bN1;
        DdNode * bRes0, * bRes1; 
 
        bP0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
        if ( bP0 == NULL )
            return NULL;
        cuddRef( bP0 );
 
        bP1  = extraBddSpaceFromMatrixPos( dd, cuddT(zA) );
        if ( bP1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bP0 );
            return NULL;
        }
        cuddRef( bP1 );
 
        bRes0  = cuddBddAndRecur( dd, bP0, bP1 );
        if ( bRes0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bP0 );
            Cudd_RecursiveDeref( dd, bP1 );
            return NULL;
        }
        cuddRef( bRes0 );
        Cudd_RecursiveDeref( dd, bP0 );
        Cudd_RecursiveDeref( dd, bP1 );
 
 
        bN0  = extraBddSpaceFromMatrixPos( dd, cuddE(zA) );
        if ( bN0 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bN0 );
 
        bN1  = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) );
        if ( bN1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bN0 );
            return NULL;
        }
        cuddRef( bN1 );
 
        bRes1  = cuddBddAndRecur( dd, bN0, bN1 );
        if ( bRes1 == NULL )
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            Cudd_RecursiveDeref( dd, bN0 );
            Cudd_RecursiveDeref( dd, bN1 );
            return NULL;
        }
        cuddRef( bRes1 );
        Cudd_RecursiveDeref( dd, bN0 );
        Cudd_RecursiveDeref( dd, bN1 );
 
 
        // consider the case when Res0 and Res1 are the same node 
        if ( bRes0 == bRes1 )
            bRes = bRes1;
        // consider the case when Res1 is complemented 
        else if ( Cudd_IsComplement(bRes1) ) 
        {
            bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
            bRes = Cudd_Not(bRes);
        } 
        else 
        {
            bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref(dd,bRes0);
                Cudd_RecursiveDeref(dd,bRes1);
                return NULL;
            }
        }
        cuddDeref( bRes0 );
        cuddDeref( bRes1 );
 
        cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes );
        return bRes;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

extraBddTuples()

DdNode * extraBddTuples ( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN )

extern

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_bddTuples().]

Description [Generates in a bottom-up fashion BDD for all combinations composed of k variables out of variables belonging to bVarsN.]

SideEffects []

SeeAlso []

Definition at line 2597 of file extraBddMisc.c.

{
    DdNode *bRes, *bRes0, *bRes1;
    statLine(dd); 
 
    /* terminal cases */
/*  if ( k < 0 || k > n )
 *      return dd->zero;
 *  if ( n == 0 )
 *      return dd->one; 
 */
    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
        return b0;
    if ( bVarsN == b1 )
        return b1;
 
    /* check cache */
    bRes = cuddCacheLookup2(dd, extraBddTuples, bVarsK, bVarsN);
    if (bRes)
        return(bRes);
 
    /* ZDD in which is variable is 0 */
/*  bRes0 = extraBddTuples( dd, k,     n-1 ); */
    bRes0 = extraBddTuples( dd, bVarsK, cuddT(bVarsN) );
    if ( bRes0 == NULL ) 
        return NULL;
    cuddRef( bRes0 );
 
    /* ZDD in which is variable is 1 */
/*  bRes1 = extraBddTuples( dd, k-1,          n-1 ); */
    if ( bVarsK == b1 )
    {
        bRes1 = b0;
        cuddRef( bRes1 );
    }
    else
    {
        bRes1 = extraBddTuples( dd, cuddT(bVarsK), cuddT(bVarsN) );
        if ( bRes1 == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bRes0 );
            return NULL;
        }
        cuddRef( bRes1 );
    }
 
    /* consider the case when Res0 and Res1 are the same node */
    if ( bRes0 == bRes1 )
        bRes = bRes1;
    /* consider the case when Res1 is complemented */
    else if ( Cudd_IsComplement(bRes1) ) 
    {
        bRes = cuddUniqueInter(dd, bVarsN->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref(dd,bRes0);
            Cudd_RecursiveDeref(dd,bRes1);
            return NULL;
        }
        bRes = Cudd_Not(bRes);
    } 
    else 
    {
        bRes = cuddUniqueInter( dd, bVarsN->index, bRes1, bRes0 );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref(dd,bRes0);
            Cudd_RecursiveDeref(dd,bRes1);
            return NULL;
        }
    }
    cuddDeref( bRes0 );
    cuddDeref( bRes1 );
 
    /* insert the result into cache */
    cuddCacheInsert2(dd, extraBddTuples, bVarsK, bVarsN, bRes);
    return bRes;
 
} /* end of extraBddTuples */

Here is the call graph for this function:

Here is the caller graph for this function:

extraDecomposeCover()

void extraDecomposeCover ( DdManager * dd, DdNode * zC, DdNode ** zC0, DdNode ** zC1, DdNode ** zC2 )

extern

Function********************************************************************

Synopsis [Finds three cofactors of the cover w.r.t. to the topmost variable.]

Description [Finds three cofactors of the cover w.r.t. to the topmost variable. Does not check the cover for being a constant. Assumes that ZDD variables encoding positive and negative polarities are adjacent in the variable order. Is different from cuddZddGetCofactors3() in that it does not compute the cofactors w.r.t. the given variable but takes the cofactors with respent to the topmost variable. This function is more efficient when used in recursive procedures because it does not require referencing of the resulting cofactors (compare cuddZddProduct() and extraZddPrimeProduct()).]

SideEffects [None]

SeeAlso [cuddZddGetCofactors3]

Definition at line 1217 of file extraBddMisc.c.

{
    if ( (zC->index & 1) == 0 ) 
    { /* the top variable is present in positive polarity and maybe in negative */
 
        DdNode *Temp = cuddE( zC );
        *zC1  = cuddT( zC );
        if ( cuddIZ(dd,Temp->index) == cuddIZ(dd,zC->index) + 1 )
        {   /* Temp is not a terminal node 
             * top var is present in negative polarity */
            *zC2 = cuddE( Temp );
            *zC0 = cuddT( Temp );
        }
        else
        {   /* top var is not present in negative polarity */
            *zC2 = Temp;
            *zC0 = dd->zero;
        }
    }
    else 
    { /* the top variable is present only in negative */
        *zC1 = dd->zero;
        *zC2 = cuddE( zC );
        *zC0 = cuddT( zC );
    }
} /* extraDecomposeCover */

extraZddCrossProduct()

DdNode * extraZddCrossProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddCrossProduct.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 799 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    int TopS, TopT;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( S == z0 || T == z0 )
        return z0;
    if ( S == z1 || T == z1 )
        return z1;
 
    /* the operation is commutative - normalize the problem */
    TopS = dd->permZ[S->index];
    TopT = dd->permZ[T->index];
 
    if ( TopS > TopT || (TopS == TopT && S > T) )
        return extraZddCrossProduct(dd, T, S);
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddCrossProduct, S, T);
    if (zRes)
        return zRes;
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
 
        if ( TopS == TopT )
        {
            /* compute the union of two cofactors of T (T0+T1) */
            zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) );
            if ( zTemp == NULL )
                return NULL;
            cuddRef( zTemp );
 
            /* compute CrossProduct without the top element for subsets (S0, T0+T1) */
            zSet0 = extraZddCrossProduct(dd, cuddE(S), zTemp );
            if ( zSet0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zTemp);
                return NULL;
            }
            cuddRef( zSet0 );
            Cudd_RecursiveDerefZdd(dd, zTemp);
 
            /* compute CrossProduct without the top element for subsets (S1, T0) */
            zSet1 = extraZddCrossProduct(dd, cuddT(S), cuddE(T) );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
 
            /* compute the union of these two partial results (zSet0 + zSet1) */
            zRes0 = cuddZddUnion(dd, zSet0, zSet1 );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                Cudd_RecursiveDerefZdd(dd, zSet1);
                return NULL;
            }
            cuddRef( zRes0 );
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
 
            /* compute CrossProduct for subsets with the top-most element */
            zRes1 = extraZddCrossProduct(dd, cuddT(S), cuddT(T) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes0);
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* create the new node */
            zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopS < TopT ) */
        {
            /* compute CrossProduct without the top element (S0, T) */
            zSet0 = extraZddCrossProduct(dd, cuddE(S), T );
            if ( zSet0 == NULL )
                return NULL;
            cuddRef( zSet0 );
 
            /* compute CrossProduct without the top element (S1, T) */
            zSet1 = extraZddCrossProduct(dd, cuddT(S), T );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
 
            /* compute the union of these two partial results (zSet0 + zSet1) */
            zRes = cuddZddUnion(dd, zSet0, zSet1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                Cudd_RecursiveDerefZdd(dd, zSet1);
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
            cuddDeref( zRes );
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddCrossProduct, S, T, zRes);
        return zRes;
    }
} /* end of extraZddCrossProduct */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddDotProduct()

DdNode * extraZddDotProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddDotProduct.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 672 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    int TopS, TopT;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( S == z0 || T == z0 )
        return z0;
    if ( S == z1 )
        return T;
    if ( T == z1 )
        return S;
 
    /* the operation is commutative - normalize the problem */
    TopS = dd->permZ[S->index];
    TopT = dd->permZ[T->index];
 
    if ( TopS > TopT || (TopS == TopT && S > T) )
        return extraZddDotProduct(dd, T, S);
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddDotProduct, S, T);
    if (zRes)
        return zRes;
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
        if ( TopS == TopT )
        {
            /* compute the union of two cofactors of T (T0+T1) */
            zTemp = cuddZddUnion(dd, cuddE(T), cuddT(T) );
            if ( zTemp == NULL )
                return NULL;
            cuddRef( zTemp );
 
            /* compute DotProduct with the top element for subsets (S1, T0+T1) */
            zSet0 = extraZddDotProduct(dd, cuddT(S), zTemp );
            if ( zSet0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zTemp);
                return NULL;
            }
            cuddRef( zSet0 );
            Cudd_RecursiveDerefZdd(dd, zTemp);
 
            /* compute DotProduct with the top element for subsets (S0, T1) */
            zSet1 = extraZddDotProduct(dd, cuddE(S), cuddT(T) );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
 
            /* compute the union of these two partial results (zSet0 + zSet1) */
            zRes1 = cuddZddUnion(dd, zSet0, zSet1 );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                Cudd_RecursiveDerefZdd(dd, zSet1);
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
 
            /* compute DotProduct for subsets without the top-most element */
            zRes0 = extraZddDotProduct(dd, cuddE(S), cuddE(T) );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
        }
        else /* if ( TopS < TopT ) */
        {
            /* compute DotProduct with the top element for subsets (S1, T) */
            zRes1 = extraZddDotProduct(dd, cuddT(S), T );
            if ( zRes1 == NULL )
                return NULL;
            cuddRef( zRes1 );
 
            /* compute DotProduct for subsets without the top-most element */
            zRes0 = extraZddDotProduct(dd, cuddE(S), T );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
        }
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddDotProduct, S, T, zRes);
        return zRes;
    }
} /* end of extraZddDotProduct */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddGetSingletons()

DdNode * extraZddGetSingletons ( DdManager * dd, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_zddGetSingletons.]

Description [Returns the set of ZDD singletons, containing those positive polarity ZDD variables that correspond to the BDD variables in bVars.]

SideEffects []

SeeAlso []

Definition at line 1001 of file extraBddSymm.c.

{
    DdNode * zRes;
 
    if ( bVars == b1 )
//    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004
        return z1;
 
    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          
 
        // solve subproblem
        zRes = extraZddGetSingletons( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );
        
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );
 
        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        cuddDeref( zRes );
 
        cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletons */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddGetSingletonsBoth()

DdNode * extraZddGetSingletonsBoth ( DdManager * dd, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_zddGetSingletons.]

Description [Returns the set of ZDD singletons, containing those pos/neg polarity ZDD variables that correspond to the BDD variables in bVars.]

SideEffects []

SeeAlso []

Definition at line 570 of file extraBddUnate.c.

{
    DdNode * zRes;
 
    if ( bVars == b1 )
        return z1;
 
    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          
 
        // solve subproblem
        zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );
 
        
        // create the negative singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );
 
        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        
 
        // create the positive singleton
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );
 
        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
 
        cuddDeref( zRes );
        cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletonsBoth */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddGetSymmetricVars()

DdNode * extraZddGetSymmetricVars ( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_zddGetSymmetricVars.]

Description [Returns the set of ZDD singletons, containing those positive ZDD variables that correspond to BDD variables x, for which it is true that bF(x=0) == bG(x=1).]

SideEffects []

SeeAlso []

Definition at line 804 of file extraBddSymm.c.

{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bF); 
    DdNode * bGR = Cudd_Regular(bG); 
 
    if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) )
    {
        if ( bF == bG )
            return extraZddGetSingletons( dd, bVars );
        else 
            return z0;
    }
    assert( bVars != b1 );
 
    if ( (zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;             
        DdNode * zPlus, * zTemp;
        DdNode * bF0, * bF1;             
        DdNode * bG0, * bG1;             
        DdNode * bVarsNew;
    
        int LevelF = cuddI(dd,bFR->index);
        int LevelG = cuddI(dd,bGR->index);
        int LevelFG;
 
        if ( LevelF < LevelG )
            LevelFG = LevelF;
        else
            LevelFG = LevelG;
 
        // at least one of the arguments is not a constant
        assert( LevelFG < dd->size );
 
        // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV
        // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG
        for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) );
        assert( LevelFG == dd->perm[bVarsNew->index] );
 
        // cofactor the functions
        if ( LevelF == LevelFG )
        {
            if ( bFR != bF ) // bF is complemented 
            {
                bF0 = Cudd_Not( cuddE(bFR) );
                bF1 = Cudd_Not( cuddT(bFR) );
            }
            else
            {
                bF0 = cuddE(bFR);
                bF1 = cuddT(bFR);
            }
        }
        else 
            bF0 = bF1 = bF;
 
        if ( LevelG == LevelFG )
        {
            if ( bGR != bG ) // bG is complemented 
            {
                bG0 = Cudd_Not( cuddE(bGR) );
                bG1 = Cudd_Not( cuddT(bGR) );
            }
            else
            {
                bG0 = cuddE(bGR);
                bG1 = cuddT(bGR);
            }
        }
        else 
            bG0 = bG1 = bG;
 
        // solve subproblems
        zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) );
        if ( zRes0 == NULL ) 
            return NULL;
        cuddRef( zRes0 );
 
        // if there is not symmetries in the negative cofactor
        // there is no need to test the positive cofactor
        if ( zRes0 == z0 )
            zRes = zRes0;  // zRes takes reference
        else
        {
            zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) );
            if ( zRes1 == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            // only those variables should belong to the resulting set 
            // for which the property is true for both cofactors
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }
 
        // add one more singleton if the property is true for this variable
        if ( bF0 == bG1 )
        {
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );
 
            // add these variable pairs to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
 
        if ( bF == bG && bVars != bVarsNew )
        { 
            // if the functions are equal, so are their cofactors
            // add those variables from V that are above F and G 
 
            DdNode * bVarsExtra;
 
            assert( LevelFG > dd->perm[bVars->index] );
 
            // create the BDD of the extra variables
            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsNew );
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( bVarsExtra );
 
            zPlus = extraZddGetSingletons( dd, bVarsExtra );
            if ( zPlus == NULL )
            {
                Cudd_RecursiveDeref( dd, bVarsExtra );
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );
            Cudd_RecursiveDeref( dd, bVarsExtra );
 
            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        cuddDeref( zRes );
 
        cuddCacheInsert( dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSymmetricVars */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMaxDotProduct()

DdNode * extraZddMaxDotProduct ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMaxDotProduct.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 938 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    int TopS, TopT;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( S == z0 || T == z0 )
        return z0;
    if ( S == z1 )
        return T;
    if ( T == z1 )
        return S;
 
    /* the operation is commutative - normalize the problem */
    TopS = dd->permZ[S->index];
    TopT = dd->permZ[T->index];
 
    if ( TopS > TopT || (TopS == TopT && S > T) )
        return extraZddMaxDotProduct(dd, T, S);
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxDotProduct, S, T);
    if (zRes)
        return zRes;
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1, *zTemp;
        if ( TopS == TopT )
        {
            /* compute the union of two cofactors of T (T0+T1) */
            zTemp = extraZddMaxUnion(dd, cuddE(T), cuddT(T) );
            if ( zTemp == NULL )
                return NULL;
            cuddRef( zTemp );
 
            /* compute MaxDotProduct with the top element for subsets (S1, T0+T1) */
            zSet0 = extraZddMaxDotProduct(dd, cuddT(S), zTemp );
            if ( zSet0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zTemp);
                return NULL;
            }
            cuddRef( zSet0 );
            Cudd_RecursiveDerefZdd(dd, zTemp);
 
            /* compute MaxDotProduct with the top element for subsets (S0, T1) */
            zSet1 = extraZddMaxDotProduct(dd, cuddE(S), cuddT(T) );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
 
            /* compute the union of these two partial results (zSet0 + zSet1) */
            zRes1 = extraZddMaxUnion(dd, zSet0, zSet1 );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                Cudd_RecursiveDerefZdd(dd, zSet1);
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
 
            /* compute MaxDotProduct for subsets without the top-most element */
            zRes0 = extraZddMaxDotProduct(dd, cuddE(S), cuddE(T) );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
        }
        else /* if ( TopS < TopT ) */
        {
            /* compute MaxDotProduct with the top element for subsets (S1, T) */
            zRes1 = extraZddMaxDotProduct(dd, cuddT(S), T );
            if ( zRes1 == NULL )
                return NULL;
            cuddRef( zRes1 );
 
            /* compute MaxDotProduct for subsets without the top-most element */
            zRes0 = extraZddMaxDotProduct(dd, cuddE(S), T );
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
        }
 
        /* remove subsets without this element covered by subsets with this element */
        zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
        if ( zRes0 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zTemp);
            Cudd_RecursiveDerefZdd(dd, zRes1);
            return NULL;
        }
        cuddRef( zRes0 );
        Cudd_RecursiveDerefZdd(dd, zTemp);
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddMaxDotProduct, S, T, zRes);
        return zRes;
    }
} /* end of extraZddMaxDotProduct */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMaximal()

DdNode * extraZddMaximal ( DdManager * dd, DdNode * zSet )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMaximal.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 294 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( zSet == z0 || zSet == z1 )
        return zSet;
 
    /* check cache */
    zRes = cuddCacheLookup1Zdd(dd, extraZddMaximal, zSet);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1;
 
        /* compute maximal for subsets without the top-most element */
        zSet0 = extraZddMaximal(dd, cuddE(zSet));
        if ( zSet0 == NULL )
            return NULL;
        cuddRef( zSet0 );
 
        /* compute maximal for subsets with the top-most element */
        zSet1 = extraZddMaximal(dd, cuddT(zSet));
        if ( zSet1 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            return NULL;
        }
        cuddRef( zSet1 );
 
        /* remove subsets without this element covered by subsets with this element */
        zRes0 = extraZddNotSubSet(dd, zSet0, zSet1);
        if ( zRes0 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
            return NULL;
        }
        cuddRef( zRes0 );
        Cudd_RecursiveDerefZdd(dd, zSet0);
 
        /* subset with this element remains unchanged */
        zRes1 = zSet1;
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert1(dd, extraZddMaximal, zSet, zRes);
        return zRes;
    }
} /* end of extraZddMaximal */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMaxNotSupSet()

DdNode * extraZddMaxNotSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMaxNotSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 799 of file extraBddSet.c.

{   
    DdNode *zRes;
    statLine(dd); 
    /* any comb is a superset of itself */
    if ( X == Y ) 
        return z0;
    /* no comb in X is superset of non-existing combs */
    if ( Y == z0 ) 
        return extraZddMaximal( dd, X ); 
    /* any comb in X is the superset of the empty comb */
    if ( Extra_zddEmptyBelongs( dd, Y ) ) 
        return z0;
    /* if X is empty, the result is empty */
    if ( X == z0 ) 
        return z0;
    /* if X is the empty comb (and Y does not contain it!), return it */
    if ( X == z1 ) 
        return z1;
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxNotSupSet, X, Y);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zRes0, *zRes1, *zTemp;
        int TopLevelX = dd->permZ[ X->index ];
        int TopLevelY = dd->permZ[ Y->index ];
 
        if ( TopLevelX < TopLevelY )
        {
            /* combinations of X without label that are supersets of combinations with Y */
            zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), Y );
            if ( zRes0 == NULL )  
                return NULL;
            cuddRef( zRes0 );
 
            /* combinations of X with label that are supersets of combinations with Y */
            zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), Y );
            if ( zRes1 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* ---------------------------------------------------- */
            /* remove subsets without this element covered by subsets with this element */
            zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zTemp);
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
            Cudd_RecursiveDerefZdd(dd, zTemp);
            /* ---------------------------------------------------- */
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else if ( TopLevelX == TopLevelY )
        {
            /* combs of X without var that are supersets of combs of Y without var */
            zRes0 = extraZddMaxNotSupSet( dd, cuddE( X ), cuddE( Y ) );
            if ( zRes0 == NULL )  
                return NULL;
            cuddRef( zRes0 );
 
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zTemp );
 
            /* combs of X with label that are supersets of combs in Temp */
            zRes1 = extraZddMaxNotSupSet( dd, cuddT( X ), zTemp );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd( dd, zTemp );
 
            /* ---------------------------------------------------- */
            /* remove subsets without this element covered by subsets with this element */
            zRes0 = extraZddNotSubSet(dd, zTemp = zRes0, zRes1);
            if ( zRes0 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zTemp);
                Cudd_RecursiveDerefZdd(dd, zRes1);
                return NULL;
            }
            cuddRef( zRes0 );
            Cudd_RecursiveDerefZdd(dd, zTemp);
            /* ---------------------------------------------------- */
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopLevelX > TopLevelY ) */
        {
            /* combs of X that are supersets of combs of Y without label */
            zRes = extraZddMaxNotSupSet( dd, X, cuddE( Y ) );
            if ( zRes == NULL )  return NULL;
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddMaxNotSupSet, X, Y, zRes);
        return zRes;
    }
} /* end of extraZddMaxNotSupSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMaxUnion()

DdNode * extraZddMaxUnion ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMaxUnion.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 454 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    int TopS, TopT;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( S == z0 )
        return T;
    if ( T == z0 )
        return S;
    if ( S == T )
        return S;
    if ( S == z1 )
        return T;
    if ( T == z1 )
        return S;
 
    /* the operation is commutative - normalize the problem */
    TopS = dd->permZ[S->index];
    TopT = dd->permZ[T->index];
 
    if ( TopS > TopT || (TopS == TopT && S > T) )
        return extraZddMaxUnion(dd, T, S);
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddMaxUnion, S, T);
    if (zRes)
        return zRes;
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1;
 
        if ( TopS == TopT )
        {
            /* compute maximal for subsets without the top-most element */
            zSet0 = extraZddMaxUnion(dd, cuddE(S), cuddE(T) );
            if ( zSet0 == NULL )
                return NULL;
            cuddRef( zSet0 );
 
            /* compute maximal for subsets with the top-most element */
            zSet1 = extraZddMaxUnion(dd, cuddT(S), cuddT(T) );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
        }
        else /* if ( TopS < TopT ) */
        {
            /* compute maximal for subsets without the top-most element */
            zSet0 = extraZddMaxUnion(dd, cuddE(S), T );
            if ( zSet0 == NULL )
                return NULL;
            cuddRef( zSet0 );
 
            /* subset with this element is just the cofactor of S */
            zSet1 = cuddT(S);
            cuddRef( zSet1 );
        }
 
        /* remove subsets without this element covered by subsets with this element */
        zRes0 = extraZddNotSubSet(dd, zSet0, zSet1);
        if ( zRes0 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
            return NULL;
        }
        cuddRef( zRes0 );
        Cudd_RecursiveDerefZdd(dd, zSet0);
 
        /* subset with this element remains unchanged */
        zRes1 = zSet1;
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddMaxUnion, S, T, zRes);
        return zRes;
    }
} /* end of extraZddMaxUnion */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMinimal()

DdNode * extraZddMinimal ( DdManager * dd, DdNode * zSet )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMinimal.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 373 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( zSet == z0 )
        return zSet;
    /* the empty combinaTon, if present, is the only minimal combinaTon */
    if ( Extra_zddEmptyBelongs(dd, zSet) )
        return z1; 
 
    /* check cache */
    zRes = cuddCacheLookup1Zdd(dd, extraZddMinimal, zSet);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1;
 
        /* compute minimal for subsets without the top-most element */
        zSet0 = extraZddMinimal(dd, cuddE(zSet));
        if ( zSet0 == NULL )
            return NULL;
        cuddRef( zSet0 );
 
        /* compute minimal for subsets with the top-most element */
        zSet1 = extraZddMinimal(dd, cuddT(zSet));
        if ( zSet1 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            return NULL;
        }
        cuddRef( zSet1 );
 
        /* subset without this element remains unchanged */
        zRes0 = zSet0;
 
        /* remove subsets with this element that contain subsets without this element */
        zRes1 = extraZddNotSupSet(dd, zSet1, zSet0);
        if ( zRes1 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
            return NULL;
        }
        cuddRef( zRes1 );
        Cudd_RecursiveDerefZdd(dd, zSet1);
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, zSet->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert1(dd, extraZddMinimal, zSet, zRes);
        return zRes;
    }
} /* end of extraZddMinimal */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddMinUnion()

DdNode * extraZddMinUnion ( DdManager * dd, DdNode * S, DdNode * T )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddMinUnion.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 564 of file extraBddMaxMin.c.

{
    DdNode *zRes;
    int TopS, TopT;
    statLine(dd); 
 
    /* consider terminal cases */
    if ( S == z0 )
        return T;
    if ( T == z0 )
        return S;
    if ( S == T )
        return S;
    /* the empty combination, if present, is the only minimal combination */
    if ( Extra_zddEmptyBelongs(dd, S) || Extra_zddEmptyBelongs(dd, T) )
        return z1; 
 
    /* the operation is commutative - normalize the problem */
    TopS = dd->permZ[S->index];
    TopT = dd->permZ[T->index];
 
    if ( TopS > TopT || (TopS == TopT && S > T) )
        return extraZddMinUnion(dd, T, S);
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddMinUnion, S, T);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zSet0, *zSet1, *zRes0, *zRes1;
        if ( TopS == TopT )
        {
            /* compute maximal for subsets without the top-most element */
            zSet0 = extraZddMinUnion(dd, cuddE(S), cuddE(T) );
            if ( zSet0 == NULL )
                return NULL;
            cuddRef( zSet0 );
 
            /* compute maximal for subsets with the top-most element */
            zSet1 = extraZddMinUnion(dd, cuddT(S), cuddT(T) );
            if ( zSet1 == NULL )
            {
                Cudd_RecursiveDerefZdd(dd, zSet0);
                return NULL;
            }
            cuddRef( zSet1 );
        }
        else /* if ( TopS < TopT ) */
        {
            /* compute maximal for subsets without the top-most element */
            zSet0 = extraZddMinUnion(dd, cuddE(S), T );
            if ( zSet0 == NULL )
                return NULL;
            cuddRef( zSet0 );
 
            /* subset with this element is just the cofactor of S */
            zSet1 = cuddT(S);
            cuddRef( zSet1 );
        }
 
        /* subset without this element remains unchanged */
        zRes0 = zSet0;
 
        /* remove subsets with this element that contain subsets without this element */
        zRes1 = extraZddNotSupSet(dd, zSet1, zSet0);
        if ( zRes1 == NULL )
        {
            Cudd_RecursiveDerefZdd(dd, zSet0);
            Cudd_RecursiveDerefZdd(dd, zSet1);
            return NULL;
        }
        cuddRef( zRes1 );
        Cudd_RecursiveDerefZdd(dd, zSet1);
 
        /* create the new node */
        zRes = cuddZddGetNode( dd, S->index, zRes1, zRes0 );
        if ( zRes == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
            return NULL;
        }
        cuddDeref( zRes0 );
        cuddDeref( zRes1 );
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddMinUnion, S, T, zRes);
        return zRes;
    }
} /* end of extraZddMinUnion */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddNotSubSet()

DdNode * extraZddNotSubSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddNotSubSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 550 of file extraBddSet.c.

{   
    DdNode *zRes;
    statLine(dd); 
    /* any comb is a subset of itself */
    if ( X == Y ) 
        return z0;
    /* combs in X are notsubsets of non-existant combs in Y */
    if ( Y == z0 ) 
        return X;   
    /* only {()} is the subset of {()} */
    if ( Y == z1 ) /* remove empty combination from X */
        return cuddZddDiff( dd, X, z1 );
    /* if X is empty, the result is empty */
    if ( X == z0 ) 
        return z0;
    /* the empty comb is contained in all combs of Y */
    if ( X == z1 ) 
        return z0;
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddNotSubSet, X, Y);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zRes0, *zRes1, *zTemp;
        int TopLevelX = dd->permZ[ X->index ];
        int TopLevelY = dd->permZ[ Y->index ];
 
        if ( TopLevelX < TopLevelY )
        {
            /* compute combs of X without var that are notsubsets of combs with Y */
            zRes0 = extraZddNotSubSet( dd, cuddE( X ), Y );
            if ( zRes0 == NULL )  
                return NULL;
            cuddRef( zRes0 );
 
            /* combs of X with var cannot be subsets of combs without var in Y */
            zRes1 = cuddT( X );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddDeref( zRes0 );
        }
        else if ( TopLevelX == TopLevelY )
        {
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )  
                return NULL;
            cuddRef( zTemp );
 
            /* compute combs of X without var that are notsubsets of combs is Temp */
            zRes0 = extraZddNotSubSet( dd, cuddE( X ), zTemp );
            if ( zRes0 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes0 );
            Cudd_RecursiveDerefZdd( dd, zTemp );
 
            /* combs of X with var that are notsubsets of combs in Y with var */
            zRes1 = extraZddNotSubSet( dd, cuddT( X ), cuddT( Y ) );
            if ( zRes1 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopLevelX > TopLevelY ) */
        {
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )  
                return NULL;
            cuddRef( zTemp );
 
            /* compute combs that are notsubsets of Temp */
            zRes = extraZddNotSubSet( dd, X, zTemp );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            cuddDeref( zRes );
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddNotSubSet, X, Y, zRes);
        return zRes;
    }
} /* end of extraZddNotSubSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddNotSupSet()

DdNode * extraZddNotSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddNotSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 676 of file extraBddSet.c.

{   
    DdNode *zRes;
    statLine(dd); 
    /* any comb is a superset of itself */
    if ( X == Y ) 
        return z0;
    /* no comb in X is superset of non-existing combs */
    if ( Y == z0 ) 
        return X;   
    /* any comb in X is the superset of the empty comb */
    if ( Extra_zddEmptyBelongs( dd, Y ) ) 
        return z0;
    /* if X is empty, the result is empty */
    if ( X == z0 ) 
        return z0;
    /* if X is the empty comb (and Y does not contain it!), return it */
    if ( X == z1 ) 
        return z1;
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddNotSupSet, X, Y);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zRes0, *zRes1, *zTemp;
        int TopLevelX = dd->permZ[ X->index ];
        int TopLevelY = dd->permZ[ Y->index ];
 
        if ( TopLevelX < TopLevelY )
        {
            /* combinations of X without label that are supersets of combinations of Y */
            zRes0 = extraZddNotSupSet( dd, cuddE( X ), Y );
            if ( zRes0 == NULL )  
                return NULL;
            cuddRef( zRes0 );
 
            /* combinations of X with label that are supersets of combinations of Y */
            zRes1 = extraZddNotSupSet( dd, cuddT( X ), Y );
            if ( zRes1 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else if ( TopLevelX == TopLevelY )
        {
            /* combs of X without var that are not supersets of combs of Y without var */
            zRes0 = extraZddNotSupSet( dd, cuddE( X ), cuddE( Y ) );
            if ( zRes0 == NULL )  
                return NULL;
            cuddRef( zRes0 );
 
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zTemp );
 
            /* combs of X with label that are supersets of combs in Temp */
            zRes1 = extraZddNotSupSet( dd, cuddT( X ), zTemp );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd( dd, zTemp );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopLevelX > TopLevelY ) */
        {
            /* combs of X that are supersets of combs of Y without label */
            zRes = extraZddNotSupSet( dd, X, cuddE( Y ) );
            if ( zRes == NULL )  return NULL;
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddNotSupSet, X, Y, zRes);
        return zRes;
    }
} /* end of extraZddNotSupSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddSelectOneSubset()

DdNode * extraZddSelectOneSubset ( DdManager * dd, DdNode * zS )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddSelectOneSubset.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1419 of file extraBddSymm.c.

{
    DdNode * zRes;
 
    if ( zS == z0 )    return z0;
    if ( zS == z1 )    return z1;
    
    // check cache
    if ( (zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS )) )
        return zRes;
    else
    {
        DdNode * zS0, * zS1, * zTemp; 
 
        zS0 = cuddE(zS);
        zS1 = cuddT(zS);
 
        if ( zS0 != z0 )
        {
            zRes = extraZddSelectOneSubset( dd, zS0 );
            if ( zRes == NULL )
                return NULL;
        }
        else // if ( zS0 == z0 )
        {
            assert( zS1 != z0 );
            zRes = extraZddSelectOneSubset( dd, zS1 );
            if ( zRes == NULL )
                return NULL;
            cuddRef( zRes );
 
            zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddDeref( zTemp );
        }
 
        // insert the result into cache
        cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
        return zRes;
    }       
} /* end of extraZddSelectOneSubset */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddSubSet()

DdNode * extraZddSubSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddSubSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 319 of file extraBddSet.c.

{   
    DdNode *zRes;
    statLine(dd); 
    /* any comb is a subset of itself */
    if ( X == Y ) 
        return X;
    /* if X is empty, the result is empty */
    if ( X == z0 ) 
        return z0;
    /* combs in X are notsubsets of non-existant combs in Y */
    if ( Y == z0 ) 
        return z0;
    /* the empty comb is contained in all combs of Y */
    if ( X == z1 ) 
        return z1;
    /* only {()} is the subset of {()} */
    if ( Y == z1 ) /* check whether the empty combination is present in X */ 
        return ( Extra_zddEmptyBelongs( dd, X )? z1: z0 );
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddSubSet, X, Y);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zRes0, *zRes1, *zTemp;
        int TopLevelX = dd->permZ[ X->index ];
        int TopLevelY = dd->permZ[ Y->index ];
 
        if ( TopLevelX < TopLevelY )
        {
            /* compute combs of X without var that are notsubsets of combs with Y */
            zRes = extraZddSubSet( dd, cuddE( X ), Y );
            if ( zRes == NULL )  return NULL;
        }
        else if ( TopLevelX == TopLevelY )
        {
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )
                return NULL;
            cuddRef( zTemp );
 
            /* compute combs of X without var that are notsubsets of combs is Temp */
            zRes0 = extraZddSubSet( dd, cuddE( X ), zTemp );
            if ( zRes0 == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes0 );
            Cudd_RecursiveDerefZdd( dd, zTemp );
 
            /* combs of X with var that are notsubsets of combs in Y with var */
            zRes1 = extraZddSubSet( dd, cuddT( X ), cuddT( Y ) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopLevelX > TopLevelY ) */
        {
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )  return NULL;
            cuddRef( zTemp );
 
            /* compute combs that are notsubsets of Temp */
            zRes = extraZddSubSet( dd, X, zTemp );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            cuddDeref( zRes );
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddSubSet, X, Y, zRes);
        return zRes;
    }
} /* end of extraZddSubSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddSupSet()

DdNode * extraZddSupSet ( DdManager * dd, DdNode * X, DdNode * Y )

extern

Function********************************************************************

Synopsis [Performs the recursive step of Extra_zddSupSet.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 430 of file extraBddSet.c.

{   
    DdNode *zRes;
    statLine(dd); 
    /* any comb is a superset of itself */
    if ( X == Y ) 
        return X;
    /* no comb in X is superset of non-existing combs */
    if ( Y == z0 ) 
        return z0;    
    /* any comb in X is the superset of the empty comb */
    if ( Extra_zddEmptyBelongs( dd, Y ) ) 
        return X;
    /* if X is empty, the result is empty */
    if ( X == z0 ) 
        return z0;
    /* if X is the empty comb (and Y does not contain it!), return empty */
    if ( X == z1 ) 
        return z0;
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddSupSet, X, Y);
    if (zRes)
        return(zRes);
    else
    {
        DdNode *zRes0, *zRes1, *zTemp;
        int TopLevelX = dd->permZ[ X->index ];
        int TopLevelY = dd->permZ[ Y->index ];
 
        if ( TopLevelX < TopLevelY )
        {
            /* combinations of X without label that are supersets of combinations with Y */
            zRes0 = extraZddSupSet( dd, cuddE( X ), Y );
            if ( zRes0 == NULL )  return NULL;
            cuddRef( zRes0 );
 
            /* combinations of X with label that are supersets of combinations with Y */
            zRes1 = extraZddSupSet( dd, cuddT( X ), Y );
            if ( zRes1 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else if ( TopLevelX == TopLevelY )
        {
            /* combs of X without var that are supersets of combs of Y without var */
            zRes0 = extraZddSupSet( dd, cuddE( X ), cuddE( Y ) );
            if ( zRes0 == NULL )  return NULL;
            cuddRef( zRes0 );
 
            /* merge combs of Y with and without var */
            zTemp = cuddZddUnion( dd, cuddE( Y ), cuddT( Y ) );
            if ( zTemp == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zTemp );
 
            /* combs of X with label that are supersets of combs in Temp */
            zRes1 = extraZddSupSet( dd, cuddT( X ), zTemp );
            if ( zRes1 == NULL )  
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddRef( zRes1 );
            Cudd_RecursiveDerefZdd( dd, zTemp );
 
            /* compose Res0 and Res1 with the given ZDD variable */
            zRes = cuddZddGetNode( dd, X->index, zRes1, zRes0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddDeref( zRes0 );
            cuddDeref( zRes1 );
        }
        else /* if ( TopLevelX > TopLevelY ) */
        {
            /* combs of X that are supersets of combs of Y without label */
            zRes = extraZddSupSet( dd, X, cuddE( Y ) );
            if ( zRes == NULL )  return NULL;
        }
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddSupSet, X, Y, zRes);
        return zRes;
    }
} /* end of extraZddSupSet */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddSymmPairsCompute()

DdNode * extraZddSymmPairsCompute ( DdManager * dd, DdNode * bFunc, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_SymmPairsCompute.]

Description [Returns the set of symmetric variable pairs represented as a set of two-literal ZDD cubes. Both variables always appear in the positive polarity in the cubes. This function works without building new BDD nodes. Some relatively small number of ZDD nodes may be built to ensure proper bookkeeping of the symmetry information.]

SideEffects []

SeeAlso []

Definition at line 580 of file extraBddSymm.c.

{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bFunc); 
 
    if ( cuddIsConstant(bFR) )
    {
        int nVars, i;
 
        // determine how many vars are in the bVars
        nVars = Extra_bddSuppSize( dd, bVars );
        if ( nVars < 2 )
            return z0;
        else
        {
            DdNode * bVarsK;
 
            // create the BDD bVarsK corresponding to K = 2;
            bVarsK = bVars;
            for ( i = 0; i < nVars-2; i++ )
                bVarsK = cuddT( bVarsK );
            return extraZddTuplesFromBdd( dd, bVarsK, bVars );
        }
    }
    assert( bVars != b1 );
 
    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;
        DdNode * zTemp, * zPlus, * zSymmVars;             
        DdNode * bF0, * bF1;             
        DdNode * bVarsNew;
        int nVarsExtra;
        int LevelF;
 
        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
        // count how many extra vars are there in bVars
        nVarsExtra = 0;
        LevelF = dd->perm[bFR->index];
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
            nVarsExtra++; 
        // the indexes (level) of variables should be synchronized now
        assert( bFR->index == bVarsNew->index );
 
        // cofactor the function
        if ( bFR != bFunc ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        // solve subproblems
        zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) );
        if ( zRes0 == NULL )
            return NULL;
        cuddRef( zRes0 );
 
        // if there is no symmetries in the negative cofactor
        // there is no need to test the positive cofactor
        if ( zRes0 == z0 )
            zRes = zRes0;  // zRes takes reference
        else
        {
            zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            // only those variables are pair-wise symmetric 
            // that are pair-wise symmetric in both cofactors
            // therefore, intersect the solutions
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }
 
        // consider the current top-most variable and find all the vars
        // that are pairwise symmetric with it
        // these variables are returned as a set of ZDD singletons
        zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) );
        if ( zSymmVars == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zSymmVars );
 
        // attach the topmost variable to the set, to get the variable pairs
        // use the positive polarity ZDD variable for the purpose
 
        // there is no need to do so, if zSymmVars is empty
        if ( zSymmVars == z0 )
            Cudd_RecursiveDerefZdd( dd, zSymmVars );
        else
        {
            zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                Cudd_RecursiveDerefZdd( dd, zSymmVars );
                return NULL;
            }
            cuddRef( zPlus );
            cuddDeref( zSymmVars );
 
            // add these variable pairs to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
 
        // only zRes is referenced at this point
 
        // if we skipped some variables, these variables cannot be symmetric with
        // any variables that are currently in the support of bF, but they can be 
        // symmetric with the variables that are in bVars but not in the support of bF
        if ( nVarsExtra )
        {
            // it is possible to improve this step:
            // (1) there is no need to enter here, if nVarsExtra < 2
 
            // create the set of topmost nVarsExtra in bVars
            DdNode * bVarsExtra;
            int nVars;
 
            // remove from bVars all the variable that are in the support of bFunc
            bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc );  
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( bVarsExtra );
 
            // determine how many vars are in the bVarsExtra
            nVars = Extra_bddSuppSize( dd, bVarsExtra );
            if ( nVars < 2 )
            {
                Cudd_RecursiveDeref( dd, bVarsExtra );
            }
            else
            {
                int i;
                DdNode * bVarsK;
 
                // create the BDD bVarsK corresponding to K = 2;
                bVarsK = bVarsExtra;
                for ( i = 0; i < nVars-2; i++ )
                    bVarsK = cuddT( bVarsK );
 
                // create the 2 variable tuples
                zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra );
                if ( zPlus == NULL )
                {
                    Cudd_RecursiveDeref( dd, bVarsExtra );
                    Cudd_RecursiveDerefZdd( dd, zRes );
                    return NULL;
                }
                cuddRef( zPlus );
                Cudd_RecursiveDeref( dd, bVarsExtra );
 
                // add these to the result
                zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
                if ( zRes == NULL )
                {
                    Cudd_RecursiveDerefZdd( dd, zTemp );
                    Cudd_RecursiveDerefZdd( dd, zPlus );
                    return NULL;
                }
                cuddRef( zRes );
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
            }
        }
        cuddDeref( zRes );
 
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes);
        return zRes;
    }
} /* end of extraZddSymmPairsCompute */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddTuplesFromBdd()

DdNode * extraZddTuplesFromBdd ( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN )

extern

Function********************************************************************

Synopsis [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]

Description [Generates in a bottom-up fashion ZDD for all combinations composed of k variables out of variables belonging to Support.]

SideEffects []

SeeAlso []

Definition at line 1341 of file extraBddSymm.c.

{
    DdNode *zRes, *zRes0, *zRes1;
    statLine(dd); 
 
    /* terminal cases */
/*  if ( k < 0 || k > n )
 *      return dd->zero;
 *  if ( n == 0 )
 *      return dd->one; 
 */
    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
        return z0;
    if ( bVarsN == b1 )
        return z1;
 
    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
    if (zRes)
        return(zRes);
 
    /* ZDD in which this variable is 0 */
/*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */
    zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
    if ( zRes0 == NULL ) 
        return NULL;
    cuddRef( zRes0 );
 
    /* ZDD in which this variable is 1 */
/*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */
    if ( bVarsK == b1 )
    {
        zRes1 = z0;
        cuddRef( zRes1 );
    }
    else
    {
        zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
        if ( zRes1 == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            return NULL;
        }
        cuddRef( zRes1 );
    }
 
    /* compose Res0 and Res1 with the given ZDD variable */
    zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
    if ( zRes == NULL ) 
    {
        Cudd_RecursiveDerefZdd( dd, zRes0 );
        Cudd_RecursiveDerefZdd( dd, zRes1 );
        return NULL;
    }
    cuddDeref( zRes0 );
    cuddDeref( zRes1 );
 
    /* insert the result into cache */
    cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
    return zRes;
 
} /* end of extraZddTuplesFromBdd */

Here is the call graph for this function:

Here is the caller graph for this function:

extraZddUnateInfoCompute()

DdNode * extraZddUnateInfoCompute ( DdManager * dd, DdNode * bFunc, DdNode * bVars )

extern

Function********************************************************************

Synopsis [Performs a recursive step of Extra_UnateInfoCompute.]

Description [Returns the set of symmetric variable pairs represented as a set of two-literal ZDD cubes. Both variables always appear in the positive polarity in the cubes. This function works without building new BDD nodes. Some relatively small number of ZDD nodes may be built to ensure proper bookkeeping of the symmetry information.]

SideEffects []

SeeAlso []

Definition at line 385 of file extraBddUnate.c.

{
    DdNode * zRes;
    DdNode * bFR = Cudd_Regular(bFunc); 
 
    if ( cuddIsConstant(bFR) )
    {
        if ( cuddIsConstant(bVars) )
            return z0;
        return extraZddGetSingletonsBoth( dd, bVars );
    }
    assert( bVars != b1 );
 
    if ( (zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars)) )
        return zRes;
    else
    {
        DdNode * zRes0, * zRes1;
        DdNode * zTemp, * zPlus;             
        DdNode * bF0, * bF1;             
        DdNode * bVarsNew;
        int nVarsExtra;
        int LevelF;
        int AddVar;
 
        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
        // count how many extra vars are there in bVars
        nVarsExtra = 0;
        LevelF = dd->perm[bFR->index];
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
            nVarsExtra++; 
        // the indexes (level) of variables should be synchronized now
        assert( bFR->index == bVarsNew->index );
 
        // cofactor the function
        if ( bFR != bFunc ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }
 
        // solve subproblems
        zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) );
        if ( zRes0 == NULL )
            return NULL;
        cuddRef( zRes0 );
 
        // if there is no symmetries in the negative cofactor
        // there is no need to test the positive cofactor
        if ( zRes0 == z0 )
            zRes = zRes0;  // zRes takes reference
        else
        {
            zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) );
            if ( zRes1 == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                return NULL;
            }
            cuddRef( zRes1 );
 
            // only those variables are pair-wise symmetric 
            // that are pair-wise symmetric in both cofactors
            // therefore, intersect the solutions
            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zRes0 );
                Cudd_RecursiveDerefZdd( dd, zRes1 );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            Cudd_RecursiveDerefZdd( dd, zRes1 );
        }
 
        // consider the current top-most variable
        AddVar = -1;
        if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos
            AddVar = 0;
        else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg
            AddVar = 1;
        if ( AddVar >= 0 )
        {
            // create the singleton
            zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );
 
            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        // only zRes is referenced at this point
 
        // if we skipped some variables, these variables cannot be symmetric with
        // any variables that are currently in the support of bF, but they can be 
        // symmetric with the variables that are in bVars but not in the support of bF
        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
        {
            // create the negative singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );
 
            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        
 
            // create the positive singleton
            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
            if ( zPlus == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zRes );
                return NULL;
            }
            cuddRef( zPlus );
 
            // add these to the result
            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
            if ( zRes == NULL )
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                Cudd_RecursiveDerefZdd( dd, zPlus );
                return NULL;
            }
            cuddRef( zRes );
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
        }
        cuddDeref( zRes );
 
        /* insert the result into cache */
        cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes);
        return zRes;
    }
} /* end of extraZddUnateInfoCompute */

Here is the call graph for this function:

Here is the caller graph for this function: