diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-07 17:15:24 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-07 17:15:24 -0700 |
commit | 887f3c21cc69f4625228cca05016a97d6927aac1 (patch) | |
tree | 733e75b6b40895b3d4d3e42e670740ec2e0fe825 /src/aig/gia/giaSatLut.c | |
parent | f05986f7b393f570b486a0d7e5cb203e66dac1f8 (diff) | |
download | abc-887f3c21cc69f4625228cca05016a97d6927aac1.tar.gz abc-887f3c21cc69f4625228cca05016a97d6927aac1.tar.bz2 abc-887f3c21cc69f4625228cca05016a97d6927aac1.zip |
Supporting edges in delay-optimization in &satlut.
Diffstat (limited to 'src/aig/gia/giaSatLut.c')
-rw-r--r-- | src/aig/gia/giaSatLut.c | 61 |
1 files changed, 44 insertions, 17 deletions
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index f314733d..55a9e303 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -40,15 +40,21 @@ struct Sbl_Man_t_ int LogN; // base-2 log of max vars int Power2; // power-2 of LogN int FirstVar; // first variable to be used + // statistics + int nTried; // nodes tried + int nImproved; // nodes improved int nRuns; // the number of runs + int nSmallWins; // the number of small windows + int nLargeWins; // the number of large windows // 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 + int fVeryVerbose; // verbose + int fVeryVeryVerbose; // verbose // window Gia_Man_t * pGia; Vec_Int_t * vLeaves; // leaf nodes @@ -194,7 +200,6 @@ void Sbl_ManClean( Sbl_Man_t * p ) Vec_IntClear( p->vPolar ); // other Gia_ManFillValue( p->pGia ); - p->nRuns++; } void Sbl_ManStop( Sbl_Man_t * p ) { @@ -426,7 +431,7 @@ int Sbl_ManEvaluateMappingEdge( Sbl_Man_t * p, int DelayGlo ) // create critical path composed of all nodes Vec_WecForEachLevel( p->vWindow, vArray, i ) if ( Vec_IntSize(vArray) > 0 ) - Vec_IntPush( p->vPath, i ); + Vec_IntPush( p->vPath, Abc_Var2Lit(i, 1) ); return 0; } @@ -943,6 +948,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) int fKeepTrying = 1; abctime clk = Abc_Clock(), clk2; int i, status, Root, Count, StartSol, nConfTotal = 0, nIters = 0; + p->nTried++; Sbl_ManClean( p ); @@ -950,21 +956,25 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) Count = Sbl_ManWindow2( p, iPivot ); if ( Count == 0 ) { + if ( p->fVeryVerbose ) printf( "Obj %d: Window with less than %d nodes does not exist.\n", iPivot, p->nVars ); + p->nSmallWins++; return 0; } - if ( p->fVerbose ) + if ( p->fVeryVerbose ) printf( "\nObj = %6d : Leaf = %2d. AND = %2d. Root = %2d. LUT = %2d.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots), Vec_IntSize(p->vNodes) ); if ( Vec_IntSize(p->vLeaves) > 128 || Vec_IntSize(p->vAnds) > p->nVars ) { + if ( p->fVeryVerbose ) printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) ); + p->nLargeWins++; return 0; } if ( Vec_IntSize(p->vAnds) < 10 ) { - if ( p->fVerbose ) + if ( p->fVeryVerbose ) printf( "Skipping.\n" ); return 0; } @@ -974,7 +984,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) // derive SAT instance Sbl_ManCreateCnf( p ); - if ( p->fVeryVerbose ) + if ( p->fVeryVeryVerbose ) 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->vCutsI1) - Vec_IntSize(p->vAnds), sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI1) ); @@ -997,7 +1007,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) { int Count = 0, LitCount = 0; int nConfBef, nConfAft; - if ( p->fVerbose ) + if ( p->fVeryVerbose ) printf( "Trying to find mapping with %d LUTs.\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) ); @@ -1010,6 +1020,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) nConfAft = (int)p->pSat->stats.conflicts; nConfTotal += nConfAft - nConfBef; nIters++; + p->nRuns++; if ( status == l_True ) p->timeSatSat += Abc_Clock() - clk2; else if ( status == l_False ) @@ -1020,7 +1031,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) break; if ( status == l_True ) { - if ( p->fVeryVerbose ) + if ( p->fVeryVeryVerbose ) { for ( i = 0; i < Vec_IntSize(p->vAnds); i++ ) printf( "%d", sat_solver_var_value(p->pSat, i) ); @@ -1041,9 +1052,9 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ ) if ( sat_solver_var_value(p->pSat, i) ) { - if ( p->fVeryVerbose ) + if ( p->fVeryVeryVerbose ) printf( "Cut %3d : Node = %3d %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) ); - if ( p->fVeryVerbose ) + if ( p->fVeryVeryVerbose ) LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar ); Vec_IntPush( p->vSolCur, i-p->FirstVar ); } @@ -1060,7 +1071,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) if ( p->fDelay && !Sbl_ManEvaluateMapping(p, p->DelayMax) ) { int iLit, value; - if ( p->fVerbose ) + if ( p->fVeryVerbose ) { printf( "Critical path of length (%d) is detected: ", Vec_IntSize(p->vPath) ); Vec_IntForEachEntry( p->vPath, iLit, i ) @@ -1080,7 +1091,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) } else fKeepTrying = 0; - if ( p->fVerbose ) + if ( p->fVeryVerbose ) { if ( status == l_False ) printf( "UNSAT " ); @@ -1094,10 +1105,15 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) printf( "Total " ); printf( "confl =%8d. ", nConfTotal ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - if ( p->fVeryVerbose && status == l_True ) + if ( p->fVeryVeryVerbose && status == l_True ) printf( "LitCount = %d.\n", LitCount ); printf( "\n" ); } + if ( nIters == 20 ) + { + printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters ); + break; + } } // update solution @@ -1112,18 +1128,24 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot ) } else nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax ); + if ( p->fVerbose ) printf( "Object %5d : Saved %2d nodes (Conf =%8d) Iter =%3d Delay = %d Edges = %4d\n", iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur ); p->timeTotal += Abc_Clock() - p->timeStart; + p->nImproved++; return 2; } + else + { +// printf( "Object %5d : Saved %2d nodes (Conf =%8d) Iter =%3d\n", iPivot, 0, nConfTotal, nIters ); + } p->timeTotal += Abc_Clock() - p->timeStart; return 1; } void Sbl_ManPrintRuntime( Sbl_Man_t * p ) { + printf( "Runtime breakdown:\n" ); 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 ); @@ -1133,9 +1155,8 @@ void Sbl_ManPrintRuntime( Sbl_Man_t * p ) 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 ) +void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose ) { int iLut, nImproveCount = 0; Sbl_Man_t * p = Sbl_ManAlloc( pGia, nNumber ); @@ -1144,8 +1165,10 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, 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; + p->fVeryVerbose = fVeryVerbose; + if ( p->fVerbose ) + printf( "Parameters: WinSize = %d AIG nodes. Conf = %d. DelayMax = %d.\n", p->nVars, p->nBTLimit, p->DelayMax ); // determine delay limit if ( fDelay && pGia->vEdge1 && p->DelayMax == 0 ) p->DelayMax = Gia_ManEvalEdgeDelay( pGia ); @@ -1159,6 +1182,10 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, break; } Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL ); + if ( p->fVerbose ) + printf( "Tried = %d. Improved = %d. Small win = %d. Large win = %d. Total SAT runs = %d.\n", + p->nTried, p->nImproved, p->nSmallWins, p->nLargeWins, p->nRuns ); + if ( p->fVerbose ) Sbl_ManPrintRuntime( p ); Sbl_ManStop( p ); } |