diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-06 16:54:06 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 16:54:06 -0800 |
commit | c6b2e085d4eb2c232a528a96e13fc7b65fd98fea (patch) | |
tree | 632708f158acc6a3b5b3201212fa2ba1a0606c30 /src/main | |
parent | 612bb0013f180a7d414f0a4b1e770aaa7ed09152 (diff) |
Make statistics output consistent. (#1647)
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index a7666dfcf..94c0c9e23 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -260,26 +260,29 @@ void CommandExecutor::printStatsFilterZeros(std::ostream& out, std::getline(iss, statName, ','); - while( !iss.eof() ) { - + while (!iss.eof()) + { std::getline(iss, statValue, '\n'); - double curFloat; - std::istringstream iss_stat_value (statValue); - iss_stat_value >> curFloat; - bool isFloat = iss_stat_value.good(); + bool skip = false; + try + { + double dval = std::stod(statValue); + skip = (dval == 0.0); + } + // Value can not be converted, don't skip + catch (const std::invalid_argument&) {} + catch (const std::out_of_range&) {} - if( (isFloat && curFloat == 0) || - statValue == " \"0\"" || - statValue == " \"[]\"") { - // skip - } else { + skip = skip || (statValue == " \"0\"" || statValue == " \"[]\""); + + if (!skip) + { out << statName << "," << statValue << std::endl; } std::getline(iss, statName, ','); } - } void CommandExecutor::flushOutputStreams() { |