From 01924ca118cad9bc8bf84de0525e54f5c4a832ec Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 31 Dec 2016 20:21:46 +0700 Subject: Updates to delay optimization project. --- src/opt/dau/dauGia.c | 2 +- src/opt/sbd/sbd.h | 2 + src/opt/sbd/sbdCore.c | 446 +++++++++++++++++++++++++++++++++----------------- src/opt/sbd/sbdCut.c | 68 ++++++-- src/opt/sbd/sbdInt.h | 39 +++-- src/opt/sbd/sbdLut.c | 1 - src/opt/sbd/sbdWin.c | 5 +- 7 files changed, 382 insertions(+), 181 deletions(-) (limited to 'src/opt') diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c index 68375039..8b0a76c3 100644 --- a/src/opt/dau/dauGia.c +++ b/src/opt/dau/dauGia.c @@ -249,7 +249,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd ) iFan = Abc_LitNotCond( iFan, fCompl ); } else - iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 ); + iFan = Gia_ManAppendXor2( pGia, iFan0, iFan1 ); } else { diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h index 6cdfafe4..6e0f6b3b 100644 --- a/src/opt/sbd/sbd.h +++ b/src/opt/sbd/sbd.h @@ -40,6 +40,8 @@ struct Sbd_Par_t_ { int nLutSize; // target LUT size int nLutNum; // target LUT count + int nCutSize; // target cut size + int nCutNum; // target cut count int nTfoLevels; // the number of TFO levels (windowing) int nTfoFanMax; // the max number of fanouts (windowing) int nWinSizeMax; // maximum window size (windowing) diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index 0b399b8a..a48e6489 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -43,12 +43,14 @@ struct Sbd_Man_t_ Vec_Int_t * vCover; // temporary Vec_Int_t * vLits; // temporary Vec_Int_t * vLits2; // temporary - int nLuts[3]; // 0=const, 1=1lut, 2=2lut + int nLuts[6]; // 0=const, 1=1lut, 2=2lut, 3=3lut + int nTried; + int nUsed; abctime timeWin; + abctime timeCut; + abctime timeCov; abctime timeCnf; abctime timeSat; - abctime timeCov; - abctime timeEnu; abctime timeQbf; abctime timeOther; abctime timeTotal; @@ -76,8 +78,6 @@ static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i ); } static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[3], p->pPars->nWords * i ); } -extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -96,17 +96,19 @@ extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ void Sbd_ParSetDefault( Sbd_Par_t * pPars ) { memset( pPars, 0, sizeof(Sbd_Par_t) ); - pPars->nLutSize = 4; // target LUT size - pPars->nLutNum = 2; // target LUT count - pPars->nTfoLevels = 2; // the number of TFO levels (windowing) - pPars->nTfoFanMax = 4; // the max number of fanouts (windowing) - pPars->nWinSizeMax = 0; // maximum window size (windowing) - pPars->nBTLimit = 0; // maximum number of SAT conflicts - pPars->nWords = 1; // simulation word count - pPars->fArea = 0; // area-oriented optimization - pPars->fCover = 0; // use complete cover procedure - pPars->fVerbose = 0; // verbose flag - pPars->fVeryVerbose = 0; // verbose flag + pPars->nLutSize = 4; // target LUT size + pPars->nLutNum = 3; // target LUT count + pPars->nCutSize = (pPars->nLutSize - 1) * pPars->nLutNum + 1; // target cut size + pPars->nCutNum = 128; // target cut count + pPars->nTfoLevels = 5; // the number of TFO levels (windowing) + pPars->nTfoFanMax = 4; // the max number of fanouts (windowing) + pPars->nWinSizeMax = 2000; // maximum window size (windowing) + pPars->nBTLimit = 0; // maximum number of SAT conflicts + pPars->nWords = 1; // simulation word count + pPars->fArea = 0; // area-oriented optimization + pPars->fCover = 0; // use complete cover procedure + pPars->fVerbose = 0; // verbose flag + pPars->fVeryVerbose = 0; // verbose flag } /**Function************************************************************* @@ -227,7 +229,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars ) for ( w = 0; w < p->pPars->nWords; w++ ) Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 ); // cut enumeration - p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, 2*pPars->nLutSize-1, 64, 1, 1 ); + p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 1, 1 ); return p; } void Sbd_ManStop( Sbd_Man_t * p ) @@ -437,6 +439,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) Gia_ManIncrementTravId( p->pGia ); Gia_ObjSetTravIdCurrentId(p->pGia, 0); Sbd_ManWindowSim_rec( p, Pivot ); + if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax ) + return 0; Sbd_ManUpdateOrder( p, Pivot ); assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) ); assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) ); @@ -461,6 +465,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) ); Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) ); } + if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax ) + return 0; // compute controlability for node if ( Vec_IntSize(p->vTfo) == 0 ) Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords ); @@ -473,7 +479,7 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) // propagate controlability to fanins for the TFI nodes starting from the pivot Sbd_ManPropagateControl( p, Pivot ); assert( Vec_IntSize(p->vDivValues) <= 64 ); - return (int)(Vec_IntSize(p->vDivValues) > 64); + return (int)(Vec_IntSize(p->vDivValues) <= 64); } /**Function************************************************************* @@ -489,10 +495,6 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) ***********************************************************************/ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot ) { - extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds ); - extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); - extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ); - int nMintCount = 1; Vec_Ptr_t * vSims; word * pSims = Sbd_ObjSim0( p, Pivot ); @@ -984,7 +986,7 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs ) int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) { int fVerbose = 0; - abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock(); + abctime clk; int nIters, nItersMax = 32; word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2]; @@ -1089,14 +1091,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) { if ( p->pPars->fVerbose ) printf( "Cannot find a feasible cover.\n" ); - clkEnu += Abc_Clock() - clk; - clkAll = Abc_Clock() - clkAll - clkSat - clkEnu; - p->timeSat += clkSat; - p->timeCov += clkAll; - p->timeEnu += clkEnu; + p->timeCov += Abc_Clock() - clk; return RetValue; } - clkEnu += Abc_Clock() - clk; + p->timeCov += Abc_Clock() - clk; if ( p->pPars->fVerbose ) printf( "Candidate support: " ), @@ -1104,7 +1102,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) clk = Abc_Clock(); *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); - clkSat += Abc_Clock() - clk; + p->timeSat += Abc_Clock() - clk; if ( *pTruth == SBD_SAT_UNDEC ) printf( "Node %d: Undecided.\n", Pivot ); @@ -1143,19 +1141,12 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) } //break; } - //printf( "Node %4d : Iter = %4d Start table = %4d Final table = %4d\n", Pivot, nIters, nRowsOld, nRows ); - clkAll = Abc_Clock() - clkAll - clkSat - clkEnu; - p->timeSat += clkSat; - p->timeCov += clkAll; - p->timeEnu += clkEnu; return RetValue; } int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth ) { - extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); - extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset ); - abctime clk, clkSat = 0, clkEnu = 0, clkAll; + abctime clk; word Onset[64] = {0}, Offset[64] = {0}, Cube; word CoverRows[64] = {0}, CoverCols[64] = {0}; int nIters, nItersMax = 32; @@ -1171,12 +1162,11 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth ) //sat_solver_delete_p( &p->pSat ); p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 ); p->timeCnf += Abc_Clock() - clk; - clkAll = Abc_Clock(); assert( nConsts <= 8 ); clk = Abc_Clock(); RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset ); - clkSat += Abc_Clock() - clk; + p->timeSat += Abc_Clock() - clk; if ( RetValue >= 0 ) { if ( p->pPars->fVeryVerbose ) @@ -1215,21 +1205,18 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth ) { if ( p->pPars->fVeryVerbose ) printf( "Cannot find a feasible cover.\n" ); - clkEnu += Abc_Clock() - clk; - clkAll = Abc_Clock() - clkAll - clkSat - clkEnu; - p->timeSat += clkSat; - p->timeCov += clkAll; - p->timeEnu += clkEnu; + p->timeCov += Abc_Clock() - clk; return 0; } - + p->timeCov += Abc_Clock() - clk; + if ( p->pPars->fVeryVerbose ) printf( "Candidate support: " ), Vec_IntPrint( p->vDivSet ); clk = Abc_Clock(); *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); - clkSat += Abc_Clock() - clk; + p->timeSat += Abc_Clock() - clk; if ( *pTruth == SBD_SAT_UNDEC ) printf( "Node %d: Undecided.\n", Pivot ); @@ -1271,65 +1258,42 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth ) break; } } - clkAll = Abc_Clock() - clkAll - clkSat - clkEnu; - p->timeSat += clkSat; - p->timeCov += clkAll; - p->timeEnu += clkEnu; return RetValue; } -int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs ) +int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int * pnStrs, Sbd_Str_t * Strs, int * pFreeVar ) { - extern int Sbd_ProblemSolve( - Gia_Man_t * p, Vec_Int_t * vMirrors, - int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, - Vec_Int_t * vTfo, Vec_Int_t * vRoots, - Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 - ); - extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); - extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset ); abctime clk = Abc_Clock(); - word Truth; - int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot); - int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots); - //int nDivs = Vec_IntSize( p->vDivVars ); int Delay = Vec_IntEntry( p->vLutLevs, Pivot ); - int i, k, iObj, nIters, RetValue; + int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodesBot1[SBD_DIV_MAX], pNodesBot2[SBD_DIV_MAX]; + int nNodesTop = 0, nNodesBot = 0, nNodesBot1 = 0, nNodesBot2 = 0, nNodesDiff = 0, nNodesDiff1 = 0, nNodesDiff2 = 0; + int i, k, iObj, nIters, RetValue = 0; - int nLeaves, pLeaves[SBD_DIV_MAX]; - - int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX];//, pNodeRefs[SBD_DIV_MAX]; - int nNodesTop = 0, nNodesBot = 0, nNodesDiff = 0; - - //sat_solver_delete_p( &p->pSat ); - p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 ); - p->timeCnf += Abc_Clock() - clk; - - // extract one cut - nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, pLeaves ); - if ( nLeaves == -1 ) - return 0; - - // solve the covering problem + // try to remove fanins for ( nIters = 0; nIters < nLeaves; nIters++ ) { + word Truth; // try to remove one variable from divisors Vec_IntClear( p->vDivSet ); for ( i = 0; i < nLeaves; i++ ) - if ( i != nIters && pLeaves[i] != -1 ) + if ( i != nLeaves-1-nIters && pLeaves[i] != -1 ) Vec_IntPush( p->vDivSet, Vec_IntEntry(p->vObj2Var, pLeaves[i]) ); assert( Vec_IntSize(p->vDivSet) < nLeaves ); // compute truth table clk = Abc_Clock(); - Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); + Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); p->timeSat += Abc_Clock() - clk; if ( Truth == SBD_SAT_UNDEC ) printf( "Node %d: Undecided.\n", Pivot ); else if ( Truth == SBD_SAT_SAT ) - continue; + { + int DelayDiff = Vec_IntEntry(p->vLutLevs, pLeaves[nLeaves-1-nIters]) - Delay; + if ( DelayDiff > -2 ) + return 0; + } else - pLeaves[nIters] = -1; + pLeaves[nLeaves-1-nIters] = -1; } Vec_IntClear( p->vDivSet ); for ( i = 0; i < nLeaves; i++ ) @@ -1338,13 +1302,14 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs ) //printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) ); if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize ) { + word Truth; *pnStrs = 1; // remap divisors Vec_IntForEachEntry( p->vDivSet, iObj, i ) Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) ); // compute truth table clk = Abc_Clock(); - Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); + Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits ); p->timeSat += Abc_Clock() - clk; assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT ); // create structure @@ -1360,7 +1325,7 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs ) assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize ); // count number of nodes on each level - nNodesTop = 0, nNodesBot = 0; + nNodesTop = nNodesBot = nNodesBot1 = nNodesBot2 = 0; Vec_IntForEachEntry( p->vDivSet, iObj, i ) { int DelayDiff = Vec_IntEntry(p->vLutLevs, iObj) - Delay; @@ -1369,60 +1334,227 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs ) if ( DelayDiff == -2 ) pNodesTop[nNodesTop++] = i; else // if ( DelayDiff < -2 ) + { pNodesBot[nNodesBot++] = i; + if ( DelayDiff == -3 ) + pNodesBot1[nNodesBot1++] = i; + else // if ( DelayDiff < -3 ) + pNodesBot2[nNodesBot2++] = i; + } Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) ); - //pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj ); } + assert( nNodesBot == nNodesBot1 + nNodesBot2 ); if ( i < Vec_IntSize(p->vDivSet) ) return 0; if ( nNodesTop > p->pPars->nLutSize-1 ) return 0; - if ( nNodesBot > p->pPars->nLutSize ) + + // try 44 + if ( Vec_IntSize(p->vDivSet) <= 2*p->pPars->nLutSize-1 ) { - // move left-over to the top - while ( nNodesBot > p->pPars->nLutSize ) - pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot]; - assert( nNodesBot == p->pPars->nLutSize ); + int nMoved = 0; + if ( nNodesBot > p->pPars->nLutSize ) // need to move bottom left-over to the top + { + while ( nNodesBot > p->pPars->nLutSize ) + pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++; + assert( nNodesBot == p->pPars->nLutSize ); + } + assert( nNodesBot <= p->pPars->nLutSize ); assert( nNodesTop <= p->pPars->nLutSize-1 ); - } - nNodesDiff = p->pPars->nLutSize-1 - nNodesTop; - - // number of structures - *pnStrs = 2 + nNodesDiff; - - Strs[0].fLut = 1; - Strs[0].nVarIns = p->pPars->nLutSize; - for ( i = 0; i < nNodesTop; i++ ) - Strs[0].VarIns[i] = pNodesTop[i]; - for ( ; i < p->pPars->nLutSize; i++ ) - Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop; - Strs[0].Res = 0; - - Strs[1].fLut = 1; - Strs[1].nVarIns = nNodesBot; - for ( i = 0; i < nNodesBot; i++ ) - Strs[1].VarIns[i] = pNodesBot[i]; - Strs[1].Res = 0; - - for ( k = 0; k < nNodesDiff; k++ ) - { - Strs[2+k].fLut = 0; - Strs[2+k].nVarIns = nNodesBot; + + Strs[0].fLut = 1; + Strs[0].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < nNodesTop; i++ ) + Strs[0].VarIns[i] = pNodesTop[i]; + for ( ; i < p->pPars->nLutSize; i++ ) + Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop; + Strs[0].Res = 0; + + Strs[1].fLut = 1; + Strs[1].nVarIns = nNodesBot; for ( i = 0; i < nNodesBot; i++ ) - Strs[2+k].VarIns[i] = pNodesBot[i]; - Strs[2+k].Res = 0; + Strs[1].VarIns[i] = pNodesBot[i]; + Strs[1].Res = 0; + + nNodesDiff = p->pPars->nLutSize-1 - nNodesTop; + assert( nNodesDiff >= 0 && nNodesDiff <= 3 ); + for ( k = 0; k < nNodesDiff; k++ ) + { + Strs[2+k].fLut = 0; + Strs[2+k].nVarIns = nNodesBot; + for ( i = 0; i < nNodesBot; i++ ) + Strs[2+k].VarIns[i] = pNodesBot[i]; + Strs[2+k].Res = 0; + } + + *pnStrs = 2 + nNodesDiff; + clk = Abc_Clock(); + RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs ); + p->timeQbf += Abc_Clock() - clk; + if ( RetValue ) + p->nLuts[2]++; + + while ( nMoved-- ) + pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop]; } - clk = Abc_Clock(); - RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, - Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, - p->vDivSet, *pnStrs, Strs ); - p->timeQbf += Abc_Clock() - clk; + if ( RetValue ) + return RetValue; + if ( p->pPars->nLutNum < 3 ) + return 0; + if ( Vec_IntSize(p->vDivSet) < 2*p->pPars->nLutSize-1 ) + return 0; + + // try 444 -- LUT(LUT, LUT) + if ( nNodesTop <= p->pPars->nLutSize-2 ) + { + int nMoved = 0; + if ( nNodesBot > 2*p->pPars->nLutSize ) // need to move bottom left-over to the top + { + while ( nNodesBot > 2*p->pPars->nLutSize ) + pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++; + assert( nNodesBot == 2*p->pPars->nLutSize ); + } + assert( nNodesBot > p->pPars->nLutSize ); + assert( nNodesBot <= 2*p->pPars->nLutSize ); + assert( nNodesTop <= p->pPars->nLutSize-2 ); + + Strs[0].fLut = 1; + Strs[0].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < nNodesTop; i++ ) + Strs[0].VarIns[i] = pNodesTop[i]; + for ( ; i < p->pPars->nLutSize; i++ ) + Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop; + Strs[0].Res = 0; + + Strs[1].fLut = 1; + Strs[1].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < Strs[1].nVarIns; i++ ) + Strs[1].VarIns[i] = pNodesBot[i]; + Strs[1].Res = 0; + + Strs[2].fLut = 1; + Strs[2].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < Strs[2].nVarIns; i++ ) + Strs[2].VarIns[i] = pNodesBot[nNodesBot-p->pPars->nLutSize+i]; + Strs[2].Res = 0; + + nNodesDiff = p->pPars->nLutSize-2 - nNodesTop; + assert( nNodesDiff >= 0 && nNodesDiff <= 2 ); + for ( k = 0; k < nNodesDiff; k++ ) + { + Strs[3+k].fLut = 0; + Strs[3+k].nVarIns = nNodesBot; + for ( i = 0; i < nNodesBot; i++ ) + Strs[3+k].VarIns[i] = pNodesBot[i]; + Strs[3+k].Res = 0; + } + + *pnStrs = 3 + nNodesDiff; + clk = Abc_Clock(); + RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs ); + p->timeQbf += Abc_Clock() - clk; + if ( RetValue ) + p->nLuts[3]++; + + while ( nMoved-- ) + pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop]; + } + if ( RetValue ) + return RetValue; + + // try 444 -- LUT(LUT(LUT)) + if ( nNodesBot1 + nNodesTop <= 2*p->pPars->nLutSize-2 ) + { + if ( nNodesBot2 > p->pPars->nLutSize ) // need to move bottom left-over to the top + { + while ( nNodesBot2 > p->pPars->nLutSize ) + pNodesBot1[nNodesBot1++] = pNodesBot2[--nNodesBot2]; + assert( nNodesBot2 == p->pPars->nLutSize ); + } + if ( nNodesBot1 > p->pPars->nLutSize-1 ) // need to move bottom left-over to the top + { + while ( nNodesBot1 > p->pPars->nLutSize-1 ) + pNodesTop[nNodesTop++] = pNodesBot1[--nNodesBot1]; + assert( nNodesBot1 == p->pPars->nLutSize-1 ); + } + assert( nNodesBot2 <= p->pPars->nLutSize ); + assert( nNodesBot1 <= p->pPars->nLutSize-1 ); + assert( nNodesTop <= p->pPars->nLutSize-1 ); + + Strs[0].fLut = 1; + Strs[0].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < nNodesTop; i++ ) + Strs[0].VarIns[i] = pNodesTop[i]; + Strs[0].VarIns[i++] = Vec_IntSize(p->vDivSet)+1; + for ( ; i < p->pPars->nLutSize; i++ ) + Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+2 + i-nNodesTop; + Strs[0].Res = 0; + nNodesDiff1 = p->pPars->nLutSize-1 - nNodesTop; + + Strs[1].fLut = 1; + Strs[1].nVarIns = p->pPars->nLutSize; + for ( i = 0; i < nNodesBot1; i++ ) + Strs[1].VarIns[i] = pNodesBot1[i]; + Strs[1].VarIns[i++] = Vec_IntSize(p->vDivSet)+2; + for ( ; i < p->pPars->nLutSize; i++ ) + Strs[1].VarIns[i] = Vec_IntSize(p->vDivSet)+2+nNodesDiff1 + i-nNodesBot1; + Strs[1].Res = 0; + nNodesDiff2 = p->pPars->nLutSize-1 - nNodesBot1; + + Strs[2].fLut = 1; + Strs[2].nVarIns = nNodesBot2; + for ( i = 0; i < Strs[2].nVarIns; i++ ) + Strs[2].VarIns[i] = pNodesBot2[i]; + Strs[2].Res = 0; + + nNodesDiff = nNodesDiff1 + nNodesDiff2; + assert( nNodesDiff >= 0 && nNodesDiff <= 3 ); + for ( k = 0; k < nNodesDiff; k++ ) + { + Strs[3+k].fLut = 0; + Strs[3+k].nVarIns = nNodesBot2; + for ( i = 0; i < nNodesBot2; i++ ) + Strs[3+k].VarIns[i] = pNodesBot2[i]; + Strs[3+k].Res = 0; + if ( k >= nNodesDiff1 ) + continue; + Strs[3+k].nVarIns += nNodesBot1; + for ( i = 0; i < nNodesBot1; i++ ) + Strs[3+k].VarIns[nNodesBot2 + i] = pNodesBot1[i]; + } - if ( RetValue ) - p->nLuts[2]++; + *pnStrs = 3 + nNodesDiff; + clk = Abc_Clock(); + RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs ); + p->timeQbf += Abc_Clock() - clk; + if ( RetValue ) + p->nLuts[4]++; + } return RetValue; } +int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs ) +{ + int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots); + int FreeVarStart = FreeVar; + int nSize, nLeaves, pLeaves[SBD_DIV_MAX]; + //sat_solver_delete_p( &p->pSat ); + abctime clk = Abc_Clock(); + p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 ); + p->timeCnf += Abc_Clock() - clk; + // extract one cut + for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ ) + { + nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves ); + if ( nLeaves == -1 ) + continue; + assert( nLeaves == nSize ); + if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) ) + return 1; + } + assert( FreeVar - FreeVarStart <= SBD_FVAR_MAX ); + return 0; +} /**Function************************************************************* @@ -1722,7 +1854,10 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs ) // extend data-structure to accommodate new nodes assert( Vec_IntSize(p->vLutLevs) == iObjLast ); for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ ) + { + Vec_IntPush( p->vMirrors, -1 ); Sbd_StoRefObj( p->pSto, i, i == Gia_ManObjNum(p->pGia)-1 ? Pivot : -1 ); + } Sbd_StoDerefObj( p->pSto, Pivot ); for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ ) { @@ -1730,7 +1865,6 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs ) assert( i == Vec_IntSize(p->vLutLevs) ); Vec_IntPush( p->vLutLevs, Delay ); Vec_IntPush( p->vObj2Var, 0 ); - Vec_IntPush( p->vMirrors, -1 ); Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 ); //Sbd_ManFindCut( p, i, p->vLits ); for ( k = 0; k < 4; k++ ) @@ -1820,22 +1954,16 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors ) ***********************************************************************/ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) { - Sbd_Str_t Strs[4]; - int i, RetValue, nStrs = 0; - word Truth = 0; - - if ( !p->pSto ) - { - if ( Sbd_ManMergeCuts( p, Pivot ) ) - return; - } - -// if ( Pivot != 15 ) -// return; - - if ( Sbd_ManWindow( p, Pivot ) ) + Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0; + int RetValue, nStrs = 0; + if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) ) return; - + if ( !Sbd_ManWindow( p, Pivot ) ) + return; + //if ( Vec_IntSize(p->vWinObjs) > 100 ) + // printf( "Obj %d : Win = %d TFO = %d. Roots = %d.\n", Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vTfo), Vec_IntSize(p->vRoots) ); + p->nTried++; + p->nUsed++; RetValue = Sbd_ManCheckConst( p, Pivot ); if ( RetValue >= 0 ) { @@ -1844,6 +1972,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) } else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) ) { + int i; Strs->fLut = 1; Strs->nVarIns = Vec_IntSize( p->vDivSet ); for ( i = 0; i < Strs->nVarIns; i++ ) @@ -1855,8 +1984,17 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) ) { Sbd_ManImplement2( p, Pivot, nStrs, Strs ); - if ( p->pPars->fVerbose ) printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize ); + if ( !p->pPars->fVerbose ) + return; + if ( Vec_IntSize(p->vDivSet) <= 4 ) + printf( "Node %5d: Detected %d\n", Pivot, p->pPars->nLutSize ); + else if ( Vec_IntSize(p->vDivSet) <= 6 || (Vec_IntSize(p->vDivSet) == 7 && nStrs == 2) ) + printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize ); + else + printf( "Node %5d: Detected %d%d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize, p->pPars->nLutSize ); } + else + p->nUsed--; } Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) { @@ -1875,6 +2013,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia ); Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime; pGia->pManTime = Tim_ManDup( pTimOld, 1 ); + //Tim_ManPrint( pGia->pManTime ); Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime ); Gia_ManForEachObjVec( vNodes, pGia, pObj, k ) { @@ -1883,9 +2022,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) break; if ( Gia_ObjIsAnd(pObj) ) { + abctime clk = Abc_Clock(); int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot ); + p->timeCut += Abc_Clock() - clk; Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay ); - if ( Delay > 1 ) + if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 ) Sbd_NtkPerformOne( p, Pivot ); } else if ( Gia_ObjIsCi(pObj) ) @@ -1903,7 +2044,6 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) Sbd_StoComputeCutsConst0( p->pSto, 0 ); else assert( 0 ); } - //Tim_ManPrint( pGia->pManTime ); Tim_ManStop( (Tim_Man_t *)pGia->pManTime ); pGia->pManTime = pTimOld; Vec_IntFree( vNodes ); @@ -1919,29 +2059,33 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 ); else if ( Gia_ObjIsAnd(pObj) ) { + abctime clk = Abc_Clock(); int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot ); + p->timeCut += Abc_Clock() - clk; Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay ); - if ( Delay > 1 ) + if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 ) Sbd_NtkPerformOne( p, Pivot ); } //if ( nNodesOld != Gia_ManObjNum(pGia) ) // break; } } - printf( "Found %d constants, %d one-LUT and %d two-LUT replacements with delay %d. ", - p->nLuts[0], p->nLuts[1], p->nLuts[2], Sbd_ManDelay(p) ); + printf( "K = %d. S = %d. N = %d. P = %d. ", + p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum ); + printf( "Try = %d. Use = %d. C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d. Lev = %d. ", + p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) ); p->timeTotal = Abc_Clock() - p->timeTotal; Abc_PrintTime( 1, "Time", p->timeTotal ); pNew = Sbd_ManDerive( pGia, p->vMirrors ); // print runtime statistics - p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu - p->timeQbf; - if ( p->pPars->fVerbose ) + p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf; + //if ( p->pPars->fVerbose ) { ABC_PRTP( "Win", p->timeWin , p->timeTotal ); + ABC_PRTP( "Cut", p->timeCut , p->timeTotal ); + ABC_PRTP( "Cov", p->timeCov , p->timeTotal ); ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal ); ABC_PRTP( "Sat", p->timeSat , p->timeTotal ); - ABC_PRTP( "Cov", p->timeCov , p->timeTotal ); - ABC_PRTP( "Enu", p->timeEnu , p->timeTotal ); ABC_PRTP( "Qbf", p->timeQbf , p->timeTotal ); ABC_PRTP( "Oth", p->timeOther, p->timeTotal ); ABC_PRTP( "ALL", p->timeTotal, p->timeTotal ); diff --git a/src/opt/sbd/sbdCut.c b/src/opt/sbd/sbdCut.c index 9c54c74a..7bcf2189 100644 --- a/src/opt/sbd/sbdCut.c +++ b/src/opt/sbd/sbdCut.c @@ -27,9 +27,9 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define SBD_MAX_CUTSIZE 8 -#define SBD_MAX_CUTNUM 1001 -#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1) +#define SBD_MAX_CUTSIZE 10 +#define SBD_MAX_CUTNUM 501 +#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1) #define SBD_CUT_NO_LEAF 0xF @@ -568,6 +568,7 @@ static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut ) { int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia)); int Delay = Vec_IntEntry(p->vDelays, iObj); + if ( pCut == NULL ) { printf( "No cut.\n" ); return; } printf( "%d {", pCut->nLeaves ); for ( i = 0; i < (int)pCut->nLeaves; i++ ) printf( " %*d", nDigits, pCut->pLeaves[i] ); @@ -724,45 +725,88 @@ int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj ) Sbd_StoMergeCuts( p, iObj ); return Vec_IntEntry( p->vDelays, iObj ); } +int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj ) +{ + return Vec_IntEntry(p->vRefs, iObj); +} void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror ) { Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj); assert( iObj == Vec_IntSize(p->vRefs) ); assert( iMirror < iObj ); - Vec_IntPush( p->vRefs, iMirror > 0 ? Vec_IntEntry(p->vRefs, iMirror) : 0 ); + Vec_IntPush( p->vRefs, 0 ); +//printf( "Ref %d\n", iObj ); + if ( iMirror > 0 ) + { + Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) ); + Vec_IntWriteEntry( p->vRefs, iMirror, 1 ); + } if ( Gia_ObjIsAnd(pObj) ) { - Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 ); - Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId1(pObj, iObj), 1 ); + int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + Vec_IntAddToEntry( p->vRefs, Fan0, 1 ); + Vec_IntAddToEntry( p->vRefs, Fan1, 1 ); } else if ( Gia_ObjIsCo(pObj) ) + { + int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + assert( Lit0m == -1 ); Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 ); + } } void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj ) { - Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj); + Gia_Obj_t * pObj; + int Lit0m, Lit1m, Fan0, Fan1; + return; + + pObj = Gia_ManObj(p->pGia, iObj); + if ( Vec_IntEntry(p->vRefs, iObj) == 0 ) + printf( "Ref count mismatch at node %d\n", iObj ); + assert( Vec_IntEntry(p->vRefs, iObj) > 0 ); Vec_IntAddToEntry( p->vRefs, iObj, -1 ); if ( Vec_IntEntry( p->vRefs, iObj ) > 0 ) return; if ( Gia_ObjIsCi(pObj) ) return; +//printf( "Deref %d\n", iObj ); assert( Gia_ObjIsAnd(pObj) ); - Sbd_StoDerefObj( p, Gia_ObjFaninId0(pObj, iObj) ); - Sbd_StoDerefObj( p, Gia_ObjFaninId1(pObj, iObj) ); + Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 ); + if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 ); } -int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves ) +int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves ) { + int fVerbose = 0; Sbd_Cut_t * pCutBest = NULL; int i; assert( p->Pivot == iObj ); + if ( fVerbose && iObj % 1000 == 0 ) + printf( "Node %6d : \n", iObj ); for ( i = 0; i < p->nCutsR; i++ ) + { + if ( fVerbose && iObj % 1000 == 0 ) + Sbd_CutPrint( p, iObj, p->ppCuts[i] ); + if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize ) + continue; if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && - (int)p->ppCuts[i]->nSlowLeaves == 0 && + (int)p->ppCuts[i]->nSlowLeaves <= 1 && (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 && (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) ) pCutBest = p->ppCuts[i]; + } + if ( fVerbose && iObj % 1000 == 0 ) + { + printf( "Best cut of size %d:\n", nSize ); + Sbd_CutPrint( p, iObj, pCutBest ); + } if ( pCutBest == NULL ) return -1; -//Sbd_CutPrint( p, iObj, pCutBest ); assert( pCutBest->nLeaves <= SBD_DIV_MAX ); for ( i = 0; i < (int)pCutBest->nLeaves; i++ ) pLeaves[i] = pCutBest->pLeaves[i]; diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h index d54285f8..668c1231 100644 --- a/src/opt/sbd/sbdInt.h +++ b/src/opt/sbd/sbdInt.h @@ -52,9 +52,10 @@ ABC_NAMESPACE_HEADER_START #define SBD_SAT_UNDEC 0x1234567812345678 #define SBD_SAT_SAT 0x8765432187654321 -#define SBD_LUTS_MAX 2 -#define SBD_SIZE_MAX 4 -#define SBD_DIV_MAX 8 +#define SBD_LUTS_MAX 2 +#define SBD_SIZE_MAX 4 +#define SBD_DIV_MAX 10 +#define SBD_FVAR_MAX 100 //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -81,16 +82,28 @@ struct Sbd_Str_t_ //////////////////////////////////////////////////////////////////////// /*=== sbdCut.c ==========================================================*/ -extern Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose ); -extern void Sbd_StoFree( Sbd_Sto_t * p ); -extern void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror ); -extern void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj ); -extern void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj ); -extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level ); -extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level ); -extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj ); -extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves ); - +extern Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose ); +extern void Sbd_StoFree( Sbd_Sto_t * p ); +extern int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj ); +extern void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror ); +extern void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj ); +extern void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj ); +extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level ); +extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level ); +extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj ); +extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves ); +/*=== sbdWin.c ==========================================================*/ +extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp ); +extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ); +extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds ); +extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset ); +/*=== sbdQbf.c ==========================================================*/ +extern int Sbd_ProblemSolve( + Gia_Man_t * p, Vec_Int_t * vMirrors, + int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, + Vec_Int_t * vTfo, Vec_Int_t * vRoots, + Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 + ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c index e8aee790..ffcb71f8 100644 --- a/src/opt/sbd/sbdLut.c +++ b/src/opt/sbd/sbdLut.c @@ -96,7 +96,6 @@ int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, } } } -//printf( "Stop par = %d.\n", VarPar ); return 1; } void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c index d5b7dd9d..b62332d1 100644 --- a/src/opt/sbd/sbdWin.c +++ b/src/opt/sbd/sbdWin.c @@ -54,7 +54,6 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf ) { Gia_Obj_t * pObj; - int nAddVars = 64; int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue; int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo); int PivotVar = Vec_IntEntry(vObj2Var, Pivot); @@ -67,7 +66,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi pSat = sat_solver_new(); else sat_solver_restart( pSat ); - sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars ); + sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX ); // create constant 0 clause sat_solver_addclause( pSat, &iLit, &iLit + 1 ); // add clauses for all nodes @@ -139,7 +138,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi sat_solver_delete( pSat ); return NULL; } - assert( sat_solver_nvars(pSat) == nVars + nAddVars ); + assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX ); } else if ( fQbf ) { -- cgit v1.2.3