summaryrefslogtreecommitdiffstats
path: root/src/bdd/dsd
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-08-22 22:18:38 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-08-22 22:18:38 -0700
commitcbbf78e6f4d8acd32b0afcdc0e4e87bc318a2590 (patch)
treedae1c1e4fa97a711905d518bbd2169e8c6e2f1f2 /src/bdd/dsd
parentc344f3e38c60147cacd8a5d414625b832192ccee (diff)
downloadabc-cbbf78e6f4d8acd32b0afcdc0e4e87bc318a2590.tar.gz
abc-cbbf78e6f4d8acd32b0afcdc0e4e87bc318a2590.tar.bz2
abc-cbbf78e6f4d8acd32b0afcdc0e4e87bc318a2590.zip
Improving print-out of 'dsd -p'.
Diffstat (limited to 'src/bdd/dsd')
-rw-r--r--src/bdd/dsd/dsd.h1
-rw-r--r--src/bdd/dsd/dsdTree.c114
2 files changed, 115 insertions, 0 deletions
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;