summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaAbsVta.c25
-rw-r--r--src/base/abci/abc.c16
3 files changed, 36 insertions, 6 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3a0fb150..803fff51 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -206,6 +206,7 @@ struct Gia_ParVta_t_
int nFramesOver; // overlap frames
int nConfLimit; // conflict limit
int nTimeOut; // timeout in seconds
+ int nRatioMin; // stop when less than this % of object is abstracted
int fUseTermVars; // use terminal variables
int fVerbose; // verbose flag
int iFrame; // the number of frames covered
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 21e31cd2..09ed91ab 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -146,10 +146,11 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesStart = 5; // starting frame
- p->nFramesOver = 2; // overlap frames
+ p->nFramesOver = 4; // overlap frames
p->nFramesMax = 0; // maximum 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->fVerbose = 0; // verbose flag
p->iFrame = -1; // the number of frames covered
@@ -647,6 +648,7 @@ void Vta_ManSatVerify( Vta_Man_t * p )
***********************************************************************/
Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
{
+ int fVerify = 0;
Abc_Cex_t * pCex = NULL;
Vec_Int_t * vOrder, * vTermsToAdd;
Vec_Ptr_t * vTermsUsed, * vTermsUnused;
@@ -654,6 +656,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
Gia_Obj_t * pObj;
int i, Counter;
+ if ( fVerify )
Vta_ManSatVerify( p );
// collect nodes in a topological order
@@ -666,6 +669,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
}
// verify
+ if ( fVerify )
Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
{
if ( !pThis->fAdded )
@@ -884,6 +888,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
}
+ if ( fVerify )
+ {
// verify
Vta_ManForEachObjVec( vOrder, p, pThis, i )
pThis->Value = VTA_VARX;
@@ -948,6 +954,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
// else
// printf( "Verification OK.\n" );
+ }
// produce true counter-example
@@ -1400,8 +1407,10 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// perform initial abstraction
if ( p->pPars->fVerbose )
{
- printf( "Running VTA with FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d.\n",
- p->pPars->nFramesStart, p->pPars->nFramesOver, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut );
+ 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->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
printf( "Frame Abs Confl Cex Core F0 F1 F2 F3 ...\n" );
}
for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
@@ -1489,6 +1498,12 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// print the result
if ( p->pPars->fVerbose )
Vta_ManAbsPrintFrame( p, vCore, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
+ // chech if the number of objects is below limit
+ if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
+ {
+ Status = -1;
+ break;
+ }
}
finish:
// analize the results
@@ -1505,8 +1520,10 @@ finish:
printf( "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
printf( "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
+ else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
+ printf( "Percentage of abstracted objects is less than %d in frame %d. ", pPars->nRatioMin, f );
else
- printf( "SAT solver ran out of resources in frame %d. ", f );
+ printf( "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
printf( "SAT solver completed %d frames and produced an abstraction. ", f );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 477adf06..6b8f117b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26711,7 +26711,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTtvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFPCTRtvh" ) ) != EOF )
{
switch ( c )
{
@@ -26770,6 +26770,17 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 0 )
goto usage;
break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nRatioMin = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nRatioMin < 0 )
+ goto usage;
+ break;
case 't':
pPars->fUseTermVars ^= 1;
break;
@@ -26813,13 +26824,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &vta [-SFPCT num] [-tvh]\n" );
+ Abc_Print( -2, "usage: &vta [-SFPCTR 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-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 );
Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 19:20:56 +0000