diff options
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 19 | ||||
-rw-r--r-- | src/aig/gia/giaAbsVta.c | 17 | ||||
-rw-r--r-- | src/base/abci/abc.c | 22 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 5 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 1 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 10 |
7 files changed, 46 insertions, 31 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 97a7b7b7..c537a31b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -223,7 +223,8 @@ struct Gia_ParVta_t_ int fDumpVabs; // dumps the abstracted model char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag - int iFrame; // the number of frames covered + int iFrame; // the number of frames covered + int nFramesNoChange; // the number of last frames without changes }; static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 6505c2f2..117ad3e0 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -509,7 +509,7 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v { int i;//, Id = Gia_ObjId(p->pGia, pObj); Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f ); - assert( (int)pRef->Sign == Sign ); +// assert( (int)pRef->Sign == Sign ); if ( pRef->fVisit ) return; if ( p->pPars->fPropFanout ) @@ -1214,8 +1214,9 @@ void Gla_ManStop( Gla_Man_t * p ) Gla_Obj_t * pGla; int i; // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n", + sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), + sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) ABC_FREE( p->pvRefis[i].pArray ); Gla_ManForEachObj( p, pGla ) @@ -1805,7 +1806,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin ); Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); - Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); + Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); } for ( f = i = iPrev = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++, iPrev = i ) { @@ -1891,9 +1892,13 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) nCoreSize = Vec_IntSize( vCore ); Gia_GlaAddToCounters( p, vCore ); if ( i == 0 ) + { + p->pPars->nFramesNoChange++; Vec_IntFree( vCore ); + } else { + p->pPars->nFramesNoChange = 0; // update the SAT solver sat_solver2_rollback( p->pSat ); // update storage @@ -1967,9 +1972,9 @@ finish: if ( Status == -1 ) { if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) - Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); + Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) - Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); else @@ -1978,7 +1983,7 @@ finish: else { p->pPars->iFrame++; - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); } } else diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index f7c1e5a5..85d51a42 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1062,8 +1062,9 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) void Vga_ManStop( Vta_Man_t * p ) { // if ( p->pPars->fVerbose ) - Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", - sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d Objs+ = %d\n", + sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), + sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); Vec_VecFreeP( (Vec_Vec_t **)&p->vCores ); Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames ); Vec_BitFreeP( &p->vSeenGla ); @@ -1534,7 +1535,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { printf( "Sequential miter is trivially UNSAT.\n" ); return 1; - } + } ABC_FREE( pAig->pCexSeq ); pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); printf( "Sequential miter is trivially SAT.\n" ); @@ -1564,7 +1565,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); // Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" ); - Abc_Print( 1, "Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" ); + Abc_Print( 1, " Frame %% Abs %% Confl Cex Vars Clas Lrns Core Time Mem\n" ); } assert( Vec_PtrSize(p->vFrames) > 0 ); for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ ) @@ -1665,9 +1666,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { // reset the counter of frames without change nCountNoChange = 1; + p->pPars->nFramesNoChange = 0; } else if ( ++nCountNoChange == 2 ) // time to send { + p->pPars->nFramesNoChange++; if ( Abc_FrameIsBridgeMode() ) { // cancel old one if it was sent @@ -1709,9 +1712,9 @@ finish: if ( Status == -1 ) { if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) - Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); + Abc_Print( 1, "Timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, f, p->pPars->nFramesNoChange ); else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) - Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + Abc_Print( 1, "Exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, f, p->pPars->nFramesNoChange ); else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 ) Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); else @@ -1720,7 +1723,7 @@ finish: else { p->pPars->iFrame++; - Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + Abc_Print( 1, "Completed %d frames with a %d-stable abstraction. ", f, p->pPars->nFramesNoChange ); } } } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 68d0e073..6caf37cb 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27891,7 +27891,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "There is no AIG.\n" ); - return 1; + return 0; } if ( Gia_ManRegNum(pAbc->pGia) == 0 ) { @@ -27971,12 +27971,12 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no AIG.\n" ); - return 1; + return 0; } if ( pAbc->pGia->vObjClasses == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" ); - return 1; + return 0; } Vec_IntFreeP( &pAbc->pGia->vGateClasses ); pAbc->pGia->vGateClasses = Gia_VtaConvertToGla( pAbc->pGia, pAbc->pGia->vObjClasses ); @@ -28034,17 +28034,17 @@ int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" ); - return 1; + return 0; } if ( pAbc->pGia->vGateClasses == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" ); - return 1; + return 0; } if ( pAbc->nFrames < 1 ) { Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames ); - return 1; + return 0; } Vec_IntFreeP( &pAbc->pGia->vObjClasses ); pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames ); @@ -28091,12 +28091,12 @@ int Abc_CommandAbc9Fla2Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no AIG.\n" ); - return 1; + return 0; } if ( pAbc->pGia->vFlopClasses == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Fla2Gla(): There is no gate-level abstraction is defined.\n" ); - return 1; + return 0; } Vec_IntFreeP( &pAbc->pGia->vGateClasses ); pAbc->pGia->vGateClasses = Gia_FlaConvertToGla( pAbc->pGia, pAbc->pGia->vFlopClasses ); @@ -28142,12 +28142,12 @@ int Abc_CommandAbc9Gla2Fla( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no AIG.\n" ); - return 1; + return 0; } if ( pAbc->pGia->vGateClasses == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Gla2Fla(): There is no gate-level abstraction is defined.\n" ); - return 1; + return 0; } Vec_IntFreeP( &pAbc->pGia->vFlopClasses ); pAbc->pGia->vFlopClasses = Gia_GlaConvertToFla( pAbc->pGia, pAbc->pGia->vGateClasses ); @@ -28194,7 +28194,7 @@ int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" ); - return 1; + return 0; } pTemp = Gia_ManReparam( pAbc->pGia, fVerbose ); Abc_CommandUpdate9( pAbc, pTemp ); diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 680b1996..eeadf09e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pNode->Id == 0 ) continue; pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts ); + assert( pNode->Id > 0 ); Vec_PtrPush( vUsed, pNode ); // update fanins Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node + { + assert( pFanin->Id > 0 ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); + } // else // problem clause // assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); } @@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pPivot && pPivot <= pNode ) { RetValue = hTemp; -// s->iProofPivot = i; pPivot = NULL; } } diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 520e8284..eace9eea 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -30,7 +30,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satVec.h" #include "satClause.h" -#include "misc/vec/vecSet.h" ABC_NAMESPACE_HEADER_START diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index cb6199ec..2cd825b7 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -164,7 +164,7 @@ static inline void proof_chain_start( sat_solver2* s, clause* c ) if ( s->fProofLogging ) { int ProofId = clause2_proofid(s, c, 0); - assert( ProofId > 0 ); + assert( (ProofId >> 2) > 0 ); veci_resize( &s->temp_proof, 0 ); veci_push( &s->temp_proof, 0 ); veci_push( &s->temp_proof, 0 ); @@ -178,7 +178,7 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var ) { clause* c = cls ? cls : var_unit_clause( s, Var ); int ProofId = clause2_proofid(s, c, var_is_partA(s,Var)); - assert( ProofId > 0 ); + assert( (ProofId >> 2) > 0 ); veci_push( &s->temp_proof, ProofId ); } } @@ -1417,7 +1417,10 @@ void sat_solver2_reducedb(sat_solver2* s) break; } if ( j < nLearnedOld / 6 ) + { + ABC_FREE( pSortValues ); return; + } // mark learned clauses to remove Counter = j = 0; @@ -1439,6 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s) s->stats.learnts--; } } + ABC_FREE( pSortValues ); // if ( j == nLearnedOld ) // return; @@ -1717,6 +1721,7 @@ void sat_solver2_verify( sat_solver2* s ) // Abc_Print(1, "Verification passed.\n" ); } */ + // checks how many watched clauses are satisfied by 0-level assignments // (this procedure may be called before setting up a new bookmark for rollback) int sat_solver2_check_watched( sat_solver2* s ) @@ -1754,7 +1759,6 @@ int sat_solver2_check_watched( sat_solver2* s ) return 0; } - int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { int restart_iter = 0; |