Improving print-out of 'dsd -p'.

4 files changed, 154 insertions, 1 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 45c017bb..b54bdee0 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3006,6 +3006,41 @@ Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the miter outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachAnd( p, pObj, i )
+        Gia_ManAppendCo( pNew, pObj->Value );
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    assert( Gia_ManIsNormalized(pNew) );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 481639dd..29982468 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -137,7 +137,10 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
     {
         ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
         ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
-        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+        if ( fVerbose )
+            Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
+        else
+            Dsd_TreePrint2( stdout, pManDsd, ppNamesCi, ppNamesCo, -1 );
         ABC_FREE( ppNamesCi );
         ABC_FREE( ppNamesCo );
     }
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 7bb6111f..49fe4552 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -116,6 +116,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_TreePrint2( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], 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 e534e00a..35c69ffe 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "dsdInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -832,6 +833,119 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
   SeeAlso     []
 
 ***********************************************************************/
+word Dsd_TreeFunc2Truth_rec( DdManager * dd, DdNode * bFunc )
+{
+    word Cof0, Cof1;
+    int Level;
+    if ( bFunc == b0 )
+        return 0;
+    if ( bFunc == b1 )
+        return ~(word)0;
+    if ( Cudd_IsComplement(bFunc) )
+        return ~Dsd_TreeFunc2Truth_rec( dd, Cudd_Not(bFunc) );
+    Level = dd->perm[bFunc->index];
+    assert( Level >= 0 && Level < 6 );
+    Cof0 = Dsd_TreeFunc2Truth_rec( dd, cuddE(bFunc) );
+    Cof1 = Dsd_TreeFunc2Truth_rec( dd, cuddT(bFunc) );
+    return (s_Truths6[Level] & Cof1) | (~s_Truths6[Level] & Cof0);
+}
+void Dsd_TreePrint2_rec( FILE * pFile, DdManager * dd, Dsd_Node_t * pNode, int fComp, char * pInputNames[] )
+{
+    int i;
+    if ( pNode->Type == DSD_NODE_CONST1 )
+    {
+        fprintf( pFile, "Const%d", !fComp );
+        return;
+    }
+    assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
+//    fprintf( pFile, "%s", (fComp ^ (pNode->Type == DSD_NODE_OR))? "!" : "" );
+    if ( pNode->Type == DSD_NODE_BUF )
+    {
+        fprintf( pFile, "%s", fComp? "!" : "" );
+        fprintf( pFile, "%s", pInputNames[pNode->S->index] );
+    }
+    else if ( pNode->Type == DSD_NODE_PRIME )
+    {
+        fprintf( pFile, " " );
+        if ( pNode->nDecs <= 6 )
+        {
+            extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
+            char pCanonPerm[6]; int uCanonPhase;
+            // compute truth table
+            DdNode * bFunc = Dsd_TreeGetPrimeFunction( dd, pNode );  
+            word uTruth = Dsd_TreeFunc2Truth_rec( dd, bFunc );
+            Cudd_Ref( bFunc );
+            Cudd_RecursiveDeref( dd, bFunc );
+            // canonicize truth table
+            uCanonPhase = Abc_TtCanonicize( &uTruth, pNode->nDecs, pCanonPerm );
+            fprintf( pFile, "%s", (fComp ^ ((uCanonPhase >> pNode->nDecs) & 1)) ? "!" : "" );
+            Abc_TtPrintHexRev( pFile, &uTruth, pNode->nDecs );
+            fprintf( pFile, "{" );
+            for ( i = 0; i < pNode->nDecs; i++ )
+            {
+                Dsd_Node_t * pInput = pNode->pDecs[(int)pCanonPerm[i]];
+                Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pInput), Dsd_IsComplement(pInput) ^ ((uCanonPhase>>i)&1), pInputNames );
+            }
+            fprintf( pFile, "} " );
+        }
+        else
+        {
+            fprintf( pFile, "|%d|", pNode->nDecs );
+            fprintf( pFile, "{" );
+            for ( i = 0; i < pNode->nDecs; i++ )
+                Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+            fprintf( pFile, "} " );
+        }
+    }
+    else if ( pNode->Type == DSD_NODE_OR )
+    {
+        fprintf( pFile, "%s", !fComp? "!" : "" );
+        fprintf( pFile, "(" );
+        for ( i = 0; i < pNode->nDecs; i++ )
+            Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), !Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+        fprintf( pFile, ")" );
+    }
+    else if ( pNode->Type == DSD_NODE_EXOR )
+    {
+        fprintf( pFile, "%s", fComp? "!" : "" );
+        fprintf( pFile, "[" );
+        for ( i = 0; i < pNode->nDecs; i++ )
+            Dsd_TreePrint2_rec( pFile, dd, Dsd_Regular(pNode->pDecs[i]), Dsd_IsComplement(pNode->pDecs[i]), pInputNames );
+        fprintf( pFile, "]" );
+    }
+}
+void Dsd_TreePrint2( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int Output )
+{
+    if ( Output == -1 )
+    {
+        int i;
+        for ( i = 0; i < pDsdMan->nRoots; i++ )
+        {
+            fprintf( pFile, "%8s = ", pOutputNames[i] );
+            Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[i]), Dsd_IsComplement(pDsdMan->pRoots[i]), pInputNames );
+            fprintf( pFile, "\n" );
+        }
+    }
+    else
+    {
+        assert( Output >= 0 && Output < pDsdMan->nRoots );
+        fprintf( pFile, "%8s = ", pOutputNames[Output] );
+        Dsd_TreePrint2_rec( pFile, pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[Output]), Dsd_IsComplement(pDsdMan->pRoots[Output]), pInputNames );
+        fprintf( pFile, "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decompostion tree into file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
 {
     Dsd_Node_t * pNodeR;