src/misc/extra/extraBddKmap.c File Reference

#include "extra.h"
Include dependency graph for extraBddKmap.c:

Go to the source code of this file.

Defines

#define MAXVARS   20
#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)'+'
#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)'+'
#define SINGLES_CROSS   (char)'+'
#define DOUBLES_CROSS   (char)'+'
#define S_HOR_CROSS_D_VER   (char)'+'
#define S_VER_CROSS_D_HOR   (char)'+'
#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)'+'
#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)'+'
#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)'+'
#define UNDERSCORE   (char)95
#define SYMBOL_ZERO   (char)' '
#define SYMBOL_ONE   (char)'1'
#define SYMBOL_DC   (char)'-'
#define SYMBOL_OVERLAP   (char)'?'
#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

Functions

static int GrayCode (int BinCode)
static int BinCode (int GrayCode)
void Extra_PrintKMap (FILE *Output, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nVars, DdNode **XVars, int fSuppType, char **pVarNames)
void Extra_PrintKMapRelation (FILE *Output, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nXVars, int nYVars, DdNode **XVars, DdNode **YVars)

Variables

static DdNode * s_XVars [MAXVARS]
static int fHorizontalVarNamesPrintedAbove = 1

Define Documentation

#define CELL_FREE   (char)32

Definition at line 125 of file extraBddKmap.c.

#define CELL_FULL   (char)219

Definition at line 126 of file extraBddKmap.c.

#define D_JOINS_D_HOR_BOT   (char)'+'

Definition at line 106 of file extraBddKmap.c.

#define D_JOINS_D_HOR_TOP   (char)'+'

Definition at line 105 of file extraBddKmap.c.

#define D_JOINS_D_VER_LEFT   (char)'+'

Definition at line 103 of file extraBddKmap.c.

#define D_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 104 of file extraBddKmap.c.

#define DOUBLE_BOT_LEFT   (char)'+'

Definition at line 87 of file extraBddKmap.c.

#define DOUBLE_BOT_RIGHT   (char)'+'

Definition at line 88 of file extraBddKmap.c.

#define DOUBLE_HORIZONTAL   (char)'-'

Definition at line 84 of file extraBddKmap.c.

#define DOUBLE_TOP_LEFT   (char)'+'

Definition at line 85 of file extraBddKmap.c.

#define DOUBLE_TOP_RIGHT   (char)'+'

Definition at line 86 of file extraBddKmap.c.

#define DOUBLE_VERTICAL   (char)'|'

Definition at line 83 of file extraBddKmap.c.

#define DOUBLES_CROSS   (char)'+'

Definition at line 92 of file extraBddKmap.c.

#define HALF_LEFT   (char)221

Definition at line 129 of file extraBddKmap.c.

#define HALF_LOWER   (char)220

Definition at line 128 of file extraBddKmap.c.

#define HALF_RIGHT   (char)222

Definition at line 130 of file extraBddKmap.c.

#define HALF_UPPER   (char)223

Definition at line 127 of file extraBddKmap.c.

#define MAXVARS   20

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

Definition at line 30 of file extraBddKmap.c.

#define S_HOR_CROSS_D_VER   (char)'+'

Definition at line 93 of file extraBddKmap.c.

#define S_JOINS_D_HOR_BOT   (char)'+'

Definition at line 112 of file extraBddKmap.c.

#define S_JOINS_D_HOR_TOP   (char)'+'

Definition at line 111 of file extraBddKmap.c.

#define S_JOINS_D_VER_LEFT   (char)'+'

Definition at line 109 of file extraBddKmap.c.

#define S_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 110 of file extraBddKmap.c.

#define S_JOINS_S_HOR_BOT   (char)'+'

Definition at line 100 of file extraBddKmap.c.

#define S_JOINS_S_HOR_TOP   (char)'+'

Definition at line 99 of file extraBddKmap.c.

#define S_JOINS_S_VER_LEFT   (char)'+'

Definition at line 97 of file extraBddKmap.c.

#define S_JOINS_S_VER_RIGHT   (char)'+'

Definition at line 98 of file extraBddKmap.c.

#define S_VER_CROSS_D_HOR   (char)'+'

Definition at line 94 of file extraBddKmap.c.

#define SINGLE_BOT_LEFT   (char)'+'

Definition at line 79 of file extraBddKmap.c.

#define SINGLE_BOT_RIGHT   (char)'+'

Definition at line 80 of file extraBddKmap.c.

#define SINGLE_HORIZONTAL   (char)'-'

Definition at line 76 of file extraBddKmap.c.

