| /**CFile**************************************************************** |
| |
| FileName [extraBddKmap.c] |
| |
| PackageName [extra] |
| |
| Synopsis [Visualizing the K-map.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 2.0. Started - September 1, 2003.] |
| |
| Revision [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| /// K-map visualization using pseudo graphics /// |
| /// Version 1.0. Started - August 20, 2000 /// |
| /// Version 2.0. Added to EXTRA - July 17, 2001 /// |
| |
| #include "extraBdd.h" |
| |
| #ifdef WIN32 |
| #include <windows.h> |
| #endif |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Constant declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| // the maximum number of variables in the Karnaugh Map |
| #define MAXVARS 20 |
| |
| /* |
| // single line |
| #define SINGLE_VERTICAL (char)179 |
| #define SINGLE_HORIZONTAL (char)196 |
| #define SINGLE_TOP_LEFT (char)218 |
| #define SINGLE_TOP_RIGHT (char)191 |
| #define SINGLE_BOT_LEFT (char)192 |
| #define SINGLE_BOT_RIGHT (char)217 |
| |
| // double line |
| #define DOUBLE_VERTICAL (char)186 |
| #define DOUBLE_HORIZONTAL (char)205 |
| #define DOUBLE_TOP_LEFT (char)201 |
| #define DOUBLE_TOP_RIGHT (char)187 |
| #define DOUBLE_BOT_LEFT (char)200 |
| #define DOUBLE_BOT_RIGHT (char)188 |
| |
| // line intersections |
| #define SINGLES_CROSS (char)197 |
| #define DOUBLES_CROSS (char)206 |
| #define S_HOR_CROSS_D_VER (char)215 |
| #define S_VER_CROSS_D_HOR (char)216 |
| |
| // single line joining |
| #define S_JOINS_S_VER_LEFT (char)180 |
| #define S_JOINS_S_VER_RIGHT (char)195 |
| #define S_JOINS_S_HOR_TOP (char)193 |
| #define S_JOINS_S_HOR_BOT (char)194 |
| |
| // double line joining |
| #define D_JOINS_D_VER_LEFT (char)185 |
| #define D_JOINS_D_VER_RIGHT (char)204 |
| #define D_JOINS_D_HOR_TOP (char)202 |
| #define D_JOINS_D_HOR_BOT (char)203 |
| |
| // single line joining double line |
| #define S_JOINS_D_VER_LEFT (char)182 |
| #define S_JOINS_D_VER_RIGHT (char)199 |
| #define S_JOINS_D_HOR_TOP (char)207 |
| #define S_JOINS_D_HOR_BOT (char)209 |
| */ |
| |
| // single line |
| #define SINGLE_VERTICAL (char)'|' |
| #define SINGLE_HORIZONTAL (char)'-' |
| #define SINGLE_TOP_LEFT (char)'+' |
| #define SINGLE_TOP_RIGHT (char)'+' |
| #define SINGLE_BOT_LEFT (char)'+' |
| #define SINGLE_BOT_RIGHT (char)'+' |
| |
| // double line |
| #define DOUBLE_VERTICAL (char)'|' |
| #define DOUBLE_HORIZONTAL (char)'-' |
| #define DOUBLE_TOP_LEFT (char)'+' |
| #define DOUBLE_TOP_RIGHT (char)'+' |
| #define DOUBLE_BOT_LEFT (char)'+' |
| #define DOUBLE_BOT_RIGHT (char)'+' |
| |
| // line intersections |
| #define SINGLES_CROSS (char)'+' |
| #define DOUBLES_CROSS (char)'+' |
| #define S_HOR_CROSS_D_VER (char)'+' |
| #define S_VER_CROSS_D_HOR (char)'+' |
| |
| // single line joining |
| #define S_JOINS_S_VER_LEFT (char)'+' |
| #define S_JOINS_S_VER_RIGHT (char)'+' |
| #define S_JOINS_S_HOR_TOP (char)'+' |
| #define S_JOINS_S_HOR_BOT (char)'+' |
| |
| // double line joining |
| #define D_JOINS_D_VER_LEFT (char)'+' |
| #define D_JOINS_D_VER_RIGHT (char)'+' |
| #define D_JOINS_D_HOR_TOP (char)'+' |
| #define D_JOINS_D_HOR_BOT (char)'+' |
| |
| // single line joining double line |
| #define S_JOINS_D_VER_LEFT (char)'+' |
| #define S_JOINS_D_VER_RIGHT (char)'+' |
| #define S_JOINS_D_HOR_TOP (char)'+' |
| #define S_JOINS_D_HOR_BOT (char)'+' |
| |
| |
| // other symbols |
| #define UNDERSCORE (char)95 |
| //#define SYMBOL_ZERO (char)248 // degree sign |
| //#define SYMBOL_ZERO (char)'o' |
| #ifdef WIN32 |
| #define SYMBOL_ZERO (char)'0' |
| #else |
| #define SYMBOL_ZERO (char)' ' |
| #endif |
| #define SYMBOL_ONE (char)'1' |
| #define SYMBOL_DC (char)'-' |
| #define SYMBOL_OVERLAP (char)'?' |
| |
| // full cells and half cells |
| #define CELL_FREE (char)32 |
| #define CELL_FULL (char)219 |
| #define HALF_UPPER (char)223 |
| #define HALF_LOWER (char)220 |
| #define HALF_LEFT (char)221 |
| #define HALF_RIGHT (char)222 |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Structure declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Type declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Variable declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| // the array of BDD variables used internally |
| static DdNode * s_XVars[MAXVARS]; |
| |
| // flag which determines where the horizontal variable names are printed |
| static int fHorizontalVarNamesPrintedAbove = 1; |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Macro declarations */ |
| /*---------------------------------------------------------------------------*/ |
| |
| |
| /**AutomaticStart*************************************************************/ |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Static function prototypes */ |
| /*---------------------------------------------------------------------------*/ |
| |
| // Oleg's way of generating the gray code |
| static int GrayCode( int BinCode ); |
| static int BinCode ( int GrayCode ); |
| |
| /**AutomaticEnd***************************************************************/ |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* Definition of exported functions */ |
| /*---------------------------------------------------------------------------*/ |
| |
| |
| /**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 [] |
| |
| ******************************************************************************/ |
| void Extra_PrintKMap( |
| FILE * Output, /* the output stream */ |
| DdManager * dd, |
| DdNode * OnSet, |
| DdNode * OffSet, |
| int nVars, |
| DdNode ** XVars, |
| int fSuppType, /* the flag which determines how support is computed */ |
| char ** pVarNames ) |
| { |
| 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" ); |
| } |
| } |
| } |
| |
| |
| |
| /**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, 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" ); |
| } |
| } |
| } |
| |
| |
| |
| /*---------------------------------------------------------------------------*/ |
| /* 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; |
| } |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
