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

Dump last frame clauses with 'pdr -d' even if the problem is SAT or undecided.

This commit is contained in:
Alan Mishchenko 2011-11-12 14:03:00 -08:00
parent c16f5d6494
commit 814ee4841b
3 changed files with 17 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/sat/pdr/pdrCore.c
View File

@ -614,8 +614,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
Pdr_ManReportInvariant( p );
Pdr_ManVerifyInvariant( p );
if ( p->pPars->fDumpInv )
Pdr_ManDumpClauses( p, (char *)"inv.pla" );
p->pPars->iFrame = k;
return 1; // UNSAT
}
@ -669,6 +667,9 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
RetValue = Pdr_ManSolveInt( p );
*ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
if ( p->pPars->fDumpInv )
Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
// if ( *ppCex && pPars->fVerbose )
// printf( "Found counter-example in frame %d after exploring %d frames.\n",
// (*ppCex)->iFrame, p->nFrames );

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

@ -144,7 +144,7 @@ extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t
/*=== pdrInv.c ==========================================================*/
extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName );
extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
/*=== pdrMan.c ==========================================================*/

17
src/sat/pdr/pdrInv.c
View File

@ -136,7 +136,10 @@ int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
if ( Vec_PtrSize(vArrayK) == 0 )
return k;
return -1;
// return -1;
// if there is no starting point (as in case of SAT or undecided), return the last frame
// printf( "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
return kMax;
}
/**Function*************************************************************
@ -227,7 +230,7 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
SeeAlso []
***********************************************************************/
void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
{
int fUseSupp = 1;
FILE * pFile;
@ -250,7 +253,10 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
// collect variable appearances
vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
// output the header
fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
if ( fProved )
fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
else
fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
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" );
@ -277,7 +283,10 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
fclose( pFile );
Vec_IntFreeP( &vFlopCounts );
Vec_PtrFree( vCubes );
printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
if ( fProved )
printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
else
printf( "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
}