abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Macros | Functions | Variables
extraBddKmap.c File Reference
#include "extraBdd.h"

Go to the source code of this file.

Macros

#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
 

Macro Definition Documentation

#define CELL_FREE   (char)32

Definition at line 136 of file extraBddKmap.c.

#define CELL_FULL   (char)219

Definition at line 137 of file extraBddKmap.c.

#define D_JOINS_D_HOR_BOT   (char)'+'

Definition at line 113 of file extraBddKmap.c.

#define D_JOINS_D_HOR_TOP   (char)'+'

Definition at line 112 of file extraBddKmap.c.

#define D_JOINS_D_VER_LEFT   (char)'+'

Definition at line 110 of file extraBddKmap.c.

#define D_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 111 of file extraBddKmap.c.

#define DOUBLE_BOT_LEFT   (char)'+'

Definition at line 94 of file extraBddKmap.c.

#define DOUBLE_BOT_RIGHT   (char)'+'

Definition at line 95 of file extraBddKmap.c.

#define DOUBLE_HORIZONTAL   (char)'-'

Definition at line 91 of file extraBddKmap.c.

#define DOUBLE_TOP_LEFT   (char)'+'

Definition at line 92 of file extraBddKmap.c.

#define DOUBLE_TOP_RIGHT   (char)'+'

Definition at line 93 of file extraBddKmap.c.

#define DOUBLE_VERTICAL   (char)'|'

Definition at line 90 of file extraBddKmap.c.

#define DOUBLES_CROSS   (char)'+'

Definition at line 99 of file extraBddKmap.c.

#define HALF_LEFT   (char)221

Definition at line 140 of file extraBddKmap.c.

#define HALF_LOWER   (char)220

Definition at line 139 of file extraBddKmap.c.

#define HALF_RIGHT   (char)222

Definition at line 141 of file extraBddKmap.c.

#define HALF_UPPER   (char)223

Definition at line 138 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 37 of file extraBddKmap.c.

#define S_HOR_CROSS_D_VER   (char)'+'

Definition at line 100 of file extraBddKmap.c.

#define S_JOINS_D_HOR_BOT   (char)'+'

Definition at line 119 of file extraBddKmap.c.

#define S_JOINS_D_HOR_TOP   (char)'+'

Definition at line 118 of file extraBddKmap.c.

#define S_JOINS_D_VER_LEFT   (char)'+'

Definition at line 116 of file extraBddKmap.c.

#define S_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 117 of file extraBddKmap.c.

#define S_JOINS_S_HOR_BOT   (char)'+'

Definition at line 107 of file extraBddKmap.c.

#define S_JOINS_S_HOR_TOP   (char)'+'

Definition at line 106 of file extraBddKmap.c.

#define S_JOINS_S_VER_LEFT   (char)'+'

Definition at line 104 of file extraBddKmap.c.

#define S_JOINS_S_VER_RIGHT   (char)'+'

Definition at line 105 of file extraBddKmap.c.

#define S_VER_CROSS_D_HOR   (char)'+'

Definition at line 101 of file extraBddKmap.c.

#define SINGLE_BOT_LEFT   (char)'+'

Definition at line 86 of file extraBddKmap.c.

#define SINGLE_BOT_RIGHT   (char)'+'

Definition at line 87 of file extraBddKmap.c.

#define SINGLE_HORIZONTAL   (char)'-'

Definition at line 83 of file extraBddKmap.c.

#define SINGLE_TOP_LEFT   (char)'+'

Definition at line 84 of file extraBddKmap.c.

#define SINGLE_TOP_RIGHT   (char)'+'

Definition at line 85 of file extraBddKmap.c.

#define SINGLE_VERTICAL   (char)'|'

Definition at line 82 of file extraBddKmap.c.

#define SINGLES_CROSS   (char)'+'

Definition at line 98 of file extraBddKmap.c.

#define SYMBOL_DC   (char)'-'

Definition at line 132 of file extraBddKmap.c.

#define SYMBOL_ONE   (char)'1'

Definition at line 131 of file extraBddKmap.c.

#define SYMBOL_OVERLAP   (char)'?'

