diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-04 12:51:05 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-04 12:51:05 -0700 |
commit | 720082753f06fbb0429def0f3e67ccc7848b89b2 (patch) | |
tree | aaf98c2dcee10e017609283fa601f3b0328935a1 /src/aig/gia/giaSatLut.c | |
parent | 4a954c1b23aad9b7189dd76164d3e5a61ca6b39f (diff) | |
download | abc-720082753f06fbb0429def0f3e67ccc7848b89b2.tar.gz abc-720082753f06fbb0429def0f3e67ccc7848b89b2.tar.bz2 abc-720082753f06fbb0429def0f3e67ccc7848b89b2.zip |
Improvements to delay-optimization in &satlut.
Diffstat (limited to 'src/aig/gia/giaSatLut.c')
-rw-r--r-- | src/aig/gia/giaSatLut.c | 399 |
1 files changed, 249 insertions, 150 deletions
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 44b5e2e1..23d1b407 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -33,49 +33,193 @@ ABC_NAMESPACE_IMPL_START typedef struct Sbl_Man_t_ Sbl_Man_t; struct Sbl_Man_t_ { - sat_solver * pSat; // SAT solver - Vec_Int_t * vCardVars; // candinality variables - int LogN; // max vars - int FirstVar; // first variable to be used - int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2) - int nInputs; // the number of inputs - int nEdges; // the number of edges + sat_solver * pSat; // SAT solver + Vec_Int_t * vCardVars; // candinality variables + int nVars; // max vars + int LogN; // base-2 log of max vars + int Power2; // power-2 of LogN + int FirstVar; // first variable to be used + int nRuns; // the number of runs + // parameters + int nBTLimit; // conflicts + int DelayMax; // external delay + int nEdges; // the number of edges + int fDelay; // delay mode + int fReverse; // reverse windowing + int fVeryVerbose; // verbose + int fVerbose; // verbose // window - Gia_Man_t * pGia; - Vec_Int_t * vLeaves; // leaf nodes - Vec_Int_t * vAnds; // AND-gates - Vec_Int_t * vNodes; // internal LUTs - Vec_Int_t * vRoots; // driver nodes (a subset of vAnds) - Vec_Int_t * vRootVars; // driver nodes (as SAT variables) + Gia_Man_t * pGia; + Vec_Int_t * vLeaves; // leaf nodes + Vec_Int_t * vAnds; // AND-gates + Vec_Int_t * vNodes; // internal LUTs + Vec_Int_t * vRoots; // driver nodes (a subset of vAnds) + Vec_Int_t * vRootVars; // driver nodes (as SAT variables) // timing - Vec_Int_t * vArrs; // arrival times - Vec_Int_t * vReqs; // required times - Vec_Wec_t * vWindow; // fanins of each node in the window - Vec_Int_t * vPath; // critical path (as SAT variables) - Vec_Int_t * vEdges; // fanin edges + Vec_Int_t * vArrs; // arrival times + Vec_Int_t * vReqs; // required times + Vec_Wec_t * vWindow; // fanins of each node in the window + Vec_Int_t * vPath; // critical path (as SAT variables) + Vec_Int_t * vEdges; // fanin edges // cuts - Vec_Wrd_t * vCutsI; // input bit patterns - Vec_Wrd_t * vCutsN; // node bit patterns - Vec_Int_t * vCutsNum; // cut counts for each obj - Vec_Int_t * vCutsStart; // starting cuts for each obj - Vec_Int_t * vCutsObj; // object to which this cut belongs - Vec_Wrd_t * vTempI; // temporary cuts - Vec_Wrd_t * vTempN; // temporary cuts - Vec_Int_t * vSolInit; // initial solution - Vec_Int_t * vSolCur; // current solution - Vec_Int_t * vSolBest; // best solution + Vec_Wrd_t * vCutsI; // input bit patterns + Vec_Wrd_t * vCutsN; // node bit patterns + Vec_Int_t * vCutsNum; // cut counts for each obj + Vec_Int_t * vCutsStart; // starting cuts for each obj + Vec_Int_t * vCutsObj; // object to which this cut belongs + Vec_Wrd_t * vTempI; // temporary cuts + Vec_Wrd_t * vTempN; // temporary cuts + Vec_Int_t * vSolInit; // initial solution + Vec_Int_t * vSolCur; // current solution + Vec_Int_t * vSolBest; // best solution // temporary - Vec_Int_t * vLits; // literals - Vec_Int_t * vAssump; // literals - Vec_Int_t * vPolar; // variables polarity + Vec_Int_t * vLits; // literals + Vec_Int_t * vAssump; // literals + Vec_Int_t * vPolar; // variables polarity + // statistics + abctime timeWin; // windowing + abctime timeCut; // cut computation + abctime timeSat; // SAT runtime + abctime timeSatSat; // satisfiable time + abctime timeSatUns; // unsatisfiable time + abctime timeSatUnd; // undecided time + abctime timeTime; // timing time + abctime timeStart; // starting time + abctime timeTotal; // all runtime + abctime timeOther; // other time }; +extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int Number ) +{ + Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 ); + p->nVars = Number; + p->LogN = Abc_Base2Log(Number); + p->Power2 = 1 << p->LogN; + p->pSat = Sbm_AddCardinSolver( p->LogN, &p->vCardVars ); + p->FirstVar = sat_solver_nvars( p->pSat ); + sat_solver_bookmark( p->pSat ); + // window + p->pGia = pGia; + p->vLeaves = Vec_IntAlloc( p->nVars ); + p->vAnds = Vec_IntAlloc( p->nVars ); + p->vNodes = Vec_IntAlloc( p->nVars ); + p->vRoots = Vec_IntAlloc( p->nVars ); + p->vRootVars = Vec_IntAlloc( p->nVars ); + // timing + p->vArrs = Vec_IntAlloc( 0 ); + p->vReqs = Vec_IntAlloc( 0 ); + p->vWindow = Vec_WecAlloc( 128 ); + p->vPath = Vec_IntAlloc( 32 ); + p->vEdges = Vec_IntAlloc( 32 ); + // cuts + p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns + p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns + p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj + p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj + p->vCutsObj = Vec_IntAlloc( 1000 ); + p->vSolInit = Vec_IntAlloc( 64 ); + p->vSolCur = Vec_IntAlloc( 64 ); + p->vSolBest = Vec_IntAlloc( 64 ); + p->vTempI = Vec_WrdAlloc( 32 ); + p->vTempN = Vec_WrdAlloc( 32 ); + // internal + p->vLits = Vec_IntAlloc( 64 ); + p->vAssump = Vec_IntAlloc( 64 ); + p->vPolar = Vec_IntAlloc( 1000 ); + // other + Gia_ManFillValue( pGia ); + return p; +} +void Sbl_ManClean( Sbl_Man_t * p ) +{ + p->timeStart = Abc_Clock(); + sat_solver_rollback( p->pSat ); + sat_solver_bookmark( p->pSat ); + // internal + Vec_IntClear( p->vLeaves ); + Vec_IntClear( p->vAnds ); + Vec_IntClear( p->vNodes ); + Vec_IntClear( p->vRoots ); + Vec_IntClear( p->vRootVars ); + // timing + Vec_IntClear( p->vArrs ); + Vec_IntClear( p->vReqs ); + Vec_WecClear( p->vWindow ); + Vec_IntClear( p->vPath ); + Vec_IntClear( p->vEdges ); + // cuts + Vec_WrdClear( p->vCutsI ); + Vec_WrdClear( p->vCutsN ); + Vec_IntClear( p->vCutsNum ); + Vec_IntClear( p->vCutsStart ); + Vec_IntClear( p->vCutsObj ); + Vec_IntClear( p->vSolInit ); + Vec_IntClear( p->vSolCur ); + Vec_IntClear( p->vSolBest ); + Vec_WrdClear( p->vTempI ); + Vec_WrdClear( p->vTempN ); + // temporary + Vec_IntClear( p->vLits ); + Vec_IntClear( p->vAssump ); + Vec_IntClear( p->vPolar ); + // other + Gia_ManFillValue( p->pGia ); + p->nRuns++; +} +void Sbl_ManStop( Sbl_Man_t * p ) +{ + sat_solver_delete( p->pSat ); + Vec_IntFree( p->vCardVars ); + // internal + Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vAnds ); + Vec_IntFree( p->vNodes ); + Vec_IntFree( p->vRoots ); + Vec_IntFree( p->vRootVars ); + // timing + Vec_IntFree( p->vArrs ); + Vec_IntFree( p->vReqs ); + Vec_WecFree( p->vWindow ); + Vec_IntFree( p->vPath ); + Vec_IntFree( p->vEdges ); + // cuts + Vec_WrdFree( p->vCutsI ); + Vec_WrdFree( p->vCutsN ); + Vec_IntFree( p->vCutsNum ); + Vec_IntFree( p->vCutsStart ); + Vec_IntFree( p->vCutsObj ); + Vec_IntFree( p->vSolInit ); + Vec_IntFree( p->vSolCur ); + Vec_IntFree( p->vSolBest ); + Vec_WrdFree( p->vTempI ); + Vec_WrdFree( p->vTempN ); + // temporary + Vec_IntFree( p->vLits ); + Vec_IntFree( p->vAssump ); + Vec_IntFree( p->vPolar ); + // other + ABC_FREE( p ); +} + +/**Function************************************************************* + Synopsis [Timing computation.] Description [] @@ -211,6 +355,7 @@ int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins ) } int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo ) { + abctime clk = Abc_Clock(); Vec_Int_t * vFanins; int i, iLut = -1, iAnd, Delay, Required, Edges; Vec_IntClear( p->vPath ); @@ -233,6 +378,7 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo ) if ( Delay > Required ) // updated timing exceeded original timing break; } + p->timeTime += Abc_Clock() - clk; if ( i == Vec_IntSize(p->vRoots) ) return 1; // derive the critical path @@ -332,7 +478,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p ) SeeAlso [] ***********************************************************************/ -static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs ) +static int Sbl_ManPrintCut( word CutI, word CutN ) { int b, Count = 0; printf( "{ " ); @@ -348,7 +494,7 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs ) } static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c ) { - return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c), Vec_IntSize(p->vLeaves) ); + return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c) ); } static inline int Sbl_CutIsFeasible( word CutI, word CutN ) { @@ -411,11 +557,11 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN ) int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj ); int i; //printf( "\nLooking for:\n" ); - //Sbl_ManPrintCut( CutI, CutN, p->nInputs ); + //Sbl_ManPrintCut( CutI, CutN ); //printf( "\n" ); for ( i = Start0; i < Limit0; i++ ) { - //Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs ); + //Sbl_ManPrintCut( pCutsI[i], pCutsN[i] ); if ( pCutsI[i] == CutI && pCutsN[i] == CutN ) return i; } @@ -423,9 +569,10 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN ) } int Sbl_ManComputeCuts( Sbl_Man_t * p ) { + abctime clk = Abc_Clock(); Gia_Obj_t * pObj; Vec_Int_t * vFanins; int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds); - assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 ); + assert( Vec_IntSize(p->vLeaves) <= p->nVars && Vec_IntSize(p->vAnds) <= p->nVars ); // assign leaf cuts Vec_IntClear( p->vCutsStart ); Vec_IntClear( p->vCutsObj ); @@ -510,6 +657,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p ) pObj->Value = ~0; Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i ) pObj->Value = ~0; + p->timeCut += Abc_Clock() - clk; return Vec_WrdSize(p->vCutsI); } int Sbl_ManCreateCnf( Sbl_Man_t * p ) @@ -573,80 +721,6 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p ) SeeAlso [] ***********************************************************************/ -Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN ) -{ - Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 ); - extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ); - p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars ); - p->LogN = LogN; - p->FirstVar = sat_solver_nvars( p->pSat ); - // window - p->pGia = pGia; - p->vLeaves = Vec_IntAlloc( 64 ); - p->vAnds = Vec_IntAlloc( 64 ); - p->vNodes = Vec_IntAlloc( 64 ); - p->vRoots = Vec_IntAlloc( 64 ); - p->vRootVars = Vec_IntAlloc( 64 ); - // timing - p->vArrs = Vec_IntAlloc( 0 ); - p->vReqs = Vec_IntAlloc( 0 ); - p->vWindow = Vec_WecAlloc( 128 ); - p->vPath = Vec_IntAlloc( 32 ); - p->vEdges = Vec_IntAlloc( 32 ); - // cuts - p->vCutsI = Vec_WrdAlloc( 1000 ); // input bit patterns - p->vCutsN = Vec_WrdAlloc( 1000 ); // node bit patterns - p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj - p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj - p->vCutsObj = Vec_IntAlloc( 1000 ); - p->vSolInit = Vec_IntAlloc( 64 ); - p->vSolCur = Vec_IntAlloc( 64 ); - p->vSolBest = Vec_IntAlloc( 64 ); - p->vTempI = Vec_WrdAlloc( 32 ); - p->vTempN = Vec_WrdAlloc( 32 ); - // internal - p->vLits = Vec_IntAlloc( 64 ); - p->vAssump = Vec_IntAlloc( 64 ); - p->vPolar = Vec_IntAlloc( 1000 ); - // other - Gia_ManFillValue( pGia ); - return p; -} - -void Sbl_ManStop( Sbl_Man_t * p ) -{ - sat_solver_delete( p->pSat ); - Vec_IntFree( p->vCardVars ); - // internal - Vec_IntFree( p->vLeaves ); - Vec_IntFree( p->vAnds ); - Vec_IntFree( p->vNodes ); - Vec_IntFree( p->vRoots ); - Vec_IntFree( p->vRootVars ); - // timing - Vec_IntFree( p->vArrs ); - Vec_IntFree( p->vReqs ); - Vec_WecFree( p->vWindow ); - Vec_IntFree( p->vPath ); - Vec_IntFree( p->vEdges ); - // cuts - Vec_WrdFree( p->vCutsI ); - Vec_WrdFree( p->vCutsN ); - Vec_IntFree( p->vCutsNum ); - Vec_IntFree( p->vCutsStart ); - Vec_IntFree( p->vCutsObj ); - Vec_IntFree( p->vSolInit ); - Vec_IntFree( p->vSolCur ); - Vec_IntFree( p->vSolBest ); - Vec_WrdFree( p->vTempI ); - Vec_WrdFree( p->vTempN ); - // temporary - Vec_IntFree( p->vLits ); - Vec_IntFree( p->vAssump ); - Vec_IntFree( p->vPolar ); - // other - ABC_FREE( p ); -} void Sbl_ManWindow( Sbl_Man_t * p ) { @@ -667,8 +741,10 @@ void Sbl_ManWindow( Sbl_Man_t * p ) int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot ) { + abctime clk = Abc_Clock(); Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds; int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds ); + p->timeWin += Abc_Clock() - clk; if ( Count == 0 ) return 0; Vec_IntClear( p->vRoots ); Vec_IntAppend( p->vRoots, vRoots ); @@ -684,41 +760,34 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot ) return Count; } -int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int nEdges, int fDelay, int fVeryVerbose, int fVerbose ) +int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) { int fKeepTrying = 1; abctime clk = Abc_Clock(), clk2; - int i, LogN = 6, nVars = 1 << LogN, status, Root; - Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN ); - int StartSol, Count, nConfTotal = 0, nIters = 0; + int i, status, Root, Count, StartSol, nConfTotal = 0, nIters = 0; - p->nEdges = nEdges; - fVerbose |= fVeryVerbose; - Vec_IntClear( p->vSolBest ); + Sbl_ManClean( p ); // compute one window Count = Sbl_ManWindow2( p, iPivot ); if ( Count == 0 ) { printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 ); - Sbl_ManStop( p ); return 0; } - if ( fVerbose ) + if ( p->fVerbose ) printf( "\nObj = %6d : Leaf = %2d. LUT = %2d. AND = %2d. Root = %2d.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) ); - if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 ) + + if ( Vec_IntSize(p->vLeaves) > p->nVars || Vec_IntSize(p->vAnds) > p->nVars ) { printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) ); - Sbl_ManStop( p ); return 0; } - if ( Vec_IntSize(p->vAnds) < 10 ) { - if ( fVerbose ) + if ( p->fVerbose ) printf( "Skipping.\n" ); - Sbl_ManStop( p ); return 0; } @@ -727,10 +796,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in // derive SAT instance Sbl_ManCreateCnf( p ); - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) Vec_IntPrint( p->vSolInit ); - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n", sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds), sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) ); @@ -740,7 +809,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in Vec_IntClear( p->vAssump ); Vec_IntPush( p->vAssump, -1 ); // unused variables - for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ ) + for ( i = Vec_IntSize(p->vAnds); i < p->Power2; i++ ) Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); // root variables Vec_IntForEachEntry( p->vRootVars, Root, i ) @@ -752,7 +821,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in while ( fKeepTrying && StartSol-fKeepTrying > 0 ) { int nConfBef, nConfAft; - if ( fVerbose ) + if ( p->fVerbose ) printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying ); // for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ ) // Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) ); @@ -760,20 +829,27 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in // solve the problem clk2 = Abc_Clock(); nConfBef = (int)p->pSat->stats.conflicts; - status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 ); + status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), p->nBTLimit, 0, 0, 0 ); + p->timeSat += Abc_Clock() - clk2; nConfAft = (int)p->pSat->stats.conflicts; nConfTotal += nConfAft - nConfBef; nIters++; + if ( status == l_True ) + p->timeSatSat += Abc_Clock() - clk2; + else if ( status == l_False ) + p->timeSatUns += Abc_Clock() - clk2; + else + p->timeSatUnd += Abc_Clock() - clk2; if ( status == l_Undef ) break; if ( status == l_True ) { int Count = 0, LitCount = 0; - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) { printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n", Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), - Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars ); + Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), p->nVars ); for ( i = 0; i < Vec_IntSize(p->vAnds); i++ ) printf( "%d", sat_solver_var_value(p->pSat, i) ); printf( "\n" ); @@ -793,15 +869,15 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) if ( sat_solver_var_value(p->pSat, i) ) { - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) printf( "Cut %3d : Node = %3d Node = %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) ); - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar ); Vec_IntPush( p->vSolCur, i-p->FirstVar ); } - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) printf( "LitCount = %d.\n", LitCount ); - if ( fVeryVerbose ) + if ( p->fVeryVerbose ) Vec_IntPrint( p->vRootVars ); //Vec_IntPrint( p->vRoots ); //Vec_IntPrint( p->vAnds ); @@ -812,10 +888,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in // check the timing if ( status == l_True ) { - if ( fDelay && !Sbl_ManEvaluateMapping(p, DelayMax) ) + if ( p->fDelay && !Sbl_ManEvaluateMapping(p, p->DelayMax) ) { int iLit, value; - if ( fVerbose ) + if ( p->fVerbose ) { printf( "Critical path of length (%d) is detected: ", Vec_IntSize(p->vPath) ); Vec_IntForEachEntry( p->vPath, iLit, i ) @@ -835,7 +911,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in } else fKeepTrying = 0; - if ( fVerbose ) + if ( p->fVerbose ) { if ( status == l_False ) printf( "UNSAT " ); @@ -856,31 +932,54 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in // update solution if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) ) { - int nDelay, nEdges; - nDelay = Sbl_ManCreateTiming( p, DelayMax, &nEdges ); + int nDelayCur, nEdgesCur; + nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax, &nEdgesCur ); Sbl_ManUpdateMapping( p ); printf( "Object %5d : Saved %d nodes (Conf =%8d) Iter =%3d Delay = %d Edges = %4d\n", - iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelay, nEdges ); - Sbl_ManStop( p ); + iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur ); + p->timeTotal += Abc_Clock() - p->timeStart; return 2; } - Sbl_ManStop( p ); + p->timeTotal += Abc_Clock() - p->timeStart; return 1; } - -void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose ) +void Sbl_ManPrintRuntime( Sbl_Man_t * p ) +{ + p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeSat - p->timeTime; + + ABC_PRTP( "Win ", p->timeWin , p->timeTotal ); + ABC_PRTP( "Cut ", p->timeCut , p->timeTotal ); + ABC_PRTP( "Sat ", p->timeSat, p->timeTotal ); + ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal ); + ABC_PRTP( " Unsat", p->timeSatUns, p->timeTotal ); + ABC_PRTP( " Undec", p->timeSatUnd, p->timeTotal ); + ABC_PRTP( "Timing", p->timeTime , p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "ALL ", p->timeTotal, p->timeTotal ); + printf( "Total runs = %d.\n", p->nRuns ); +} +void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose ) { - int iLut; + int iLut, nImproveCount = 0; + Sbl_Man_t * p = Sbl_ManAlloc( pGia, nNumber ); + p->nBTLimit = nBTLimit; // conflicts + p->DelayMax = DelayMax; // external delay + p->nEdges = nEdges; // the number of edges + p->fDelay = fDelay; // delay mode + p->fReverse = fReverse; // reverse windowing + p->fVeryVerbose = fVeryVerbose; // verbose + p->fVerbose = fVerbose | fVeryVerbose; Gia_ManComputeOneWinStart( pGia, fReverse ); Gia_ManForEachLut2( pGia, iLut ) { -// if ( iLut > 259 ) -// break; - if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, nEdges, fDelay, fVeryVerbose, fVerbose ) != 2 ) + if ( Sbl_ManTestSat( p, iLut ) != 2 ) continue; -// break; + if ( ++nImproveCount == nImproves ) + break; } Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL ); + Sbl_ManPrintRuntime( p ); + Sbl_ManStop( p ); } //////////////////////////////////////////////////////////////////////// |