#define SINGLE_TOP_LEFT   (char)'+'

Definition at line 77 of file extraBddKmap.c.

#define SINGLE_TOP_RIGHT   (char)'+'

Definition at line 78 of file extraBddKmap.c.

#define SINGLE_VERTICAL   (char)'|'

Definition at line 75 of file extraBddKmap.c.

#define SINGLES_CROSS   (char)'+'

Definition at line 91 of file extraBddKmap.c.

#define SYMBOL_DC   (char)'-'

Definition at line 121 of file extraBddKmap.c.

#define SYMBOL_ONE   (char)'1'

Definition at line 120 of file extraBddKmap.c.

#define SYMBOL_OVERLAP   (char)'?'

Definition at line 122 of file extraBddKmap.c.

#define SYMBOL_ZERO   (char)' '

Definition at line 119 of file extraBddKmap.c.

#define UNDERSCORE   (char)95

Definition at line 116 of file extraBddKmap.c.

Function Documentation

int BinCode ( int  GrayCode  )  [static]

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 776 of file extraBddKmap.c.

00777 {
00778   int bc = GrayCode;
00779   while( GrayCode >>= 1 ) bc ^= GrayCode;
00780   return bc;
00781 }

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 190 of file extraBddKmap.c.

00199 {
00200     int d, p, n, s, v, h, w;
00201     int nVarsVer;
00202     int nVarsHor;
00203     int nCellsVer;
00204     int nCellsHor;
00205     int nSkipSpaces;
00206 
00207     // make sure that on-set and off-set do not overlap
00208     if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
00209     {
00210         fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
00211         return;
00212     }
00213 /*
00214     if ( OnSet == b1 )
00215     {
00216         fprintf( Output, "PrintKMap(): Constant 1\n" );
00217         return;
00218     }
00219     if ( OffSet == b1 )
00220     {
00221         fprintf( Output, "PrintKMap(): Constant 0\n" );
00222         return;
00223     }
00224 */
00225     if ( nVars < 0 || nVars > MAXVARS )
00226     {
00227         fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
00228         return;
00229     }
00230 
00231     // determine the support if it is not given
00232     if ( XVars == NULL )
00233     {
00234         if ( fSuppType == 0 )
00235         {   // assume that the support includes the first nVars of the manager
00236             assert( nVars );
00237             for ( v = 0; v < nVars; v++ )
00238                 s_XVars[v] = Cudd_bddIthVar( dd, v );
00239         }
00240         else if ( fSuppType == 1 )
00241         {   // assume that the support includes the topmost nVars of the manager
00242             assert( nVars );
00243             for ( v = 0; v < nVars; v++ )
00244                 s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
00245         }
00246         else // determine the support
00247         {
00248             DdNode * SuppOn, * SuppOff, * Supp;
00249             int cVars = 0;
00250             DdNode * TempSupp;
00251 
00252             // determine support
00253             SuppOn = Cudd_Support( dd, OnSet );         Cudd_Ref( SuppOn );
00254             SuppOff = Cudd_Support( dd, OffSet );       Cudd_Ref( SuppOff );
00255             Supp = Cudd_bddAnd( dd, SuppOn, SuppOff );  Cudd_Ref( Supp );
00256             Cudd_RecursiveDeref( dd, SuppOn );
00257             Cudd_RecursiveDeref( dd, SuppOff );
00258 
00259             nVars = Cudd_SupportSize( dd, Supp );
00260             if ( nVars > MAXVARS )
00261             {
00262                 fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
00263                 Cudd_RecursiveDeref( dd, Supp );
00264                 return;
00265             }
00266 
00267             // assign variables
00268             for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
00269                 s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );
00270 
00271             Cudd_RecursiveDeref( dd, TempSupp );
00272         }
00273     }
00274     else
00275     {
00276         // copy variables
00277         assert( XVars );
00278         for ( v = 0; v < nVars; v++ )
00279             s_XVars[v] = XVars[v];
00280     }
00281 
00283     // determine the Karnaugh map parameters
00284     nVarsVer = nVars/2;
00285     nVarsHor = nVars - nVarsVer;
00286     nCellsVer = (1<<nVarsVer);
00287     nCellsHor = (1<<nVarsHor);
00288     nSkipSpaces = nVarsVer + 1;
00289 
00291     // print variable names
00292     fprintf( Output, "\n" );
00293     for ( w = 0; w < nVarsVer; w++ )
00294         if ( pVarNames == NULL )
00295             fprintf( Output, "%c", 'a'+nVarsHor+w );
00296         else
00297             fprintf( Output, " %s", pVarNames[nVarsHor+w] );
00298 
00299     if ( fHorizontalVarNamesPrintedAbove )
00300     {
00301         fprintf( Output, " \\ " );
00302         for ( w = 0; w < nVarsHor; w++ )
00303             if ( pVarNames == NULL )
00304                 fprintf( Output, "%c", 'a'+w );
00305             else
00306                 fprintf( Output, "%s ", pVarNames[w] );
00307     }
00308     fprintf( Output, "\n" );
00309 
00310     if ( fHorizontalVarNamesPrintedAbove )
00311     {
00313         // print horizontal digits
00314         for ( d = 0; d < nVarsHor; d++ )
00315         {
00316             for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
00317             for ( n = 0; n < nCellsHor; n++ )
00318                 if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
00319                     fprintf( Output, "1   " );
00320                 else
00321                     fprintf( Output, "0   " );
00322             fprintf( Output, "\n" );
00323         }
00324     }
00325 
00327     // print the upper line
00328     for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00329     fprintf( Output, "%c", DOUBLE_TOP_LEFT );
00330     for ( s = 0; s < nCellsHor; s++ )
00331     {
00332         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00333         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00334         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00335         if ( s != nCellsHor-1 )
00336             if ( s&1 )
00337                 fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
00338             else
00339                 fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
00340     }
00341     fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
00342     fprintf( Output, "\n" );
00343 
00345     // print the map
00346     for ( v = 0; v < nCellsVer; v++ )
00347     {
00348         DdNode * CubeVerBDD;
00349 
00350         // print horizontal digits
00351 //      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00352         for ( n = 0; n < nVarsVer; n++ )
00353             if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
00354                 fprintf( Output, "1" );
00355             else
00356                 fprintf( Output, "0" );
00357         fprintf( Output, " " );
00358 
00359         // find vertical cube
00360         CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 );    Cudd_Ref( CubeVerBDD );
00361 
00362         // print text line
00363         fprintf( Output, "%c", DOUBLE_VERTICAL );
00364         for ( h = 0; h < nCellsHor; h++ )
00365         {
00366             DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
00367 
00368             fprintf( Output, " " );
00369 //          fprintf( Output, "x" );
00371             // determine what should be printed
00372             CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 );    Cudd_Ref( CubeHorBDD );
00373             Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                   Cudd_Ref( Prod );
00374             Cudd_RecursiveDeref( dd, CubeHorBDD );
00375 
00376             ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
00377             ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
00378             Cudd_RecursiveDeref( dd, Prod );
00379 
00380             if ( ValueOnSet == b1 && ValueOffSet == b0 )
00381                 fprintf( Output, "%c", SYMBOL_ONE );
00382             else if ( ValueOnSet == b0 && ValueOffSet == b1 )
00383                 fprintf( Output, "%c", SYMBOL_ZERO );
00384             else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
00385                 fprintf( Output, "%c", SYMBOL_DC );
00386             else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
00387                 fprintf( Output, "%c", SYMBOL_OVERLAP );
00388             else
00389                 assert(0);
00390 
00391             Cudd_RecursiveDeref( dd, ValueOnSet );
00392             Cudd_RecursiveDeref( dd, ValueOffSet );
00394             fprintf( Output, " " );
00395 
00396             if ( h != nCellsHor-1 )
00397                 if ( h&1 )
00398                     fprintf( Output, "%c", DOUBLE_VERTICAL );
00399                 else
00400                     fprintf( Output, "%c", SINGLE_VERTICAL );
00401         }
00402         fprintf( Output, "%c", DOUBLE_VERTICAL );
00403         fprintf( Output, "\n" );
00404 
00405         Cudd_RecursiveDeref( dd, CubeVerBDD );
00406 
00407         if ( v != nCellsVer-1 )
00408         // print separator line
00409         {
00410             for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00411             if ( v&1 )
00412             {
00413                 fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
00414                 for ( s = 0; s < nCellsHor; s++ )
00415                 {
00416                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00417                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00418                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00419                     if ( s != nCellsHor-1 )
00420                         if ( s&1 )
00421                             fprintf( Output, "%c", DOUBLES_CROSS );
00422                         else
00423                             fprintf( Output, "%c", S_VER_CROSS_D_HOR );
00424                 }
00425                 fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
00426             }
00427             else
00428             {
00429                 fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
00430                 for ( s = 0; s < nCellsHor; s++ )
00431                 {
00432                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00433                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00434                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00435                     if ( s != nCellsHor-1 )
00436                         if ( s&1 )
00437                             fprintf( Output, "%c", S_HOR_CROSS_D_VER );
00438                         else
00439                             fprintf( Output, "%c", SINGLES_CROSS );
00440                 }
00441                 fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
00442             }
00443             fprintf( Output, "\n" );
00444         }
00445     }
00446     
00448     // print the lower line
00449     for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00450     fprintf( Output, "%c", DOUBLE_BOT_LEFT );
00451     for ( s = 0; s < nCellsHor; s++ )
00452     {
00453         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00454         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00455         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00456         if ( s != nCellsHor-1 )
00457             if ( s&1 )
00458                 fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
00459             else
00460                 fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
00461     }
00462     fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
00463     fprintf( Output, "\n" );
00464 
00465     if ( !fHorizontalVarNamesPrintedAbove )
00466     {
00468         // print horizontal digits
00469         for ( d = 0; d < nVarsHor; d++ )
00470         {
00471             for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
00472             for ( n = 0; n < nCellsHor; n++ )
00473                 if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
00474                     fprintf( Output, "1   " );
00475                 else
00476                     fprintf( Output, "0   " );
00477 
00479             fprintf( Output, "%c", (char)('a'+d) );
00481             fprintf( Output, "\n" );
00482         }
00483     }
00484 }

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 500 of file extraBddKmap.c.

