#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"

Data Structures
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) ((ABC_PTRUINT_T)(a) % TSIZE)

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

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

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

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

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

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)

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

#define a0 (dd)->zero

Definition at line 79 of file extraBdd.h.

#define a1 (dd)->one

Definition at line 80 of file extraBdd.h.

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

Definition at line 200 of file extraBdd.h.

#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.

#define b1 (dd)->one

Definition at line 76 of file extraBdd.h.

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

Definition at line 83 of file extraBdd.h.

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

Definition at line 86 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)

Definition at line 89 of file extraBdd.h.

#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)

DD_P3

#define DD_P3

Definition: cuddInt.h:157

DD_P2

#define DD_P2

Definition: cuddInt.h:156

DD_P1

#define DD_P1

Definition: cuddInt.h:155

Definition at line 92 of file extraBdd.h.

#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)

DD_P3

#define DD_P3

Definition: cuddInt.h:157

DD_P2

#define DD_P2

Definition: cuddInt.h:156

DD_P1

#define DD_P1

Definition: cuddInt.h:155

Definition at line 96 of file extraBdd.h.

#define z0 (dd)->zero

Definition at line 77 of file extraBdd.h.

#define z1 (dd)->one

Definition at line 78 of file extraBdd.h.

Typedef Documentation

typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t

Definition at line 155 of file extraBdd.h.

typedef struct Extra_ImageTree_t_ Extra_ImageTree_t

Definition at line 146 of file extraBdd.h.

typedef struct Extra_SymmInfo_t_ Extra_SymmInfo_t

Definition at line 212 of file extraBdd.h.

typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t

Definition at line 276 of file extraBdd.h.

typedef struct Extra_UnateVar_t_ Extra_UnateVar_t

Definition at line 269 of file extraBdd.h.

Function Documentation

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

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 */

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

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 );
 }

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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;
 }

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

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;
 }

DdNode* Extra_bddCreateAnd	(	DdManager *	dd,
		int	nVars
	)

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;
 }

DdNode* Extra_bddCreateExor	(	DdManager *	dd,
		int	nVars
	)

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;
 }

DdNode* Extra_bddCreateOr	(	DdManager *	dd,
		int	nVars
	)

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;
 }

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

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 */

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

DdNode* Extra_bddImageRead ( Extra_ImageTree_t * pTree )

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

Synopsis [Reads the image from the tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file extraBddImage.c.

 {
     return pTree->pRoot->bImage;
 }

DdNode* Extra_bddImageRead2 ( Extra_ImageTree2_t * pTree )

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

Synopsis [Returns the previously computed image.]

Description []

SideEffects []

SeeAlso []

Definition at line 1150 of file extraBddImage.c.

 {
     return pTree->bImage;
 }

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

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;
 }

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

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;
 }

void Extra_bddImageTreeDelete ( Extra_ImageTree_t * pTree )

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 );
 }

void Extra_bddImageTreeDelete2 ( Extra_ImageTree2_t * pTree )

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 );
 }

int Extra_bddIsVar ( DdNode * bFunc )

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)) );
 }

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

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 */

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

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 */

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

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 */

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

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 */

void Extra_bddPrint	(	DdManager *	dd,
		DdNode *	F
	)

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");
 }

void Extra_bddPrintSupport	(	DdManager *	dd,
		DdNode *	F
	)

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 );
 }

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

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 */

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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;
 }

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

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. */
     ddSupportStep( Cudd_Regular( f ), support );
     ddClearFlag( 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 */

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

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;
 }

int Extra_bddSuppSize	(	DdManager *	dd,
		DdNode *	bSupp
	)

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;
 }

int Extra_bddVarIsInCube	(	DdNode *	bCube,
		int	iVar
	)

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;
 }

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

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" );
         }
     }
 }

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

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" );
         }
     }
 }

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

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 */

void Extra_StopManager ( DdManager * dd )

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 );
 }

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

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. */
     ddSupportStep(Cudd_Regular(f),support);
     ddClearFlag(Cudd_Regular(f));
 
     return(support);
 
 } /* end of Extra_SupportArray */

Extra_SymmInfo_t* Extra_SymmPairsAllocate ( int nVars )

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 */

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

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 */

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

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 */

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

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 */

void Extra_SymmPairsDissolve ( Extra_SymmInfo_t * p )

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 */

void Extra_SymmPairsPrint ( Extra_SymmInfo_t * p )

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 */

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

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;
 }

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

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 */

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

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_UnateInfo_t* Extra_UnateComputeFast	(	DdManager *	dd,
		DdNode *	bFunc
	)

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 */

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

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 */

Extra_UnateInfo_t* Extra_UnateInfoAllocate ( int nVars )

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 */

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

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 */

void Extra_UnateInfoDissolve ( Extra_UnateInfo_t * p )

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 */

void Extra_UnateInfoPrint ( Extra_UnateInfo_t * p )

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, ' ', 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 */

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

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++ )
         ddSupportStep( Cudd_Regular(F[i]), support );
     for ( i = 0; i < n; i++ )
         ddClearFlag( Cudd_Regular(F[i]) );
 
     return support;
 }

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1772 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 */

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

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 */

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

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 */

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

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 */

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

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;
     }
 }

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

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;
     }
 }

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

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;
     }
 }

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

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 */

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

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;
     }
 }

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

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;
     }
 }

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

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;
     }
 }

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

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;
     }
 }

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

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

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 */

Data Structures

Macros

Typedefs

Functions

Macro Definition Documentation

Typedef Documentation

Function Documentation