extrabddkmap.c

主要进行大规模的电路综合

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



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

******************************************************************************/
void Extra_PrintKMapRelation( 
  FILE * Output,  /* the output stream */
  DdManager * dd, 
  DdNode * OnSet, 
  DdNode * OffSet, 
  int nXVars, 
  int nYVars, 
  DdNode ** XVars, 
  DdNode ** YVars ) /* the flag which determines how support is computed */
{
	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 );					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 );	    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" );
		}
	}
}



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

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int GrayCode ( int BinCode )
{
  return BinCode ^ ( BinCode >> 1 );
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
int BinCode ( int GrayCode )
{
  int bc = GrayCode;
  while( GrayCode >>= 1 ) bc ^= GrayCode;
  return bc;
}