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

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

#include "extra.h"

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

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

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

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

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


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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

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


/*
    LinearSpace(f) = Space(f,f)

    Space(f,g)
	{
		if ( f = const )
		{ 
		    if ( f = g )  return 1;
			else          return 0;
		}
		if ( g = const )  return 0;
		return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx');
	}

	Equations(s) = Pos(s) + Neg(s);

	Pos(s)
	{
		if ( s  = 0 )   return 1;
		if ( s  = 1 )   return 0;
		if ( sx'= 0 )   return Pos(sx) + x;
		if ( sx = 0 )   return Pos(sx');
		return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)];
	}

	Neg(s)
	{
		if ( s  = 0 )   return 1;
		if ( s  = 1 )   return 0;
		if ( sx'= 0 )   return Neg(sx);
		if ( sx = 0 )   return Neg(sx') + x;
		return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)];
	}


    SpaceP(A)
	{
		if ( A = 0 )    return 1;
		if ( A = 1 )    return 1;
		return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax);
	}

    SpaceN(A)
	{
		if ( A = 0 )    return 1;
		if ( A = 1 )    return 0;
		return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax);
	}


    LinInd(A)
	{
		if ( A = const )     return 1;
		if ( !LinInd(Ax') )  return 0;
		if ( !LinInd(Ax)  )  return 0;
		if (  LinSumOdd(Ax')  & LinSumEven(Ax) != 0 )  return 0;
		if (  LinSumEven(Ax') & LinSumEven(Ax) != 0 )  return 0;
		return 1;
	}

	LinSumOdd(A)
	{
		if ( A = 0 )    return 0;                 // Odd0  ---e-- Odd1
		if ( A = 1 )    return 1;                 //       \   o
		Odd0  = LinSumOdd(Ax');  // x is absent   //         \ 
		Even0 = LinSumEven(Ax'); // x is absent   //       /   o  
		Odd1  = LinSumOdd(Ax);   // x is present  // Even0 ---e-- Even1 
		Even1 = LinSumEven(Ax);  // x is absent
		return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)];
	}

	LinSumEven(A)
	{
		if ( A = 0 )    return 0;
		if ( A = 1 )    return 0;
		Odd0  = LinSumOdd(Ax');  // x is absent
		Even0 = LinSumEven(Ax'); // x is absent
		Odd1  = LinSumOdd(Ax);   // x is present
		Even1 = LinSumEven(Ax);  // x is absent
		return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)];
	}
	
*/

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
{
	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 = 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 )
	{
		fprintf(outStream,  "Cannot derive linear space, because DD manager does not have enough variables.\n" );
		fflush( outStream );
		free( pSupport );
		return NULL;
	}

	// create the permutation arrays
	pPermute     = ALLOC( int, dd->size );
	pPermuteBack = ALLOC( int, dd->size );
	pCompose     = 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] );
	free( pPermute );
	free( pPermuteBack );
	free( pCompose );
    free( pSupport );

	Cudd_Deref( bSpace );
	return bSpace;
}



/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars )
{
	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;
}



/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace )
{
    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;
}


/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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


/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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


/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

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

/**Function*************************************************************

  Synopsis    [Counts the number of literals in one combination.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb )
{
	int Counter;
	if ( zComb == z0 )
		return 0;
	Counter = 0;
	for ( ; zComb != z1; zComb = cuddT(zComb) )
		Counter++;
	return Counter;
}

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

***********************************************************************/
DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations )
{
	DdNode ** pzRes;
	int * pVarsNonCan;
	DdNode * zEquRem;
	int iVarNonCan;
	DdNode * zExor, * zTemp;

	// get the set of non-canonical variables
	pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
	Extra_SupportArray( dd, bFuncRed, pVarsNonCan );

	// allocate storage for the EXOR sets
	pzRes = 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 );

	free( pVarsNonCan );
	return pzRes;
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Performs the recursive steps of Extra_bddSpaceFromFunction.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
{
	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)bF > (unsigned)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 */



/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF )
{
	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;
	}
}



/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF )
{
	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;
	}
}



/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
{
	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;
	}
}

/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF )
{
	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;
	}
}


/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF )
{
	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;
	}
}




/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA )
{
	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;
	}
}


/**Function*************************************************************

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

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA )
{
	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;
	}
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

