Version abc80130

7 files changed, 67 insertions, 287 deletions

diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index b73b81ab..5396bacd 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -28,12 +28,8 @@
 #ifndef __DSD_H__
 #define __DSD_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
-///                      TYPEDEF DEFINITIONS                         ///
+///                      TYPEDEF DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Dsd_Manager_t_   Dsd_Manager_t;
@@ -59,14 +55,14 @@ enum Dsd_Type_t_ {
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 // complementation and testing for pointers for decomposition entries
-#define Dsd_IsComplement(p)  (((int)((unsigned long) (p) & 01)))
-#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned long)(p) & ~01)) 
-#define Dsd_Not(p)           ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) 
-#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((unsigned long)(p) ^ (c)))
+#define Dsd_IsComplement(p)  (((int)((long) (p) & 01)))
+#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned)(p) & ~01)) 
+#define Dsd_Not(p)           ((Dsd_Node_t *)((long)(p) ^ 01)) 
+#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((long)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
@@ -80,7 +76,7 @@ enum Dsd_Type_t_ {
           Index++ )
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== dsdApi.c =======================================================*/
@@ -95,7 +91,6 @@ extern void            Dsd_NodeSetMark( Dsd_Node_t * p, int Mark );
 extern DdManager *     Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
 extern Dsd_Node_t *    Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
 extern Dsd_Node_t *    Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );
-extern Dsd_Node_t *    Dsd_ManagerReadConst1( Dsd_Manager_t * pMan );
 /*=== dsdMan.c =======================================================*/
 extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose );
 extern void            Dsd_ManagerStop( Dsd_Manager_t * dMan );
@@ -105,7 +100,6 @@ extern Dsd_Node_t *    Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc
 /*=== dsdTree.c =======================================================*/
 extern void            Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax );
 extern void            Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax );
-extern int             Dsd_TreeGetAigCost( Dsd_Node_t * pNode );
 extern int             Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * dMan );
 extern int             Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot );
 extern int             Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan );
@@ -114,16 +108,11 @@ extern int             Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, in
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
 extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
-extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
+
+#endif
\ No newline at end of file
diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c
index d1c90e23..daf3080f 100644
--- a/src/bdd/dsd/dsdApi.c
+++ b/src/bdd/dsd/dsdApi.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -89,7 +89,6 @@ void          Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark;     }
 ***********************************************************************/
 Dsd_Node_t *  Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i )  { return pMan->pRoots[i];  } 
 Dsd_Node_t *  Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } 
-Dsd_Node_t *  Dsd_ManagerReadConst1( Dsd_Manager_t * pMan )       { return pMan->pConst1;    } 
 DdManager *   Dsd_ManagerReadDd( Dsd_Manager_t * pMan )           { return pMan->dd;         } 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 58b824d2..608aa2e3 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -43,7 +43,7 @@ static Dds_Cache_t * pCache;
 static int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function********************************************************************
@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
 
 /**Function********************************************************************
 
-  Synopsis    [Deallocates the local cache.]
+  Synopsis    [Delocates the local cache.]
 
   Description []
 
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 62ce7e99..5008c24e 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -23,7 +23,7 @@
 #include "dsd.h"
 
 ////////////////////////////////////////////////////////////////////////
-///                      TYPEDEF DEFINITIONS                         ///
+///                      TYPEDEF DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
  
 typedef unsigned char byte;
@@ -42,7 +42,6 @@ struct Dsd_Manager_t_
     int            nRootsAlloc;// the number of primary outputs
     Dsd_Node_t **  pInputs;    // the primary input nodes
     Dsd_Node_t **  pRoots;     // the primary output nodes
-    Dsd_Node_t *   pConst1;    // the constant node
     int            fVerbose;   // the verbosity level 
 };
 
@@ -59,7 +58,7 @@ struct Dsd_Node_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 #define MAXINPUTS 1000
@@ -83,9 +82,9 @@ extern void         Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
 extern void         Dsd_TreeUnmark( Dsd_Manager_t * dMan );
 extern DdNode *     Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
 
+
+#endif
\ No newline at end of file
diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c
index 6e43f0f4..4529e75a 100644
--- a/src/bdd/dsd/dsdMan.c
+++ b/src/bdd/dsd/dsdMan.c
@@ -73,7 +73,6 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
     pNode->G = b1;  Cudd_Ref( pNode->G );
     pNode->S = b1;  Cudd_Ref( pNode->S );
     st_insert( dMan->Table, (char*)b1, (char*)pNode );
-    dMan->pConst1 = pNode;
 
     Dsd_CheckCacheAllocate( 5000 );
     return dMan;
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 543ad387..08c029e1 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -1255,7 +1255,7 @@ EXIT:
     s_CacheEntries++;
 
 
-/*
+#if 0
     if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
     {
         // write the function, for which verification does not work
@@ -1277,7 +1277,7 @@ EXIT:
         cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
         Cudd_RecursiveDerefZdd( dd, zNewFunc );
     }
-*/
+#endif
 
     }
 
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 2855d68d..7905cbdd 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -29,7 +29,7 @@ static int  Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode );
 static int  Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars );
 static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes );
 static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames );
