diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
commit | e91abd6307e15d9d4a4985146025e12ae6780cff (patch) | |
tree | c4425a5f5686587b6fcf29a582412363537e23a1 /src/proof/pdr | |
parent | f14ee271abe8d38a6dad8789d4b4dbc207fe23c4 (diff) | |
download | abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.gz abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.bz2 abc-e91abd6307e15d9d4a4985146025e12ae6780cff.zip |
Improvements to inductive generalization in IC3/PDR by Zyad Hassan.
Diffstat (limited to 'src/proof/pdr')
-rw-r--r-- | src/proof/pdr/pdr.h | 3 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 255 | ||||
-rw-r--r-- | src/proof/pdr/pdrInt.h | 4 | ||||
-rw-r--r-- | src/proof/pdr/pdrSat.c | 6 | ||||
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 4 | ||||
-rw-r--r-- | src/proof/pdr/pdrUtil.c | 79 |
6 files changed, 342 insertions, 9 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 529a161f..b73a54df 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -49,6 +49,7 @@ struct Pdr_Par_t_ int nTimeOut; // timeout in seconds int nTimeOutGap; // approximate timeout in seconds since the last change int nTimeOutOne; // approximate timeout in seconds per one output + int nRandomSeed; // value to seed the SAT solver with int fTwoRounds; // use two rounds for generalization int fMonoCnf; // monolythic CNF int fDumpInv; // dump inductive invariant @@ -57,6 +58,8 @@ struct Pdr_Par_t_ int fShiftStart; // allows clause pushing to start from an intermediate frame int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe int fSkipGeneral; // skips expensive generalization step + int fSkipDown; // skips the application of down + int fCtgs; // handle CTGs in down int fVerbose; // verbose output` int fVeryVerbose; // very verbose output int fNotVerbose; // not printing line by line progress diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index b81a1a2a..71a61c81 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -20,6 +20,7 @@ #include "pdrInt.h" #include "base/main/main.h" +#include "misc/hash/hash.h" ABC_NAMESPACE_IMPL_START @@ -57,7 +58,10 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) 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->nRandomSeed = 91648253; // value to seed the SAT solver with pPars->fTwoRounds = 0; // use two rounds for generalization + pPars->fSkipDown = 1; // apply down in generalization + pPars->fCtgs = 0; // handle CTGs in down pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant pPars->fUseSupp = 1; // using support variables in the invariant @@ -296,6 +300,190 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube ) +{ + int * pOrder; + int i, j, n, Lit, RetValue; + Pdr_Set_t * pCubeTmp; + // perform generalization + if ( p->pPars->fSkipGeneral ) + return 0; + + // sort literals by their occurences + pOrder = Pdr_ManSortByPriority( p, *ppCube ); + // try removing literals + for ( j = 0; j < (*ppCube)->nLits; j++ ) + { + // use ordering + // i = j; + i = pOrder[j]; + + assert( (*ppCube)->Lits[i] != -1 ); + // check init state + if ( Pdr_SetIsInit(*ppCube, i) ) + continue; + // try removing this literal + Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1; + RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0 ); + if ( RetValue == -1 ) + return -1; + (*ppCube)->Lits[i] = Lit; + if ( RetValue == 0 ) + continue; + + // remove j-th entry + for ( n = j; n < (*ppCube)->nLits-1; n++ ) + pOrder[n] = pOrder[n+1]; + j--; + + // success - update the cube + *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i ); + Pdr_SetDeref( pCubeTmp ); + assert( (*ppCube)->nLits > 0 ); + i--; + + // get the ordering by decreasing priorit + pOrder = Pdr_ManSortByPriority( p, *ppCube ); + } + return 0; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added ) +{ + int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult; + int kMax = Vec_PtrSize(p->vSolvers)-1; + Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg; + while ( RetValue == 0 ) + { + ctgAttempts = 0; + while ( p->pPars->fCtgs && RetValue == 0 && k > 1 && ctgAttempts < 3 ) + { + pCtg = Pdr_SetDup ( pPred ); + //Check CTG for inductiveness + if ( Pdr_SetIsInit( pCtg, -1 ) ) + { + Pdr_SetDeref( pCtg ); + break; + } + if (*added == 0) + { + for ( i = 1; i <= k; i++ ) + Pdr_ManSolverAddClause( p, i, pIndCube); + *added = 1; + } + ctgAttempts++; + CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0 ); + if ( CtgRetValue != 1 ) + { + Pdr_SetDeref( pCtg ); + break; + } + pCubeMin = Pdr_ManReduceClause( p, k-1, pCtg ); + if ( pCubeMin == NULL ) + pCubeMin = Pdr_SetDup ( pCtg ); + + for ( l = k; l < kMax; l++ ) + if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0 ) ) + break; + micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin ); + assert ( micResult != -1 ); + + // add new clause + if ( p->pPars->fVeryVerbose ) + { + Abc_Print( 1, "Adding cube " ); + Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL ); + Abc_Print( 1, " to frame %d.\n", l ); + } + // set priority flops + for ( i = 0; i < pCubeMin->nLits; i++ ) + { + assert( pCubeMin->Lits[i] >= 0 ); + assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); + } + + Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref + p->nCubes++; + // add clause + for ( i = 1; i <= l; i++ ) + Pdr_ManSolverAddClause( p, i, pCubeMin ); + RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 ); + assert( RetValue >= 0 ); + Pdr_SetDeref( pCtg ); + if ( RetValue == 1 ) + { + //printf ("IT'S A ONE\n"); + return 1; + } + } + + //join + if ( p->pPars->fVeryVerbose ) + { + printf("Cube:\n"); + ZPdr_SetPrint( *ppCube ); + printf("\nPred:\n"); + ZPdr_SetPrint( pPred ); + } + *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep ); + Pdr_SetDeref( pCubeTmp ); + Pdr_SetDeref( pPred ); + if ( *ppCube == NULL ) + return 0; + if ( p->pPars->fVeryVerbose ) + { + printf("Intersection:\n"); + ZPdr_SetPrint( *ppCube ); + } + if ( Pdr_SetIsInit( *ppCube, -1 ) ) + { + if ( p->pPars->fVeryVerbose ) + printf ("Failed initiation\n"); + return 0; + } + RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 ); + if ( RetValue == -1 ) + return -1; + if ( RetValue == 1 ) + { + //printf ("*********IT'S A ONE\n"); + break; + } + if ( RetValue == 0 && (*ppCube)->nLits == 1) + { + Pdr_SetDeref( pPred ); // fixed memory leak + // A workaround for the incomplete assignment returned by the SAT + // solver + return 0; + } + } + return 1; +} +/**Function************************************************************* + Synopsis [Returns 1 if the state could be blocked.] Description [] @@ -307,10 +495,12 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) ***********************************************************************/ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin ) { - Pdr_Set_t * pCubeMin, * pCubeTmp = NULL; + Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL; int i, j, n, Lit, RetValue; abctime clk = Abc_Clock(); int * pOrder; + int added = 0; + Hash_Int_t * keep = NULL; // if there is no induction, return *ppCubeMin = NULL; RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 ); @@ -318,9 +508,11 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP return -1; if ( RetValue == 0 ) { - p->tGeneral += Abc_Clock() - clk; + p->tGeneral += clock() - clk; return 0; } + + keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 ); // reduce clause using assumptions // pCubeMin = Pdr_SetDup( pCube ); @@ -340,13 +532,22 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP // i = j; i = pOrder[j]; - // check init state assert( pCubeMin->Lits[i] != -1 ); + if ( keep && Hash_IntExists( keep, pCubeMin->Lits[i] ) ) + { + //printf("Undroppable\n"); + continue; + } + + // check init state if ( Pdr_SetIsInit(pCubeMin, i) ) continue; // try removing this literal - Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); + Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; + if ( p->pPars->fSkipDown ) + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); + else + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -354,7 +555,39 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP } pCubeMin->Lits[i] = Lit; if ( RetValue == 0 ) + { + if ( p->pPars->fSkipDown ) + continue; + pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i ); + RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added ); + if ( p->pPars->fCtgs ) + //CTG handling code messes up with the internal order array + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + if ( RetValue == -1 ) + { + Pdr_SetDeref( pCubeMin ); + Pdr_SetDeref( pCubeCpy ); + Pdr_SetDeref( pPred ); + return -1; + } + if ( RetValue == 0 ) + { + if ( keep ) + Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 ); + if ( pCubeCpy ) + Pdr_SetDeref( pCubeCpy ); continue; + } + //Inductive subclause + added = 0; + Pdr_SetDeref( pCubeMin ); + pCubeMin = pCubeCpy; + assert( pCubeMin->nLits > 0 ); + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + j = -1; + continue; + } + added = 0; // remove j-th entry for ( n = j; n < pCubeMin->nLits-1; n++ ) @@ -383,7 +616,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP if ( Pdr_SetIsInit(pCubeMin, i) ) continue; // try removing this literal - Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; + Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) { @@ -411,8 +644,18 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP } assert( ppCubeMin != NULL ); + if ( p->pPars->fVeryVerbose ) + { + printf("Cube:\n"); + for ( i = 0; i < pCubeMin->nLits; i++) + { + printf ("%d ", pCubeMin->Lits[i]); + } + printf("\n"); + } *ppCubeMin = pCubeMin; p->tGeneral += Abc_Clock() - clk; + if ( keep ) Hash_IntFree( keep ); return 1; } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 6a08a150..9c1e9840 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -30,6 +30,7 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver.h" #include "pdr.h" +#include "misc/hash/hashInt.h" ABC_NAMESPACE_HEADER_START @@ -196,10 +197,13 @@ extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int n extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ); extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ); extern void Pdr_SetDeref( Pdr_Set_t * p ); +extern Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep ); 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 int ZPdr_SetIsInit( Pdr_Set_t * p ); extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); +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 Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 2e6130aa..eb94a826 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -51,7 +51,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) assert( Vec_VecSize(p->vClauses) == k ); assert( Vec_IntSize(p->vActVars) == k ); // create new solver - pSat = sat_solver_new(); +// pSat = sat_solver_new(); + pSat = zsat_solver_new_seed(p->pPars->nRandomSeed); pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) ); Vec_PtrPush( p->vSolvers, pSat ); Vec_VecExpand( p->vClauses, k ); @@ -86,7 +87,8 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ) p->nStarts++; // sat_solver_delete( pSat ); // pSat = sat_solver_new(); - sat_solver_restart( pSat ); +// sat_solver_restart( pSat ); + zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed ); // create new SAT solver pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) ); // write new SAT solver diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 32d1c857..37f84667 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -476,7 +476,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); assert( Vec_IntSize(vRes) > 0 ); p->tTsim += Abc_Clock() - clk; pRes = Pdr_SetCreate( vRes, vPiLits ); - assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); + //ZH: Disabled assertion because this invariant doesn't hold with down + //because of the join operation which can bring in initial states + //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); return pRes; } diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 32e97772..8fb83fd2 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -260,6 +260,85 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun SeeAlso [] ***********************************************************************/ +void ZPdr_SetPrint( Pdr_Set_t * p ) +{ + int i; + for ( i = 0; i < p->nLits; i++) + printf ("%d ", p->Lits[i]); + printf ("\n"); + +} + +/**Function************************************************************* + + Synopsis [Return the intersection of p1 and p2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep ) +{ + Pdr_Set_t * pIntersection; + Vec_Int_t * vCommonLits, * vPiLits; + int i, j, nLits; + nLits = p1->nLits; + if ( p2->nLits < nLits ) + nLits = p2->nLits; + vCommonLits = Vec_IntAlloc( nLits ); + vPiLits = Vec_IntAlloc( 1 ); + for ( i = 0, j = 0; i < p1->nLits && j < p2->nLits; ) + { + if ( p1->Lits[i] > p2->Lits[j] ) + { + if ( Hash_IntExists( keep, p2->Lits[j] ) ) + { + //about to drop a literal that should not be dropped + Vec_IntFree( vCommonLits ); + Vec_IntFree( vPiLits ); + return NULL; + } + j++; + } + else if ( p1->Lits[i] < p2->Lits[j] ) + { + if ( Hash_IntExists( keep, p1->Lits[i] ) ) + { + //about to drop a literal that should not be dropped + Vec_IntFree( vCommonLits ); + Vec_IntFree( vPiLits ); + return NULL; + } + i++; + } + else + { + Vec_IntPush( vCommonLits, p1->Lits[i] ); + i++; + j++; + } + } + pIntersection = Pdr_SetCreate( vCommonLits, vPiLits ); + Vec_IntFree( vCommonLits ); + Vec_IntFree( vPiLits ); + return pIntersection; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ) { char * pBuff; |