Skip to content

A
abc
Commit 937979d9 by Alan Mishchenko
Options

Improvements to the interpolation command 'int'; change of default switch -t.

parent eabc42a2
Showing with 104 additions and 40 deletions
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;
......
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 );
......
src/aig/int/module.make
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 \
......
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" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment