summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/int/intCore.c66
-rw-r--r--src/aig/int/intInt.h54
-rw-r--r--src/aig/int/module.make3
-rw-r--r--src/base/abci/abc.c21
4 files changed, 104 insertions, 40 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 \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9860528..733e2722 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8427,6 +8427,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
extern void Bbl_ManSimpleDemo();
extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
+ extern void Abc_NktMffcTest( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -8489,13 +8490,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Empty network.\n" );
return 1;
}
+/*
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
Abc_Print( -1, "Only works for sequential networks.\n" );
return 1;
}
-
- Abc_NtkDarTest( pNtk, nLevels );
+*/
+// if ( fBmc )
+// Abc_NtkBddDec( pNtk, 1 );
+// else
+// Abc_NktMffcTest( pNtk );
+// Abc_NtkDarTest( pNtk, nLevels );
// Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk );
@@ -18603,7 +18609,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, "CFTNLrtpomcgbkdvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbkdvh" ) ) != EOF )
{
switch ( c )
{
@@ -18640,7 +18646,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nSecLimit < 0 )
goto usage;
break;
- case 'N':
+ case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
@@ -18760,12 +18766,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: int [-CFTN num] [-L file] [-rtpomcgbkdvh]\n" );
+ Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdvh]\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 );
Abc_Print( -2, "\t-T num : the limit on runtime per output in seconds [default = %d]\n", pPars->nSecLimit );
- Abc_Print( -2, "\t-N num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
+ Abc_Print( -2, "\t-K num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
+ Abc_Print( -2, "\t (K = 1 works in all cases; K > 1 works without -t and -b)\n" );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-r : toggle rewriting of the unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" );
Abc_Print( -2, "\t-t : toggle adding transition into the initial state [default = %s]\n", pPars->fTransLoop? "yes": "no" );
@@ -18774,7 +18781,7 @@ usage:
Abc_Print( -2, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
- Abc_Print( -2, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+ 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-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 12:28:43 +0000