summaryrefslogtreecommitdiffstats
path: root/src/aig/bdc/bdcDec.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/bdc/bdcDec.c')
-rw-r--r--src/aig/bdc/bdcDec.c115
1 files changed, 109 insertions, 6 deletions
diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c
index 13a33196..55ce97a0 100644
--- a/src/aig/bdc/bdcDec.c
+++ b/src/aig/bdc/bdcDec.c
@@ -30,6 +30,82 @@
/**Function*************************************************************
+ Synopsis [Minimizes the support of the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ int v, clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ // compute support
+ pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
+ Kit_TruthSupport( pIsf->puOff, p->nVars );
+ // go through the support variables
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( (pIsf->uSupp & (1 << v)) == 0 )
+ continue;
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+ Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+ if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+ continue;
+// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+// continue;
+ // remove the variable
+ Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+ Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+// Kit_TruthExist( pIsf->puOn, p->nVars, v );
+// Kit_TruthExist( pIsf->puOff, p->nVars, v );
+ pIsf->uSupp &= ~(1 << v);
+ }
+ if ( p->pPars->fVerbose )
+ p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes the support of the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ int v, clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ // go through the support variables
+ pIsf->uSupp = 0;
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
+ !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
+ continue;
+ if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+ {
+ Kit_TruthExist( pIsf->puOn, p->nVars, v );
+ Kit_TruthExist( pIsf->puOff, p->nVars, v );
+ continue;
+ }
+ pIsf->uSupp |= (1 << v);
+ }
+ if ( p->pPars->fVerbose )
+ p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
Synopsis [Updates the ISF of the right after the left was decompoosed.]
Description []
@@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// check if there is any reuse for the components
if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
{
+ p->numReuse++;
+ p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
{
+ p->numReuse++;
+ p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
@@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// compare the two-component costs
if ( WeightOr > WeightAnd )
{
+ if ( WeightOr < BDC_SCALE )
+ p->numWeaks++;
+ p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
+ if ( WeightAnd < BDC_SCALE )
+ p->numWeaks++;
+ p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
@@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
int Var, VarMin, nSuppMin, nSuppCur;
unsigned uSupp0, uSupp1;
+ int clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
VarMin = -1;
nSuppMin = 1000;
for ( Var = 0; Var < p->nVars; Var++ )
@@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
nSuppMin = nSuppCur;
VarMin = Var;
-// break;
+ break;
}
}
if ( VarMin >= 0 )
@@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
Bdc_SuppMinimize( p, pIsfL );
Bdc_SuppMinimize( p, pIsfR );
}
+ if ( p->pPars->fVerbose )
+ p->timeMuxes += clock() - clk;
return VarMin;
}
@@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
Bdc_Isf_t IsfL, * pIsfL = &IsfL;
Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+ int iVar, clk;
/*
printf( "Init function (%d):\n", LocalCounter );
Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
@@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
*/
// check computed results
assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
- if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ pFunc = Bdc_TableLookup( p, pIsf );
+ if ( p->pPars->fVerbose )
+ p->timeCache += clock() - clk;
+ if ( pFunc )
return pFunc;
// decide on the decomposition type
+ if ( p->pPars->fVerbose )
+ clk = clock();
Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ p->timeCheck += clock() - clk;
if ( Type == BDC_TYPE_MUX )
{
- int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ p->timeMuxes += clock() - clk;
+ p->numMuxes++;
pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
if ( pFunc0 == NULL || pFunc1 == NULL )
@@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
// create new gate
pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
}
- if ( pFunc == NULL )
- return NULL;
- assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
return pFunc;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 05:28:00 +0000