summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c12
-rw-r--r--src/base/abci/abcDelay.c2
-rw-r--r--src/base/abci/abcIf.c59
-rw-r--r--src/map/if/if.h2
-rw-r--r--src/map/if/ifCore.c13
-rw-r--r--src/map/if/ifCut.c143
-rw-r--r--src/map/if/ifMan.c1
-rw-r--r--src/map/if/ifMap.c4
-rw-r--r--src/opt/mfs/mfsCore.c2
-rw-r--r--src/opt/mfs/mfsInt.h4
-rw-r--r--src/opt/mfs/mfsInter.c102
-rw-r--r--src/opt/mfs/mfsMan.c1
-rw-r--r--src/sat/bsat/module.make1
13 files changed, 330 insertions, 16 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aea02c0e..368ee2a8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10750,7 +10750,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nAreaIters = 2;
pPars->DelayTarget = -1;
pPars->Epsilon = (float)0.001;
- pPars->fPreprocess = 1;
+ pPars->fPreprocess = 1;
pPars->fArea = 0;
pPars->fFancy = 0;
pPars->fExpRed = 1;
@@ -10898,8 +10898,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
// get LUT size from the library
pPars->nLutSize = pPars->pLutLib->LutMax;
// if variable pin delay, force truth table computation
- if ( pPars->pLutLib->fVarPinDelays )
- pPars->fTruth = 1;
+// if ( pPars->pLutLib->fVarPinDelays )
+// pPars->fTruth = 1;
}
if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
@@ -10924,11 +10924,15 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (c = Abc_NtkGetChoiceNum( pNtk )) )
{
printf( "Performing LUT mapping with %d choices.\n", c );
- pPars->fTruth = 1;
+// pPars->fTruth = 1;
+ pPars->fExpRed = 0;
}
// enable truth table computation if cut minimization is selected
if ( pPars->fCutMin )
+ {
pPars->fTruth = 1;
+ pPars->fExpRed = 0;
+ }
// complain if truth tables are requested but the cut size is too large
if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 67e051f3..553bb2fc 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -96,7 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
***********************************************************************/
float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
{
- int fUseSorting = 0;
+ int fUseSorting = 1;
int pPinPerm[32];
float pPinDelays[32];
If_Lib_t * pLutLib;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 742a3a02..bf351a47 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -252,8 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
pCutBest = If_ObjCutBest( pIfObj );
- if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
- If_CutRotatePins( pIfMan, pCutBest );
+// if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
+// If_CutRotatePins( pIfMan, pCutBest );
if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
@@ -346,6 +346,54 @@ Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_
return gFunc;
}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively derives the truth table for the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+ If_Cut_t * pCut;
+ If_Obj_t * pTemp;
+ Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+ // get the best cut
+ pCut = If_ObjCutBest(pIfObj);
+ // if the cut is visited, return the result
+ if ( If_CutData(pCut) )
+ return If_CutData(pCut);
+ // mark the node as visited
+ Vec_PtrPush( vVisited, pCut );
+ // insert the worst case
+ If_CutSetData( pCut, (void *)1 );
+ // skip in case of primary input
+ if ( If_ObjIsCi(pIfObj) )
+ return If_CutData(pCut);
+ // compute the functions of the children
+ for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+ {
+ gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited );
+ if ( gFunc0 == (void *)1 )
+ continue;
+ gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited );
+ if ( gFunc1 == (void *)1 )
+ continue;
+ // both branches are solved
+ gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) );
+ if ( pTemp->fPhase != pIfObj->fPhase )
+ gFunc = Hop_Not(gFunc);
+ If_CutSetData( pCut, gFunc );
+ break;
+ }
+ return If_CutData(pCut);
+}
+
/**Function*************************************************************
Synopsis [Derives the truth table for one cut.]
@@ -371,7 +419,12 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
// recursively compute the function while collecting visited cuts
Vec_PtrClear( pIfMan->vTemp );
- gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp );
+ gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp );
+ if ( gFunc == (void *)1 )
+ {
+ printf( "Abc_NodeIfToHop(): Computing local AIG has failed.\n" );
+ return NULL;
+ }
// printf( "%d ", Vec_PtrSize(p->vTemp) );
// clean the cuts
If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 32d458dc..6c33e03f 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -166,6 +166,8 @@ struct If_Man_t_
int nSmallSupp; // the small support
// timing manager
Tim_Man_t * pManTim;
+ // statistics
+// int timeTruth;
};
// priority cut
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 16a14153..99b99af7 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -110,14 +110,14 @@ int If_ManPerformMappingComb( If_Man_t * p )
If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Delay" );
// try to improve area by expanding and reducing the cuts
- if ( p->pPars->fExpRed && !p->pPars->fTruth )
+ if ( p->pPars->fExpRed )
If_ManImproveMapping( p );
// area flow oriented mapping
for ( i = 0; i < p->pPars->nFlowIters; i++ )
{
If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, "Flow" );
- if ( p->pPars->fExpRed && !p->pPars->fTruth )
+ if ( p->pPars->fExpRed )
If_ManImproveMapping( p );
}
@@ -125,7 +125,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
for ( i = 0; i < p->pPars->nAreaIters; i++ )
{
If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, "Area" );
- if ( p->pPars->fExpRed && !p->pPars->fTruth )
+ if ( p->pPars->fExpRed )
If_ManImproveMapping( p );
}
@@ -139,6 +139,13 @@ int If_ManPerformMappingComb( If_Man_t * p )
// printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) );
s_MappingTime = clock() - clkTotal;
// printf( "Special POs = %d.\n", If_ManCountSpecialPos(p) );
+ {
+ extern int If_CutGetCones( If_Man_t * p );
+ extern int If_CutCountTotalFanins( If_Man_t * p );
+// If_CutGetCones( p );
+// If_CutCountTotalFanins( p );
+ }
+
return 1;
}
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index cc842c19..08653d95 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -980,6 +980,149 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
return aResult;
}
+/**Function*************************************************************
+
+ Synopsis [Computes the cone of the cut in AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int If_CutGetCutMinLevel( If_Man_t * p, If_Cut_t * pCut )
+{
+ If_Obj_t * pLeaf;
+ int i, nMinLevel = IF_INFINITY;
+ If_CutForEachLeaf( p, pCut, pLeaf, i )
+ nMinLevel = IF_MIN( nMinLevel, (int)pLeaf->Level );
+ return nMinLevel;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cone of the cut in AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int If_CutGetCone_rec( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
+{
+ If_Obj_t * pTemp;
+ int i, RetValue;
+ // check if the node is in the cut
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ if ( pCut->pLeaves[i] == pObj->Id )
+ return 1;
+ else if ( pCut->pLeaves[i] > pObj->Id )
+ break;
+ // return if we reached the boundary
+ if ( If_ObjIsCi(pObj) )
+ return 0;
+ // check the choice node
+ for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+ {
+ // check if the node itself is bound
+ RetValue = If_CutGetCone_rec( p, If_ObjFanin0(pTemp), pCut );
+ if ( RetValue )
+ RetValue &= If_CutGetCone_rec( p, If_ObjFanin1(pTemp), pCut );
+ if ( RetValue )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cone of the cut in AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int If_CutGetCones( If_Man_t * p )
+{
+ If_Obj_t * pObj;
+ int i, Counter = 0;
+ int clk = clock();
+ If_ManForEachObj( p, pObj, i )
+ {
+ if ( If_ObjIsAnd(pObj) && pObj->nRefs )
+ {
+ Counter += !If_CutGetCone_rec( p, pObj, If_ObjCutBest(pObj) );
+// printf( "%d ", If_CutGetCutMinLevel( p, If_ObjCutBest(pObj) ) );
+ }
+ }
+ printf( "Cound not find boundary for %d nodes.\n", Counter );
+ PRT( "Cones", clock() - clk );
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cone of the cut in AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void If_CutFoundFanins_rec( If_Obj_t * pObj, Vec_Int_t * vLeaves )
+{
+ if ( pObj->nRefs || If_ObjIsCi(pObj) )
+ {
+ Vec_IntPushUnique( vLeaves, pObj->Id );
+ return;
+ }
+ If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves );
+ If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cone of the cut in AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int If_CutCountTotalFanins( If_Man_t * p )
+{
+ If_Obj_t * pObj;
+ Vec_Int_t * vLeaves;
+ int i, nFaninsTotal = 0, Counter = 0;
+ int clk = clock();
+ vLeaves = Vec_IntAlloc( 100 );
+ If_ManForEachObj( p, pObj, i )
+ {
+ if ( If_ObjIsAnd(pObj) && pObj->nRefs )
+ {
+ nFaninsTotal += If_ObjCutBest(pObj)->nLeaves;
+ Vec_IntClear( vLeaves );
+ If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves );
+ If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves );
+ Counter += Vec_IntSize(vLeaves);
+ }
+ }
+ printf( "Total cut inputs = %d. Total fanins incremental = %d.\n", nFaninsTotal, Counter );
+ PRT( "Fanins", clock() - clk );
+ Vec_IntFree( vLeaves );
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 1528b08c..7bb7fcd1 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -124,6 +124,7 @@ void If_ManRestart( If_Man_t * p )
***********************************************************************/
void If_ManStop( If_Man_t * p )
{
+// PRT( "Truth", p->timeTruth );
// printf( "Small support = %d.\n", p->nSmallSupp );
Vec_PtrFree( p->vCis );
Vec_PtrFree( p->vCos );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 1ac5ef21..fafd454d 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -119,7 +119,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// compute the truth table
pCut->fCompl = 0;
if ( p->pPars->fTruth )
+ {
+// int clk = clock();
If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+// p->timeTruth += clock() - clk;
+ }
// compute the application-specific cost and depth
pCut->fUser = (p->pPars->pFuncCost != NULL);
pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0;
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 7e6cd454..4a2e96e7 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -68,7 +68,7 @@ clk = clock();
p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
- p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+ p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
if ( p->pSat == NULL )
{
p->nNodesBad++;
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index f98f6239..b7fa6ef0 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -85,6 +85,7 @@ struct Mfs_Man_t_
int nNodesBad;
int nTotalDivs;
int nTimeOuts;
+ int nDcMints;
// node/edge stats
int nTotalNodesBeg;
int nTotalNodesEnd;
@@ -115,8 +116,9 @@ struct Mfs_Man_t_
/*=== mfsDiv.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
/*=== mfsInter.c ==========================================================*/
-extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
+extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert );
extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
+extern int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands );
/*=== mfsMan.c ==========================================================*/
extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars );
extern void Mfs_ManStop( Mfs_Man_t * p );
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 24617cd9..5944fd5b 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -82,7 +82,7 @@ int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
SeeAlso []
***********************************************************************/
-sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
+sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
{
sat_solver * pSat;
Aig_Obj_t * pObjPo;
@@ -90,7 +90,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
// get the literal for the output of F
pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
- Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
+ Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
// collect the outputs of the divisors
Vec_IntClear( p->vProjVars );
@@ -210,6 +210,100 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
SeeAlso []
***********************************************************************/
+unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
+{
+ sat_solver * pSat;
+ Sto_Man_t * pCnf = NULL;
+ unsigned * puTruth;
+ int nFanins, status;
+ int c, i, * pGloVars;
+
+ // derive the SAT solver for interpolation
+ pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert );
+
+ // solve the problem
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( status != l_False )
+ {
+ p->nTimeOuts++;
+ return NULL;
+ }
+ // get the learned clauses
+ pCnf = sat_solver_store_release( pSat );
+ sat_solver_delete( pSat );
+
+ // set the global variables
+ pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
+ for ( c = 0; c < nCands; c++ )
+ {
+ // get the variable number of this divisor
+ i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+ // get the corresponding SAT variable
+ pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+ }
+
+ // derive the interpolant
+ nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+ Sto_ManFree( pCnf );
+ assert( nFanins == nCands );
+ return puTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs interpolation.]
+
+ Description [Derives the new function of the node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands )
+{
+ unsigned * pTruth, uTruth0[2], uTruth1[2];
+ int nCounter;
+ pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 0 );
+ if ( nCands == 6 )
+ {
+ uTruth1[0] = pTruth[0];
+ uTruth1[1] = pTruth[1];
+ }
+ else
+ {
+ uTruth1[0] = pTruth[0];
+ uTruth1[1] = pTruth[0];
+ }
+ pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 1 );
+ if ( nCands == 6 )
+ {
+ uTruth0[0] = ~pTruth[0];
+ uTruth0[1] = ~pTruth[1];
+ }
+ else
+ {
+ uTruth0[0] = ~pTruth[0];
+ uTruth0[1] = ~pTruth[0];
+ }
+ nCounter = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] );
+ nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] );
+// printf( "%d ", nCounter );
+ return nCounter;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs interpolation.]
+
+ Description [Derives the new function of the node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
@@ -222,8 +316,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
int nFanins, status;
int c, i, * pGloVars;
+// p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
+
// derive the SAT solver for interpolation
- pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
+ pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
// solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 99a60ef6..5f947aeb 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -122,6 +122,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
else
Abc_NtkMfsPrintResubStats( p );
+// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
}
else
{
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index 1e52cc0a..f6805600 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -1,6 +1,7 @@
SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satInter.c \
src/sat/bsat/satInterA.c \
+ src/sat/bsat/satInterP.c \
src/sat/bsat/satSolver.c \
src/sat/bsat/satStore.c \
src/sat/bsat/satTrace.c \
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 14:12:33 +0000