summaryrefslogtreecommitdiffstats
path: root/src/aig/int
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/int')
-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
4 files changed, 54 insertions, 19 deletions
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:22:01 +0000