From c4446189a9ca5a187a2ede26a7102866d2c5ae8e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 14 Jan 2016 20:42:22 -0800 Subject: Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network. --- src/proof/pdr/pdr.h | 1 + src/proof/pdr/pdrCore.c | 24 ++++---- src/proof/pdr/pdrInt.h | 6 +- src/proof/pdr/pdrInv.c | 150 ++++++++++++++++++++++++++++++++++++++++++++++-- src/proof/pdr/pdrMan.c | 1 + src/proof/pdr/pdrSat.c | 11 +++- src/proof/pdr/pdrUtil.c | 40 +++++++++++++ 7 files changed, 214 insertions(+), 19 deletions(-) (limited to 'src/proof/pdr') diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index adbdafca..e4b764a1 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -44,6 +44,7 @@ struct Pdr_Par_t_ int nRecycle; // limit on vars for recycling int nFrameMax; // limit on frame count int nConfLimit; // limit on SAT solver conflicts + int nConfGenLimit; // limit on SAT solver conflicts during generalization int nRestLimit; // limit on the number of proof-obligations int nTimeOut; // timeout in seconds int nTimeOutGap; // approximate timeout in seconds since the last change diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 78cc16c1..8e81795b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -55,6 +55,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->nTimeOut = 0; // timeout in seconds pPars->nTimeOutGap = 0; // timeout in seconds since the last solved pPars->nConfLimit = 0; // limit on SAT solver conflicts + pPars->nConfGenLimit = 0; // limit on SAT solver conflicts during generalization pPars->nRestLimit = 0; // limit on the number of proof-obligations pPars->fTwoRounds = 0; // use two rounds for generalization pPars->fMonoCnf = 0; // monolythic CNF @@ -115,7 +116,7 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) // make sure the cube works { int RetValue; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 ); assert( RetValue ); } */ @@ -162,7 +163,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) } // check if the clause can be moved to the next frame - RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ); + RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0 ); if ( RetValue2 == -1 ) return -1; if ( !RetValue2 ) @@ -310,7 +311,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP int * pOrder; // if there is no induction, return *ppCubeMin = NULL; - RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) return -1; if ( RetValue == 0 ) @@ -343,7 +344,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP continue; // try removing this literal Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -381,7 +382,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP continue; // try removing this literal Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -494,7 +495,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) assert( pPred == NULL ); for ( k = pThis->iFrame; k < kMax; k++ ) { - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 ); if ( RetValue == -1 ) { Pdr_OblDeref( pThis ); @@ -659,7 +660,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->iFrame = k; return -1; } - RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 ); if ( RetValue == 1 ) break; if ( RetValue == -1 ) @@ -911,10 +912,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) RetValue = Pdr_ManSolveInt( p ); if ( RetValue == 0 ) assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); - if ( RetValue == 1 ) - Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) ); - else - Abc_FrameSetInv( NULL ); if ( p->vCexes ) { assert( p->pAig->vSeqModelVec == NULL ); @@ -922,7 +919,12 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p->vCexes = NULL; } if ( p->pPars->fDumpInv ) + { + Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); + Abc_FrameSetStr( Pdr_ManDumpString(p) ); + Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) ); Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 ); + } p->tTotal += Abc_Clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index bd9fe87c..6a08a150 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -101,6 +101,7 @@ struct Pdr_Man_t_ Vec_Int_t * vSuppLits; // support literals Pdr_Set_t * pCubeJust; // justification abctime * pTime4Outs;// timeout per output + Vec_Ptr_t * vInfCubes; // infinity clauses/cubes // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -167,8 +168,10 @@ extern Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p ); extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ); +extern Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ); extern void Pdr_ManReportInvariant( Pdr_Man_t * p ); extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p ); +extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ); /*=== pdrMan.c ==========================================================*/ extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); extern void Pdr_ManStop( Pdr_Man_t * p ); @@ -182,7 +185,7 @@ extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, in extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues ); extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); -extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ); +extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf ); /*=== pdrTsim.c ==========================================================*/ extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrUtil.c ==========================================================*/ @@ -197,6 +200,7 @@ extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove ); extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); +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 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 ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 860462c3..b548cf68 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -110,11 +110,15 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) int i, n; vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; for ( n = 0; n < pCube->nLits; n++ ) { assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) ); Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 ); } + } return vFlopCount; } @@ -202,7 +206,10 @@ int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart ) Vec_Int_t * vFlopCounts; Vec_Ptr_t * vCubes; int i, Entry, Counter = 0; - vCubes = Pdr_ManCollectCubes( p, kStart ); + if ( p->vInfCubes == NULL ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); vFlopCounts = Pdr_ManCountFlops( p, vCubes ); Vec_IntForEachEntry( vFlopCounts, Entry, i ) Counter += (Entry > 0); @@ -338,7 +345,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Vec_Ptr_t * vCubes; Pdr_Set_t * pCube; char ** pNamesCi; - int i, kStart; + int i, kStart, Count = 0; // create file pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) @@ -348,9 +355,20 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) } // collect cubes kStart = Pdr_ManFindInvariantStart( p ); - vCubes = Pdr_ManCollectCubes( p, kStart ); + if ( fProved ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); // Pdr_ManDumpAig( p->pAig, vCubes ); + // count cubes + Count = 0; + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; + Count++; + } // collect variable appearances vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; // output the header @@ -361,7 +379,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() ); fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) ); fprintf( pFile, ".o 1\n" ); - fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) ); + fprintf( pFile, ".p %d\n", Count ); // output flop names pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 ); if ( pNamesCi ) @@ -377,6 +395,8 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { + if ( pCube->nRefs == -1 ) + continue; Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); fprintf( pFile, " 1\n" ); } @@ -390,6 +410,48 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ) +{ + int fUseSupp = 1; + Vec_Str_t * vStr; + Vec_Int_t * vFlopCounts; + Vec_Ptr_t * vCubes; + Pdr_Set_t * pCube; + int i, kStart; + vStr = Vec_StrAlloc( 1000 ); + // collect cubes + kStart = Pdr_ManFindInvariantStart( p ); + if ( p->vInfCubes == NULL ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); + Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); + // collect variable appearances + vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; + // output cubes + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; + Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); + } + Vec_IntFreeP( &vFlopCounts ); + Vec_PtrFree( vCubes ); + Vec_StrPush( vStr, '\0' ); + return vStr; +} + /**Function************************************************************* @@ -469,6 +531,86 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p ) Vec_PtrFree( vCubes ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + Pdr_Set_t * pCube; + int i, kThis, RetValue, fChanges = 0, Counter = 0; + // create solver with the cubes + kThis = Vec_PtrSize(p->vSolvers); + pSat = Pdr_ManCreateSolver( p, kThis ); + // add the clauses + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + 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) ); + assert( RetValue ); + sat_solver_compress( pSat ); + } + // check each clause + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + 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-inductive + { + pCube->nRefs = -1; + fChanges = 1; + } + else + Counter++; + } + //printf( "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; + abctime clk = Abc_Clock(); + // collect cubes used in the inductive invariant + kStart = Pdr_ManFindInvariantStart( p ); + vCubes = Pdr_ManCollectCubes( p, kStart ); + // refine as long as there are changes + if ( fReduce ) + while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); + // collect remaining clauses + vResult = Vec_IntAlloc( 1000 ); + Vec_IntPush( vResult, 0 ); + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) // skip non-inductive + continue; + 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; + return vResult; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 9a73b697..b58c479b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -163,6 +163,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_IntFree( p->vCi2Rem ); // CIs to be removed Vec_IntFree( p->vRes ); // final result Vec_IntFree( p->vSuppLits ); // support literals + Vec_PtrFreeP( &p->vInfCubes ); ABC_FREE( p->pCubeJust ); ABC_FREE( p->pTime4Outs ); if ( p->vCexes ) diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 244d0311..f3681adb 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -283,7 +283,7 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) SeeAlso [] ***********************************************************************/ -int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ) +int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf ) { int fUseLit = 1; int fLitUsed = 0; @@ -329,10 +329,15 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr // solve clk = Abc_Clock(); Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); - RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 ); sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) - return -1; + { + if ( fTryConf && p->pPars->nConfGenLimit ) + RetValue = l_True; + else + return -1; + } /* if ( RetValue == l_True ) { diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 1536c1cc..53a8a54a 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -249,6 +249,46 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun ABC_FREE( pBuff ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ) +{ + char * pBuff; + int i, k = 0, Entry; + pBuff = ABC_ALLOC( char, nRegs + 1 ); + for ( i = 0; i < nRegs; i++ ) + pBuff[i] = '-'; + pBuff[i] = 0; + for ( i = 0; i < p->nLits; i++ ) + { + if ( p->Lits[i] == -1 ) + continue; + pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); + } + if ( vFlopCounts ) + { + // skip some literals + Vec_IntForEachEntry( vFlopCounts, Entry, i ) + if ( Entry ) + pBuff[k++] = pBuff[i]; + pBuff[k] = 0; + } + Vec_StrPushBuffer( vStr, pBuff, k ); + Vec_StrPush( vStr, ' ' ); + Vec_StrPush( vStr, '0' ); + Vec_StrPush( vStr, '\n' ); + ABC_FREE( pBuff ); +} + /**Function************************************************************* Synopsis [Return 1 if pOld set-theoretically contains pNew.] -- cgit v1.2.3