ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
extraBddKmap.c File Reference
#include "extraBdd.h"
Include dependency graph for extraBddKmap.c:

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

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)
 

Macro Definition Documentation

◆ CELL_FREE

#define CELL_FREE   (char)32

Definition at line 136 of file extraBddKmap.c.

◆ CELL_FULL

#define CELL_FULL   (char)219

Definition at line 137 of file extraBddKmap.c.

◆ D_JOINS_D_HOR_BOT

#define D_JOINS_D_HOR_BOT   (char)'+'

Definition at line 113 of file extraBddKmap.c.

◆ D_JOINS_D_HOR_TOP

#define D_JOINS_D_HOR_TOP   (char)'+'

Definition at line 112 of file extraBddKmap.c.

◆ D_JOINS_D_VER_LEFT

#define D_JOINS_D_VER_LEFT   (char)'+'

Definition at line 110 of file extraBddKmap.c.

◆ D_JOINS_D_VER_RIGHT

#define D_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 111 of file extraBddKmap.c.

◆ DOUBLE_BOT_LEFT

#define DOUBLE_BOT_LEFT   (char)'+'

Definition at line 94 of file extraBddKmap.c.

◆ DOUBLE_BOT_RIGHT

#define DOUBLE_BOT_RIGHT   (char)'+'

Definition at line 95 of file extraBddKmap.c.

◆ DOUBLE_HORIZONTAL

#define DOUBLE_HORIZONTAL   (char)'-'

Definition at line 91 of file extraBddKmap.c.

◆ DOUBLE_TOP_LEFT

#define DOUBLE_TOP_LEFT   (char)'+'

Definition at line 92 of file extraBddKmap.c.

◆ DOUBLE_TOP_RIGHT

#define DOUBLE_TOP_RIGHT   (char)'+'

Definition at line 93 of file extraBddKmap.c.

◆ DOUBLE_VERTICAL

#define DOUBLE_VERTICAL   (char)'|'

Definition at line 90 of file extraBddKmap.c.

◆ DOUBLES_CROSS

#define DOUBLES_CROSS   (char)'+'

Definition at line 99 of file extraBddKmap.c.

◆ HALF_LEFT

#define HALF_LEFT   (char)221

Definition at line 140 of file extraBddKmap.c.

◆ HALF_LOWER

#define HALF_LOWER   (char)220

Definition at line 139 of file extraBddKmap.c.

◆ HALF_RIGHT

#define HALF_RIGHT   (char)222

Definition at line 141 of file extraBddKmap.c.

◆ HALF_UPPER

#define HALF_UPPER   (char)223

Definition at line 138 of file extraBddKmap.c.

◆ MAXVARS

#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.

◆ S_HOR_CROSS_D_VER

#define S_HOR_CROSS_D_VER   (char)'+'

Definition at line 100 of file extraBddKmap.c.

◆ S_JOINS_D_HOR_BOT

#define S_JOINS_D_HOR_BOT   (char)'+'

Definition at line 119 of file extraBddKmap.c.

◆ S_JOINS_D_HOR_TOP

#define S_JOINS_D_HOR_TOP   (char)'+'

Definition at line 118 of file extraBddKmap.c.

◆ S_JOINS_D_VER_LEFT

#define S_JOINS_D_VER_LEFT   (char)'+'

Definition at line 116 of file extraBddKmap.c.

◆ S_JOINS_D_VER_RIGHT

#define S_JOINS_D_VER_RIGHT   (char)'+'

Definition at line 117 of file extraBddKmap.c.

◆ S_JOINS_S_HOR_BOT

#define S_JOINS_S_HOR_BOT   (char)'+'

Definition at line 107 of file extraBddKmap.c.

◆ S_JOINS_S_HOR_TOP

#define S_JOINS_S_HOR_TOP   (char)'+'

Definition at line 106 of file extraBddKmap.c.

◆ S_JOINS_S_VER_LEFT

#define S_JOINS_S_VER_LEFT   (char)'+'

Definition at line 104 of file extraBddKmap.c.

◆ S_JOINS_S_VER_RIGHT

#define S_JOINS_S_VER_RIGHT   (char)'+'

Definition at line 105 of file extraBddKmap.c.

◆ S_VER_CROSS_D_HOR

#define S_VER_CROSS_D_HOR   (char)'+'

Definition at line 101 of file extraBddKmap.c.

◆ SINGLE_BOT_LEFT

#define SINGLE_BOT_LEFT   (char)'+'

Definition at line 86 of file extraBddKmap.c.

◆ SINGLE_BOT_RIGHT

#define SINGLE_BOT_RIGHT   (char)'+'

Definition at line 87 of file extraBddKmap.c.

◆ SINGLE_HORIZONTAL

#define SINGLE_HORIZONTAL   (char)'-'

Definition at line 83 of file extraBddKmap.c.

◆ SINGLE_TOP_LEFT

#define SINGLE_TOP_LEFT   (char)'+'

Definition at line 84 of file extraBddKmap.c.

◆ SINGLE_TOP_RIGHT

#define SINGLE_TOP_RIGHT   (char)'+'

Definition at line 85 of file extraBddKmap.c.

◆ SINGLE_VERTICAL

#define SINGLE_VERTICAL   (char)'|'

Definition at line 82 of file extraBddKmap.c.

◆ SINGLES_CROSS

#define SINGLES_CROSS   (char)'+'

Definition at line 98 of file extraBddKmap.c.

◆ SYMBOL_DC

#define SYMBOL_DC   (char)'-'

Definition at line 132 of file extraBddKmap.c.

◆ SYMBOL_ONE

#define SYMBOL_ONE   (char)'1'

Definition at line 131 of file extraBddKmap.c.

◆ SYMBOL_OVERLAP

#define SYMBOL_OVERLAP   (char)'?'

Definition at line 133 of file extraBddKmap.c.

◆ SYMBOL_ZERO

#define SYMBOL_ZERO   (char)' '

Definition at line 129 of file extraBddKmap.c.

◆ UNDERSCORE

#define UNDERSCORE   (char)95

Definition at line 123 of file extraBddKmap.c.

Function Documentation

◆ Extra_PrintKMap()

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
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}
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
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
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
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Extra_PrintKMapRelation()

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
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}
Here is the call graph for this function: