summaryrefslogtreecommitdiffstats
path: root/src/aig/bdc/bdcCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/bdc/bdcCore.c')
-rw-r--r--src/aig/bdc/bdcCore.c128
1 files changed, 100 insertions, 28 deletions
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index 157927b1..f0b0f3bc 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -42,15 +42,12 @@
Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
{
Bdc_Man_t * p;
- unsigned * pData;
- int i, k, nBits;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
- p->nNodesLimit = 0; // will be set later
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
@@ -62,22 +59,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
p->vSpots = Vec_IntAlloc( 256 );
// truth tables
- p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
- // set elementary truth tables
- nBits = (1 << pPars->nVarsMax);
- Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
- for ( k = 0; k < pPars->nVarsMax; k++ )
- {
- pData = Vec_PtrEntry( p->vTruths, k+1 );
- Kit_TruthClear( pData, p->nVars );
- for ( i = 0; i < nBits; i++ )
- if ( i & (1 << k) )
- pData[i>>5] |= (1 << (i&31));
- }
- p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
- p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
- p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
- p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
+ p->vTruths = Vec_PtrAllocTruthTables( p->pPars->nVarsMax );
+ p->puTemp1 = ALLOC( unsigned, 4 * p->nWords );
+ p->puTemp2 = p->puTemp1 + p->nWords;
+ p->puTemp3 = p->puTemp2 + p->nWords;
+ p->puTemp4 = p->puTemp3 + p->nWords;
// start the internal ISFs
p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL );
p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
@@ -102,6 +88,7 @@ void Bdc_ManFree( Bdc_Man_t * p )
Vec_IntFree( p->vMemory );
Vec_IntFree( p->vSpots );
Vec_PtrFree( p->vTruths );
+ free( p->puTemp1 );
free( p->pNodes );
free( p->pTable );
free( p );
@@ -126,16 +113,25 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
Bdc_TableClear( p );
Vec_IntClear( p->vMemory );
// add constant 1 and elementary vars
- p->nNodes = p->nNodesNew = 0;
- for ( i = 0; i <= p->pPars->nVarsMax; i++ )
+ p->nNodes = 0;
+ p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0);
+ // add constant 1
+ pNode = Bdc_FunNew( p );
+ pNode->Type = BDC_TYPE_CONST1;
+ pNode->puFunc = NULL;
+ pNode->uSupp = 0;
+ Bdc_TableAdd( p, pNode );
+ // add variables
+ for ( i = 0; i < p->nVars; i++ )
{
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_PI;
pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
- pNode->uSupp = i? (1 << (i-1)) : 0;
+ pNode->uSupp = (1 << i);
Bdc_TableAdd( p, pNode );
}
// add the divisors
+ if ( vDivs )
Vec_PtrForEachEntry( vDivs, puTruth, i )
{
pNode = Bdc_FunNew( p );
@@ -146,6 +142,40 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
if ( i == p->nDivsLimit )
break;
}
+ assert( p->nNodesNew == 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Clears the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+ Bdc_Fun_t * pNode;
+ int i;
+ printf( " 0 : Const 1\n" );
+ for ( i = 1; i < p->nNodes; i++ )
+ {
+ printf( " %d : ", i );
+ pNode = p->pNodes + i;
+ if ( pNode->Type == BDC_TYPE_PI )
+ printf( "PI " );
+ else
+ {
+ printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
+ printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
+ }
+ Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
+ printf( "\n" );
+ }
+ printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
}
/**Function*************************************************************
@@ -162,25 +192,67 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
+ assert( nVars <= p->pPars->nVarsMax );
// set current manager parameters
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( nVars );
+ p->nNodesMax = nNodesMax;
Bdc_ManPrepare( p, vDivs );
- p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
// copy the function
Bdc_IsfStart( p, pIsf );
- Bdc_IsfClean( pIsf );
- pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
- Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
- Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
- // call decomposition
+ if ( puCare )
+ {
+ Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
+ Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
+ }
+ else
+ {
+ Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars );
+ Kit_TruthNot( pIsf->puOff, puFunc, p->nVars );
+ }
Bdc_SuppMinimize( p, pIsf );
+ // call decomposition
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
if ( p->pRoot == NULL )
return -1;
return p->nNodesNew;
}
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of one function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
+{
+ static int Counter = 0;
+ static int Total = 0;
+ Bdc_Par_t Pars = {0}, * pPars = &Pars;
+ Bdc_Man_t * p;
+ int RetValue;
+// unsigned uCare = ~0x888f888f;
+ unsigned uCare = ~0;
+// unsigned uFunc = 0x88888888;
+// unsigned uFunc = 0xf888f888;
+// unsigned uFunc = 0x117e117e;
+// unsigned uFunc = 0x018b018b;
+ unsigned uFunc = uTruth;
+
+ pPars->nVarsMax = 8;
+ p = Bdc_ManAlloc( pPars );
+ RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 );
+ Total += RetValue;
+ printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total );
+// Bdc_ManDecPrint( p );
+ Bdc_ManFree( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:23:57 +0000