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

Merge pull request #320 from YosysHQ/povik/revert-pdr 

Revert recent PDR changes
This commit is contained in:
alanminko 2024-08-12 17:17:24 -07:00 committed by GitHub
parent 81fcf8494e de8620d777
commit 324ceeaa08
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
9 changed files with 55 additions and 478 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -30251,7 +30251,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Pdr_ManSetDefaultParams( pPars ); Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -30372,21 +30372,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pInvFileName = argv[globalUtilOptind]; pPars->pInvFileName = argv[globalUtilOptind];
globalUtilOptind++; globalUtilOptind++;
break; 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': case 'a':
pPars->fSolveAll ^= 1; pPars->fSolveAll ^= 1;
break; break;
case 'l':
pPars->fAnytime ^= 1;
break;
case 'x': case 'x':
pPars->fStoreCex ^= 1; pPars->fStoreCex ^= 1;
break; break;
@ -30491,7 +30479,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-X <prefix>] [-axrmuyfqipdegjonctkvwzh]\n" ); Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-LI <file>] [-axrmuyfqipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\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 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" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@ -30506,9 +30494,7 @@ usage:
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); 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-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-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 <pref>*.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-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-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-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" ); Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );

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

@ -72,7 +72,6 @@ struct Pdr_Par_t_
int fSilent; // totally silent execution int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output int fSolveAll; // do not stop when found a SAT output
int fStoreCex; // enable storing counter-examples in MO mode int fStoreCex; // enable storing counter-examples in MO mode
int fAnytime; // enable anytime scheduling
int fUseBridge; // use bridge interface int fUseBridge; // use bridge interface
int fUsePropOut; // use property output int fUsePropOut; // use property output
int nFailOuts; // the number of failed outputs int nFailOuts; // the number of failed outputs
@ -85,7 +84,6 @@ struct Pdr_Par_t_
abctime timeLastSolved; // the time when the last output was solved 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) 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 * pInvFileName; // invariable file name
char * pCexFilePrefix; // CEX output prefix
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -97,7 +95,6 @@ struct Pdr_Par_t_
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== pdrCore.c ==========================================================*/ /*=== pdrCore.c ==========================================================*/
extern void Pdr_OutputCexToDir( Pdr_Par_t * pPars, Abc_Cex_t * pCex );
extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ); extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars ); extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );

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

