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 ******************************************************************************/
Extra_PrintKMap(FILE * Output,DdManager * dd,DdNode * OnSet,DdNode * OffSet,int nVars,DdNode ** XVars,int fSuppType,char ** pVarNames)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 ******************************************************************************/
Extra_PrintKMapRelation(FILE * Output,DdManager * dd,DdNode * OnSet,DdNode * OffSet,int nXVars,int nYVars,DdNode ** XVars,DdNode ** YVars)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 ******************************************************************************/
GrayCode(int BinCode)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 ******************************************************************************/
BinCode(int GrayCode)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
877