ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraBddKmap.c
Go to the documentation of this file.
1
18
22
23#include "extraBdd.h"
24
25#ifdef WIN32
26#include <windows.h>
27#endif
28
29ABC_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
157static DdNode * s_XVars[MAXVARS];
158
159// flag which determines where the horizontal variable names are printed
160static int fHorizontalVarNamesPrintedAbove = 1;
161
162/*---------------------------------------------------------------------------*/
163/* Macro declarations */
164/*---------------------------------------------------------------------------*/
165
166
168
169/*---------------------------------------------------------------------------*/
170/* Static function prototypes */
171/*---------------------------------------------------------------------------*/
172
173// Oleg's way of generating the gray code
174static int GrayCode( int BinCode );
175static int BinCode ( int GrayCode );
176
178
179
180/*---------------------------------------------------------------------------*/
181/* Definition of exported functions */
182/*---------------------------------------------------------------------------*/
183
184
201void 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
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
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 {
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
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
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" );
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 );
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
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 {
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
560 fprintf( Output, "%c", (char)('a'+d) );
562 fprintf( Output, "\n" );
563 }
564 }
565}
566
567
568
581void 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
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
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 {
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
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
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" );
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 );
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
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 {
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
827 fprintf( Output, "%c", (char)('a'+d) );
829 fprintf( Output, "\n" );
830 }
831 }
832}
833
834
835
836/*---------------------------------------------------------------------------*/
837/* Definition of static functions */
838/*---------------------------------------------------------------------------*/
839
851int GrayCode ( int BinCode )
852{
853 return BinCode ^ ( BinCode >> 1 );
854}
855
867int BinCode ( int GrayCode )
868{
869 int bc = GrayCode;
870 while( GrayCode >>= 1 ) bc ^= GrayCode;
871 return bc;
872}
873
874
875ABC_NAMESPACE_IMPL_END
876
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
b0
#define b0
Definition bbrImage.c:96
b1
#define b1
Definition bbrImage.c:97
GrayCode
int GrayCode(int BinCode)
Definition casCore.c:480
p
Cube * p
Definition exorList.c:222
MAXVARS
#define MAXVARS
Definition extraBddKmap.c:37
S_VER_CROSS_D_HOR
#define S_VER_CROSS_D_HOR
Definition extraBddKmap.c:101
SINGLES_CROSS
#define SINGLES_CROSS
Definition extraBddKmap.c:98
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
D_JOINS_D_VER_LEFT
#define D_JOINS_D_VER_LEFT
Definition extraBddKmap.c:110
SYMBOL_OVERLAP
#define SYMBOL_OVERLAP
Definition extraBddKmap.c:133
D_JOINS_D_HOR_BOT
#define D_JOINS_D_HOR_BOT
Definition extraBddKmap.c:113
SYMBOL_DC
#define SYMBOL_DC
Definition extraBddKmap.c:132
DOUBLE_HORIZONTAL
#define DOUBLE_HORIZONTAL
Definition extraBddKmap.c:91
SYMBOL_ONE
#define SYMBOL_ONE
Definition extraBddKmap.c:131
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
SINGLE_VERTICAL
#define SINGLE_VERTICAL
Definition extraBddKmap.c:82
SINGLE_HORIZONTAL
#define SINGLE_HORIZONTAL
Definition extraBddKmap.c:83
S_JOINS_D_VER_LEFT
#define S_JOINS_D_VER_LEFT
Definition extraBddKmap.c:116
DOUBLE_BOT_LEFT
#define DOUBLE_BOT_LEFT
Definition extraBddKmap.c:94
DOUBLE_BOT_RIGHT
#define DOUBLE_BOT_RIGHT
Definition extraBddKmap.c:95
DOUBLES_CROSS
#define DOUBLES_CROSS
Definition extraBddKmap.c:99
S_JOINS_D_HOR_BOT
#define S_JOINS_D_HOR_BOT
Definition extraBddKmap.c:119
DOUBLE_VERTICAL
#define DOUBLE_VERTICAL
Definition extraBddKmap.c:90
S_JOINS_D_VER_RIGHT
#define S_JOINS_D_VER_RIGHT
Definition extraBddKmap.c:117
D_JOINS_D_VER_RIGHT
#define D_JOINS_D_VER_RIGHT
Definition extraBddKmap.c:111
DOUBLE_TOP_LEFT
#define DOUBLE_TOP_LEFT
Definition extraBddKmap.c:92
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
SYMBOL_ZERO
#define SYMBOL_ZERO
Definition extraBddKmap.c:129
S_HOR_CROSS_D_VER
#define S_HOR_CROSS_D_VER
Definition extraBddKmap.c:100
D_JOINS_D_HOR_TOP
#define D_JOINS_D_HOR_TOP
Definition extraBddKmap.c:112
Extra_bddBitsToCube
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
Definition extraBddMisc.c:730
assert
#define assert(ex)
Definition util_old.h:213