summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/int/intCore.c66
-rw-r--r--src/aig/int/intInt.h54
-rw-r--r--src/aig/int/module.make3
3 files changed, 90 insertions, 33 deletions
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index c0df48fb..646c83e1 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -50,7 +50,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
p->nSecLimit = 0; // time limit in seconds
p->nFramesK = 1; // the number of timeframes to use in induction
p->fRewrite = 0; // use additional rewriting to simplify timeframes
- p->fTransLoop = 1; // add transition into the init state under new PI var
+ p->fTransLoop = 0; // add transition into the init state under new PI var
p->fUsePudlak = 0; // use Pudluk interpolation procedure
p->fUseOther = 0; // use other undisclosed option
p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
@@ -78,6 +78,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
{
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
Inter_Man_t * p;
+ Inter_Check_t * pCheck = NULL;
Aig_Man_t * pAigTemp;
int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
// sanity checks
@@ -116,12 +117,14 @@ p->timeCnf += clock() - clk;
Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
p->pCnfAig->nVars, p->pCnfAig->nClauses );
}
-
+
// derive interpolant
*piFrame = -1;
p->nFrames = 1;
for ( s = 0; ; s++ )
{
+ Cnf_Dat_t * pCnfInter2;
+
clk2 = clock();
// initial state
if ( pPars->fUseBackward )
@@ -157,6 +160,23 @@ p->timeCnf += clock() - clk;
s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
ABC_PRT( "Time", clock() - clk2 );
}
+
+
+ //////////////////////////////////////////
+ // start containment checking
+ if ( !(pPars->fTransLoop || pPars->fUseBackward) )
+ {
+ pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
+ // try new containment check for the initial state
+clk = clock();
+ pCnfInter2 = Cnf_Derive( p->pInter, 1 );
+p->timeCnf += clock() - clk;
+ RetValue = Inter_CheckPerform( pCheck, pCnfInter2 );
+// assert( RetValue == 0 );
+ Cnf_DataFree( pCnfInter2 );
+ }
+ //////////////////////////////////////////
+
// iterate the interpolation procedure
for ( i = 0; ; i++ )
{
@@ -166,6 +186,7 @@ p->timeCnf += clock() - clk;
printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return -1;
}
@@ -199,6 +220,7 @@ p->timeCnf += clock() - clk;
*piFrame = p->nFrames;
pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return 0;
}
// likely spurious counter-example
@@ -213,6 +235,7 @@ p->timeCnf += clock() - clk;
assert( p->nConfCur >= p->nConfLimit );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return -1;
}
assert( RetValue == 1 ); // found new interpolant
@@ -234,6 +257,7 @@ p->timeRwr += clock() - clk;
printf( "The problem is trivially true for all states.\n" );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return 1;
}
@@ -242,7 +266,18 @@ clk = clock();
if ( pPars->fCheckKstep ) // k-step unique-state induction
{
if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
- Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+ {
+ if ( pPars->fTransLoop || pPars->fUseBackward )
+ Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+ else
+ { // new containment check
+clk2 = clock();
+ pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );
+p->timeCnf += clock() - clk2;
+ Status = Inter_CheckPerform( pCheck, pCnfInter2 );
+ Cnf_DataFree( pCnfInter2 );
+ }
+ }
else
Status = 0;
}
@@ -260,6 +295,7 @@ p->timeEqu += clock() - clk;
printf( "Proved containment of interpolants.\n" );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return 1;
}
if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
@@ -267,6 +303,7 @@ p->timeEqu += clock() - clk;
printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
p->timeTotal = clock() - clkTotal;
Inter_ManStop( p );
+ Inter_CheckStop( pCheck );
return -1;
}
// save interpolant and convert it into CNF
@@ -277,14 +314,22 @@ p->timeEqu += clock() - clk;
}
else
{
- p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
- Aig_ManStop( pAigTemp );
- Aig_ManStop( p->pInterNew );
- // compress the interpolant
+ if ( pPars->fUseBackward )
+ {
+ p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
+ Aig_ManStop( pAigTemp );
+ Aig_ManStop( p->pInterNew );
+ // compress the interpolant
clk = clock();
- p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
- Aig_ManStop( pAigTemp );
+ p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
+ Aig_ManStop( pAigTemp );
p->timeRwr += clock() - clk;
+ }
+ else // forward with the new containment checking (using only the frontier)
+ {
+ Aig_ManStop( p->pInter );
+ p->pInter = p->pInterNew;
+ }
}
p->pInterNew = NULL;
Cnf_DataFree( p->pCnfInter );
@@ -292,6 +337,9 @@ clk = clock();
p->pCnfInter = Cnf_Derive( p->pInter, 0 );
p->timeCnf += clock() - clk;
}
+
+ // start containment checking
+ Inter_CheckStop( pCheck );
}
assert( 0 );
return RetValue;
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index 72079a49..d5e8ed00 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -79,6 +79,9 @@ struct Inter_Man_t_
int timeTotal;
};
+// containment checking manager
+typedef struct Inter_Check_t_ Inter_Check_t;
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -87,38 +90,43 @@ struct Inter_Man_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== intContain.c ==========================================================*/
-extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
-extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
-extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
+/*=== intCheck.c ============================================================*/
+extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
+extern void Inter_CheckStop( Inter_Check_t * p );
+extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf );
+
+/*=== intContain.c ============================================================*/
+extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
-/*=== intCtrex.c ==========================================================*/
-extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
+/*=== intCtrex.c ============================================================*/
+extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
-/*=== intDup.c ==========================================================*/
-extern Aig_Man_t * Inter_ManStartInitState( int nRegs );
-extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p );
-extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
+/*=== intDup.c ============================================================*/
+extern Aig_Man_t * Inter_ManStartInitState( int nRegs );
+extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p );
+extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
-/*=== intFrames.c ==========================================================*/
-extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
+/*=== intFrames.c ============================================================*/
+extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
-/*=== 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 );
+/*=== 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 );
-/*=== intM114.c ==========================================================*/
-extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
+/*=== intM114.c ============================================================*/
+extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
-/*=== intM114p.c ==========================================================*/
+/*=== intM114p.c ============================================================*/
#ifdef ABC_USE_LIBRARIES
-extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
+extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
#endif
-/*=== intUtil.c ==========================================================*/
-extern int Inter_ManCheckInitialState( Aig_Man_t * p );
-extern int Inter_ManCheckAllStates( Aig_Man_t * p );
+/*=== intUtil.c ============================================================*/
+extern int Inter_ManCheckInitialState( Aig_Man_t * p );
+extern int Inter_ManCheckAllStates( Aig_Man_t * p );
diff --git a/src/aig/int/module.make b/src/aig/int/module.make
index cf0f827f..8e0e4319 100644
--- a/src/aig/int/module.make
+++ b/src/aig/int/module.make
@@ -1,4 +1,5 @@
-SRC += src/aig/int/intContain.c \
+SRC += src/aig/int/intCheck.c \
+ src/aig/int/intContain.c \
src/aig/int/intCore.c \
src/aig/int/intCtrex.c \
src/aig/int/intDup.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 12:30:08 +0000