-static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                      STATIC VARIABLES                            ///
@@ -243,58 +243,6 @@ void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts AIG nodes needed to implement this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode )
-{
-    int i, Counter = 0;
-
-    assert( pNode );
-    assert( !Dsd_IsComplement( pNode ) );
-    assert( pNode->nVisits >= 0 );
-
-    if ( pNode->nDecs < 2 )
-        return 0;
-
-    // we don't want the two-input gates to count for non-decomposable blocks
-    if ( pNode->Type == DSD_NODE_OR )
-        Counter += pNode->nDecs - 1;
-    else if ( pNode->Type == DSD_NODE_EXOR )
-        Counter += 3*(pNode->nDecs - 1);
-    else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 )
-        Counter += 3;
-
-    // call recursively
-    for ( i = 0; i < pNode->nDecs; i++ )
-        Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts AIG nodes needed to implement this node.]
-
-  Description [Assumes that the only primes of the DSD tree are MUXes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dsd_TreeGetAigCost( Dsd_Node_t * pNode )
-{
-    return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Counts non-terminal nodes of the DSD tree.]
 
   Description [Nonterminal nodes include all the nodes with the
@@ -683,21 +631,27 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
         pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
 
     Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
-    if ( !fComp )
-        fprintf( pFile, "%s = ", pOutputName );
-    else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
+    fprintf( pFile, "%s: ", pOutputName );
     pInputNums = ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
-         fprintf( pFile, " Constant 1.\n" );
+        if ( fComp )
+            fprintf( pFile, " Constant 0.\n" );
+        else
+            fprintf( pFile, " Constant 1.\n" );
     }
     else if ( pNode->Type == DSD_NODE_BUF )
     {
+        if ( fComp )
+            fprintf( pFile, " NOT(" );
+        else
+            fprintf( pFile, " " );
         if ( fShortNames )
-            fprintf( pFile, "%d", 'a' + pNode->S->index );
+            fprintf( pFile, "%d", pNode->S->index );
         else
             fprintf( pFile, "%s", pInputNames[pNode->S->index] );
+        if ( fComp )
+            fprintf( pFile, ")" );
         fprintf( pFile, "\n" );
     }
     else if ( pNode->Type == DSD_NODE_PRIME )
@@ -710,25 +664,25 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             fCompNew = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
                     fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
+                fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -736,39 +690,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( pInputNums[i] )
             {
                 pInput   = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_OR )
     {
         // print the line
-        fprintf( pFile, "OR(" );
+        if ( fComp )
+            fprintf( pFile, "AND(" );
+        else
+            fprintf( pFile, "OR(" );
         for ( i = 0; i < pNode->nDecs; i++ )
         {
             pInput = Dsd_Regular( pNode->pDecs[i] );
             fCompNew  = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
-                    fprintf( pFile, "%c", 'a' + pInput->S->index );
+                    fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
+                fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -776,208 +734,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( pInputNums[i] )
             {
                 pInput = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew  = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fComp ^ fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_EXOR )
     {
         // print the line
-        fprintf( pFile, "EXOR(" );
+        if ( fComp )
+            fprintf( pFile, "NEXOR(" );
+        else
+            fprintf( pFile, "EXOR(" );
         for ( i = 0; i < pNode->nDecs; i++ )
         {
             pInput = Dsd_Regular( pNode->pDecs[i] );
             fCompNew  = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
-                    fprintf( pFile, "%c", 'a' + pInput->S->index );
+                    fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
-        }
-        fprintf( pFile, " )\n" );
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
-            }
-    }
-    free( pInputNums );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the decompostion tree into file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
-{
-    Dsd_Node_t * pNodeR;
-    int SigCounter = 1;
-    pNodeR = Dsd_Regular(pNode);
-    Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints one node of the decomposition tree.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter )
-{
-    char Buffer[100];
-    Dsd_Node_t * pInput;
-    int * pInputNums;
-    int fCompNew, i;
-
-    assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || 
-        pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
-
-    Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
-    if ( !fComp )
-        fprintf( pFile, "%s = ", pOutputName );
-    else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
-    pInputNums = ALLOC( int, pNode->nDecs );
-    if ( pNode->Type == DSD_NODE_CONST1 )
-    {
-        fprintf( pFile, " Constant 1.\n" );
-    }
-    else if ( pNode->Type == DSD_NODE_BUF )
-    {
-        fprintf( pFile, " " );
-        fprintf( pFile, "%c", 'a' + pNode->S->index );
-        fprintf( pFile, "\n" );
-    }
-    else if ( pNode->Type == DSD_NODE_PRIME )
-    {
-        // print the line
-        fprintf( pFile, "PRIME(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput   = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew = (int)( pInput != pNode->pDecs[i] );
-            assert( fCompNew == 0 );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, " <%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
-        }
-        fprintf( pFile, " )\n" );
-/*
-        fprintf( pFile, " )  " );  
-        {
-            DdNode * bLocal;
-            bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd );  Cudd_Ref( bLocal );
-            Extra_bddPrint( dd, bLocal );
-            Cudd_RecursiveDeref( dd, bLocal );
-        }
-*/
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput   = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
-            }
-    }
-    else if ( pNode->Type == DSD_NODE_OR )
-    {
-        // print the line
-        fprintf( pFile, "OR(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew  = (int)( pInput != pNode->pDecs[i] );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, " <%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
-        }
-        fprintf( pFile, " )\n" );
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
-            }
-    }
-    else if ( pNode->Type == DSD_NODE_EXOR )
-    {
-        // print the line
-        fprintf( pFile, "EXOR(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew  = (int)( pInput != pNode->pDecs[i] );
-            assert( fCompNew == 0 );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -985,8 +778,9 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
             if ( pInputNums[i] )
             {
                 pInput = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew  = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     free( pInputNums );