00509 {
00510     int d, p, n, s, v, h, w;
00511     int nVars;
00512     int nVarsVer;
00513     int nVarsHor;
00514     int nCellsVer;
00515     int nCellsHor;
00516     int nSkipSpaces;
00517 
00518     // make sure that on-set and off-set do not overlap
00519     if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
00520     {
00521         fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
00522         return;
00523     }
00524 
00525     if ( OnSet == b1 )
00526     {
00527         fprintf( Output, "PrintKMap(): Constant 1\n" );
00528         return;
00529     }
00530     if ( OffSet == b1 )
00531     {
00532         fprintf( Output, "PrintKMap(): Constant 0\n" );
00533         return;
00534     }
00535 
00536     nVars = nXVars + nYVars;
00537     if ( nVars < 0 || nVars > MAXVARS )
00538     {
00539         fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
00540         return;
00541     }
00542 
00543 
00545     // determine the Karnaugh map parameters
00546     nVarsVer = nXVars;
00547     nVarsHor = nYVars;
00548     nCellsVer = (1<<nVarsVer);
00549     nCellsHor = (1<<nVarsHor);
00550     nSkipSpaces = nVarsVer + 1;
00551 
00553     // print variable names
00554     fprintf( Output, "\n" );
00555     for ( w = 0; w < nVarsVer; w++ )
00556         fprintf( Output, "%c", 'a'+nVarsHor+w );
00557     if ( fHorizontalVarNamesPrintedAbove )
00558     {
00559         fprintf( Output, " \\ " );
00560         for ( w = 0; w < nVarsHor; w++ )
00561             fprintf( Output, "%c", 'a'+w );
00562     }
00563     fprintf( Output, "\n" );
00564 
00565     if ( fHorizontalVarNamesPrintedAbove )
00566     {
00568         // print horizontal digits
00569         for ( d = 0; d < nVarsHor; d++ )
00570         {
00571             for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
00572             for ( n = 0; n < nCellsHor; n++ )
00573                 if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
00574                     fprintf( Output, "1   " );
00575                 else
00576                     fprintf( Output, "0   " );
00577             fprintf( Output, "\n" );
00578         }
00579     }
00580 
00582     // print the upper line
00583     for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00584     fprintf( Output, "%c", DOUBLE_TOP_LEFT );
00585     for ( s = 0; s < nCellsHor; s++ )
00586     {
00587         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00588         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00589         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00590         if ( s != nCellsHor-1 )
00591             if ( s&1 )
00592                 fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
00593             else
00594                 fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
00595     }
00596     fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
00597     fprintf( Output, "\n" );
00598 
00600     // print the map
00601     for ( v = 0; v < nCellsVer; v++ )
00602     {
00603         DdNode * CubeVerBDD;
00604 
00605         // print horizontal digits
00606 //      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00607         for ( n = 0; n < nVarsVer; n++ )
00608             if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
00609                 fprintf( Output, "1" );
00610             else
00611                 fprintf( Output, "0" );
00612         fprintf( Output, " " );
00613 
00614         // find vertical cube
00615 //      CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor );    Cudd_Ref( CubeVerBDD );
00616         CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 );                 Cudd_Ref( CubeVerBDD );
00617 
00618         // print text line
00619         fprintf( Output, "%c", DOUBLE_VERTICAL );
00620         for ( h = 0; h < nCellsHor; h++ )
00621         {
00622             DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
00623 
00624             fprintf( Output, " " );
00625 //          fprintf( Output, "x" );
00627             // determine what should be printed
00628 //          CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars );    Cudd_Ref( CubeHorBDD );
00629             CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 );        Cudd_Ref( CubeHorBDD );
00630             Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                           Cudd_Ref( Prod );
00631             Cudd_RecursiveDeref( dd, CubeHorBDD );
00632 
00633             ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
00634             ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
00635             Cudd_RecursiveDeref( dd, Prod );
00636 
00637             if ( ValueOnSet == b1 && ValueOffSet == b0 )
00638                 fprintf( Output, "%c", SYMBOL_ONE );
00639             else if ( ValueOnSet == b0 && ValueOffSet == b1 )
00640                 fprintf( Output, "%c", SYMBOL_ZERO );
00641             else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
00642                 fprintf( Output, "%c", SYMBOL_DC );
00643             else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
00644                 fprintf( Output, "%c", SYMBOL_OVERLAP );
00645             else
00646                 assert(0);
00647 
00648             Cudd_RecursiveDeref( dd, ValueOnSet );
00649             Cudd_RecursiveDeref( dd, ValueOffSet );
00651             fprintf( Output, " " );
00652 
00653             if ( h != nCellsHor-1 )
00654                 if ( h&1 )
00655                     fprintf( Output, "%c", DOUBLE_VERTICAL );
00656                 else
00657                     fprintf( Output, "%c", SINGLE_VERTICAL );
00658         }
00659         fprintf( Output, "%c", DOUBLE_VERTICAL );
00660         fprintf( Output, "\n" );
00661 
00662         Cudd_RecursiveDeref( dd, CubeVerBDD );
00663 
00664         if ( v != nCellsVer-1 )
00665         // print separator line
00666         {
00667             for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00668             if ( v&1 )
00669             {
00670                 fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
00671                 for ( s = 0; s < nCellsHor; s++ )
00672                 {
00673                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00674                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00675                     fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00676                     if ( s != nCellsHor-1 )
00677                         if ( s&1 )
00678                             fprintf( Output, "%c", DOUBLES_CROSS );
00679                         else
00680                             fprintf( Output, "%c", S_VER_CROSS_D_HOR );
00681                 }
00682                 fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
00683             }
00684             else
00685             {
00686                 fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
00687                 for ( s = 0; s < nCellsHor; s++ )
00688                 {
00689                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00690                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00691                     fprintf( Output, "%c", SINGLE_HORIZONTAL );
00692                     if ( s != nCellsHor-1 )
00693                         if ( s&1 )
00694                             fprintf( Output, "%c", S_HOR_CROSS_D_VER );
00695                         else
00696                             fprintf( Output, "%c", SINGLES_CROSS );
00697                 }
00698                 fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
00699             }
00700             fprintf( Output, "\n" );
00701         }
00702     }
00703     
00705     // print the lower line
00706     for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
00707     fprintf( Output, "%c", DOUBLE_BOT_LEFT );
00708     for ( s = 0; s < nCellsHor; s++ )
00709     {
00710         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00711         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00712         fprintf( Output, "%c", DOUBLE_HORIZONTAL );
00713         if ( s != nCellsHor-1 )
00714             if ( s&1 )
00715                 fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
00716             else
00717                 fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
00718     }
00719     fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
00720     fprintf( Output, "\n" );
00721 
00722     if ( !fHorizontalVarNamesPrintedAbove )
00723     {
00725         // print horizontal digits
00726         for ( d = 0; d < nVarsHor; d++ )
00727         {
00728             for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
00729             for ( n = 0; n < nCellsHor; n++ )
00730                 if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
00731                     fprintf( Output, "1   " );
00732                 else
00733                     fprintf( Output, "0   " );
00734 
00736             fprintf( Output, "%c", (char)('a'+d) );
00738             fprintf( Output, "\n" );
00739         }
00740     }
00741 }

static int GrayCode ( int  BinCode  )  [static]

AutomaticStart

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 760 of file extraBddKmap.c.

00761 {
00762   return BinCode ^ ( BinCode >> 1 );
00763 }

Variable Documentation

int fHorizontalVarNamesPrintedAbove = 1 [static]

Definition at line 149 of file extraBddKmap.c.

DdNode* s_XVars[MAXVARS] [static]

Definition at line 146 of file extraBddKmap.c.

Generated on Tue Jan 5 12:19:14 2010 for abc70930 by  doxygen 1.6.1