luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Promising modification of the generalization procedure in 'pdr'.

This commit is contained in:
Alan Mishchenko 2017-02-16 10:03:34 -08:00
parent bcc6d2686f
commit c7b68c5e3f
5 changed files with 34 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/abci/abc.c
View File

@ -26171,7 +26171,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, "MFCDQTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctvwzh" ) ) != EOF )
{
switch ( c )
{
@ -26313,6 +26313,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
pPars->fSkipGeneral ^= 1;
break;
case 'j':
pPars->fSimpleGeneral ^= 1;
break;
case 'o':
pPars->fUsePropOut ^= 1;
break;
@ -26366,7 +26369,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctvwzh]\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" );
@ -26392,6 +26395,7 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Abc_Print( -2, "\t-e : toggle using only support variables in the invariant [default = %s]\n", pPars->fUseSupp? "yes": "no" );
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-j : toggle using simplified generalization step [default = %s]\n", pPars->fSimpleGeneral? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using property output as inductive hypothesis [default = %s]\n", pPars->fUsePropOut? "yes": "no" );
Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" );
Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" );

1
src/proof/pdr/pdr.h
View File

@ -60,6 +60,7 @@ struct Pdr_Par_t_
int fShortest; // forces bug traces to be shortest
int fShiftStart; // allows clause pushing to start from an intermediate frame
int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
int fSimpleGeneral; // simplified generalization
int fSkipGeneral; // skips expensive generalization step
int fSkipDown; // skips the application of down
int fCtgs; // handle CTGs in down

37
src/proof/pdr/pdrCore.c
View File

@ -125,7 +125,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, 0 );
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
assert( RetValue );
}
*/
@ -172,7 +172,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, 0 );
RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
if ( RetValue2 == -1 )
return -1;
if ( !RetValue2 )
@ -336,7 +336,7 @@ int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
continue;
// try removing this literal
Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1;
RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0 );
RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
return -1;
(*ppCube)->Lits[i] = Lit;
@ -392,7 +392,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
*added = 1;
}
ctgAttempts++;
CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0 );
CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0, 1 );
if ( CtgRetValue != 1 )
{
Pdr_SetDeref( pCtg );
@ -403,7 +403,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
pCubeMin = Pdr_SetDup ( pCtg );
for ( l = k; l < kMax; l++ )
if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0 ) )
if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0, 1 ) )
break;
micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
assert ( micResult != -1 );
@ -430,7 +430,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
// add clause
for ( i = 1; i <= l; i++ )
Pdr_ManSolverAddClause( p, i, pCubeMin );
RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
assert( RetValue >= 0 );
Pdr_SetDeref( pCtg );
if ( RetValue == 1 )
@ -464,7 +464,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
printf ("Failed initiation\n");
return 0;
}
RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
return -1;
if ( RetValue == 1 )
@ -530,7 +530,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
*ppCubeMin = NULL;
if ( p->pPars->fFlopOrder )
Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
if ( p->pPars->fFlopOrder )
Vec_IntSelectSort( pCube->Lits, pCube->nLits );
if ( RetValue == -1 )
@ -552,6 +552,16 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// perform generalization
if ( !p->pPars->fSkipGeneral )
{
// assume the unminimized cube
if ( p->pPars->fSimpleGeneral )
{
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
assert( RetValue1 == 1 );
sat_solver_compress( pSat );
}
// sort literals by their occurences
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
// try removing literals
@ -571,12 +581,13 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// check init state
if ( Pdr_SetIsInit(pCubeMin, i) )
continue;
// try removing this literal
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
if ( p->pPars->fSkipDown )
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
else
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 );
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1, !p->pPars->fSimpleGeneral );
if ( RetValue == -1 )
{
Pdr_SetDeref( pCubeMin );
@ -641,7 +652,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, 0 );
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == -1 )
{
Pdr_SetDeref( pCubeMin );
@ -759,7 +770,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, 0 );
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0, 1 );
if ( RetValue == -1 )
{
Pdr_OblDeref( pThis );
@ -940,7 +951,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = iFrame;
return -1;
}
RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0 );
RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == 1 )
break;
if ( RetValue == -1 )

2
src/proof/pdr/pdrInt.h
View File

@ -199,7 +199,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, int fTryConf );
extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit );
/*=== pdrTsim.c ==========================================================*/
extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
/*=== pdrTsim2.c ==========================================================*/

4
src/proof/pdr/pdrSat.c
View File

@ -287,9 +287,9 @@ 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 fTryConf )
int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )
{
int fUseLit = 1;
//int fUseLit = 0;
int fLitUsed = 0;
sat_solver * pSat;
Vec_Int_t * vLits;