Version abc60220

2 files changed, 248 insertions, 49 deletions

diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 3fd365d7..04385933 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -101,6 +101,7 @@ 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 );
@@ -109,6 +110,7 @@ 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 );
 
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 7905cbdd..2f83ddd5 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,6 +243,58 @@ 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
@@ -631,27 +683,21 @@ 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 );
-    fprintf( pFile, "%s: ", pOutputName );
+    if ( !fComp )
+        fprintf( pFile, "%s = ", pOutputName );
+    else
+        fprintf( pFile, "NOT(%s) = ", pOutputName );
     pInputNums = ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
-        if ( fComp )
-            fprintf( pFile, " Constant 0.\n" );
-        else
-            fprintf( pFile, " Constant 1.\n" );
+         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", pNode->S->index );
+            fprintf( pFile, "%d", 'a' + 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 )
@@ -664,25 +710,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
@@ -690,43 +736,39 @@ 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] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_OR )
     {
         // print the line
-        if ( fComp )
-            fprintf( pFile, "AND(" );
-        else
-            fprintf( pFile, "OR(" );
+        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, "%d", pInput->S->index );
+                    fprintf( pFile, "%c", 'a' + 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
@@ -734,43 +776,199 @@ 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] ), fComp ^ fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_EXOR )
     {
         // print the line
-        if ( fComp )
-            fprintf( pFile, "NEXOR(" );
-        else
-            fprintf( pFile, "EXOR(" );
+        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, "%d", pInput->S->index );
+                    fprintf( pFile, "%c", 'a' + pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[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
+        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" );
+        // 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 );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, " <%d>", pInputNums[i] );
             }
+            if ( fCompNew )
+                fprintf( pFile, "\'" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -778,9 +976,8 @@ 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] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
             }
     }
     free( pInputNums );