--stats-every-query option: print increment in addition to cumulative value of each...

the increment is printed in parantheses at the end, e.g.
sat::decisions, 100 (50)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 601359cea015505ce485c99f5789a8d481821ed1..34b484910252a40b2fa376953f84701b7dc09bf7 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -19,12 +19,13 @@
 
 #include "main/main.h"
 
-#include "main/options.h"
 #include "smt/options.h"
 
 namespace CVC4 {
 namespace main {
 
+void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
+
 CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_exprMgr(exprMgr),
   d_smtEngine(SmtEngine(&exprMgr)),
@@ -68,6 +69,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
+
   Result res;
   CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
   if(cs != NULL) {
@@ -77,9 +79,14 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(q != NULL) {
     d_result = res = q->getResult();
   }
+
   if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) {
-    flushStatistics(*d_options[options::err]);
+    std::ostringstream ossCurStats;
+    flushStatistics(ossCurStats);
+    printStatsIncremental(*d_options[options::err], d_lastStatistics, ossCurStats.str());
+    d_lastStatistics = ossCurStats.str();
   }
+
   // dump the model/proof if option is set
   if(status) {
     if( d_options[options::produceModels] &&
@@ -108,5 +115,57 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
   return !cmd->fail();
 }
 
+void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString) {
+  if(prvsStatsString == "") {
+      out << curStatsString;
+      return;
+  }
+
+  // read each line
+  // if a number, subtract and add that to parantheses
+  std::istringstream issPrvs(prvsStatsString);
+  std::istringstream issCur(curStatsString);
+
+  std::string prvsStatName, prvsStatValue, curStatName, curStatValue;
+
+  std::getline(issPrvs, prvsStatName, ',');
+  std::getline(issCur, curStatName, ',');
+
+  /**
+   * Stat are assumed to one-per line: "<statName>, <statValue>"
+   *   e.g. "sat::decisions, 100"
+   * Output is of the form: "<statName>, <statValue> (<statDiffFromPrvs>)"
+   *   e.g. "sat::decisions, 100 (20)"
+   * If the value is not numeric, no change is made.
+   */
+  while( !issCur.eof() ) {
+
+    std::getline(issCur, curStatValue, '\n');
+
+    if(curStatName == prvsStatName) {
+      std::getline(issPrvs, prvsStatValue, '\n');
+
+      double prvsFloat, curFloat;
+      bool isFloat =
+        (std::istringstream(prvsStatValue) >> prvsFloat) &&
+        (std::istringstream(curStatValue) >> curFloat);
+
+      if(isFloat) {
+        out << curStatName << ", " << curStatValue << " "
+            << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")"
+            << std::endl;
+      } else {
+        out << curStatName << ", " << curStatValue << std::endl;
+      }
+
+      std::getline(issPrvs, prvsStatName, ',');
+    } else {
+      out << curStatName << ", " << curStatValue << std::endl;
+    }
+
+    std::getline(issCur, curStatName, ',');
+  }
+}
+
 }/* CVC4::main namespace */
 }/* CVC4 namespace */

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index cbc71b07533787ddb236e16866c8b3320866f471..5395cc804031f34202dc362542d5200dd68ef396 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -28,6 +28,8 @@ namespace CVC4 {
 namespace main {
 
 class CommandExecutor {
+private:
+  std::string d_lastStatistics;
 
 protected:
   ExprManager& d_exprMgr;

diff --git a/src/main/options b/src/main/options
index 13f4d18edc541cdc3f58ec3f0c88903cb9426266..35e3df7d293e465cc160209def0086385a470516 100644 (file)
--- a/src/main/options
+++ b/src/main/options
@@ -22,8 +22,6 @@ option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-incl
 
 expert-option earlyExit --early-exit bool :default true
  do not run destructors at exit; default on except in debug builds
-expert-option statsEveryQuery --stats-every-query bool :default false
- print stats after every satisfiability or validity query
 
 # portfolio options
 option threads --threads=N unsigned :default 2 :predicate greater(0)

diff --git a/src/options/base_options b/src/options/base_options
index a6f24c7f35c39eca9e6c81942c243eb8510fae1b..dd4da0f31f3be6a949a5ad9e1ef62508f8293a26 100644 (file)
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -107,6 +107,10 @@ common-option statistics statistics --stats bool :predicate CVC4::smt::statsEnab
  give statistics on exit
 undocumented-alias --statistics = --stats
 undocumented-alias --no-statistics = --no-stats
+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 parseOnly parse-only --parse-only bool :read-write
  exit after parsing input