Version abc51005

4 files changed, 830 insertions, 3 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 839aa0b4..bb776ab7 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -106,7 +106,7 @@ typedef unsigned long long uint64;
 /*     Various Utilities                                                     */
 /*===========================================================================*/
 
-/*=== extraUtilBdd.c ========================================================*/
+/*=== extraBddMisc.c ========================================================*/
 extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
 extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
 extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
@@ -125,6 +125,14 @@ extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n
 extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
 extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
+extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
+
+/*=== extraBddKmap.c ================================================================*/
+
+/* displays the Karnaugh Map of a function */
+extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
+/* displays the Karnaugh Map of a relation */
+extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
 
 /*=== extraBddSymm.c =================================================================*/
 
diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c
new file mode 100644
index 00000000..bb43db68
--- /dev/null
+++ b/src/misc/extra/extraBddKmap.c
@@ -0,0 +1,783 @@
+/**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     ///
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+// the maximum number of variables in the Karnaugh Map
+#define MAXVARS 20
+
+/*
+// single line
+#define SINGLE_VERTICAL     (char)179
+#define SINGLE_HORIZONTAL   (char)196
+#define SINGLE_TOP_LEFT     (char)218
+#define SINGLE_TOP_RIGHT    (char)191
+#define SINGLE_BOT_LEFT     (char)192
+#define SINGLE_BOT_RIGHT    (char)217
+
+// double line
+#define DOUBLE_VERTICAL     (char)186
+#define DOUBLE_HORIZONTAL   (char)205
+#define DOUBLE_TOP_LEFT     (char)201
+#define DOUBLE_TOP_RIGHT    (char)187
+#define DOUBLE_BOT_LEFT     (char)200
+#define DOUBLE_BOT_RIGHT    (char)188
+
+// line intersections
+#define SINGLES_CROSS       (char)197
+#define DOUBLES_CROSS       (char)206
+#define S_HOR_CROSS_D_VER   (char)215
+#define S_VER_CROSS_D_HOR   (char)216
+
+// single line joining
+#define S_JOINS_S_VER_LEFT  (char)180
+#define S_JOINS_S_VER_RIGHT (char)195
+#define S_JOINS_S_HOR_TOP   (char)193
+#define S_JOINS_S_HOR_BOT   (char)194
+
+// double line joining
+#define D_JOINS_D_VER_LEFT  (char)185
+#define D_JOINS_D_VER_RIGHT (char)204
+#define D_JOINS_D_HOR_TOP   (char)202
+#define D_JOINS_D_HOR_BOT   (char)203
+
+// single line joining double line
+#define S_JOINS_D_VER_LEFT  (char)182
+#define S_JOINS_D_VER_RIGHT (char)199
+#define S_JOINS_D_HOR_TOP   (char)207
+#define S_JOINS_D_HOR_BOT   (char)209
+*/
+
+// single line
+#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)'+'
+
+// double line
+#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)'+'
+
+// line intersections
+#define SINGLES_CROSS       (char)'+'
+#define DOUBLES_CROSS       (char)'+'
+#define S_HOR_CROSS_D_VER   (char)'+'
+#define S_VER_CROSS_D_HOR   (char)'+'
+
+// single line joining
+#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)'+'
+
+// double line joining
+#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)'+'
+
+// single line joining double line
+#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)'+'
+
+
+// other symbols
+#define UNDERSCORE          (char)95
+//#define SYMBOL_ZERO       (char)248   // degree sign
+//#define SYMBOL_ZERO         (char)'o'
+#define SYMBOL_ZERO         (char)' '
+#define SYMBOL_ONE          (char)'1'
+#define SYMBOL_DC           (char)'-'
+#define SYMBOL_OVERLAP      (char)'?'
+
+// full cells and half cells
+#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
+
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+// the array of BDD variables used internally
+static DdNode * s_XVars[MAXVARS];
+
+// flag which determines where the horizontal variable names are printed
+static int fHorizontalVarNamesPrintedAbove = 1;
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+// Oleg's way of generating the gray code
+static int GrayCode( int BinCode );
+static int BinCode ( int GrayCode );
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**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     []
+
+******************************************************************************/
+void Extra_PrintKMap( 
+  FILE * Output,  /* the output stream */
+  DdManager * dd, 
+  DdNode * OnSet, 
+  DdNode * OffSet, 
+  int nVars, 
+  DdNode ** XVars, 
+  int fSuppType, /* the flag which determines how support is computed */
+  char ** pVarNames )
+{
+    int d, p, n, s, v, h, w;
+    int nVarsVer;
+    int nVarsHor;
+    int nCellsVer;
+    int nCellsHor;
+    int nSkipSpaces;
+
+    // make sure that on-set and off-set do not overlap
+    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
+    {
+        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
+        return;
+    }
+/*
+    if ( OnSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 1\n" );
+        return;
+    }
+    if ( OffSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 0\n" );
+        return;
+    }
+*/
+    if ( nVars < 0 || nVars > MAXVARS )
+    {
+        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
+        return;
+    }
+
+    // determine the support if it is not given
+    if ( XVars == NULL )
+    {
+        if ( fSuppType == 0 )
+        {   // assume that the support includes the first nVars of the manager
+            assert( nVars );
+            for ( v = 0; v < nVars; v++ )
+                s_XVars[v] = Cudd_bddIthVar( dd, v );
+        }
+        else if ( fSuppType == 1 )
+        {   // assume that the support includes the topmost nVars of the manager
+            assert( nVars );
+            for ( v = 0; v < nVars; v++ )
+                s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
+        }
+        else // determine the support
+        {
+            DdNode * SuppOn, * SuppOff, * Supp;
+            int cVars = 0;
+            DdNode * TempSupp;
+
+            // determine support
+            SuppOn = Cudd_Support( dd, OnSet );         Cudd_Ref( SuppOn );
+            SuppOff = Cudd_Support( dd, OffSet );       Cudd_Ref( SuppOff );
+            Supp = Cudd_bddAnd( dd, SuppOn, SuppOff );  Cudd_Ref( Supp );
+            Cudd_RecursiveDeref( dd, SuppOn );
+            Cudd_RecursiveDeref( dd, SuppOff );
+
+            nVars = Cudd_SupportSize( dd, Supp );
+            if ( nVars > MAXVARS )
+            {
+                fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
+                Cudd_RecursiveDeref( dd, Supp );
+                return;
+            }
+
+            // assign variables
+            for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
+                s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );
+
+            Cudd_RecursiveDeref( dd, TempSupp );
+        }
+    }
+    else
+    {
+        // copy variables
+        assert( XVars );
+        for ( v = 0; v < nVars; v++ )
+            s_XVars[v] = XVars[v];
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // determine the Karnaugh map parameters
+    nVarsVer = nVars/2;
+    nVarsHor = nVars - nVarsVer;
+    nCellsVer = (1<<nVarsVer);
+    nCellsHor = (1<<nVarsHor);
+    nSkipSpaces = nVarsVer + 1;
+
+    ////////////////////////////////////////////////////////////////////
+    // print variable names
+    fprintf( Output, "\n" );
+    for ( w = 0; w < nVarsVer; w++ )
+        if ( pVarNames == NULL )
+            fprintf( Output, "%c", 'a'+nVarsHor+w );
+        else
+            fprintf( Output, " %s", pVarNames[nVarsHor+w] );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        fprintf( Output, " \\ " );
+        for ( w = 0; w < nVarsHor; w++ )
+            if ( pVarNames == NULL )
+                fprintf( Output, "%c", 'a'+w );
+            else
+                fprintf( Output, "%s ", pVarNames[w] );
+    }
+    fprintf( Output, "\n" );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+            fprintf( Output, "\n" );
+        }
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // print the upper line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
+    }
+    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
+    fprintf( Output, "\n" );
+
+    ////////////////////////////////////////////////////////////////////
+    // print the map
+    for ( v = 0; v < nCellsVer; v++ )
+    {
+        DdNode * CubeVerBDD;
+
+        // print horizontal digits
+//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+        for ( n = 0; n < nVarsVer; n++ )
+            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
+                fprintf( Output, "1" );
+            else
+                fprintf( Output, "0" );
+        fprintf( Output, " " );
+
+        // find vertical cube
+        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 );    Cudd_Ref( CubeVerBDD );
+
+        // print text line
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        for ( h = 0; h < nCellsHor; h++ )
+        {
+            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
+
+            fprintf( Output, " " );
+//          fprintf( Output, "x" );
+            ///////////////////////////////////////////////////////////////
+            // determine what should be printed
+            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 );    Cudd_Ref( CubeHorBDD );
+            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                   Cudd_Ref( Prod );
+            Cudd_RecursiveDeref( dd, CubeHorBDD );
+
+            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
+            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
+            Cudd_RecursiveDeref( dd, Prod );
+
+            if ( ValueOnSet == b1 && ValueOffSet == b0 )
+                fprintf( Output, "%c", SYMBOL_ONE );
+            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
+                fprintf( Output, "%c", SYMBOL_ZERO );
+            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
+                fprintf( Output, "%c", SYMBOL_DC );
+            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
+                fprintf( Output, "%c", SYMBOL_OVERLAP );
+            else
+                assert(0);
+
+            Cudd_RecursiveDeref( dd, ValueOnSet );
+            Cudd_RecursiveDeref( dd, ValueOffSet );
+            ///////////////////////////////////////////////////////////////
+            fprintf( Output, " " );
+
+            if ( h != nCellsHor-1 )
+                if ( h&1 )
+                    fprintf( Output, "%c", DOUBLE_VERTICAL );
+                else
+                    fprintf( Output, "%c", SINGLE_VERTICAL );
+        }
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        fprintf( Output, "\n" );
+
+        Cudd_RecursiveDeref( dd, CubeVerBDD );
+
+        if ( v != nCellsVer-1 )
+        // print separator line
+        {
+            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+            if ( v&1 )
+            {
+                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", DOUBLES_CROSS );
+                        else
+                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
+                }
+                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
+            }
+            else
+            {
+                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
+                        else
+                            fprintf( Output, "%c", SINGLES_CROSS );
+                }
+                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
+            }
+            fprintf( Output, "\n" );
+        }
+    }
+    
+    ////////////////////////////////////////////////////////////////////
+    // print the lower line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
+    }
+    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
+    fprintf( Output, "\n" );
+
+    if ( !fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+
+            /////////////////////////////////
+            fprintf( Output, "%c", (char)('a'+d) );
+            /////////////////////////////////
+            fprintf( Output, "\n" );
+        }
+    }
+}
+
+
+
+/**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     []
+
+******************************************************************************/
+void Extra_PrintKMapRelation( 
+  FILE * Output,  /* the output stream */
+  DdManager * dd, 
+  DdNode * OnSet, 
+  DdNode * OffSet, 
+  int nXVars, 
+  int nYVars, 
+  DdNode ** XVars, 
+  DdNode ** YVars ) /* the flag which determines how support is computed */
+{
+    int d, p, n, s, v, h, w;
+    int nVars;
+    int nVarsVer;
+    int nVarsHor;
+    int nCellsVer;
+    int nCellsHor;
+    int nSkipSpaces;
+
+    // make sure that on-set and off-set do not overlap
+    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
+    {
+        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
+        return;
+    }
+
+    if ( OnSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 1\n" );
+        return;
+    }
+    if ( OffSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 0\n" );
+        return;
+    }
+
+    nVars = nXVars + nYVars;
+    if ( nVars < 0 || nVars > MAXVARS )
+    {
+        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
+        return;
+    }
+
+
+    ////////////////////////////////////////////////////////////////////
+    // determine the Karnaugh map parameters
+    nVarsVer = nXVars;
+    nVarsHor = nYVars;
+    nCellsVer = (1<<nVarsVer);
+    nCellsHor = (1<<nVarsHor);
+    nSkipSpaces = nVarsVer + 1;
+
+    ////////////////////////////////////////////////////////////////////
+    // print variable names
+    fprintf( Output, "\n" );
+    for ( w = 0; w < nVarsVer; w++ )
+        fprintf( Output, "%c", 'a'+nVarsHor+w );
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        fprintf( Output, " \\ " );
+        for ( w = 0; w < nVarsHor; w++ )
+            fprintf( Output, "%c", 'a'+w );
+    }
+    fprintf( Output, "\n" );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+            fprintf( Output, "\n" );
+        }
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // print the upper line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
+    }
+    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
+    fprintf( Output, "\n" );
+
+    ////////////////////////////////////////////////////////////////////
+    // print the map
+    for ( v = 0; v < nCellsVer; v++ )
+    {
+        DdNode * CubeVerBDD;
+
+        // print horizontal digits
+//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+        for ( n = 0; n < nVarsVer; n++ )
+            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
+                fprintf( Output, "1" );
+            else
+                fprintf( Output, "0" );
+        fprintf( Output, " " );
+
+        // find vertical cube
+//      CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor );    Cudd_Ref( CubeVerBDD );
+        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 );                 Cudd_Ref( CubeVerBDD );
+
+        // print text line
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        for ( h = 0; h < nCellsHor; h++ )
+        {
+            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
+
+            fprintf( Output, " " );
+//          fprintf( Output, "x" );
+            ///////////////////////////////////////////////////////////////
+            // determine what should be printed
+//          CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars );    Cudd_Ref( CubeHorBDD );
+            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 );        Cudd_Ref( CubeHorBDD );
+            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                           Cudd_Ref( Prod );
+            Cudd_RecursiveDeref( dd, CubeHorBDD );
+
+            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
+            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
+            Cudd_RecursiveDeref( dd, Prod );
+
+            if ( ValueOnSet == b1 && ValueOffSet == b0 )
+                fprintf( Output, "%c", SYMBOL_ONE );
+            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
+                fprintf( Output, "%c", SYMBOL_ZERO );
+            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
+                fprintf( Output, "%c", SYMBOL_DC );
+            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
+                fprintf( Output, "%c", SYMBOL_OVERLAP );
+            else
+                assert(0);
+
+            Cudd_RecursiveDeref( dd, ValueOnSet );
+            Cudd_RecursiveDeref( dd, ValueOffSet );
+            ///////////////////////////////////////////////////////////////
+            fprintf( Output, " " );
+
+            if ( h != nCellsHor-1 )
+                if ( h&1 )
+                    fprintf( Output, "%c", DOUBLE_VERTICAL );
+                else
+                    fprintf( Output, "%c", SINGLE_VERTICAL );
+        }
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        fprintf( Output, "\n" );
+
+        Cudd_RecursiveDeref( dd, CubeVerBDD );
+
+        if ( v != nCellsVer-1 )
+        // print separator line
+        {
+            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+            if ( v&1 )
+            {
+                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", DOUBLES_CROSS );
+                        else
+                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
+                }
+                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
+            }
+            else
+            {
+                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
+                        else
+                            fprintf( Output, "%c", SINGLES_CROSS );
+                }
+                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
+            }
+            fprintf( Output, "\n" );
+        }
+    }
+    
+    ////////////////////////////////////////////////////////////////////
+    // print the lower line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
+    }
+    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
+    fprintf( Output, "\n" );
+
+    if ( !fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+
+            /////////////////////////////////
+            fprintf( Output, "%c", (char)('a'+d) );
+            /////////////////////////////////
+            fprintf( Output, "\n" );
+        }
+    }
+}
+
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int GrayCode ( int BinCode )
+{
+  return BinCode ^ ( BinCode >> 1 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int BinCode ( int GrayCode )
+{
+  int bc = GrayCode;
+  while( GrayCode >>= 1 ) bc ^= GrayCode;
+  return bc;
+}
+
+
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 373ce5c5..932ed525 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+  Revision    [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -684,6 +684,41 @@ DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
     return bProd;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Computes the cube of BDD variables corresponding to bits it the bit-code]
+
+  Description [Returns a bdd composed of elementary bdds found in array BddVars[] such 
+  that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, 
+  the most significant bit is encoded with the first bdd variable). If the variables 
+  BddVars are not specified, takes the first CodeWidth variables of the manager]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst )
+{
+    int z;
+    DdNode * bTemp, * bVar, * bVarBdd, * bResult;
+
+    bResult = b1;   Cudd_Ref( bResult );
+    for ( z = 0; z < CodeWidth; z++ )
+    {
+        bVarBdd = (pbVars)? pbVars[z]: dd->vars[z];
+        if ( fMsbFirst )
+            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 );
+        else
+            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 );
+        bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar );     Cudd_Ref( bResult );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bResult );
+
+    return bResult;
+}  /* end of Extra_bddBitsToCube */
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 6cbf5d2c..42a0d84f 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/misc/extra/extraBddMisc.c \
+SRC +=    src/misc/extra/extraBddKmap.c \
+    src/misc/extra/extraBddMisc.c \
     src/misc/extra/extraBddSymm.c \
     src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilCanon.c \