summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-02-11 22:54:59 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-02-11 22:54:59 -0800
commit862ebb214d2009edf70e54ff795fe97ccd967449 (patch)
tree5c4ce97993e00e7045d8550fb323f6342ec5c751
parent49c5beefd40fc8047a07778fca26c8aea7d280f6 (diff)
downloadabc-862ebb214d2009edf70e54ff795fe97ccd967449.tar.gz
abc-862ebb214d2009edf70e54ff795fe97ccd967449.tar.bz2
abc-862ebb214d2009edf70e54ff795fe97ccd967449.zip
Variable timeframe abstraction.
-rw-r--r--src/aig/gia/giaAbsVta.c4
-rw-r--r--src/base/abci/abc.c2
2 files changed, 4 insertions, 2 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index d406b3ce..764f5d30 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1521,7 +1521,7 @@ finish:
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 );
+ printf( "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
printf( "Abstraction stopped for unknown reason in frame %d. ", f );
}
@@ -1546,6 +1546,8 @@ finish:
ABC_PRTP( "TOTAL ", clock() - clk, clock() - clk );
Vga_ManStop( p );
+
+ fflush( stdout );
return RetValue;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 17c57966..8ae4e467 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26831,7 +26831,7 @@ usage:
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 );
+ Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (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");