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

Dump inductive invariant or last interpolant after interpolation.

This commit is contained in:
Alan Mishchenko 2011-11-12 16:56:41 -08:00
parent b38df9feec
commit c1ac6b9b3e
7 changed files with 108 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/aig/aig.h
View File

@ -522,6 +522,7 @@ extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int f
extern Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
extern Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
extern Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );

47
src/aig/aig/aigDup.c
View File

@ -1295,6 +1295,53 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG with only one primary output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
{
Aig_Man_t * p, * pNew;
Aig_Obj_t * pObj;
int i, k;
if ( Vec_PtrSize(vArray) == 0 )
return NULL;
p = Vec_PtrEntry( vArray, 0 );
Vec_PtrForEachEntry( Aig_Man_t *, vArray, pNew, k )
{
assert( Aig_ManRegNum(pNew) == 0 );
assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(p) );
}
// create the new manager
pNew = Aig_ManStart( 10000 );
pNew->pName = Aig_UtilStrsav( p->pName );
Aig_ManForEachPi( p, pObj, i )
Aig_ObjCreatePi(pNew);
// create the PIs
Vec_PtrForEachEntry( Aig_Man_t *, vArray, p, k )
{
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ManPi( pNew, i );
Aig_ManForEachNode( p, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

1
src/aig/int/int.h
View File

@ -62,6 +62,7 @@ struct Inter_ManParams_t_
int fUseBackward; // perform backward interpolation
int fUseSeparate; // solve each output separately
int fDropSatOuts; // replace by 1 the solved outputs
int fDropInvar; // dump inductive invariant into file
int fVerbose; // print verbose statistics
int iFrameMax; // the time frame reached
};

16
src/aig/int/intCore.c
View File

@ -179,6 +179,8 @@ p->timeCnf += clock() - clk;
RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
// assert( RetValue == 0 );
Cnf_DataFree( pCnfInter2 );
if ( p->vInters )
Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
}
//////////////////////////////////////////
@ -190,7 +192,7 @@ p->timeCnf += clock() - clk;
if ( pPars->fVerbose )
printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_ManStop( p, 0 );
Inter_CheckStop( pCheck );
return -1;
}
@ -237,7 +239,7 @@ p->timeCnf += clock() - clk;
else if ( RetValue == -1 )
printf( "Error: The problem timed out.\n" );
}
Inter_ManStop( p );
Inter_ManStop( p, 0 );
Inter_CheckStop( pCheck );
return 0;
}
@ -260,7 +262,7 @@ p->timeCnf += clock() - clk;
printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
}
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_ManStop( p, 0 );
Inter_CheckStop( pCheck );
return -1;
}
@ -283,7 +285,7 @@ p->timeRwr += clock() - clk;
if ( pPars->fVerbose )
printf( "The problem is trivially true for all states.\n" );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_ManStop( p, 1 );
Inter_CheckStop( pCheck );
return 1;
}
@ -305,6 +307,8 @@ timeTemp = clock() - clk2;
Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
Cnf_DataFree( pCnfInter2 );
if ( p->vInters )
Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
}
}
else
@ -323,7 +327,7 @@ p->timeEqu += clock() - clk - timeTemp;
if ( pPars->fVerbose )
printf( "Proved containment of interpolants.\n" );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_ManStop( p, 1 );
Inter_CheckStop( pCheck );
return 1;
}
@ -331,7 +335,7 @@ p->timeEqu += clock() - clk - timeTemp;
{
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
Inter_ManStop( p, 1 );
Inter_CheckStop( pCheck );
return -1;
}

2
src/aig/int/intInt.h
View File

@ -114,7 +114,7 @@ extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int
/*=== intMan.c ============================================================*/
extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
extern void Inter_ManClean( Inter_Man_t * p );
extern void Inter_ManStop( Inter_Man_t * p );
extern void Inter_ManStop( Inter_Man_t * p, int fProved );
/*=== intM114.c ============================================================*/
extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );

54
src/aig/int/intMan.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "intInt.h"
#include "ioa.h"
ABC_NAMESPACE_IMPL_START
@ -51,7 +52,9 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
p->nConfLimit = pPars->nBTLimit;
p->fVerbose = pPars->fVerbose;
p->pAig = pAig;
p->pAig = pAig;
if ( pPars->fDropInvar )
p->vInters = Vec_PtrAlloc( 100 );
return p;
}
@ -68,6 +71,14 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
***********************************************************************/
void Inter_ManClean( Inter_Man_t * p )
{
if ( p->vInters )
{
Aig_Man_t * pMan;
int i;
Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i )
Aig_ManStop( pMan );
Vec_PtrClear( p->vInters );
}
if ( p->pCnfInter )
Cnf_DataFree( p->pCnfInter );
if ( p->pCnfFrames )
@ -78,6 +89,29 @@ void Inter_ManClean( Inter_Man_t * p )
Aig_ManStop( p->pFrames );
}
/**Function*************************************************************
Synopsis [Writes interpolant into a file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Inter_ManInterDump( Inter_Man_t * p, int fProved )
{
Aig_Man_t * pMan;
pMan = Aig_ManDupArray( p->vInters );
Ioa_WriteAiger( pMan, "invar.aig", 0, 0 );
Aig_ManStop( pMan );
if ( fProved )
printf( "Inductive invariant is dumped into file \"invar.aig\".\n" );
else
printf( "Interpolants are dumped into file \"inter.aig\".\n" );
}
/**Function*************************************************************
Synopsis [Frees the interpolation manager.]
@ -89,7 +123,7 @@ void Inter_ManClean( Inter_Man_t * p )
SeeAlso []
***********************************************************************/
void Inter_ManStop( Inter_Man_t * p )
void Inter_ManStop( Inter_Man_t * p, int fProved )
{
if ( p->fVerbose )
{
@ -104,26 +138,22 @@ void Inter_ManStop( Inter_Man_t * p )
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
if ( p->vInters )
Inter_ManInterDump( p, fProved );
if ( p->pCnfAig )
Cnf_DataFree( p->pCnfAig );
if ( p->pCnfFrames )
Cnf_DataFree( p->pCnfFrames );
if ( p->pCnfInter )
Cnf_DataFree( p->pCnfInter );
Vec_IntFree( p->vVarsAB );
if ( p->pAigTrans )
Aig_ManStop( p->pAigTrans );
if ( p->pFrames )
Aig_ManStop( p->pFrames );
if ( p->pInter )
Aig_ManStop( p->pInter );
if ( p->pInterNew )
Aig_ManStop( p->pInterNew );
Inter_ManClean( p );
Vec_PtrFreeP( &p->vInters );
Vec_IntFreeP( &p->vVarsAB );
ABC_FREE( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -19316,7 +19316,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Inter_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbkdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbkdfvh" ) ) != EOF )
{
switch ( c )
{
@ -19403,6 +19403,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDropSatOuts ^= 1;
break;
case 'f':
pPars->fDropInvar ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -19473,7 +19476,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdvh]\n" );
Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdfvh]\n" );
Abc_Print( -2, "\t uses interpolation to prove the property\n" );
Abc_Print( -2, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax );
@ -19491,6 +19494,7 @@ usage:
Abc_Print( -2, "\t-b : toggle using backward interpolation (works with -t) [default = %s]\n", pPars->fUseBackward? "yes": "no" );
Abc_Print( -2, "\t-k : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" );
Abc_Print( -2, "\t-d : drops (replaces by 0) sat outputs (with -k is used) [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
Abc_Print( -2, "\t-f : toggle dumping inductive invariant into a file [default = %s]\n", pPars->fDropInvar? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;