From ec8419c84b7fab43b11f5748ddd1d5c8b70685ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 12 Aug 2024 22:53:40 +0200 Subject: [PATCH 1/3] Revert "Improved anytime pdr" This reverts commit 5444cf281c0cff7d583444bf0dbdffa36aec1ca9. --- src/base/abci/abc.c | 6 +- src/proof/pdr/pdr.h | 1 - src/proof/pdr/pdrCore.c | 333 ++++------------------------------------ src/proof/pdr/pdrIncr.c | 4 +- src/proof/pdr/pdrInt.h | 8 - src/proof/pdr/pdrInv.c | 77 +++------- src/proof/pdr/pdrMan.c | 3 +- src/proof/pdr/pdrSat.c | 3 +- src/proof/pdr/pdrUtil.c | 39 ----- 9 files changed, 51 insertions(+), 423 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 346a1ae92..9bd21963b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30247,7 +30247,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -30380,9 +30380,6 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': pPars->fSolveAll ^= 1; break; - case 'l': - pPars->fAnytime ^= 1; - break; case 'x': pPars->fStoreCex ^= 1; break; @@ -30504,7 +30501,6 @@ usage: Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" ); Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as *.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled"); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); - Abc_Print( -2, "\t-l : toggle anytime schedule when solving all outputs [default = %s]\n", pPars->fAnytime? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 8f62e9b69..00d15a8bc 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -72,7 +72,6 @@ struct Pdr_Par_t_ int fSilent; // totally silent execution int fSolveAll; // do not stop when found a SAT output int fStoreCex; // enable storing counter-examples in MO mode - int fAnytime; // enable anytime scheduling int fUseBridge; // use bridge interface int fUsePropOut; // use property output int nFailOuts; // the number of failed outputs diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 225b6b34a..842324c90 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -136,150 +136,6 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) return pCubeMin; } -void Pdr_ManCompactNullClauses( Pdr_Man_t * p, int k ) -{ - Pdr_Set_t * pCubeK; - Vec_Ptr_t * vArrayK; - int j; - vArrayK = Vec_VecEntry( p->vClauses, k ); - Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) - { - if ( pCubeK != NULL ) - continue; - Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); - Vec_PtrPop(vArrayK); - j--; - } -} - -int Pdr_ManPushInfAndRecycledClauses( Pdr_Man_t * p ) -{ - Pdr_Set_t * pTemp, * pCubeK; - Vec_Ptr_t * vArrayK, * vArrayK1; - Aig_Obj_t * pObj; - int j, k, m, RetValue2, fReduce = p->fNewInfClauses; - - p->fNewInfClauses = 0; - - k = Vec_PtrSize(p->vSolvers) - 2; - assert (k >= 0); - - if ( fReduce && p->pPars->fVeryVerbose ) - Abc_Print( 1, "Reducing inf and recycled clauses for frame %d.\n", k ); - - vArrayK = Vec_VecEntry( p->vClauses, k ); - vArrayK1 = Vec_VecEntry( p->vClauses, k + 1 ); - - Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetBoundSizeLextCompare ); - - Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) - { - if ( pCubeK == NULL || pCubeK->iBound != PDR_INF_BOUND ) - continue; - - if (fReduce) - { - // remove cubes in the same frame that are contained by pCubeK - Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) - { - if ( pTemp == NULL ) - continue; - // This is not needed here due to the sort order we're using - // if ( pTemp->iBound > pCubeK->iBound ) - // continue; - if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp - continue; - pTemp->iBound = 0; - Pdr_SetDeref( pTemp ); - Vec_PtrWriteEntry( vArrayK, m, NULL ); - } - } - - // Is it already implied by other clauses? - RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0; - if ( RetValue2 == -1 ) - { - Pdr_ManCompactNullClauses( p, k ); - return -1; - } - if ( RetValue2 == 1 ) - { - pCubeK->iBound = 0; - p->nInfClauses--; - Pdr_SetDeref( pCubeK ); - Vec_PtrWriteEntry( vArrayK, j, NULL ); - continue; - } - - Pdr_ManSolverAddClause( p, k+1, pCubeK ); - Vec_PtrWriteEntry( vArrayK, j, NULL ); - Vec_PtrPush( vArrayK1, pCubeK ); - } - - if ( (p->pPars->fAnytime || p->pPars->fSolveAll) && fReduce ) - { - Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) - { - if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) >= 0 ) - continue; - RetValue2 = Pdr_ManCheckCube( p, k+1, NULL, NULL, p->pPars->nConfLimit, 0, 1 ); - if ( RetValue2 == -1 ) - { - Pdr_ManCompactNullClauses( p, k ); - return -1; - } - if ( RetValue2 == 1 ) - { - // if the output is already in timeout we need to adjust the stats! - if ( Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == -1 ) - p->pPars->nDropOuts--; - Abc_Print( 1, "Proved output %d in frame %d.\n", p->iOutCur, k ); - p->pPars->nProveOuts++; - Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 1 ); - } - } - } - - // Extra debug checks - - // Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, j ) - // { - // assert( pCubeK1->iBound == PDR_INF_BOUND ); - // assert( Pdr_ManCheckCubeCs( p, k+1, pCubeK1 ) != 0 ); - // assert( Pdr_ManCheckCube( p, k, pCubeK1, NULL, 0, 0, 1 ) != 0 ); - // } - - Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) - { - if ( pCubeK == NULL || pCubeK->iBound <= k ) - continue; - - // Is it already implied by other clauses? - RetValue2 = fReduce ? Pdr_ManCheckCubeCs( p, k+1, pCubeK ) : 0; - if ( RetValue2 == -1 ) - { - Pdr_ManCompactNullClauses( p, k ); - return -1; - } - if ( RetValue2 == 1 ) - { - Pdr_SetDeref( pCubeK ); - Vec_PtrWriteEntry( vArrayK, j, NULL ); - continue; - } - - Pdr_ManSolverAddClause( p, k+1, pCubeK ); - Vec_PtrWriteEntry( vArrayK, j, NULL ); - Vec_PtrPush( vArrayK1, pCubeK ); - } - - // Compact NULL entries - Pdr_ManCompactNullClauses( p, k ); - - return 0; -} - - /**Function************************************************************* Synopsis [Returns 1 if the state could be blocked.] @@ -297,6 +153,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) Vec_Ptr_t * vArrayK, * vArrayK1; int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1; + int Counter = 0; abctime clk = Abc_Clock(); assert( p->iUseFrame > 0 ); Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) @@ -305,11 +162,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) vArrayK1 = Vec_VecEntry( p->vClauses, k+1 ); Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) { + Counter++; + // remove cubes in the same frame that are contained by pCubeK Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) { - if ( pTemp->iBound > pCubeK->iBound ) - continue; if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp continue; Pdr_SetDeref( pTemp ); @@ -341,9 +198,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) // check if the clause subsumes others Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i ) { - // Subsuming a clause of the invariant with a non-invariant clause could break the invariant - if ( pCubeK1->iBound > pCubeK->iBound ) - continue; if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1 continue; Pdr_SetDeref( pCubeK1 ); @@ -352,7 +206,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) i--; } // add the last clause - pCubeK->iBound = k+1; Vec_PtrPush( vArrayK1, pCubeK ); Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); Vec_PtrPop(vArrayK); @@ -370,8 +223,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) // remove cubes in the same frame that are contained by pCubeK Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) { - if ( pTemp->iBound > pCubeK->iBound ) - continue; if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp continue; /* @@ -1057,9 +908,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) while ( !Pdr_QueueIsEmpty(p) ) { Counter++; - if (Counter % 100 == 0) { - Pdr_ManPrintProgress( p, 1, Abc_Clock() - p->tStart ); - } pThis = Pdr_QueueHead( p ); if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) ) return 0; // SAT @@ -1139,7 +987,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } - pCubeMin->iBound = k; Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref p->nCubes++; // add clause @@ -1229,36 +1076,24 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_Set_t * pCube = NULL; Aig_Obj_t * pObj; Abc_Cex_t * pCexNew; - int iFrame, i, RetValue = -1, SomeActive = 1, ClausesAdded = 1; + int iFrame, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; - p->tStart = clkStart; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved - if ( p->pPars->fSolveAll || p->pPars->fAnytime ) - Saig_ManForEachPo( p->pAig, pObj, i ) - if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) && Vec_IntEntry( p->pPars->vOutMap, i ) == -2) + if ( p->pPars->fSolveAll ) + Saig_ManForEachPo( p->pAig, pObj, iFrame ) + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) { - Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat - Abc_Print( 1, "Proved output %d in frame 0 (trivial).\n", i ); + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat p->pPars->nProveOuts++; if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, i ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } // create the first timeframe p->pPars->timeLastSolved = Abc_Clock(); Pdr_ManCreateSolver( p, (iFrame = 0) ); - if ( p->vInfCubes != NULL ) - { - Vec_PtrForEachEntry( Pdr_Set_t *, p->vInfCubes, pCube, i ) - { - Pdr_ManSolverAddClause( p, 0, pCube ); - Vec_VecPush( p->vClauses, 0, pCube ); - } - pCube = NULL; - } - while ( 1 ) { int fRefined = 0; @@ -1278,15 +1113,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->nFrames = iFrame; assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = Abc_MaxInt(iFrame, 1); - SomeActive = 0; Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) ) continue; - // skip otuput that was already solved - if ( p->pPars->vOutMap && Vec_IntEntry( p->pPars->vOutMap, p->iOutCur ) == 1 ) - continue; // skip output whose time has run out if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 ) continue; @@ -1328,7 +1159,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->timeLastSolved = Abc_Clock(); continue; } - SomeActive += 1; // try to solve this output if ( p->pTime4Outs ) { @@ -1373,7 +1203,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) } if ( RetValue == 0 ) { - ClausesAdded = 1; RetValue = Pdr_ManBlockCube( p, pCube ); if ( RetValue == -1 ) { @@ -1447,7 +1276,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // all SAT Pdr_QueueClean( p ); pCube = NULL; - SomeActive--; break; // keep solving } if ( p->pPars->fVerbose ) @@ -1461,19 +1289,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) abctime timeSince = Abc_Clock() - clkOne; assert( p->pTime4Outs[p->iOutCur] > 0 ); p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0; - if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) ) // undecided + if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided { - SomeActive--; p->pPars->nDropOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); if ( !p->pPars->fNotVerbose ) - { - if ( p->pPars->fAnytime ) - Abc_Print( 1, "Timing out on output %*d in frame %d (retrying in next anytime pass).\n", nOutDigits, p->iOutCur, iFrame ); - else - Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); - } + Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); } p->timeToStopOne = 0; } @@ -1494,10 +1316,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); - - if ( p->pPars->fAnytime && ClausesAdded ) - Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) ); - Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManCreateSolver( p, ++iFrame ); if ( fPrintClauses ) @@ -1506,23 +1324,14 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintClauses( p, 0 ); } // push clauses into this timeframe - RetValue = 0; - if ( p->pPars->fAnytime ) - { - RetValue = Pdr_ManPushInfAndRecycledClauses( p ); - ClausesAdded = 0; - } - - RetValue = RetValue == -1 ? -1 : Pdr_ManPushClauses( p ); - if ( RetValue == -1 || !SomeActive ) + RetValue = Pdr_ManPushClauses( p ); + if ( RetValue == -1 ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) { - if ( !SomeActive ) - Abc_Print( 1, "All outputs solved or timed out in frame %d.\n", iFrame ); - else if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); @@ -1534,34 +1343,22 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); - if ( !p->pPars->fAnytime ) - { - if ( !p->pPars->fSilent ) - Pdr_ManReportInvariant( p ); - if ( !p->pPars->fSilent ) - Pdr_ManVerifyInvariant( p ); - } + if ( !p->pPars->fSilent ) + Pdr_ManReportInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManVerifyInvariant( p ); p->pPars->iFrame = iFrame; + // count the number of UNSAT outputs + p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' if ( p->pPars->vOutMap ) - { - for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ ) - if ( Vec_IntEntry(p->pPars->vOutMap, i) == -2 ) // unknown + for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ ) + if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown { - Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat - Abc_Print( 1, "Proved output %d in frame %d (converged).\n", i ); - p->pPars->nProveOuts++; + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, i ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } - if ( p->pPars->nDropOuts > 0 ) - return -1; - } - else - { - // count the number of UNSAT outputs - p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; - } if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) return 1; // UNSAT if ( p->pPars->nFailOuts > 0 ) @@ -1619,61 +1416,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return -1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_ManResetReuseInvariant( Pdr_Man_t * p ) -{ - int i, k, nTimeOutU; - Pdr_Set_t * pCla; - sat_solver * pSat; - - Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) ); - - Vec_PtrClear( p->vInfCubes ); - Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k ) - Vec_PtrPush( p->vInfCubes, pCla ); - - Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i ) - sat_solver_delete( pSat ); - Vec_PtrFree( p->vSolvers ); - Vec_VecFree( p->vClauses ); - Pdr_QueueStop( p ); - Vec_IntFree( p->vActVars ); - - p->vSolvers = Vec_PtrAlloc( 0 ); - p->vClauses = Vec_VecAlloc( 0 ); - p->pQueue = NULL; - p->vActVars = Vec_IntAlloc( 256 ); - - - Vec_IntFill (p->vPrio, Vec_IntSize(p->vPrio), 0); - p->nAbsFlops = 0; - - for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ ) - { - p->pTime4Outs[i] = p->pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; - - if ( Vec_IntEntry(p->pPars->vOutMap, i) == -1 ) // timeout - Vec_IntWriteEntry( p->pPars->vOutMap, i, -2 ); // unknown - } - - p->pPars->nDropOuts = 0; - p->pPars->nTimeOutOne *= 2; - nTimeOutU = p->pPars->nTimeOutOne * (Saig_ManPoNum(p->pAig) - p->pPars->nProveOuts - p->pPars->nFailOuts); - p->pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX - - Abc_Print( 1, "Starting new anytime pass, reusing clauses.\n" ); -} - /**Function************************************************************* Synopsis [] @@ -1688,21 +1430,12 @@ void Pdr_ManResetReuseInvariant( Pdr_Man_t * p ) int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; - int k, RetValue, nTimeOutU; + int k, RetValue; abctime clk = Abc_Clock(); - if ( pPars->fAnytime ) - { - if ( pPars->nTimeOutOne == 0 ) - pPars->nTimeOutOne = 200; - } - if ( pPars->nTimeOutOne && !(pPars->fSolveAll || pPars->fAnytime) ) + if ( pPars->nTimeOutOne && !pPars->fSolveAll ) pPars->nTimeOutOne = 0; if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 ) - { - nTimeOutU = pPars->nTimeOutOne * (Saig_ManPoNum(pAig) - pPars->nProveOuts - pPars->nFailOuts); - pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX - } - + pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0); if ( pPars->fVerbose ) { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); @@ -1718,17 +1451,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) } ABC_FREE( pAig->pSeqModel ); p = Pdr_ManStart( pAig, pPars, NULL ); - - while (1) { - - RetValue = Pdr_ManSolveInt( p ); - if ( RetValue == -1 && Saig_ManPoNum(p->pAig) == pPars->nProveOuts + pPars->nFailOuts ) - RetValue = pPars->nFailOuts == 0; - if ( RetValue == -1 && pPars->fAnytime ) - Pdr_ManResetReuseInvariant( p ); - else - break; - } + RetValue = Pdr_ManSolveInt( p ); if ( RetValue == 0 ) assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); if ( p->vCexes ) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 28cf491e4..6ba68db99 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -379,7 +379,6 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) int iFrame, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; - p->tStart = clkStart; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; // assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved @@ -679,8 +678,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) //if ( p->pPars->fUseAbs && p->vAbsFlops ) // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); // open a new timeframe - p->nQueLim = iFrame + p->pPars->nRestLimit; - p->nQueLimStep = 1; + p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManCreateSolver( p, ++iFrame ); diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index b1375e1be..4a96b071b 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -58,8 +58,6 @@ #define sat_solver_compress(s) #endif -#define PDR_INF_BOUND ((int)((~((unsigned int)0)) >> 1)) - ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// @@ -78,7 +76,6 @@ struct Pdr_Set_t_ { word Sign; // signature int nRefs; // ref counter - int iBound; // known to hold up to this frame, INT_MAX = inf int nTotal; // total literals int nLits; // num flop literals int Lits[0]; @@ -159,11 +156,8 @@ struct Pdr_Man_t_ int nQueCur; int nQueMax; int nQueLim; - int nQueLimStep; int nXsimRuns; int nXsimLits; - int nInfClauses; - int fNewInfClauses; // runtime abctime timeToStop; abctime timeToStopOne; @@ -178,7 +172,6 @@ struct Pdr_Man_t_ abctime tCnf; abctime tAbs; abctime tTotal; - abctime tStart; }; //////////////////////////////////////////////////////////////////////// @@ -260,7 +253,6 @@ extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec extern void ZPdr_SetPrint( Pdr_Set_t * p ); extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); -extern int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); extern void Pdr_OblDeref( Pdr_Obl_t * p ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index d1ae5d9d1..ae61ce2c0 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -48,15 +48,14 @@ ABC_NAMESPACE_IMPL_START void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) { Vec_Ptr_t * vVec; - int i, ThisSize, Length, LengthStart, kLast, Value, Width; + int i, ThisSize, Length, LengthStart; if ( Vec_PtrSize(p->vSolvers) < 2 ) { Abc_Print(1, "Frame " ); Abc_Print(1, "Clauses " ); Abc_Print(1, "Max Queue " ); Abc_Print(1, "Flops " ); - if ( p->pPars->fUseAbs ) - Abc_Print(1, "Cex " ); + Abc_Print(1, "Cex " ); Abc_Print(1, "Time" ); Abc_Print(1, "\n" ); return; @@ -65,12 +64,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) return; // count the total length of the printout Length = 0; - kLast = Vec_VecSize( p->vClauses ) - 1; - Vec_VecForEachLevel( p->vClauses, vVec, i ) - Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1 - (i == kLast ? p->nInfClauses : 0) ); - if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 ) - Length += 2 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+1); + Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); // determine the starting point LengthStart = Abc_MaxInt( 0, Length - 60 ); Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 ); @@ -83,37 +78,26 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) Length = 0; Vec_VecForEachLevel( p->vClauses, vVec, i ) { - Value = Vec_PtrSize(vVec) - (i == kLast ? p->nInfClauses : 0); - Width = 1 + Abc_Base10Log(Value+1); if ( Length < LengthStart ) { - Length += Width; + Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); continue; } - Abc_Print( 1, " %d", Value ); - Length += Width; - ThisSize += Width; - } - if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 ) - { - Abc_Print( 1, " ~%d", Vec_PtrSize(p->vInfCubes) ); - Length += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2); - ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+2); + Abc_Print( 1, " %d", Vec_PtrSize(vVec) ); + Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); + ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1); } for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%5d", p->nQueMax ); Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); if ( p->pPars->fUseAbs ) - Abc_Print( 1, "%4d", p->nCexes ); + Abc_Print( 1, "%4d", p->nCexes ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); if ( p->pPars->nTimeOutOne ) Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); - if ( p->pPars->fAnytime ) - Abc_Print( 1, " PRV =%3d", p->pPars->nProveOuts ); - Abc_Print( 1, "%s", fClose ? "\n":"\r" ); if ( fClose ) p->nQueMax = 0, p->nCexes = 0; @@ -139,7 +123,7 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound != PDR_INF_BOUND ) + if ( pCube->nRefs == -1 ) continue; for ( n = 0; n < pCube->nLits; n++ ) { @@ -392,7 +376,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Count = 0; Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound != PDR_INF_BOUND ) + if ( pCube->nRefs == -1 ) continue; Count++; } @@ -422,7 +406,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound != PDR_INF_BOUND ) + if ( pCube->nRefs == -1 ) continue; Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); fprintf( pFile, " 1\n" ); @@ -468,7 +452,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound != PDR_INF_BOUND ) + if ( pCube->nRefs == -1 ) continue; Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); } @@ -582,7 +566,7 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) // add the clauses Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) // skip known non-inf + if ( pCube->nRefs == -1 ) // skip non-inductive continue; vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); @@ -592,45 +576,31 @@ int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) // check each clause Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound >= 0 ) // skip clauses with known inf-ness + if ( pCube->nRefs == -1 ) // skip non-inductive continue; vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); - if ( RetValue != l_False ) // mark as non-inf + if ( RetValue != l_False ) // mark as non-inductive { - pCube->iBound = ~pCube->iBound; + pCube->nRefs = -1; fChanges = 1; } else Counter++; } - - - Vec_Ptr_t *vLevel; - sat_solver_delete( (sat_solver *)Vec_PtrPop( p->vSolvers ) ); - vLevel = (Vec_Ptr_t *)Vec_PtrPop( (Vec_Ptr_t *)p->vClauses ); - assert (Vec_PtrSize( vLevel ) == 0); - Vec_PtrFree( vLevel ); - Vec_IntPop( p->vActVars ); //Abc_Print(1, "Clauses = %d.\n", Counter ); //sat_solver_delete( pSat ); return fChanges; } - Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) { Vec_Int_t * vResult; Vec_Ptr_t * vCubes; Pdr_Set_t * pCube; - int i, v, kStart, kMax; + int i, v, kStart; // collect cubes used in the inductive invariant - kMax = Vec_PtrSize( p->vSolvers ); kStart = Pdr_ManFindInvariantStart( p ); vCubes = Pdr_ManCollectCubes( p, kStart ); - // mark all non-inf clauses as candidates - Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) - if (pCube->iBound != PDR_INF_BOUND) - pCube->iBound = ~pCube->iBound; // refine as long as there are changes if ( fReduce ) while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); @@ -639,23 +609,14 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) Vec_IntPush( vResult, 0 ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { - if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) { - Vec_PtrWriteEntry( vCubes, i, Vec_PtrEntryLast( vCubes ) ); - Vec_PtrPop( vCubes ); - i--; + if ( pCube->nRefs == -1 ) // skip non-inductive continue; - } - if (pCube->iBound != PDR_INF_BOUND) - { - p->nInfClauses++; - p->fNewInfClauses = 1; - pCube->iBound = PDR_INF_BOUND; - } Vec_IntAddToEntry( vResult, 0, 1 ); Vec_IntPush( vResult, pCube->nLits ); for ( v = 0; v < pCube->nLits; v++ ) Vec_IntPush( vResult, pCube->Lits[v] ); } + //Vec_PtrFree( vCubes ); Vec_PtrFreeP( &p->vInfCubes ); p->vInfCubes = vCubes; Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 052dd731e..7686ec03b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -296,9 +296,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; } if ( pPars->fSolveAll ) - p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); - if ( pPars->fSolveAll || p->pPars->fAnytime ) { + p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) ); Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 ); } diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index becf713fd..b1a5b66c4 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -99,8 +99,7 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ) // add the clauses Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) - if ( pCube != NULL ) - Pdr_ManSolverAddClause( p, k, pCube ); + Pdr_ManSolverAddClause( p, k, pCube ); return pSat; } diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index e4b9fd18d..b2eaa2c76 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -71,7 +71,6 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ) p->nLits = Vec_IntSize(vLits); p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits); p->nRefs = 1; - p->iBound = 0; p->Sign = 0; for ( i = 0; i < p->nLits; i++ ) { @@ -105,7 +104,6 @@ Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ) p->nLits = pSet->nLits - 1; p->nTotal = pSet->nTotal - 1; p->nRefs = 1; - p->iBound = 0; p->Sign = 0; for ( i = 0; i < pSet->nTotal; i++ ) { @@ -140,7 +138,6 @@ Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ) p->nLits = nLits; p->nTotal = nLits + pSet->nTotal - pSet->nLits; p->nRefs = 1; - p->iBound = 0; p->Sign = 0; for ( i = 0; i < nLits; i++ ) { @@ -174,7 +171,6 @@ Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ) p->nLits = pSet->nLits; p->nTotal = pSet->nTotal; p->nRefs = 1; - p->iBound = 0; p->Sign = pSet->Sign; for ( i = 0; i < pSet->nTotal; i++ ) p->Lits[i] = pSet->Lits[i]; @@ -505,41 +501,6 @@ int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) return 0; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_SetBoundSizeLextCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ) -{ - Pdr_Set_t * p1 = *pp1; - Pdr_Set_t * p2 = *pp2; - if (p1->iBound > p2->iBound) - return -1; - if (p1->iBound < p2->iBound) - return 1; - if (p1->nLits < p2->nLits) - return -1; - if (p1->nLits > p2->nLits) - return 1; - - int i; - for ( i = 0; i < p1->nLits && i < p2->nLits; i++ ) - { - if ( p1->Lits[i] > p2->Lits[i] ) - return -1; - if ( p1->Lits[i] < p2->Lits[i] ) - return 1; - } - return 0; -} - /**Function************************************************************* Synopsis [] From 39f6fbb052d41489ea2b49c109d5d4724ce8d673 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 12 Aug 2024 22:53:48 +0200 Subject: [PATCH 2/3] Revert "Fix pdr timing output" This reverts commit c8d64b8682473be6f82b3b8c85a89687b08f398a. --- src/proof/pdr/pdrCore.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 842324c90..371dda168 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -1035,7 +1035,7 @@ void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ) FILE * pCexFile; iCexPathSize = snprintf( NULL, 0, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ) + 1; - pCexPath = (char *)malloc( iCexPathSize ); + pCexPath = malloc( iCexPathSize ); snprintf( pCexPath, iCexPathSize, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ); Abc_Print( 1, "Writing CEX for output %d to %s\n", pCex->iPo, pCexPath ); pCexFile = fopen( pCexPath, "w" ); From de8620d777645c7455793acb392707588b236d86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 12 Aug 2024 22:53:53 +0200 Subject: [PATCH 3/3] Revert "pdr -X to write CEXes immediately" This reverts commit e62e8ac52850e1916e8b9a586fbba306179390df. --- src/base/abci/abc.c | 14 ++------------ src/proof/pdr/pdr.h | 2 -- src/proof/pdr/pdrCore.c | 41 ++--------------------------------------- src/proof/pdr/pdrIncr.c | 4 +--- 4 files changed, 5 insertions(+), 56 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9bd21963b..066af958a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30247,7 +30247,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF ) { switch ( c ) { @@ -30368,15 +30368,6 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pInvFileName = argv[globalUtilOptind]; globalUtilOptind++; break; - case 'X': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-X\" should be followed by a directory name.\n" ); - goto usage; - } - pPars->pCexFilePrefix = argv[globalUtilOptind]; - globalUtilOptind++; - break; case 'a': pPars->fSolveAll ^= 1; break; @@ -30484,7 +30475,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCDQTHGS ] [-LI ] [-X ] [-axrmuyfqipdegjonctkvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDQTHGS ] [-LI ] [-axrmuyfqipdegjonctkvwzh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); @@ -30499,7 +30490,6 @@ usage: Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-I file: the invariant file name [default = %s]\n", pPars->pInvFileName ? pPars->pInvFileName : "default name" ); - Abc_Print( -2, "\t-X pref: when solving all outputs, store CEXes immediately as *.aiw [default = %s]\n", pPars->pCexFilePrefix ? pPars->pCexFilePrefix : "disabled"); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 00d15a8bc..d8a548d5c 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -84,7 +84,6 @@ struct Pdr_Par_t_ abctime timeLastSolved; // the time when the last output was solved Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) char * pInvFileName; // invariable file name - char * pCexFilePrefix; // CEX output prefix }; //////////////////////////////////////////////////////////////////////// @@ -96,7 +95,6 @@ struct Pdr_Par_t_ //////////////////////////////////////////////////////////////////////// /*=== pdrCore.c ==========================================================*/ -extern void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ); extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars ); diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 371dda168..34a327034 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -80,7 +80,6 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->nDropOuts = 0; // the number of timed out outputs pPars->timeLastSolved = 0; // last one solved pPars->pInvFileName = NULL; // invariant file name - pPars->pCexFilePrefix = NULL; // CEX output prefix } /**Function************************************************************* @@ -1027,38 +1026,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) return 1; } -void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex ) -{ - int i, f, iBit; - size_t iCexPathSize; - char * pCexPath; - FILE * pCexFile; - - iCexPathSize = snprintf( NULL, 0, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ) + 1; - pCexPath = malloc( iCexPathSize ); - snprintf( pCexPath, iCexPathSize, "%s%d.aiw", pPars->pCexFilePrefix, pCex->iPo ); - Abc_Print( 1, "Writing CEX for output %d to %s\n", pCex->iPo, pCexPath ); - pCexFile = fopen( pCexPath, "w" ); - free( pCexPath ); - - fprintf( pCexFile, "1\n"); - fprintf( pCexFile, "b%d\n", pCex->iPo); - - iBit = 0; - for ( i = 0; i < pCex->nRegs; i++, iBit++ ) - putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile ); - putc( '\n', pCexFile ); - - for ( f = 0; f <= pCex->iFrame; f++ ) - { - for ( i = 0; i < pCex->nPis; i++, iBit++ ) - putc( '0' + Abc_InfoHasBit(pCex->pData, iBit), pCexFile ); - putc( '\n', pCexFile ); - } - fprintf( pCexFile, ".\n"); - fclose( pCexFile ); -} - /**Function************************************************************* Synopsis [] @@ -1133,7 +1100,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pAig->pSeqModel = pCexNew; return 0; // SAT } - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( !p->pPars->fNotVerbose ) @@ -1142,8 +1109,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - if ( p->pPars->pCexFilePrefix ) - Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { @@ -1252,13 +1217,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - if ( p->pPars->pCexFilePrefix ) - Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 6ba68db99..9ca72ba69 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -484,7 +484,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) p->pAig->pSeqModel = pCexNew; return 0; // SAT } - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex || p->pPars->pCexFilePrefix) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( !p->pPars->fNotVerbose ) @@ -493,8 +493,6 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); if ( p->pPars->fUseBridge ) Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - if ( p->pPars->pCexFilePrefix ) - Pdr_OutputCexToDir( p->pPars, pCexNew ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) {