Skip to content

A
abc
Commit 3b1cf097 by Alan Mishchenko
Options

Added bridge integration for multi-output 'pdr -a'.

parent e87f0dd6
Showing with 44 additions and 13 deletions
src/aig/gia/gia.h
......@@ -762,6 +762,18 @@ static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x )
ch = x;
Vec_StrPush( vStr, ch );
}
static inline void Gia_AigerWriteUnsignedFile( FILE * pFile, unsigned x )
{
unsigned char ch;
while (x & ~0x7f)
{
ch = (x & 0x7f) | 0x80;
fputc( ch, pFile );
x >>= 7;
}
ch = x;
fputc( ch, pFile );
}
static inline int Gia_AigerWriteUnsignedBuffer( unsigned char * pBuffer, int Pos, unsigned x )
{
unsigned char ch;
......
src/base/abci/abc.c
......@@ -12547,7 +12547,7 @@ usage:
***********************************************************************/
int Abc_CommandSendStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex );
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "" ) ) != EOF )
......@@ -12570,7 +12570,7 @@ int Abc_CommandSendStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Status is \"sat\", but current CEX is not available.\n" );
return 1;
}
Gia_ManToBridgeResult( stdout, pAbc->Status, pAbc->pCex );
Gia_ManToBridgeResult( stdout, pAbc->Status, pAbc->pCex, 0 );
return 0;
usage:
......@@ -23754,6 +23754,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// run the procedure
pPars->fUseBridge = pAbc->fBatchMode;
pAbc->Status = Abc_NtkDarPdr( pNtk, pPars );
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
src/misc/util/utilBridge.c
......@@ -191,7 +191,7 @@ int Gia_ManToBridgeBadAbs( FILE * pFile )
SeeAlso []
***********************************************************************/
void Gia_ManFromBridgeHolds( FILE * pFile )
void Gia_ManFromBridgeHolds( FILE * pFile, int iPoProved )
{
fprintf( pFile, "%.6d", 101 /*message type = Result*/);
fprintf( pFile, " " );
......@@ -200,11 +200,12 @@ void Gia_ManFromBridgeHolds( FILE * pFile )
fputc( (char)BRIDGE_VALUE_1, pFile ); // true
fputc( (char)1, pFile ); // size of vector (Armin's encoding)
fputc( (char)0, pFile ); // number of the property (Armin's encoding)
// fputc( (char)0, pFile ); // number of the property (Armin's encoding)
Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
fputc( (char)0, pFile ); // no invariant
fflush(pFile);
}
void Gia_ManFromBridgeUnknown( FILE * pFile )
void Gia_ManFromBridgeUnknown( FILE * pFile, int iPoProved )
{
fprintf( pFile, "%.6d", 101 /*message type = Result*/);
fprintf( pFile, " " );
......@@ -213,7 +214,8 @@ void Gia_ManFromBridgeUnknown( FILE * pFile )
fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
fputc( (char)1, pFile ); // size of vector (Armin's encoding)
fputc( (char)0, pFile ); // number of the property (Armin's encoding)
// fputc( (char)0, pFile ); // number of the property (Armin's encoding)
Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
fflush(pFile);
}
void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
......@@ -222,7 +224,8 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
// Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
Gia_AigerWriteUnsigned( vStr, pCex->iPo ); // number of the property (Armin's encoding)
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
......@@ -246,14 +249,14 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
Vec_StrFree( vStr );
fflush(pFile);
}
int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex )
int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved )
{
if ( Result == 0 ) // sat
Gia_ManFromBridgeCex( pFile, pCex );
else if ( Result == 1 ) // unsat
Gia_ManFromBridgeHolds( pFile );
Gia_ManFromBridgeHolds( pFile, iPoProved );
else if ( Result == -1 ) // undef
Gia_ManFromBridgeUnknown( pFile );
Gia_ManFromBridgeUnknown( pFile, iPoProved );
else assert( 0 );
return 1;
}
......
src/proof/pdr/pdr.h
......@@ -59,6 +59,7 @@ struct Pdr_Par_t_
int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output
int fStoreCex; // enable storing counter-examples in MO mode
int fUseBridge; // use bridge interface
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of timed out outputs
int nProveOuts; // the number of proved outputs
......
src/proof/pdr/pdrCore.c
......@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -574,6 +576,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
int fPrintClauses = 0;
Pdr_Set_t * pCube = NULL;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew;
int k, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0;
......@@ -603,15 +606,19 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( !p->pPars->fSolveAll )
{
p->pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
p->pAig->pSeqModel = pCexNew;
return 0; // SAT
}
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
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->fVerbose )
......@@ -709,9 +716,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
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 );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
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->fVerbose )
......@@ -794,7 +804,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->vOutMap )
for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
{
Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, k );
}
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT
if ( p->pPars->nFailOuts > 0 )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment