From 320c429bc46728c1faddfc561c166810aa134a04 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 1 Mar 2008 08:01:00 -0800 Subject: Version abc80301 --- src/opt/mfs/mfs.h | 1 + src/opt/mfs/mfsInt.h | 1 + src/opt/mfs/mfsInter.c | 4 ++-- src/opt/mfs/mfsMan.c | 4 ++-- src/opt/mfs/mfsResub.c | 41 +++++++++++++++++++++++++++++++++-------- 5 files changed, 39 insertions(+), 12 deletions(-) (limited to 'src/opt/mfs') diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index cb2da431..d3f7277d 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -47,6 +47,7 @@ struct Mfs_Par_t_ int nDivMax; // the maximum number of divisors int nWinSizeMax; // the maximum size of the window int nGrowthLevel; // the maximum allowed growth in level + int nBTLimit; // the maximum number of conflicts in one SAT run int fResub; // performs resubstitution int fArea; // performs optimization for area int fMoreEffort; // performs high-affort minimization diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 3c0349bb..f98f6239 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -84,6 +84,7 @@ struct Mfs_Man_t_ int nMintsTotal; int nNodesBad; int nTotalDivs; + int nTimeOuts; // node/edge stats int nTotalNodesBeg; int nTotalNodesEnd; diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 65acd4eb..24617cd9 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -226,10 +226,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands ) pSat = Abc_MfsCreateSolverResub( p, pCands, nCands ); // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); if ( status != l_False ) { - printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" ); + p->nTimeOuts++; return NULL; } // get the learned clauses diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index 421f62af..99a60ef6 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p ) p->nTotalEdgesBeg-p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg ); printf( "\n" ); - printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n", - Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls ); + printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n", + Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts ); if ( p->pPars->fSwapEdge ) printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 4171c111..8908da2f 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -100,10 +100,15 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands ) unsigned * pData; int RetValue, iVar, i; p->nSatCalls++; - RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); - assert( RetValue == l_False || RetValue == l_True ); + RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); +// assert( RetValue == l_False || RetValue == l_True ); if ( RetValue == l_False ) return 1; + if ( RetValue != l_True ) + { + p->nTimeOuts++; + return -1; + } p->nSatCexes++; // store the counter-example Vec_IntForEachEntry( p->vProjVars, iVar, i ) @@ -135,7 +140,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; unsigned * pData; int pCands[MFS_FANIN_MAX]; - int iVar, i, nCands, nWords, w, clk; + int RetValue, iVar, i, nCands, nWords, w, clk; Abc_Obj_t * pFanin; Hop_Obj_t * pFunc; assert( iFanin >= 0 ); @@ -163,7 +168,10 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); } - if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) ) + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) { if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin ); @@ -173,6 +181,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; // update the network Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); p->timeInt += clock() - clk; @@ -225,7 +235,10 @@ p->timeInt += clock() - clk; return 0; pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); - if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) ) + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) { if ( fVeryVerbose ) printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar ); @@ -235,6 +248,8 @@ p->timeInt += clock() - clk; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 ); + if ( pFunc == NULL ) + return 0; // update the network Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); @@ -263,7 +278,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80; unsigned * pData, * pData2; int pCands[MFS_FANIN_MAX]; - int iVar, iVar2, i, w, nCands, clk, nWords, fBreak; + int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak; Abc_Obj_t * pFanin; Hop_Obj_t * pFunc; assert( iFanin >= 0 ); @@ -292,7 +307,10 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i; pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); } - if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) ) + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) { if ( fVeryVerbose ) printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 ); @@ -300,6 +318,8 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands ); + if ( pFunc == NULL ) + return 0; // update the network Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc ); p->timeInt += clock() - clk; @@ -360,7 +380,10 @@ p->timeInt += clock() - clk; pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); - if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ) ) + RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 ); + if ( RetValue == -1 ) + return 0; + if ( RetValue == 1 ) { if ( fVeryVerbose ) printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 ); @@ -368,6 +391,8 @@ p->timeInt += clock() - clk; clk = clock(); // derive the function pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 ); + if ( pFunc == NULL ) + return 0; // update the network Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar2) ); Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) ); -- cgit v1.2.3