summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-02-11 22:30:04 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-02-11 22:30:04 -0800
commit49c5beefd40fc8047a07778fca26c8aea7d280f6 (patch)
tree984226c11ba7bac3670325b7937054bb17c20254 /src
parent95d7b478fda5d56125469b874ce67b7adc56d791 (diff)
downloadabc-49c5beefd40fc8047a07778fca26c8aea7d280f6.tar.gz
abc-49c5beefd40fc8047a07778fca26c8aea7d280f6.tar.bz2
abc-49c5beefd40fc8047a07778fca26c8aea7d280f6.zip
Variable timeframe abstraction.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h4
-rw-r--r--src/aig/gia/giaAbsVta.c10
-rw-r--r--src/base/abci/abc.c28
3 files changed, 21 insertions, 21 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 803fff51..1069f5d2 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -201,9 +201,9 @@ struct Gia_ParSim_t_
typedef struct Gia_ParVta_t_ Gia_ParVta_t;
struct Gia_ParVta_t_
{
- int nFramesStart; // starting frame
int nFramesMax; // maximum frames
- int nFramesOver; // overlap frames
+ int nFramesStart; // starting frame
+ int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 09ed91ab..d406b3ce 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -145,13 +145,13 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
- p->nFramesStart = 5; // starting frame
- p->nFramesOver = 4; // overlap frames
p->nFramesMax = 0; // maximum frames
+ p->nFramesStart = 5; // starting frame
+ p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
- p->fUseTermVars = 0; // use terminal variables
+ p->fUseTermVars = 1; // use terminal variables
p->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
}
@@ -1409,7 +1409,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
printf( "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
printf( "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
- p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax,
+ p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
printf( "Frame Abs Confl Cex Core F0 F1 F2 F3 ...\n" );
}
@@ -1435,7 +1435,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load the time frame
- for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
+ for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6b8f117b..17c57966 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26711,30 +26711,30 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTRtvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCTRtvh" ) ) != EOF )
{
switch ( c )
{
- case 'S':
+ case 'F':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- pPars->nFramesStart = atoi(argv[globalUtilOptind]);
+ pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( pPars->nFramesStart < 0 )
+ if ( pPars->nFramesMax < 0 )
goto usage;
break;
- case 'F':
+ case 'S':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
- pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+ pPars->nFramesStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( pPars->nFramesMax < 0 )
+ if ( pPars->nFramesStart < 0 )
goto usage;
break;
case 'P':
@@ -26743,9 +26743,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
- pPars->nFramesOver = atoi(argv[globalUtilOptind]);
+ pPars->nFramesPast = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( pPars->nFramesOver < 0 )
+ if ( pPars->nFramesPast < 0 )
goto usage;
break;
case 'C':
@@ -26824,11 +26824,11 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &vta [-SFPCTR num] [-tvh]\n" );
+ Abc_Print( -2, "usage: &vta [-FSPCTR num] [-tvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
- Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
- Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesOver );
+ Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
+ Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-R num : stop when less than this %% of object is abstracted (0<=num<=100) [default = %d]\n", pPars->nRatioMin );