diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-27 18:15:05 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-27 18:15:05 +0700 |
| commit | fcd3133a9f2817893aa60d1ec2d1b94a1f5a7b5a (patch) | |
| tree | c89a2f7ef6a1a2031d5d2b6730b2a0c42d7733cf | |
| parent | 398c4ec92c4e25fa588a6b3bcbd016df91e57771 (diff) | |
| download | abc-fcd3133a9f2817893aa60d1ec2d1b94a1f5a7b5a.tar.gz abc-fcd3133a9f2817893aa60d1ec2d1b94a1f5a7b5a.tar.bz2 abc-fcd3133a9f2817893aa60d1ec2d1b94a1f5a7b5a.zip | |
Updates to delay optimization project.
| -rw-r--r-- | src/opt/sbd/sbdCore.c | 5 | ||||
| -rw-r--r-- | src/opt/sbd/sbdLut.c | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index 5c5fe35a..15874dc6 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -75,6 +75,8 @@ 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 /// //////////////////////////////////////////////////////////////////////// @@ -975,7 +977,6 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) int fVerbose = 0; abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock(); int nIters, nItersMax = 32; - 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 ); word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2]; int i, k, n, Node, Index, nCubes[2] = {0}, nRows = 0, nRowsOld; @@ -1147,7 +1148,7 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth ) extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset ); abctime clk = Abc_Clock(); word Onset[64] = {0}, Offset[64] = {0}, Cube; - word CoverRows[256] = {0}, CoverCols[64] = {{0}}; + word CoverRows[64] = {0}, CoverCols[64] = {0}; int nIters, nItersMax = 32; int i, k, nRows = 0; diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c index b68ecc26..b924a33b 100644 --- a/src/opt/sbd/sbdLut.c +++ b/src/opt/sbd/sbdLut.c @@ -197,7 +197,7 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 ); sat_solver * pSatQbf = sat_solver_new(); - int PivotVar = Vec_IntEntry(vObj2Var, Pivot); + //int PivotVar = Vec_IntEntry(vObj2Var, Pivot); int nVars = Vec_IntSize( vDivSet ); int nPars = Sbd_ProblemCountParams( nStrs, pStr0 ); |