summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c47
-rw-r--r--src/aig/int/int.h1
-rw-r--r--src/aig/int/intCore.c16
-rw-r--r--src/aig/int/intInt.h2
-rw-r--r--src/aig/int/intMan.c54
-rw-r--r--src/base/abci/abc.c8
7 files changed, 108 insertions, 21 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 731f7c84..40d7a90c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -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 );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index dcd2e477..4c3b2840 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -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 ///
diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index 907691ed..4b8d78bb 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -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
};
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index 0cd5eb36..3bd111be 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -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;
}
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index 3eab7883..66ff9578 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -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 );
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
index 2faef198..d6219f6b 100644
--- a/src/aig/int/intMan.c
+++ b/src/aig/int/intMan.c
@@ -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 )
@@ -80,6 +91,29 @@ void Inter_ManClean( Inter_Man_t * p )
/**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.]
Description []
@@ -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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a1d32f5b..ed40fee0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:05:46 +0000