option to hide stats which are zero (off by default), also some aliases

diff --git a/src/expr/options b/src/expr/options
index cf893a7a54f9cee345243022372f39b4f8f1f5b3..ee4d40b2cf3befb12e0fc5c0f50cd8c1814f9615 100644 (file)
--- 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 60b99132daa182872a5417cdd7eb57245d0a4a75..4c33088d436dba035c998aa0406f324c27f3c54c 100644 (file)
--- 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 f3ba38a6a4b5f2ea51b40492c0dc9fa36961abf4..ed94e68f6f659e9a8a3752b7f83cf3fc37306c86 100644 (file)
--- 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