From 398c4ec92c4e25fa588a6b3bcbd016df91e57771 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Dec 2016 18:08:39 +0700 Subject: Updates to delay optimization project. --- src/opt/sbd/sbdCore.c | 158 ++++++++++++++++++++++++++++++++++++++++++-------- src/opt/sbd/sbdInt.h | 1 + src/opt/sbd/sbdLut.c | 108 ++++++++++++++++++++++++++-------- src/opt/sbd/sbdWin.c | 35 +++++++++++ 4 files changed, 254 insertions(+), 48 deletions(-) (limited to 'src/opt') diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index 563e6e98..5c5fe35a 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -777,15 +777,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) } } -void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows ) +void Sbd_ManMatrPrint( Sbd_Man_t * p, word Cover[], int nCol, int nRows ) { int i, k; for ( i = 0; i <= nCol; i++ ) { printf( "%2d : ", i ); + printf( "%d ", i == nCol ? Vec_IntEntry(p->vLutLevs, p->Pivot) : Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) ); for ( k = 0; k < nRows; k++ ) - for ( k = 0; k < nRows; k++ ) - printf( "%d", (int)((Cover[i] >> k) & 1) ); + printf( "%d", (int)((Cover[i] >> k) & 1) ); printf( "\n"); } printf( "\n"); @@ -801,18 +801,18 @@ static inline void Sbd_ManCoverReverseOrder( word Cover[64] ) } } -static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube ) +static inline int Sbd_ManAddCube1( int nRowLimit, word Cover[], int nRows, word Cube ) { int n, m; if ( 0 ) { printf( "Adding cube: " ); - for ( n = 0; n < 64; n++ ) + for ( n = 0; n < nRowLimit; n++ ) printf( "%d", (int)((Cube >> n) & 1) ); printf( "\n" ); } // do not add contained Cube - assert( nRows <= 64 ); + assert( nRows <= nRowLimit ); for ( n = 0; n < nRows; n++ ) if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained return nRows; @@ -820,7 +820,7 @@ static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube ) for ( n = m = 0; n < nRows; n++ ) if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained Cover[m++] = Cover[n]; - if ( m < 64 ) + if ( m < nRowLimit ) Cover[m++] = Cube; for ( n = m; n < nRows; n++ ) Cover[n] = 0; @@ -855,7 +855,7 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] ) return nRows; } -static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs ) +static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[], int nDivs ) { int c0, c1, c2, c3; word Target = Cover[nDivs]; @@ -1052,7 +1052,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) { Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]); assert( Cube ); - nRows = Sbd_ManAddCube1( Cover, nRows, Cube ); + nRows = Sbd_ManAddCube1( 64, Cover, nRows, Cube ); } Sbd_ManCoverReverseOrder( Cover ); @@ -1072,7 +1072,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ ) { if ( p->pPars->fVerbose ) - Sbd_ManMatrPrint( Cover, nDivs, nRows ); + Sbd_ManMatrPrint( p, Cover, nDivs, nRows ); clk = Abc_Clock(); if ( !Sbd_ManFindCands( p, Cover, nDivs ) ) @@ -1141,10 +1141,123 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth ) return RetValue; } -int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, - int nLuts, int nSels, int nVarsDivs[SBD_LUTS_MAX], - int pVarsDivs[SBD_LUTS_MAX][SBD_SIZE_MAX], word Truths[SBD_LUTS_MAX] ) +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 = Abc_Clock(); + word Onset[64] = {0}, Offset[64] = {0}, Cube; + word CoverRows[256] = {0}, CoverCols[64] = {{0}}; + int nIters, nItersMax = 32; + int i, k, nRows = 0; + + 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 nConsts = 4; + int RetValue; + + if ( p->pSat ) + sat_solver_delete( p->pSat ); + p->pSat = NULL; + + 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; + + assert( nConsts <= 8 ); + RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset ); + if ( RetValue >= 0 ) + { + if ( p->pPars->fVerbose ) + printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot ); + Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 ); + p->nConsts++; + return RetValue; + } + + // create rows of the table + nRows = 0; + for ( i = 0; i < nConsts; i++ ) + for ( k = 0; k < nConsts; k++ ) + { + Cube = Onset[i] ^ Offset[k]; + assert( Cube ); + nRows = Sbd_ManAddCube1( 256, CoverRows, nRows, Cube ); + } + assert( nRows <= 64 ); + + // create columns of the table + for ( i = 0; i < nRows; i++ ) + for ( k = 0; k <= nDivs; k++ ) + if ( (CoverRows[i] >> k) & 1 ) + Abc_TtXorBit(&CoverCols[k], i); + + // solve the covering problem + for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ ) + { + if ( p->pPars->fVerbose ) + Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows ); + + clk = Abc_Clock(); + if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) ) + { + 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; + return 0; + } + //clkEnu += Abc_Clock() - clk; + + if ( p->pPars->fVerbose ) + 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; + + if ( *pTruth == SBD_SAT_UNDEC ) + printf( "Node %d: Undecided.\n", Pivot ); + else if ( *pTruth == SBD_SAT_SAT ) + { + if ( p->pPars->fVerbose ) + { + int i; + printf( "Node %d: SAT.\n", Pivot ); + for ( i = 0; i < nDivs; i++ ) + printf( "%d", Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) ); + printf( "\n" ); + for ( i = 0; i < nDivs; i++ ) + printf( "%d", i % 10 ); + printf( "\n" ); + for ( i = 0; i < nDivs; i++ ) + printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' ); + printf( "\n" ); + for ( i = 0; i < nDivs; i++ ) + printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' ); + printf( "\n" ); + } + // add row to the covering table + for ( i = 0; i < nDivs; i++ ) + if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD ) + CoverCols[i] |= ((word)1 << nRows); + CoverCols[nDivs] |= ((word)1 << nRows); + nRows++; + } + else + { + if ( p->pPars->fVerbose ) + { + printf( "Node %d: UNSAT. ", Pivot ); + Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" ); + } + return 1; + } + } return 0; } @@ -1465,7 +1578,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) if ( Sbd_ManMergeCuts( p, Pivot ) ) return; -// if ( Pivot != 13 ) +// if ( Pivot != 70 ) // return; if ( p->pPars->fVerbose ) @@ -1481,7 +1594,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue ); //printf( " --> Pivot %4d. Constant %d.\n", Pivot, RetValue ); } - else if ( Sbd_ManExplore( p, Pivot, &Truth ) ) + else if ( Sbd_ManExplore2( p, Pivot, &Truth ) ) { Sbd_ManImplement( p, Pivot, Truth ); //printf( " --> Pivot %4d. Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) ); @@ -1493,26 +1606,23 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot ) 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, word Truths[SBD_LUTS_MAX] + Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 ); - Sbd_Str_t Strs[2] = { - {1, 4, {0, 1, 2, 7}}, - {1, 4, {3, 4, 5, 6}} - }; - - word Truths[SBD_LUTS_MAX]; +// Sbd_Str_t Strs[2] = { {1, 4, {0, 1, 2, 8}}, {1, 4, {3, 4, 5, 6}} }; +// Sbd_Str_t Strs[2] = { {1, 4, {1, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}} }; + Sbd_Str_t Strs[3] = { {1, 4, {8, 4, 5, 7}}, {1, 4, {0, 1, 2, 3}}, {0, 4, {0, 1, 2, 3}} }; Vec_Int_t * vDivSet = Vec_IntAlloc( 8 ); int i, RetValue; - for ( i = 0; i < 7; i++ ) + for ( i = 0; i < 6; i++ ) Vec_IntPush( vDivSet, i+1 ); RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, - vDivSet, 2, Strs, Truths ); + vDivSet, 3, Strs ); if ( RetValue ) { printf( "Solving succeded.\n" ); diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h index 3646c6b9..5395e148 100644 --- a/src/opt/sbd/sbdInt.h +++ b/src/opt/sbd/sbdInt.h @@ -66,6 +66,7 @@ struct Sbd_Str_t_ int fLut; // LUT or SEL int nVarIns; // input count int VarIns[SBD_DIV_MAX]; // input vars + word Res; // result of solving }; //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c index 42bb0955..b68ecc26 100644 --- a/src/opt/sbd/sbdLut.c +++ b/src/opt/sbd/sbdLut.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "sbdInt.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -46,17 +47,18 @@ int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 ) { Sbd_Str_t * pStr; int nPars = 0; for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) - nPars += (pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns); + nPars += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns; return nPars; } // add clauses for the structure -void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) +int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) { // variable order: inputs, structure outputs, parameters Sbd_Str_t * pStr; int VarOut = nVars; int VarPar = nVars + nStrs; int m, k, n, status, pLits[SBD_SIZE_MAX+2]; +//printf( "Start par = %d. ", VarPar ); for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ ) { if ( pStr->fLut ) @@ -72,12 +74,14 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n ); pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n ); status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 ); - assert( status ); + if ( !status ) + return 0; } } } else { + assert( pStr->nVarIns <= SBD_DIV_MAX ); for ( k = 0; k < pStr->nVarIns; k++, VarPar++ ) { for ( n = 0; n < 2; n++ ) @@ -86,22 +90,32 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars pLits[1] = Abc_Var2Lit( pVars[VarOut], n ); pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n ); status = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( status ); + if ( !status ) + return 0; } } } } +//printf( "Stop par = %d.\n", VarPar ); + return 1; } void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) { Sbd_Str_t * pStr; int VarPar = nVars + nStrs; - int m, m2, pLits[2], status; + int m, m2, status, pLits[SBD_DIV_MAX]; // make sure selector parameters are mutually exclusive - for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarPar = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns ) + for ( pStr = pStr0; pStr < pStr0 + nStrs; VarPar += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns, pStr++ ) { if ( pStr->fLut ) continue; + // one variable should be selected + assert( pStr->nVarIns <= SBD_DIV_MAX ); + for ( m = 0; m < pStr->nVarIns; m++ ) + pLits[m] = Abc_Var2Lit( pVars[VarPar + m], 0 ); + status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns ); + assert( status ); + // two variables cannot be selected for ( m = 0; m < pStr->nVarIns; m++ ) for ( m2 = m+1; m2 < pStr->nVarIns; m2++ ) { @@ -120,15 +134,44 @@ void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits ) for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) { nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns; - printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", pStr-pStr0 ); - for ( m = 0; m < nIters; m++ ) - printf( "%d", Abc_LitIsCompl(Vec_IntEntry(vLits, iLit++)) ); - printf( "\n" ); + printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", (int)(pStr-pStr0) ); + for ( m = 0; m < nIters; m++, iLit++ ) + printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ); + printf( " {" ); + for ( m = 0; m < pStr->nVarIns; m++ ) + printf( " %d", pStr->VarIns[m] ); + printf( " }\n" ); } assert( iLit == Vec_IntSize(vLits) ); } -void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits, word Truths[SBD_LUTS_MAX] ) +void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits ) { + Sbd_Str_t * pStr; + int m, nIters, iLit = 0; + for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ ) + { + pStr->Res = 0; + if ( pStr->fLut ) + { + nIters = 1 << pStr->nVarIns; + for ( m = 0; m < nIters; m++, iLit++ ) + if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ) + Abc_TtSetBit( &pStr->Res, m ); + Abc_TtStretch6( &pStr->Res, pStr->nVarIns, 6 ); + } + else + { + nIters = 0; + for ( m = 0; m < pStr->nVarIns; m++, iLit++ ) + if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) ) + { + pStr->Res = pStr->VarIns[m]; + nIters++; + } + assert( nIters == 1 ); + } + } + assert( iLit == Vec_IntSize(vLits) ); } /**Function************************************************************* @@ -145,38 +188,39 @@ void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits 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, word Truths[SBD_LUTS_MAX] ) // divisors, structures + Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 ) // divisors, structures { 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 ); + int fVerbose = 1; Vec_Int_t * vLits = Vec_IntAlloc( 100 ); 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 nVars = Vec_IntSize( vDivSet ); int nPars = Sbd_ProblemCountParams( nStrs, pStr0 ); int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots); - int VarCecPar = VarCecOut + 1; - int VarCecFree = VarCecPar + nPars; + int VarCecPar = VarCecOut + nStrs; int VarQbfPar = 0; int VarQbfFree = nPars; int pVarsCec[256]; int pVarsQbf[256]; - int i, iVar, iLit; + int i, iVar, iLit, nIters; int RetValue = 0; - assert( Vec_IntSize(vDivSet) <= SBD_SIZE_MAX ); + assert( Vec_IntSize(vDivSet) <= SBD_DIV_MAX ); assert( nVars + nStrs + nPars <= 256 ); // collect CEC variables Vec_IntForEachEntry( vDivSet, iVar, i ) pVarsCec[i] = iVar; - pVarsCec[nVars] = VarCecOut; - for ( i = 1; i < nStrs; i++ ) - pVarsCec[nVars + i] = VarCecFree++; + for ( i = 0; i < nStrs; i++ ) + pVarsCec[nVars + i] = VarCecOut + i; for ( i = 0; i < nPars; i++ ) pVarsCec[nVars + nStrs + i] = VarCecPar + i; @@ -197,13 +241,24 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_IntClear( vLits ); for ( i = 0; i < nPars; i++ ) Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) ); - while ( 1 ) + for ( nIters = 0; nIters < (1 << nVars); nIters++ ) { // check if these parameters solve the problem int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 ); if ( status == l_False ) // solution found break; assert( status == l_True ); +// Vec_IntForEachEntry( vWinObjs, iVar, i ) +// printf( "Node = %4d. SatVar = %4d. Value = %d.\n", iVar, i, sat_solver_var_value(pSatCec, i) ); + + if ( fVerbose ) + { + printf( "Iter %3d : ", nIters ); + for ( i = 0; i < nPars; i++ ) + printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) ); + printf( " " ); + } + Vec_IntClear( vLits ); // create new QBF variables for ( i = 0; i < nVars + nStrs; i++ ) @@ -211,15 +266,20 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, // set their values Vec_IntForEachEntry( vDivSet, iVar, i ) { - iLit = Abc_Var2Lit( pVarsQbf[i], sat_solver_var_value(pSatCec, iVar) ); + iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) ); status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); assert( status ); + if ( fVerbose ) + printf( "%d", sat_solver_var_value(pSatCec, iVar) ); } iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) ); status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 ); assert( status ); + if ( fVerbose ) + printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) ); // add clauses to the QBF problem - Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ); + if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) ) + break; // solution does not exist // check if solution still exists status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 ); if ( status == l_False ) // solution does not exist @@ -228,12 +288,12 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors, // find the new values of parameters assert( Vec_IntSize(vLits) == 0 ); for ( i = 0; i < nPars; i++ ) - Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, sat_solver_var_value(pSatQbf, VarQbfPar + i)) ); + Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, !sat_solver_var_value(pSatQbf, VarQbfPar + i)) ); } if ( Vec_IntSize(vLits) > 0 ) { Sbd_ProblemPrintSolution( nStrs, pStr0, vLits ); - Sbd_ProblemCollectSolution( nStrs, pStr0, vLits, Truths ); + Sbd_ProblemCollectSolution( nStrs, pStr0, vLits ); RetValue = 1; } else diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c index fc79caa7..d5b7dd9d 100644 --- a/src/opt/sbd/sbdWin.c +++ b/src/opt/sbd/sbdWin.c @@ -141,6 +141,17 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi } assert( sat_solver_nvars(pSat) == nVars + nAddVars ); } + else if ( fQbf ) + { + int n, pLits[2]; + for ( n = 0; n < 2; n++ ) + { + pLits[0] = Abc_Var2Lit( PivotVar, n ); + pLits[1] = Abc_Var2Lit( LastVar, n ); + RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + } // finalize RetValue = sat_solver_simplify( pSat ); if ( RetValue == 0 ) @@ -418,6 +429,30 @@ int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, return -1; } +int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset ) +{ + int nBTLimit = 0; + int n, i, k, status, iLit, iVar; + word * pPats[2] = {pOnset, pOffset}; + assert( Vec_IntSize(vDivVars) < 64 ); + for ( n = 0; n < 2; n++ ) + for ( i = 0; i < nConsts; i++ ) + { + sat_solver_random_polarity( pSat ); + iLit = Abc_Var2Lit( PivotVar, n ); + status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -2; + if ( status == l_False ) + return n; + pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars); + Vec_IntForEachEntry( vDivVars, iVar, k ) + if ( sat_solver_var_value(pSat, iVar) ) + Abc_TtXorBit(&pPats[n][i], k); + } + return -1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3