Definition at line 133 of file extraBddKmap.c.

#define SYMBOL_ZERO   (char)' '

Definition at line 129 of file extraBddKmap.c.

#define UNDERSCORE   (char)95

Definition at line 123 of file extraBddKmap.c.

Function Documentation

int BinCode ( int  GrayCode)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 867 of file extraBddKmap.c.

868 {
869  int bc = GrayCode;
870  while( GrayCode >>= 1 ) bc ^= GrayCode;
871  return bc;
872 }
GrayCode
static int GrayCode(int BinCode)
Definition: extraBddKmap.c:851
void Extra_PrintKMap ( FILE *  Output,
DdManager *  dd,
DdNode *  OnSet,
DdNode *  OffSet,
int  nVars,
DdNode **  XVars,
int  fSuppType,
char **  pVarNames 
)

AutomaticEnd Function********************************************************************

Synopsis [Prints the K-map of the function.]

Description [If the pointer to the array of variables XVars is NULL, fSuppType determines how the support will be determined. fSuppType == 0 – takes the first nVars of the manager fSuppType == 1 – takes the topmost nVars of the manager fSuppType == 2 – determines support from the on-set and the offset ]

SideEffects []

SeeAlso []

Definition at line 201 of file extraBddKmap.c.

210 {
211  int fPrintTruth = 1;
212  int d, p, n, s, v, h, w;
213  int nVarsVer;
214  int nVarsHor;
215  int nCellsVer;
216  int nCellsHor;
217  int nSkipSpaces;
218 
219  // make sure that on-set and off-set do not overlap
220  if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
221  {
222  fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
223  return;
224  }
225  if ( nVars == 0 )
226  { printf( "Function is constant %d.\n", !Cudd_IsComplement(OnSet) ); return; }
227 
228  // print truth table for debugging
229  if ( fPrintTruth )
230  {
231  DdNode * bCube, * bPart;
232  printf( "Truth table: " );
233  if ( nVars == 0 )
234  printf( "Constant" );
235  else if ( nVars == 1 )
236  printf( "1-var function" );
237  else
238  {
239 // printf( "0x" );
240  for ( d = (1<<(nVars-2)) - 1; d >= 0; d-- )
241  {
242  int Value = 0;
243  for ( s = 0; s < 4; s++ )
244  {
245  bCube = Extra_bddBitsToCube( dd, 4*d+s, nVars, dd->vars, 0 ); Cudd_Ref( bCube );
246  bPart = Cudd_Cofactor( dd, OnSet, bCube ); Cudd_Ref( bPart );
247  Value |= ((int)(bPart == b1) << s);
248  Cudd_RecursiveDeref( dd, bPart );
249  Cudd_RecursiveDeref( dd, bCube );
250  }
251  if ( Value < 10 )
252  fprintf( stdout, "%d", Value );
253  else
254  fprintf( stdout, "%c", 'a' + Value-10 );
255  }
256  }
257  printf( "\n" );
258  }
259 
260 
261 /*
262  if ( OnSet == b1 )
263  {
264  fprintf( Output, "PrintKMap(): Constant 1\n" );
265  return;
266  }
267  if ( OffSet == b1 )
268  {
269  fprintf( Output, "PrintKMap(): Constant 0\n" );
270  return;
271  }
272 */
273  if ( nVars < 0 || nVars > MAXVARS )
274  {
275  fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
276  return;
277  }
278 
279  // determine the support if it is not given
280  if ( XVars == NULL )
281  {
282  if ( fSuppType == 0 )
283  { // assume that the support includes the first nVars of the manager
284  assert( nVars );
285  for ( v = 0; v < nVars; v++ )
286  s_XVars[v] = Cudd_bddIthVar( dd, v );
287  }
288  else if ( fSuppType == 1 )
289  { // assume that the support includes the topmost nVars of the manager
290  assert( nVars );
291  for ( v = 0; v < nVars; v++ )
292  s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
293  }
294  else // determine the support
295  {
296  DdNode * SuppOn, * SuppOff, * Supp;
297  int cVars = 0;
298  DdNode * TempSupp;
299 
300  // determine support
301  SuppOn = Cudd_Support( dd, OnSet ); Cudd_Ref( SuppOn );
302  SuppOff = Cudd_Support( dd, OffSet ); Cudd_Ref( SuppOff );
303  Supp = Cudd_bddAnd( dd, SuppOn, SuppOff ); Cudd_Ref( Supp );
304  Cudd_RecursiveDeref( dd, SuppOn );
305  Cudd_RecursiveDeref( dd, SuppOff );
306 
307  nVars = Cudd_SupportSize( dd, Supp );
308  if ( nVars > MAXVARS )
309  {
310  fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
311  Cudd_RecursiveDeref( dd, Supp );
312  return;
313  }
314 
315  // assign variables
316  for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
317  s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );
318 
319  Cudd_RecursiveDeref( dd, TempSupp );
320  }
321  }
322  else
323  {
324  // copy variables
325  assert( XVars );
326  for ( v = 0; v < nVars; v++ )
327  s_XVars[v] = XVars[v];
328  }
329 
330  ////////////////////////////////////////////////////////////////////
331  // determine the Karnaugh map parameters
332  nVarsVer = nVars/2;
333  nVarsHor = nVars - nVarsVer;
334 
335  nCellsVer = (1<<nVarsVer);
336  nCellsHor = (1<<nVarsHor);
337  nSkipSpaces = nVarsVer + 1;
338 
339  ////////////////////////////////////////////////////////////////////
340  // print variable names
341  fprintf( Output, "\n" );
342  for ( w = 0; w < nVarsVer; w++ )
343  if ( pVarNames == NULL )
344  fprintf( Output, "%c", 'a'+nVarsHor+w );
345  else
346  fprintf( Output, " %s", pVarNames[nVarsHor+w] );
347 
348  if ( fHorizontalVarNamesPrintedAbove )
349  {
350  fprintf( Output, " \\ " );
351  for ( w = 0; w < nVarsHor; w++ )
352  if ( pVarNames == NULL )
353  fprintf( Output, "%c", 'a'+w );
354  else
355  fprintf( Output, "%s ", pVarNames[w] );
356  }
357  fprintf( Output, "\n" );
358 
359  if ( fHorizontalVarNamesPrintedAbove )
360  {
361  ////////////////////////////////////////////////////////////////////
362  // print horizontal digits
363  for ( d = 0; d < nVarsHor; d++ )
364  {
365  for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
366  for ( n = 0; n < nCellsHor; n++ )
367  if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
368  fprintf( Output, "1 " );
369  else
370  fprintf( Output, "0 " );
371  fprintf( Output, "\n" );
372  }
373  }
374 
375  ////////////////////////////////////////////////////////////////////
376  // print the upper line
377  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
378  fprintf( Output, "%c", DOUBLE_TOP_LEFT );
379  for ( s = 0; s < nCellsHor; s++ )
380  {
381  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
382  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
383  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
384  if ( s != nCellsHor-1 )
385  {
386  if ( s&1 )
387  fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
388  else
389  fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
390  }
391  }
392  fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
393  fprintf( Output, "\n" );
394 
395  ////////////////////////////////////////////////////////////////////
396  // print the map
397  for ( v = 0; v < nCellsVer; v++ )
398  {
399  DdNode * CubeVerBDD;
400 
401  // print horizontal digits
402 // for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
403  for ( n = 0; n < nVarsVer; n++ )
404  if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
405  fprintf( Output, "1" );
406  else
407  fprintf( Output, "0" );
408  fprintf( Output, " " );
409 
410  // find vertical cube
411  CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 ); Cudd_Ref( CubeVerBDD );
412 
413  // print text line
414  fprintf( Output, "%c", DOUBLE_VERTICAL );
415  for ( h = 0; h < nCellsHor; h++ )
416  {
417  DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
418 
419  fprintf( Output, " " );
420 // fprintf( Output, "x" );
421  ///////////////////////////////////////////////////////////////
422  // determine what should be printed
423  CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 ); Cudd_Ref( CubeHorBDD );
424  Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod );
425  Cudd_RecursiveDeref( dd, CubeHorBDD );
426 
427  ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet );
428  ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet );
429  Cudd_RecursiveDeref( dd, Prod );
430 
431 #ifdef WIN32
432  {
433  HANDLE hConsole = GetStdHandle(STD_OUTPUT_HANDLE);
434  char Symb = 0, Color = 0;
435  if ( ValueOnSet == b1 && ValueOffSet == b0 )
436  Symb = SYMBOL_ONE, Color = 14; // yellow
437  else if ( ValueOnSet == b0 && ValueOffSet == b1 )
438  Symb = SYMBOL_ZERO, Color = 11; // blue
439  else if ( ValueOnSet == b0 && ValueOffSet == b0 )
440  Symb = SYMBOL_DC, Color = 10; // green
441  else if ( ValueOnSet == b1 && ValueOffSet == b1 )
442  Symb = SYMBOL_OVERLAP, Color = 12; // red
443  else
444  assert(0);
445  SetConsoleTextAttribute( hConsole, Color );
446  fprintf( Output, "%c", Symb );
447  SetConsoleTextAttribute( hConsole, 7 );
448  }
449 #else
450  {
451  if ( ValueOnSet == b1 && ValueOffSet == b0 )
452  fprintf( Output, "%c", SYMBOL_ONE );
453  else if ( ValueOnSet == b0 && ValueOffSet == b1 )
454  fprintf( Output, "%c", SYMBOL_ZERO );
455  else if ( ValueOnSet == b0 && ValueOffSet == b0 )
456  fprintf( Output, "%c", SYMBOL_DC );
457  else if ( ValueOnSet == b1 && ValueOffSet == b1 )
458  fprintf( Output, "%c", SYMBOL_OVERLAP );
459  else
460  assert(0);
461  }
462 #endif
463 
464  Cudd_RecursiveDeref( dd, ValueOnSet );
465  Cudd_RecursiveDeref( dd, ValueOffSet );
466  ///////////////////////////////////////////////////////////////
467  fprintf( Output, " " );
468 
469  if ( h != nCellsHor-1 )
470  {
471  if ( h&1 )
472  fprintf( Output, "%c", DOUBLE_VERTICAL );
473  else
474  fprintf( Output, "%c", SINGLE_VERTICAL );
475  }
476  }
477  fprintf( Output, "%c", DOUBLE_VERTICAL );
478  fprintf( Output, "\n" );
479 
480  Cudd_RecursiveDeref( dd, CubeVerBDD );
481 
482  if ( v != nCellsVer-1 )
483  // print separator line
484  {
485  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
486  if ( v&1 )
487  {
488  fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
489  for ( s = 0; s < nCellsHor; s++ )
490  {
491  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
492  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
493  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
494  if ( s != nCellsHor-1 )
495  {
496  if ( s&1 )
497  fprintf( Output, "%c", DOUBLES_CROSS );
498  else
499  fprintf( Output, "%c", S_VER_CROSS_D_HOR );
500  }
501  }
502  fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
503  }
504  else
505  {
506  fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
507  for ( s = 0; s < nCellsHor; s++ )
508  {
509  fprintf( Output, "%c", SINGLE_HORIZONTAL );
510  fprintf( Output, "%c", SINGLE_HORIZONTAL );
511  fprintf( Output, "%c", SINGLE_HORIZONTAL );
512  if ( s != nCellsHor-1 )
513  {
514  if ( s&1 )
515  fprintf( Output, "%c", S_HOR_CROSS_D_VER );
516  else
517  fprintf( Output, "%c", SINGLES_CROSS );
518  }
519  }
520  fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
521  }
522  fprintf( Output, "\n" );
523  }
524  }
525 
526  ////////////////////////////////////////////////////////////////////
527  // print the lower line
528  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
529  fprintf( Output, "%c", DOUBLE_BOT_LEFT );
530  for ( s = 0; s < nCellsHor; s++ )
531  {
532  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
533  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
534  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
535  if ( s != nCellsHor-1 )
536  {
537  if ( s&1 )
538  fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
539  else
540  fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
541  }
542  }
543  fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
544  fprintf( Output, "\n" );
545 
546  if ( !fHorizontalVarNamesPrintedAbove )
547  {
548  ////////////////////////////////////////////////////////////////////
549  // print horizontal digits
550  for ( d = 0; d < nVarsHor; d++ )
551  {
552  for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
553  for ( n = 0; n < nCellsHor; n++ )
554  if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
555  fprintf( Output, "1 " );
556  else
557  fprintf( Output, "0 " );
558 
559  /////////////////////////////////
560  fprintf( Output, "%c", (char)('a'+d) );
561  /////////////////////////////////
562  fprintf( Output, "\n" );
563  }
564  }
565 }
DOUBLE_BOT_LEFT
#define DOUBLE_BOT_LEFT
Definition: extraBddKmap.c:94
DOUBLE_TOP_LEFT
#define DOUBLE_TOP_LEFT
Definition: extraBddKmap.c:92
Cudd_T
#define Cudd_T(node)
Definition: cudd.h:440
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
SINGLES_CROSS
#define SINGLES_CROSS
Definition: extraBddKmap.c:98
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cudd_Support
DdNode * Cudd_Support(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:740
D_JOINS_D_VER_LEFT
#define D_JOINS_D_VER_LEFT
Definition: extraBddKmap.c:110
b1
#define b1
Definition: extraBdd.h:76
S_HOR_CROSS_D_VER
#define S_HOR_CROSS_D_VER
Definition: extraBddKmap.c:100
DOUBLE_BOT_RIGHT
#define DOUBLE_BOT_RIGHT
Definition: extraBddKmap.c:95
D_JOINS_D_VER_RIGHT
#define D_JOINS_D_VER_RIGHT
Definition: extraBddKmap.c:111
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
DOUBLES_CROSS
#define DOUBLES_CROSS
Definition: extraBddKmap.c:99
DOUBLE_TOP_RIGHT
#define DOUBLE_TOP_RIGHT
Definition: extraBddKmap.c:93
s_XVars
static DdNode * s_XVars[MAXVARS]
Definition: extraBddKmap.c:157
S_JOINS_D_HOR_TOP
#define S_JOINS_D_HOR_TOP
Definition: extraBddKmap.c:118
D_JOINS_D_HOR_BOT
#define D_JOINS_D_HOR_BOT
Definition: extraBddKmap.c:113
SYMBOL_OVERLAP
#define SYMBOL_OVERLAP
Definition: extraBddKmap.c:133
GrayCode
static int GrayCode(int BinCode)
Definition: extraBddKmap.c:851
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
DOUBLE_VERTICAL
#define DOUBLE_VERTICAL
Definition: extraBddKmap.c:90
D_JOINS_D_HOR_TOP
#define D_JOINS_D_HOR_TOP
Definition: extraBddKmap.c:112
SYMBOL_ONE
#define SYMBOL_ONE
Definition: extraBddKmap.c:131
DOUBLE_HORIZONTAL
#define DOUBLE_HORIZONTAL
Definition: extraBddKmap.c:91
b0
#define b0
Definition: extraBdd.h:75
DdNode::index
DdHalfWord index
Definition: cudd.h:279
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
S_JOINS_D_VER_LEFT
#define S_JOINS_D_VER_LEFT
Definition: extraBddKmap.c:116
SYMBOL_DC
#define SYMBOL_DC
Definition: extraBddKmap.c:132
DdManager::one
DdNode * one
Definition: cuddInt.h:345
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Extra_bddBitsToCube
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
Definition: extraBddMisc.c:730
SINGLE_VERTICAL
#define SINGLE_VERTICAL
Definition: extraBddKmap.c:82
fHorizontalVarNamesPrintedAbove
static int fHorizontalVarNamesPrintedAbove
Definition: extraBddKmap.c:160
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
SYMBOL_ZERO
#define SYMBOL_ZERO
Definition: extraBddKmap.c:129
MAXVARS
#define MAXVARS
Definition: extraBddKmap.c:37
S_VER_CROSS_D_HOR
#define S_VER_CROSS_D_HOR
Definition: extraBddKmap.c:101
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
S_JOINS_D_VER_RIGHT
#define S_JOINS_D_VER_RIGHT
Definition: extraBddKmap.c:117
S_JOINS_D_HOR_BOT
#define S_JOINS_D_HOR_BOT
Definition: extraBddKmap.c:119
SINGLE_HORIZONTAL
#define SINGLE_HORIZONTAL
Definition: extraBddKmap.c:83
void Extra_PrintKMapRelation ( FILE *  Output,
DdManager *  dd,
DdNode *  OnSet,
DdNode *  OffSet,
int  nXVars,
int  nYVars,
DdNode **  XVars,
DdNode **  YVars 
)

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

Synopsis [Prints the K-map of the relation.]

Description [Assumes that the relation depends the first nXVars of XVars and the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.]

SideEffects []

SeeAlso []

Definition at line 581 of file extraBddKmap.c.

590 {
591  int d, p, n, s, v, h, w;
592  int nVars;
593  int nVarsVer;
594  int nVarsHor;
595  int nCellsVer;
596  int nCellsHor;
597  int nSkipSpaces;
598 
599  // make sure that on-set and off-set do not overlap
600  if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
601  {
602  fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
603  return;
604  }
605 
606  if ( OnSet == b1 )
607  {
608  fprintf( Output, "PrintKMap(): Constant 1\n" );
609  return;
610  }
611  if ( OffSet == b1 )
612  {
613  fprintf( Output, "PrintKMap(): Constant 0\n" );
614  return;
615  }
616 
617  nVars = nXVars + nYVars;
618  if ( nVars < 0 || nVars > MAXVARS )
619  {
620  fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
621  return;
622  }
623 
624 
625  ////////////////////////////////////////////////////////////////////
626  // determine the Karnaugh map parameters
627  nVarsVer = nXVars;
628  nVarsHor = nYVars;
629  nCellsVer = (1<<nVarsVer);
630  nCellsHor = (1<<nVarsHor);
631  nSkipSpaces = nVarsVer + 1;
632 
633  ////////////////////////////////////////////////////////////////////
634  // print variable names
635  fprintf( Output, "\n" );
636  for ( w = 0; w < nVarsVer; w++ )
637  fprintf( Output, "%c", 'a'+nVarsHor+w );
638  if ( fHorizontalVarNamesPrintedAbove )
639  {
640  fprintf( Output, " \\ " );
641  for ( w = 0; w < nVarsHor; w++ )
642  fprintf( Output, "%c", 'a'+w );
643  }
644  fprintf( Output, "\n" );
645 
646  if ( fHorizontalVarNamesPrintedAbove )
647  {
648  ////////////////////////////////////////////////////////////////////
649  // print horizontal digits
650  for ( d = 0; d < nVarsHor; d++ )
651  {
652  for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
653  for ( n = 0; n < nCellsHor; n++ )
654  if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
655  fprintf( Output, "1 " );
656  else
657  fprintf( Output, "0 " );
658  fprintf( Output, "\n" );
659  }
660  }
661 
662  ////////////////////////////////////////////////////////////////////
663  // print the upper line
664  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
665  fprintf( Output, "%c", DOUBLE_TOP_LEFT );
666  for ( s = 0; s < nCellsHor; s++ )
667  {
668  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
669  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
670  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
671  if ( s != nCellsHor-1 )
672  {
673  if ( s&1 )
674  fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
675  else
676  fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
677  }
678  }
679  fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
680  fprintf( Output, "\n" );
681 
682  ////////////////////////////////////////////////////////////////////
683  // print the map
684  for ( v = 0; v < nCellsVer; v++ )
685  {
686  DdNode * CubeVerBDD;
687 
688  // print horizontal digits
689 // for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
690  for ( n = 0; n < nVarsVer; n++ )
691  if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
692  fprintf( Output, "1" );
693  else
694  fprintf( Output, "0" );
695  fprintf( Output, " " );
696 
697  // find vertical cube
698 // CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor ); Cudd_Ref( CubeVerBDD );
699  CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 ); Cudd_Ref( CubeVerBDD );
700 
701  // print text line
702  fprintf( Output, "%c", DOUBLE_VERTICAL );
703  for ( h = 0; h < nCellsHor; h++ )
704  {
705  DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
706 
707  fprintf( Output, " " );
708 // fprintf( Output, "x" );
709  ///////////////////////////////////////////////////////////////
710  // determine what should be printed
711 // CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars ); Cudd_Ref( CubeHorBDD );
712  CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 ); Cudd_Ref( CubeHorBDD );
713  Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod );
714  Cudd_RecursiveDeref( dd, CubeHorBDD );
715 
716  ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet );
717  ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet );
718  Cudd_RecursiveDeref( dd, Prod );
719 
720  if ( ValueOnSet == b1 && ValueOffSet == b0 )
721  fprintf( Output, "%c", SYMBOL_ONE );
722  else if ( ValueOnSet == b0 && ValueOffSet == b1 )
723  fprintf( Output, "%c", SYMBOL_ZERO );
724  else if ( ValueOnSet == b0 && ValueOffSet == b0 )
725  fprintf( Output, "%c", SYMBOL_DC );
726  else if ( ValueOnSet == b1 && ValueOffSet == b1 )
727  fprintf( Output, "%c", SYMBOL_OVERLAP );
728  else
729  assert(0);
730 
731  Cudd_RecursiveDeref( dd, ValueOnSet );
732  Cudd_RecursiveDeref( dd, ValueOffSet );
733  ///////////////////////////////////////////////////////////////
734  fprintf( Output, " " );
735 
736  if ( h != nCellsHor-1 )
737  {
738  if ( h&1 )
739  fprintf( Output, "%c", DOUBLE_VERTICAL );
740  else
741  fprintf( Output, "%c", SINGLE_VERTICAL );
742  }
743  }
744  fprintf( Output, "%c", DOUBLE_VERTICAL );
745  fprintf( Output, "\n" );
746 
747  Cudd_RecursiveDeref( dd, CubeVerBDD );
748 
749  if ( v != nCellsVer-1 )
750  // print separator line
751  {
752  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
753  if ( v&1 )
754  {
755  fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
756  for ( s = 0; s < nCellsHor; s++ )
757  {
758  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
759  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
760  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
761  if ( s != nCellsHor-1 )
762  {
763  if ( s&1 )
764  fprintf( Output, "%c", DOUBLES_CROSS );
765  else
766  fprintf( Output, "%c", S_VER_CROSS_D_HOR );
767  }
768  }
769  fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
770  }
771  else
772  {
773  fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
774  for ( s = 0; s < nCellsHor; s++ )
775  {
776  fprintf( Output, "%c", SINGLE_HORIZONTAL );
777  fprintf( Output, "%c", SINGLE_HORIZONTAL );
778  fprintf( Output, "%c", SINGLE_HORIZONTAL );
779  if ( s != nCellsHor-1 )
780  {
781  if ( s&1 )
782  fprintf( Output, "%c", S_HOR_CROSS_D_VER );
783  else
784  fprintf( Output, "%c", SINGLES_CROSS );
785  }
786  }
787  fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
788  }
789  fprintf( Output, "\n" );
790  }
791  }
792 
793  ////////////////////////////////////////////////////////////////////
794  // print the lower line
795  for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
796  fprintf( Output, "%c", DOUBLE_BOT_LEFT );
797  for ( s = 0; s < nCellsHor; s++ )
798  {
799  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
800  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
801  fprintf( Output, "%c", DOUBLE_HORIZONTAL );
802  if ( s != nCellsHor-1 )
803  {
804  if ( s&1 )
805  fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
806  else
807  fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
808  }
809  }
810  fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
811  fprintf( Output, "\n" );
812 
813  if ( !fHorizontalVarNamesPrintedAbove )
814  {
815  ////////////////////////////////////////////////////////////////////
816  // print horizontal digits
817  for ( d = 0; d < nVarsHor; d++ )
818  {
819  for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
820  for ( n = 0; n < nCellsHor; n++ )
821  if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
822  fprintf( Output, "1 " );
823  else
824  fprintf( Output, "0 " );
825 
826  /////////////////////////////////
827  fprintf( Output, "%c", (char)('a'+d) );
828  /////////////////////////////////
829  fprintf( Output, "\n" );
830  }
831  }
832 }
DOUBLE_BOT_LEFT
#define DOUBLE_BOT_LEFT
Definition: extraBddKmap.c:94
DOUBLE_TOP_LEFT
#define DOUBLE_TOP_LEFT
Definition: extraBddKmap.c:92
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
SINGLES_CROSS
#define SINGLES_CROSS
Definition: extraBddKmap.c:98
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
D_JOINS_D_VER_LEFT
#define D_JOINS_D_VER_LEFT
Definition: extraBddKmap.c:110
b1
#define b1
Definition: extraBdd.h:76
S_HOR_CROSS_D_VER
#define S_HOR_CROSS_D_VER
Definition: extraBddKmap.c:100
DOUBLE_BOT_RIGHT
#define DOUBLE_BOT_RIGHT
Definition: extraBddKmap.c:95
D_JOINS_D_VER_RIGHT
#define D_JOINS_D_VER_RIGHT
Definition: extraBddKmap.c:111
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
DOUBLES_CROSS
#define DOUBLES_CROSS
Definition: extraBddKmap.c:99
DOUBLE_TOP_RIGHT
#define DOUBLE_TOP_RIGHT
Definition: extraBddKmap.c:93
S_JOINS_D_HOR_TOP
#define S_JOINS_D_HOR_TOP
Definition: extraBddKmap.c:118
D_JOINS_D_HOR_BOT
#define D_JOINS_D_HOR_BOT
Definition: extraBddKmap.c:113
SYMBOL_OVERLAP
#define SYMBOL_OVERLAP
Definition: extraBddKmap.c:133
GrayCode
static int GrayCode(int BinCode)
Definition: extraBddKmap.c:851
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
DOUBLE_VERTICAL
#define DOUBLE_VERTICAL
Definition: extraBddKmap.c:90
D_JOINS_D_HOR_TOP
#define D_JOINS_D_HOR_TOP
Definition: extraBddKmap.c:112
SYMBOL_ONE
#define SYMBOL_ONE
Definition: extraBddKmap.c:131
DOUBLE_HORIZONTAL
#define DOUBLE_HORIZONTAL
Definition: extraBddKmap.c:91
b0
#define b0
Definition: extraBdd.h:75
S_JOINS_D_VER_LEFT
#define S_JOINS_D_VER_LEFT
Definition: extraBddKmap.c:116
SYMBOL_DC
#define SYMBOL_DC
Definition: extraBddKmap.c:132
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Extra_bddBitsToCube
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
Definition: extraBddMisc.c:730
SINGLE_VERTICAL
#define SINGLE_VERTICAL
Definition: extraBddKmap.c:82
fHorizontalVarNamesPrintedAbove
static int fHorizontalVarNamesPrintedAbove
Definition: extraBddKmap.c:160
assert
#define assert(ex)
Definition: util_old.h:213
SYMBOL_ZERO
#define SYMBOL_ZERO
Definition: extraBddKmap.c:129
MAXVARS
#define MAXVARS
Definition: extraBddKmap.c:37
S_VER_CROSS_D_HOR
#define S_VER_CROSS_D_HOR
Definition: extraBddKmap.c:101
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
S_JOINS_D_VER_RIGHT
#define S_JOINS_D_VER_RIGHT
Definition: extraBddKmap.c:117
S_JOINS_D_HOR_BOT
#define S_JOINS_D_HOR_BOT
Definition: extraBddKmap.c:119
SINGLE_HORIZONTAL
#define SINGLE_HORIZONTAL
Definition: extraBddKmap.c:83
static int GrayCode ( int  BinCode)
static

AutomaticStart

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 851 of file extraBddKmap.c.

852 {
853  return BinCode ^ ( BinCode >> 1 );
854 }
BinCode
static int BinCode(int GrayCode)
Definition: extraBddKmap.c:867

Variable Documentation

int fHorizontalVarNamesPrintedAbove = 1
static

Definition at line 160 of file extraBddKmap.c.

DdNode* s_XVars[MAXVARS]
static

Definition at line 157 of file extraBddKmap.c.