diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-05 20:35:15 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:45:38 -0400 |
commit | d9391910e499d03b5a01345b572dc89c930bdb51 (patch) | |
tree | 8ef4793014f2f7ef88b3cc154297c7bce584582b /src/main/driver_unified.cpp | |
parent | 5c42662fe5cea3051341c8292202357e2a5e7dd3 (diff) |
option to hide stats which are zero (off by default), also some aliases
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 37 |
1 files changed, 36 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 60b99132d..4c33088d4 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -85,6 +85,35 @@ void printUsage(Options& opts, bool full) { } } +void printStatsFilterZeros(std::ostream& out, const std::string& statsString) { + // read each line, if a number, check zero and skip if so + // Stat are assumed to one-per line: "<statName>, <statValue>" + + std::istringstream iss(statsString); + std::string statName, statValue; + + std::getline(iss, statName, ','); + + while( !iss.eof() ) { + + std::getline(iss, statValue, '\n'); + + double curFloat; + bool isFloat = (std::istringstream(statValue) >> curFloat); + + if( (isFloat && curFloat == 0) || + statValue == " \"0\"" || + statValue == " \"[]\"") { + // skip + } else { + out << statName << "," << statValue << std::endl; + } + + std::getline(iss, statName, ','); + } + +} + int runCvc4(int argc, char* argv[], Options& opts) { // Timer statistic @@ -419,7 +448,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Set the global executor pointer to NULL first. If we get a // signal while dumping statistics, we don't want to try again. if(opts[options::statistics]) { - pExecutor->flushStatistics(*opts[options::err]); + if(opts[options::statsHideZeros] == false) { + pExecutor->flushStatistics(*opts[options::err]); + } else { + std::ostringstream ossStats; + pExecutor->flushStatistics(ossStats); + printStatsFilterZeros(*opts[options::err], ossStats.str()); + } } // make sure to flush replay output log before early-exit |