From 416ffc117ab7d0ea2ec3b8aaeb4724f25031db7a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 27 Mar 2008 08:01:00 -0700 Subject: Version abc80327 --- src/opt/mfs/mfsCore.c | 57 +++++++++++++++++++++++++++++++++++++++------------ src/opt/mfs/mfsInt.h | 6 +++++- src/opt/mfs/mfsMan.c | 8 ++++---- src/opt/mfs/mfsSat.c | 25 ++++++++++++++-------- 4 files changed, 70 insertions(+), 26 deletions(-) (limited to 'src/opt') diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c index 59ee7488..2a2c9d43 100644 --- a/src/opt/mfs/mfsCore.c +++ b/src/opt/mfs/mfsCore.c @@ -101,6 +101,7 @@ p->timeSat += clock() - clk; int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Hop_Obj_t * pObj; + int RetValue; extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare ); int nGain, clk; @@ -129,8 +130,15 @@ clk = clock(); if ( p->pSat == NULL ) return 0; // solve the SAT problem - Abc_NtkMfsSolveSat( p, pNode ); + RetValue = Abc_NtkMfsSolveSat( p, pNode ); + p->nTotConfLevel += p->pSat->stats.conflicts; p->timeSat += clock() - clk; + if ( RetValue == 0 ) + { + p->nTimeOutsLevel++; + p->nTimeOuts++; + return 0; + } // minimize the local function of the node using bi-decomposition assert( p->nFanins == Abc_ObjFaninNum(pNode) ); pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare ); @@ -139,6 +147,7 @@ p->timeSat += clock() - clk; { p->nNodesDec++; p->nNodesGained += nGain; + p->nNodesGainedLevel += nGain; pNode->pData = pObj; } return 1; @@ -163,7 +172,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) ProgressBar * pProgress; Mfs_Man_t * p; Abc_Obj_t * pObj; - int i, nFaninMax, clk = clock(); + Vec_Vec_t * vLevels; + Vec_Ptr_t * vNodes; + int i, k, nNodes, nFaninMax, clk = clock(), clk2; int nTotalNodesBeg = Abc_NtkNodeNum(pNtk); int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk); @@ -223,24 +234,44 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars ) Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel ); // compute don't-cares for each node + nNodes = 0; p->nTotalNodesBeg = nTotalNodesBeg; p->nTotalEdgesBeg = nTotalEdgesBeg; - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); - Abc_NtkForEachNode( pNtk, pObj, i ) + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); + vLevels = Abc_NtkLevelize( pNtk ); + Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 ) { - if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) - continue; - if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) - continue; if ( !p->pPars->fVeryVerbose ) - Extra_ProgressBarUpdate( pProgress, i, NULL ); - if ( pPars->fResub ) - Abc_NtkMfsResub( p, pObj ); - else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) - Abc_NtkMfsNode( p, pObj ); + Extra_ProgressBarUpdate( pProgress, nNodes, NULL ); + p->nNodesGainedLevel = 0; + p->nTotConfLevel = 0; + p->nTimeOutsLevel = 0; + clk2 = clock(); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax ) + break; + if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX ) + continue; + if ( pPars->fResub ) + Abc_NtkMfsResub( p, pObj ); + else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 ) + Abc_NtkMfsNode( p, pObj ); + } + nNodes += Vec_PtrSize(vNodes); + if ( pPars->fVerbose ) + { + printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %% ", + k, Vec_PtrSize(vNodes), + 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes), + 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes), + 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) ); + PRT( "Time", clock() - clk2 ); + } } Extra_ProgressBarStop( pProgress ); Abc_NtkStopReverseLevels( pNtk ); + Vec_VecFree( vLevels ); // perform the sweeping if ( !pPars->fResub ) diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index f4da45ef..37521189 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -70,6 +70,7 @@ struct Mfs_Man_t_ Bdc_Man_t * pManDec; int nNodesDec; int nNodesGained; + int nNodesGainedLevel; // solving data Aig_Man_t * pAigWin; // window AIG with constraints Cnf_Dat_t * pCnf; // the CNF for the window @@ -78,6 +79,8 @@ struct Mfs_Man_t_ Vec_Int_t * vMem; // memory for intermediate SOPs Vec_Vec_t * vLevels; // levelized structure for updating Vec_Ptr_t * vFanins; // the new set of fanins + int nTotConfLim; // total conflict limit + int nTotConfLevel; // total conflicts on this level // the result of solving int nFanins; // the number of fanins int nWords; // the number of words @@ -91,6 +94,7 @@ struct Mfs_Man_t_ int nNodesBad; int nTotalDivs; int nTimeOuts; + int nTimeOutsLevel; int nDcMints; double dTotalRatios; // node/edge stats @@ -136,7 +140,7 @@ extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode ); extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsSat.c ==========================================================*/ -extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); +extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ); /*=== mfsStrash.c ==========================================================*/ extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode ); extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode ); diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index f1b3f44c..d0642368 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -126,13 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p ) } else { - printf( "Nodes = %d. DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", - p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, + printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n", + Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare, 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal ); // printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", // 1.0-(p->dTotalRatios/p->nNodesTried) ); - printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n", - p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained ); + printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n", + p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts ); } /* PRTP( "Win", p->timeWin , p->timeTotal ); diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index 2529e207..5023bf62 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -42,9 +42,14 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) { int Lits[MFS_FANIN_MAX]; - int RetValue, iVar, b, Mint; - RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); - assert( RetValue == l_False || RetValue == l_True ); + int RetValue, nBTLimit, iVar, b, Mint; + if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts ) + return -1; + nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0; + RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); + assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False ); + if ( RetValue == l_Undef ) + return -1; if ( RetValue == l_False ) return 0; p->nCares++; @@ -77,12 +82,12 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) SideEffects [] SeeAlso [] - + ***********************************************************************/ -void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) +int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) { Aig_Obj_t * pObjPo; - int i; + int RetValue, i; // collect projection variables Vec_IntClear( p->vProjVars ); Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) ) @@ -98,7 +103,10 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) // iterate through the SAT assignments p->nCares = 0; - while ( Abc_NtkMfsSolveSat_iter(p) ); + p->nTotConfLim = p->pPars->nBTLimit; + while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 ); + if ( RetValue == -1 ) + return 0; // write statistics p->nMintsCare += p->nCares; @@ -113,7 +121,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) // map the care if ( p->nFanins > 4 ) - return; + return 1; if ( p->nFanins == 4 ) p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16); if ( p->nFanins == 3 ) @@ -122,6 +130,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) | (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28); assert( p->nFanins != 1 ); + return 1; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3