summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigInd.c14
-rw-r--r--src/base/abci/abc.c26
-rw-r--r--src/base/abci/abcDar.c4
4 files changed, 33 insertions, 13 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 89622491..475f476d 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -131,7 +131,7 @@ extern Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPo
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigInd.c ==========================================================*/
-extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
+extern int Saig_ManInduction( Aig_Man_t * p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index 114db997..c7b50461 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -142,7 +142,7 @@ void Saig_ManAddUniqueness( sat_solver * pSat, Vec_Int_t * vState, int nRegs, in
SeeAlso []
***********************************************************************/
-int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
+int Saig_ManInduction( Aig_Man_t * p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
{
sat_solver * pSat;
Aig_Man_t * pAigPart;
@@ -152,7 +152,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
- abctime clk;
+ abctime clk, nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
assert( fUnique == 0 || fUniqueAll == 0 );
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetCioIds( p );
@@ -168,6 +168,10 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
pSat = sat_solver_new();
sat_solver_setnvars( pSat, 1000 );
+ // set runtime limit
+ if ( nTimeToStop )
+ sat_solver_set_runtime_limit( pSat, nTimeToStop );
+
// iterate backward unrolling
RetValue = -1;
nSatVarNum = 0;
@@ -312,7 +316,7 @@ nextrun:
}
printf( "\n" );
}
- if ( f == nFramesMax - 1 )
+ if ( nFramesMax && f == nFramesMax - 1 )
{
// derive counter-example
assert( status == l_True );
@@ -357,7 +361,9 @@ nextrun:
}
if ( fVerbose )
{
- if ( status == l_Undef )
+ if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
+ printf( "Timeout (%d sec) was reached during iteration %d.\n", nTimeOut, f+1 );
+ else if ( status == l_Undef )
printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 );
else if ( fUnique || fUniqueAll )
printf( "Completed %d interations and added %d uniqueness constraints.\n", f+1, nConstrs );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3d593d2e..cdd391e2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22492,6 +22492,7 @@ usage:
int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ int nTimeOut;
int nFramesMax;
int nConfMax;
int fUnique;
@@ -22500,17 +22501,18 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int fVeryVerbose;
int c;
- extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
+ extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
// set defaults
- nFramesMax = 100;
- nConfMax = 1000;
+ nTimeOut = 0;
+ nFramesMax = 0;
+ nConfMax = 0;
fUnique = 0;
fUniqueAll = 0;
fGetCex = 0;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FCuaxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCTuaxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -22536,6 +22538,17 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nTimeOut = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nTimeOut < 0 )
+ goto usage;
+ break;
case 'u':
fUnique ^= 1;
break;
@@ -22584,7 +22597,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
+ pAbc->Status = Abc_NtkDarInduction( pNtk, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
if ( fGetCex )
{
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
@@ -22592,10 +22605,11 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
return 0;
usage:
- Abc_Print( -2, "usage: ind [-FC num] [-uaxvwh]\n" );
+ Abc_Print( -2, "usage: ind [-FCT num] [-uaxvwh]\n" );
Abc_Print( -2, "\t runs the inductive case of the K-step induction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+ Abc_Print( -2, "\t-T num : the limit on runtime per output in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-u : toggle adding uniqueness constraints on demand [default = %s]\n", fUnique? "yes": "no" );
Abc_Print( -2, "\t-a : toggle adding uniqueness constraints always [default = %s]\n", fUniqueAll? "yes": "no" );
Abc_Print( -2, "\t-x : toggle returning CEX to induction for the top frame [default = %s]\n", fGetCex? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 552b124c..04b104e5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3451,7 +3451,7 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC
SeeAlso []
***********************************************************************/
-int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
abctime clkTotal = Abc_Clock();
@@ -3459,7 +3459,7 @@ int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUn
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return -1;
- RetValue = Saig_ManInduction( pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
+ RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 22:16:44 +0000