@ -80,7 +80,6 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->nDropOuts = 0; // the number of timed out outputs pPars->nDropOuts = 0; // the number of timed out outputs
pPars->timeLastSolved = 0; // last one solved pPars->timeLastSolved = 0; // last one solved
pPars->pInvFileName = NULL; // invariant file name pPars->pInvFileName = NULL; // invariant file name
pPars->pCexFilePrefix = NULL; // CEX output prefix
} }
/**Function************************************************************* /**Function*************************************************************
@ -136,150 +135,6 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
return pCubeMin; 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************************************************************* /**Function*************************************************************
Synopsis [Returns 1 if the state could be blocked.] Synopsis [Returns 1 if the state could be blocked.]
@ -297,6 +152,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
Vec_Ptr_t * vArrayK, * vArrayK1; Vec_Ptr_t * vArrayK, * vArrayK1;
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1; int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
int Counter = 0;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
assert( p->iUseFrame > 0 ); assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
@ -305,11 +161,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 ); vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{ {
Counter++;
// remove cubes in the same frame that are contained by pCubeK // remove cubes in the same frame that are contained by pCubeK
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
{ {
if ( pTemp->iBound > pCubeK->iBound )
continue;
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue; continue;
Pdr_SetDeref( pTemp ); Pdr_SetDeref( pTemp );
@ -341,9 +197,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// check if the clause subsumes others // check if the clause subsumes others
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i ) 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 if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
continue; continue;
Pdr_SetDeref( pCubeK1 ); Pdr_SetDeref( pCubeK1 );
@ -352,7 +205,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
i--; i--;
} }
// add the last clause // add the last clause
pCubeK->iBound = k+1;
Vec_PtrPush( vArrayK1, pCubeK ); Vec_PtrPush( vArrayK1, pCubeK );
Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) ); Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
Vec_PtrPop(vArrayK); Vec_PtrPop(vArrayK);
@ -370,8 +222,6 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// remove cubes in the same frame that are contained by pCubeK // remove cubes in the same frame that are contained by pCubeK
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 ) Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
{ {
if ( pTemp->iBound > pCubeK->iBound )
continue;
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
continue; continue;
/* /*
@ -1057,9 +907,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
while ( !Pdr_QueueIsEmpty(p) ) while ( !Pdr_QueueIsEmpty(p) )
{ {
Counter++; Counter++;
if (Counter % 100 == 0) {
Pdr_ManPrintProgress( p, 1, Abc_Clock() - p->tStart );
}
pThis = Pdr_QueueHead( p ); pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) ) if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) )
return 0; // SAT return 0; // SAT
@ -1139,7 +986,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
p->nAbsFlops++; p->nAbsFlops++;
Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
} }
pCubeMin->iBound = k;
Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
p->nCubes++; p->nCubes++;
// add clause // add clause
@ -1180,38 +1026,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
return 1; 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 = (char *)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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -1229,36 +1043,24 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_Set_t * pCube = NULL; Pdr_Set_t * pCube = NULL;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew; 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) ); int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0; abctime clkStart = Abc_Clock(), clkOne = 0;
p->tStart = clkStart;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
assert( Vec_PtrSize(p->vSolvers) == 0 ); assert( Vec_PtrSize(p->vSolvers) == 0 );
// in the multi-output mode, mark trivial POs (those fed by const0) as solved // in the multi-output mode, mark trivial POs (those fed by const0) as solved
if ( p->pPars->fSolveAll || p->pPars->fAnytime ) if ( p->pPars->fSolveAll )
Saig_ManForEachPo( p->pAig, pObj, i ) Saig_ManForEachPo( p->pAig, pObj, iFrame )
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) && Vec_IntEntry( p->pPars->vOutMap, i ) == -2) if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
{ {
Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
Abc_Print( 1, "Proved output %d in frame 0 (trivial).\n", i );
p->pPars->nProveOuts++; p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, i ); Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
} }
// create the first timeframe // create the first timeframe
p->pPars->timeLastSolved = Abc_Clock(); p->pPars->timeLastSolved = Abc_Clock();
Pdr_ManCreateSolver( p, (iFrame = 0) ); 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 ) while ( 1 )
{ {
int fRefined = 0; int fRefined = 0;
@ -1278,15 +1080,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->nFrames = iFrame; p->nFrames = iFrame;
assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
p->iUseFrame = Abc_MaxInt(iFrame, 1); p->iUseFrame = Abc_MaxInt(iFrame, 1);
SomeActive = 0;
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{ {
// skip disproved outputs // skip disproved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) ) if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
continue; 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 // skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 ) if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
continue; continue;
@ -1302,7 +1100,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pAig->pSeqModel = pCexNew; p->pAig->pSeqModel = pCexNew;
return 0; // SAT 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++; p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( !p->pPars->fNotVerbose ) if ( !p->pPars->fNotVerbose )
@ -1311,8 +1109,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, 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) ) if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{ {
@ -1328,7 +1124,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->timeLastSolved = Abc_Clock(); p->pPars->timeLastSolved = Abc_Clock();
continue; continue;
} }
SomeActive += 1;
// try to solve this output // try to solve this output
if ( p->pTime4Outs ) if ( p->pTime4Outs )
{ {
@ -1373,7 +1168,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
} }
if ( RetValue == 0 ) if ( RetValue == 0 )
{ {
ClausesAdded = 1;
RetValue = Pdr_ManBlockCube( p, pCube ); RetValue = Pdr_ManBlockCube( p, pCube );
if ( RetValue == -1 ) if ( RetValue == -1 )
{ {
@ -1423,13 +1217,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT return 0; // SAT
} }
p->pPars->nFailOuts++; 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 ); if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, 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) ) if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{ {
@ -1447,7 +1239,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // all SAT return 0; // all SAT
Pdr_QueueClean( p ); Pdr_QueueClean( p );
pCube = NULL; pCube = NULL;
SomeActive--;
break; // keep solving break; // keep solving
} }
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
@ -1461,19 +1252,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
abctime timeSince = Abc_Clock() - clkOne; abctime timeSince = Abc_Clock() - clkOne;
assert( p->pTime4Outs[p->iOutCur] > 0 ); assert( p->pTime4Outs[p->iOutCur] > 0 );
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 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++; p->pPars->nDropOuts++;
if ( p->pPars->vOutMap ) if ( p->pPars->vOutMap )
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( !p->pPars->fNotVerbose ) if ( !p->pPars->fNotVerbose )
{ Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
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 );
}
} }
p->timeToStopOne = 0; p->timeToStopOne = 0;
} }
@ -1494,10 +1279,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
// open a new timeframe // open a new timeframe
p->nQueLim = p->pPars->nRestLimit; p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL ); assert( pCube == NULL );
if ( p->pPars->fAnytime && ClausesAdded )
Vec_IntFree( Pdr_ManDeriveInfinityClauses( p, 1 ) );
Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManSetPropertyOutput( p, iFrame );
Pdr_ManCreateSolver( p, ++iFrame ); Pdr_ManCreateSolver( p, ++iFrame );
if ( fPrintClauses ) if ( fPrintClauses )
@ -1506,23 +1287,14 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintClauses( p, 0 ); Pdr_ManPrintClauses( p, 0 );
} }
// push clauses into this timeframe // push clauses into this timeframe
RetValue = 0; RetValue = Pdr_ManPushClauses( p );
if ( p->pPars->fAnytime ) if ( RetValue == -1 )
{
RetValue = Pdr_ManPushInfAndRecycledClauses( p );
ClausesAdded = 0;
}
RetValue = RetValue == -1 ? -1 : Pdr_ManPushClauses( p );
if ( RetValue == -1 || !SomeActive )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
{ {
if ( !SomeActive ) if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "All outputs solved or timed out in frame %d.\n", iFrame );
else if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else else
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
@ -1534,34 +1306,22 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{ {
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fAnytime ) if ( !p->pPars->fSilent )
{ Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent ) if ( !p->pPars->fSilent )
Pdr_ManReportInvariant( p ); Pdr_ManVerifyInvariant( p );
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
}
p->pPars->iFrame = iFrame; 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' // convert previously 'unknown' into 'unsat'
if ( p->pPars->vOutMap ) if ( p->pPars->vOutMap )
{ for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
for ( i = 0; i < Saig_ManPoNum(p->pAig); i++ ) if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
if ( Vec_IntEntry(p->pPars->vOutMap, i) == -2 ) // unknown
{ {
Vec_IntWriteEntry( p->pPars->vOutMap, i, 1 ); // unsat Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
Abc_Print( 1, "Proved output %d in frame %d (converged).\n", i );
p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge ) 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) ) if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT return 1; // UNSAT
if ( p->pPars->nFailOuts > 0 ) if ( p->pPars->nFailOuts > 0 )
@ -1619,61 +1379,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return -1; 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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -1688,21 +1393,12 @@ void Pdr_ManResetReuseInvariant( Pdr_Man_t * p )
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{ {
Pdr_Man_t * p; Pdr_Man_t * p;
int k, RetValue, nTimeOutU; int k, RetValue;
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
if ( pPars->fAnytime ) if ( pPars->nTimeOutOne && !pPars->fSolveAll )
{
if ( pPars->nTimeOutOne == 0 )
pPars->nTimeOutOne = 200;
}
if ( pPars->nTimeOutOne && !(pPars->fSolveAll || pPars->fAnytime) )
pPars->nTimeOutOne = 0; pPars->nTimeOutOne = 0;
if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 ) if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
{ pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
nTimeOutU = pPars->nTimeOutOne * (Saig_ManPoNum(pAig) - pPars->nProveOuts - pPars->nFailOuts);
pPars->nTimeOut = (nTimeOutU + 999) / 10; // TODO XXX
}
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
@ -1718,17 +1414,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
} }
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
p = Pdr_ManStart( pAig, pPars, NULL ); p = Pdr_ManStart( pAig, pPars, NULL );
RetValue = Pdr_ManSolveInt( p );
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;
}
if ( RetValue == 0 ) if ( RetValue == 0 )
assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
if ( p->vCexes ) if ( p->vCexes )

8
src/proof/pdr/pdrIncr.c
View File

@ -379,7 +379,6 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
int iFrame, RetValue = -1; int iFrame, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0; abctime clkStart = Abc_Clock(), clkOne = 0;
p->tStart = clkStart;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
// assert( Vec_PtrSize(p->vSolvers) == 0 ); // assert( Vec_PtrSize(p->vSolvers) == 0 );
// in the multi-output mode, mark trivial POs (those fed by const0) as solved // in the multi-output mode, mark trivial POs (those fed by const0) as solved
@ -485,7 +484,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
p->pAig->pSeqModel = pCexNew; p->pAig->pSeqModel = pCexNew;
return 0; // SAT 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++; p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( !p->pPars->fNotVerbose ) if ( !p->pPars->fNotVerbose )
@ -494,8 +493,6 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
if ( p->pPars->pCexFilePrefix )
Pdr_OutputCexToDir( p->pPars, pCexNew );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, 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) ) if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{ {
@ -679,8 +676,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
//if ( p->pPars->fUseAbs && p->vAbsFlops ) //if ( p->pPars->fUseAbs && p->vAbsFlops )
// printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
// open a new timeframe // open a new timeframe
p->nQueLim = iFrame + p->pPars->nRestLimit; p->nQueLim = p->pPars->nRestLimit;
p->nQueLimStep = 1;
assert( pCube == NULL ); assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, iFrame ); Pdr_ManSetPropertyOutput( p, iFrame );
Pdr_ManCreateSolver( p, ++iFrame ); Pdr_ManCreateSolver( p, ++iFrame );

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

@ -58,8 +58,6 @@
#define sat_solver_compress(s) #define sat_solver_compress(s)
#endif #endif
#define PDR_INF_BOUND ((int)((~((unsigned int)0)) >> 1))
ABC_NAMESPACE_HEADER_START ABC_NAMESPACE_HEADER_START
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -78,7 +76,6 @@ struct Pdr_Set_t_
{ {
word Sign; // signature word Sign; // signature
int nRefs; // ref counter int nRefs; // ref counter
int iBound; // known to hold up to this frame, INT_MAX = inf
int nTotal; // total literals int nTotal; // total literals
int nLits; // num flop literals int nLits; // num flop literals
int Lits[0]; int Lits[0];
@ -159,11 +156,8 @@ struct Pdr_Man_t_
int nQueCur; int nQueCur;
int nQueMax; int nQueMax;
int nQueLim; int nQueLim;
int nQueLimStep;
int nXsimRuns; int nXsimRuns;
int nXsimLits; int nXsimLits;
int nInfClauses;
int fNewInfClauses;
// runtime // runtime
abctime timeToStop; abctime timeToStop;
abctime timeToStopOne; abctime timeToStopOne;
@ -178,7 +172,6 @@ struct Pdr_Man_t_
abctime tCnf; abctime tCnf;
abctime tAbs; abctime tAbs;
abctime tTotal; 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 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 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_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_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
extern void Pdr_OblDeref( Pdr_Obl_t * p ); extern void Pdr_OblDeref( Pdr_Obl_t * p );

77
src/proof/pdr/pdrInv.c
View File

@ -48,15 +48,14 @@ ABC_NAMESPACE_IMPL_START
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
{ {
Vec_Ptr_t * vVec; Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart, kLast, Value, Width; int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 ) if ( Vec_PtrSize(p->vSolvers) < 2 )
{ {
Abc_Print(1, "Frame " ); Abc_Print(1, "Frame " );
Abc_Print(1, "Clauses " ); Abc_Print(1, "Clauses " );
Abc_Print(1, "Max Queue " ); Abc_Print(1, "Max Queue " );
Abc_Print(1, "Flops " ); Abc_Print(1, "Flops " );
if ( p->pPars->fUseAbs ) Abc_Print(1, "Cex " );
Abc_Print(1, "Cex " );
Abc_Print(1, "Time" ); Abc_Print(1, "Time" );
Abc_Print(1, "\n" ); Abc_Print(1, "\n" );
return; return;
@ -65,12 +64,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
return; return;
// count the total length of the printout // count the total length of the printout
Length = 0; Length = 0;
kLast = Vec_VecSize( p->vClauses ) - 1;
Vec_VecForEachLevel( p->vClauses, vVec, i ) Vec_VecForEachLevel( p->vClauses, vVec, i )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1 - (i == kLast ? p->nInfClauses : 0) ); Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
if ( p->vInfCubes != NULL && Vec_PtrSize(p->vInfCubes) > 0 )
Length += 2 + Abc_Base10Log(Vec_PtrSize(p->vInfCubes)+1);
// determine the starting point // determine the starting point
LengthStart = Abc_MaxInt( 0, Length - 60 ); LengthStart = Abc_MaxInt( 0, Length - 60 );
Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 ); 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; Length = 0;
Vec_VecForEachLevel( p->vClauses, vVec, i ) Vec_VecForEachLevel( p->vClauses, vVec, i )
{ {
Value = Vec_PtrSize(vVec) - (i == kLast ? p->nInfClauses : 0);
Width = 1 + Abc_Base10Log(Value+1);
if ( Length < LengthStart ) if ( Length < LengthStart )
{ {
Length += Width; Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
continue; continue;
} }
Abc_Print( 1, " %d", Value ); Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
Length += Width; Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
ThisSize += Width; ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
}
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);
} }
for ( i = ThisSize; i < 70; i++ ) for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " ); Abc_Print( 1, " " );
Abc_Print( 1, "%5d", p->nQueMax ); Abc_Print( 1, "%5d", p->nQueMax );
Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops ); Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
if ( p->pPars->fUseAbs ) 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 ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll ) if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
if ( p->pPars->nTimeOutOne ) if ( p->pPars->nTimeOutOne )
Abc_Print( 1, " T/O =%3d", p->pPars->nDropOuts ); 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" ); Abc_Print( 1, "%s", fClose ? "\n":"\r" );
if ( fClose ) if ( fClose )
p->nQueMax = 0, p->nCexes = 0; 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) ); vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{ {
if ( pCube->iBound != PDR_INF_BOUND ) if ( pCube->nRefs == -1 )
continue; continue;
for ( n = 0; n < pCube->nLits; n++ ) for ( n = 0; n < pCube->nLits; n++ )
{ {
@ -392,7 +376,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
Count = 0; Count = 0;
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{ {
if ( pCube->iBound != PDR_INF_BOUND ) if ( pCube->nRefs == -1 )
continue; continue;
Count++; Count++;
} }
@ -422,7 +406,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
// output cubes // output cubes
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{ {
if ( pCube->iBound != PDR_INF_BOUND ) if ( pCube->nRefs == -1 )
continue; continue;
Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
fprintf( pFile, " 1\n" ); fprintf( pFile, " 1\n" );
@ -468,7 +452,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
// output cubes // output cubes
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{ {
if ( pCube->iBound != PDR_INF_BOUND ) if ( pCube->nRefs == -1 )
continue; continue;
Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); 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 // add the clauses
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) 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; continue;
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); 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 // check each clause
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) 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; continue;
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); 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 ); 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; fChanges = 1;
} }
else else
Counter++; 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 ); //Abc_Print(1, "Clauses = %d.\n", Counter );
//sat_solver_delete( pSat ); //sat_solver_delete( pSat );
return fChanges; return fChanges;
} }
Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
{ {
Vec_Int_t * vResult; Vec_Int_t * vResult;
Vec_Ptr_t * vCubes; Vec_Ptr_t * vCubes;
Pdr_Set_t * pCube; Pdr_Set_t * pCube;
int i, v, kStart, kMax; int i, v, kStart;
// collect cubes used in the inductive invariant // collect cubes used in the inductive invariant
kMax = Vec_PtrSize( p->vSolvers );
kStart = Pdr_ManFindInvariantStart( p ); kStart = Pdr_ManFindInvariantStart( p );
vCubes = Pdr_ManCollectCubes( p, kStart ); 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 // refine as long as there are changes
if ( fReduce ) if ( fReduce )
while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); 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_IntPush( vResult, 0 );
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{ {
if ( pCube->iBound >= 0 && pCube->iBound != PDR_INF_BOUND ) { if ( pCube->nRefs == -1 ) // skip non-inductive
Vec_PtrWriteEntry( vCubes, i, Vec_PtrEntryLast( vCubes ) );
Vec_PtrPop( vCubes );
i--;
continue; continue;
}
if (pCube->iBound != PDR_INF_BOUND)
{
p->nInfClauses++;
p->fNewInfClauses = 1;
pCube->iBound = PDR_INF_BOUND;
}
Vec_IntAddToEntry( vResult, 0, 1 ); Vec_IntAddToEntry( vResult, 0, 1 );
Vec_IntPush( vResult, pCube->nLits ); Vec_IntPush( vResult, pCube->nLits );
for ( v = 0; v < pCube->nLits; v++ ) for ( v = 0; v < pCube->nLits; v++ )
Vec_IntPush( vResult, pCube->Lits[v] ); Vec_IntPush( vResult, pCube->Lits[v] );
} }
//Vec_PtrFree( vCubes );
Vec_PtrFreeP( &p->vInfCubes ); Vec_PtrFreeP( &p->vInfCubes );
p->vInfCubes = vCubes; p->vInfCubes = vCubes;
Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) ); Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );

3
src/proof/pdr/pdrMan.c
View File

@ -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; p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
} }
if ( pPars->fSolveAll ) 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) ); p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 ); Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
} }

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

@ -99,8 +99,7 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
// add the clauses // add the clauses
Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
if ( pCube != NULL ) Pdr_ManSolverAddClause( p, k, pCube );
Pdr_ManSolverAddClause( p, k, pCube );
return pSat; return pSat;
} }

39
src/proof/pdr/pdrUtil.c
View File

@ -71,7 +71,6 @@ Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
p->nLits = Vec_IntSize(vLits); p->nLits = Vec_IntSize(vLits);
p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits); p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
p->nRefs = 1; p->nRefs = 1;
p->iBound = 0;
p->Sign = 0; p->Sign = 0;
for ( i = 0; i < p->nLits; i++ ) 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->nLits = pSet->nLits - 1;
p->nTotal = pSet->nTotal - 1; p->nTotal = pSet->nTotal - 1;
p->nRefs = 1; p->nRefs = 1;
p->iBound = 0;
p->Sign = 0; p->Sign = 0;
for ( i = 0; i < pSet->nTotal; i++ ) 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->nLits = nLits;
p->nTotal = nLits + pSet->nTotal - pSet->nLits; p->nTotal = nLits + pSet->nTotal - pSet->nLits;
p->nRefs = 1; p->nRefs = 1;
p->iBound = 0;
p->Sign = 0; p->Sign = 0;
for ( i = 0; i < nLits; i++ ) for ( i = 0; i < nLits; i++ )
{ {
@ -174,7 +171,6 @@ Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
p->nLits = pSet->nLits; p->nLits = pSet->nLits;
p->nTotal = pSet->nTotal; p->nTotal = pSet->nTotal;
p->nRefs = 1; p->nRefs = 1;
p->iBound = 0;
p->Sign = pSet->Sign; p->Sign = pSet->Sign;
for ( i = 0; i < pSet->nTotal; i++ ) for ( i = 0; i < pSet->nTotal; i++ )
p->Lits[i] = pSet->Lits[i]; p->Lits[i] = pSet->Lits[i];
@ -505,41 +501,6 @@ int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
return 0; 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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []