summaryrefslogtreecommitdiffstats
path: root/src/bdd/dsd
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/dsd')
-rw-r--r--src/bdd/dsd/dsd.h29
-rw-r--r--src/bdd/dsd/dsdApi.c3
-rw-r--r--src/bdd/dsd/dsdCheck.c4
-rw-r--r--src/bdd/dsd/dsdInt.h9
-rw-r--r--src/bdd/dsd/dsdMan.c1
-rw-r--r--src/bdd/dsd/dsdProc.c4
-rw-r--r--src/bdd/dsd/dsdTree.c304
7 files changed, 287 insertions, 67 deletions
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 5396bacd..b73b81ab 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -28,8 +28,12 @@
#ifndef __DSD_H__
#define __DSD_H__
+#ifdef __cplusplus
+extern "C" {
+#endif
+
////////////////////////////////////////////////////////////////////////
-/// TYPEDEF DEFITIONS ///
+/// TYPEDEF DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Dsd_Manager_t_ Dsd_Manager_t;
@@ -55,14 +59,14 @@ enum Dsd_Type_t_ {
};
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFITIONS ///
+/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// complementation and testing for pointers for decomposition entries
-#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)))
+#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)))
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
@@ -76,7 +80,7 @@ enum Dsd_Type_t_ {
Index++ )
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFITIONS ///
+/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== dsdApi.c =======================================================*/
@@ -91,6 +95,7 @@ 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 );
@@ -100,6 +105,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 );
@@ -108,11 +114,16 @@ 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 daf3080f..d1c90e23 100644
--- a/src/bdd/dsd/dsdApi.c
+++ b/src/bdd/dsd/dsdApi.c
@@ -23,7 +23,7 @@
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFITIONS ///
+/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
@@ -89,6 +89,7 @@ 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 608aa2e3..58b824d2 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 DEFITIONS ///
+/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function********************************************************************
@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
/**Function********************************************************************
- Synopsis [Delocates the local cache.]
+ Synopsis [Deallocates the local cache.]
Description []
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 5008c24e..62ce7e99 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -23,7 +23,7 @@
#include "dsd.h"
////////////////////////////////////////////////////////////////////////
-/// TYPEDEF DEFITIONS ///
+/// TYPEDEF DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef unsigned char byte;
@@ -42,6 +42,7 @@ 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
};
@@ -58,7 +59,7 @@ struct Dsd_Node_t_
};
////////////////////////////////////////////////////////////////////////
-/// MACRO DEFITIONS ///
+/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define MAXINPUTS 1000
@@ -82,9 +83,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 4529e75a..6e43f0f4 100644
--- a/src/bdd/dsd/dsdMan.c
+++ b/src/bdd/dsd/dsdMan.c
@@ -73,6 +73,7 @@ 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 08c029e1..543ad387 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 7905cbdd..2855d68d 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,208 @@ 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" );
+/*
+ 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 );
}
else
{
pInputNums[i] = (*pSigCounter)++;
fprintf( pFile, " <%d>", pInputNums[i] );
}
+ if ( fCompNew )
+ fprintf( pFile, "\'" );
}
fprintf( pFile, " )\n" );
// call recursively for the following blocks
@@ -778,9 +985,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 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 07:40:36 +0000