diff options
| -rw-r--r-- | src/expr/options | 5 | ||||
| -rw-r--r-- | src/main/driver_unified.cpp | 37 | ||||
| -rw-r--r-- | src/options/base_options | 5 |
3 files changed, 46 insertions, 1 deletions
diff --git a/src/expr/options b/src/expr/options index cf893a7a5..ee4d40b2c 100644 --- a/src/expr/options +++ b/src/expr/options @@ -7,8 +7,13 @@ module EXPR "expr/options.h" Expression package option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h" print exprs to depth N (0 == default, -1 == no limit) +undocumented-alias --expr-depth = --default-expr-depth + option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h" dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) +undocumented-alias --dag-thresh = --default-dag-thresh +undocumented-alias --dag-threshold = --default-dag-thresh + option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h" print types with variables when printing exprs 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 diff --git a/src/options/base_options b/src/options/base_options index f3ba38a6a..ed94e68f6 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -111,6 +111,11 @@ option statsEveryQuery --stats-every-query bool :default false :link --stats in incremental mode, print stats after every satisfiability or validity query undocumented-alias --statistics-every-query = --stats-every-query undocumented-alias --no-statistics-every-query = --no-stats-every-query +option statsHideZeros --stats-hide-zeros/--stats-show-zeros bool :default false + hide statistics which are zero +/show statistics even when they are zero (default) +undocumented-alias --hide-zero-stats = --stats-hide-zeros +undocumented-alias --show-zero-stats = --stats-show-zeros option parseOnly parse-only --parse-only bool :read-write exit after parsing input |