abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraBddKmap.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraBddKmap.c]
4 
5  PackageName [extra]
6 
7  Synopsis [Visualizing the K-map.]
8 
9  Author [Alan Mishchenko]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 2.0. Started - September 1, 2003.]
14 
15  Revision [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 /// K-map visualization using pseudo graphics ///
20 /// Version 1.0. Started - August 20, 2000 ///
21 /// Version 2.0. Added to EXTRA - July 17, 2001 ///
22 
23 #include "extraBdd.h"
24 
25 #ifdef WIN32
26 #include <windows.h>
27 #endif
28 
29 ABC_NAMESPACE_IMPL_START
30 
31 
32 /*---------------------------------------------------------------------------*/
33 /* Constant declarations */
34 /*---------------------------------------------------------------------------*/
35 
36 // the maximum number of variables in the Karnaugh Map
37 #define MAXVARS 20
38 
39 /*
40 // single line
41 #define SINGLE_VERTICAL (char)179
42 #define SINGLE_HORIZONTAL (char)196
43 #define SINGLE_TOP_LEFT (char)218
44 #define SINGLE_TOP_RIGHT (char)191
45 #define SINGLE_BOT_LEFT (char)192
46 #define SINGLE_BOT_RIGHT (char)217
47 
48 // double line
49 #define DOUBLE_VERTICAL (char)186
50 #define DOUBLE_HORIZONTAL (char)205
51 #define DOUBLE_TOP_LEFT (char)201
52 #define DOUBLE_TOP_RIGHT (char)187
53 #define DOUBLE_BOT_LEFT (char)200
54 #define DOUBLE_BOT_RIGHT (char)188
55 
56 // line intersections
57 #define SINGLES_CROSS (char)197
58 #define DOUBLES_CROSS (char)206
59 #define S_HOR_CROSS_D_VER (char)215
60 #define S_VER_CROSS_D_HOR (char)216
61 
62 // single line joining
63 #define S_JOINS_S_VER_LEFT (char)180
64 #define S_JOINS_S_VER_RIGHT (char)195
65 #define S_JOINS_S_HOR_TOP (char)193
66 #define S_JOINS_S_HOR_BOT (char)194
67 
68 // double line joining
69 #define D_JOINS_D_VER_LEFT (char)185
70 #define D_JOINS_D_VER_RIGHT (char)204
71 #define D_JOINS_D_HOR_TOP (char)202
72 #define D_JOINS_D_HOR_BOT (char)203
73 
74 // single line joining double line
75 #define S_JOINS_D_VER_LEFT (char)182
76 #define S_JOINS_D_VER_RIGHT (char)199
77 #define S_JOINS_D_HOR_TOP (char)207
78 #define S_JOINS_D_HOR_BOT (char)209
79 */
80 
81 // single line
82 #define SINGLE_VERTICAL (char)'|'
83 #define SINGLE_HORIZONTAL (char)'-'
84 #define SINGLE_TOP_LEFT (char)'+'
85 #define SINGLE_TOP_RIGHT (char)'+'
86 #define SINGLE_BOT_LEFT (char)'+'
87 #define SINGLE_BOT_RIGHT (char)'+'
88 
89 // double line
90 #define DOUBLE_VERTICAL (char)'|'
91 #define DOUBLE_HORIZONTAL (char)'-'
92 #define DOUBLE_TOP_LEFT (char)'+'
93 #define DOUBLE_TOP_RIGHT (char)'+'
94 #define DOUBLE_BOT_LEFT (char)'+'
95 #define DOUBLE_BOT_RIGHT (char)'+'
96 
97 // line intersections
98 #define SINGLES_CROSS (char)'+'
99 #define DOUBLES_CROSS (char)'+'
100 #define S_HOR_CROSS_D_VER (char)'+'
101 #define S_VER_CROSS_D_HOR (char)'+'
102 
103 // single line joining
104 #define S_JOINS_S_VER_LEFT (char)'+'
105 #define S_JOINS_S_VER_RIGHT (char)'+'
106 #define S_JOINS_S_HOR_TOP (char)'+'
107 #define S_JOINS_S_HOR_BOT (char)'+'
108 
109 // double line joining
110 #define D_JOINS_D_VER_LEFT (char)'+'
111 #define D_JOINS_D_VER_RIGHT (char)'+'
112 #define D_JOINS_D_HOR_TOP (char)'+'
113 #define D_JOINS_D_HOR_BOT (char)'+'
114 
115 // single line joining double line
116 #define S_JOINS_D_VER_LEFT (char)'+'
117 #define S_JOINS_D_VER_RIGHT (char)'+'
118 #define S_JOINS_D_HOR_TOP (char)'+'
119 #define S_JOINS_D_HOR_BOT (char)'+'
120 
121 
122 // other symbols
123 #define UNDERSCORE (char)95
124 //#define SYMBOL_ZERO (char)248 // degree sign
125 //#define SYMBOL_ZERO (char)'o'
126 #ifdef WIN32
127 #define SYMBOL_ZERO (char)'0'
128 #else
129 #define SYMBOL_ZERO (char)' '
130 #endif
131 #define SYMBOL_ONE (char)'1'
132 #define SYMBOL_DC (char)'-'
133 #define SYMBOL_OVERLAP (char)'?'
134 
135 // full cells and half cells
136 #define CELL_FREE (char)32
137 #define CELL_FULL (char)219
138 #define HALF_UPPER (char)223
139 #define HALF_LOWER (char)220
140 #define HALF_LEFT (char)221
141 #define HALF_RIGHT (char)222
142 
143 
144 /*---------------------------------------------------------------------------*/
145 /* Structure declarations */
146 /*---------------------------------------------------------------------------*/
147 
148 /*---------------------------------------------------------------------------*/
149 /* Type declarations */
150 /*---------------------------------------------------------------------------*/
151 
152 /*---------------------------------------------------------------------------*/
153 /* Variable declarations */
154 /*---------------------------------------------------------------------------*/
155 
156 // the array of BDD variables used internally
157 static DdNode * s_XVars[MAXVARS];
158 
159 // flag which determines where the horizontal variable names are printed
160 static int fHorizontalVarNamesPrintedAbove = 1;
161 
162 /*---------------------------------------------------------------------------*/
163 /* Macro declarations */
164 /*---------------------------------------------------------------------------*/
165 
166 
167 /**AutomaticStart*************************************************************/
168 
169 /*---------------------------------------------------------------------------*/
170 /* Static function prototypes */
171 /*---------------------------------------------------------------------------*/
172 
173 // Oleg's way of generating the gray code
174 static int GrayCode( int BinCode );
175 static int BinCode ( int GrayCode );
176 
177 /**AutomaticEnd***************************************************************/
178 
179 
180 /*---------------------------------------------------------------------------*/
181 /* Definition of exported functions */
182 /*---------------------------------------------------------------------------*/
183 
184 
185 /**Function********************************************************************
186 
187  Synopsis [Prints the K-map of the function.]
188 
189  Description [If the pointer to the array of variables XVars is NULL,
190  fSuppType determines how the support will be determined.
191  fSuppType == 0 -- takes the first nVars of the manager
192  fSuppType == 1 -- takes the topmost nVars of the manager
193  fSuppType == 2 -- determines support from the on-set and the offset
194  ]
195 
196  SideEffects []
197 
198  SeeAlso []
199 
200 ******************************************************************************/
201 void Extra_PrintKMap(
202  FILE * Output, /* the output stream */
203  DdManager * dd,
204  DdNode * OnSet,
205  DdNode * OffSet,
206  int nVars,
207  DdNode ** XVars,
208  int fSuppType, /* the flag which determines how support is computed */
209  char ** pVarNames )
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 }
566 
567 
568 
569 /**Function********************************************************************
570 
571  Synopsis [Prints the K-map of the relation.]
572 
573  Description [Assumes that the relation depends the first nXVars of XVars and
574  the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.]
575 
576  SideEffects []
577 
578  SeeAlso []
579 
580 ******************************************************************************/
581 void Extra_PrintKMapRelation(
582  FILE * Output, /* the output stream */
583  DdManager * dd,
584  DdNode * OnSet,
585  DdNode * OffSet,
586  int nXVars,
587  int nYVars,
588  DdNode ** XVars,
589  DdNode ** YVars ) /* the flag which determines how support is computed */
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 }
833 
834 
835 
836 /*---------------------------------------------------------------------------*/
837 /* Definition of static functions */
838 /*---------------------------------------------------------------------------*/
839 
840 /**Function********************************************************************
841 
842  Synopsis []
843 
844  Description []
845 
846  SideEffects []
847 
848  SeeAlso []
849 
850 ******************************************************************************/
851 int GrayCode ( int BinCode )
852 {
853  return BinCode ^ ( BinCode >> 1 );
854 }
855 
856 /**Function********************************************************************
857 
858  Synopsis []
859 
860  Description []
861 
862  SideEffects []
863 
864  SeeAlso []
865 
866 ******************************************************************************/
867 int BinCode ( int GrayCode )
868 {
869  int bc = GrayCode;
870  while( GrayCode >>= 1 ) bc ^= GrayCode;
871  return bc;
872 }
873 
874 
875 ABC_NAMESPACE_IMPL_END
876 
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
Extra_PrintKMap
void Extra_PrintKMap(FILE *Output, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nVars, DdNode **XVars, int fSuppType, char **pVarNames)
Definition: extraBddKmap.c:201
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
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Extra_PrintKMapRelation
void Extra_PrintKMapRelation(FILE *Output, DdManager *dd, DdNode *OnSet, DdNode *OffSet, int nXVars, int nYVars, DdNode **XVars, DdNode **YVars)
Definition: extraBddKmap.c:581
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
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
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
BinCode
static int BinCode(int GrayCode)
Definition: extraBddKmap.c:867