Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

1 files changed, 89 insertions, 27 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index aa43cff0f..b2dbaf39b 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -22,10 +22,6 @@
 #include <string>
 
 #include "main/main.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
-#include "options/printer_options.h"
-#include "options/smt_options.h"
 #include "smt_util/command.h"
 
 
@@ -55,12 +51,19 @@ CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_smtEngine(new SmtEngine(&exprMgr)),
   d_options(options),
   d_stats("driver"),
-  d_result() {
+  d_result(),
+  d_replayStream(NULL)
+{}
+
+void CommandExecutor::setReplayStream(ExprStream* replayStream) {
+  assert(d_replayStream == NULL);
+  d_replayStream = replayStream;
+  d_smtEngine->setReplayStream(d_replayStream);
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if( d_options[options::parseOnly] ) {
+  if( d_options.getParseOnly() ) {
     return true;
   }
 
@@ -70,15 +73,15 @@ bool CommandExecutor::doCommand(Command* cmd)
     bool status = true;
 
     for(CommandSequence::iterator subcmd = seq->begin();
-        (status || d_options[options::continuedExecution]) && subcmd != seq->end();
+        (status || d_options.getContinuedExecution()) && subcmd != seq->end();
         ++subcmd) {
       status = doCommand(*subcmd);
     }
 
     return status;
   } else {
-    if(d_options[options::verbosity] > 2) {
-      *d_options[options::out] << "Invoking: " << *cmd << std::endl;
+    if(d_options.getVerbosity() > 2) {
+      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -87,8 +90,8 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  if(d_options[options::statistics]) {
-    flushStatistics(*d_options[options::err]);
+  if(d_options.getStatistics()) {
+    flushStatistics(*d_options.getErr());
   }
   delete d_smtEngine;
   d_smtEngine = new SmtEngine(&d_exprMgr);
@@ -97,8 +100,8 @@ void CommandExecutor::reset()
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if(d_options[options::verbosity] >= -1) {
-    status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]);
+  if(d_options.getVerbosity() >= -1) {
+    status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
   } else {
     status = smtEngineInvoke(d_smtEngine, cmd, NULL);
   }
@@ -113,42 +116,53 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if((cs != NULL || q != NULL) && d_options[options::statsEveryQuery]) {
+  if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
     flushStatistics(ossCurStats);
-    printStatsIncremental(*d_options[options::err], d_lastStatistics, ossCurStats.str());
+    std::ostream& err = *d_options.getErr();
+    printStatsIncremental(err, d_lastStatistics, ossCurStats.str());
     d_lastStatistics = ossCurStats.str();
   }
 
   // dump the model/proof/unsat core if option is set
   if(status) {
     Command* g = NULL;
-    if( d_options[options::produceModels] &&
-        d_options[options::dumpModels] &&
+    if( d_options.getProduceModels() &&
+        d_options.getDumpModels() &&
         ( res.asSatisfiabilityResult() == Result::SAT ||
           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
       g = new GetModelCommand();
     }
-    if( d_options[options::proof] &&
-        d_options[options::dumpProofs] &&
+    if( d_options.getProof() &&
+        d_options.getDumpProofs() &&
         res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetProofCommand();
     }
-    if( d_options[options::dumpInstantiations] &&
-        ( ( d_options[options::instFormatMode] != INST_FORMAT_MODE_SZS &&
-            ( res.asSatisfiabilityResult() == Result::SAT || (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
-          res.asSatisfiabilityResult() == Result::UNSAT ) ) {
+
+    if( d_options.getDumpInstantiations() &&
+        ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
+            ( res.asSatisfiabilityResult() == Result::SAT ||
+              (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
+          res.asSatisfiabilityResult() == Result::UNSAT ) )
+    {
       g = new GetInstantiationsCommand();
     }
-    if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){
+
+    if( d_options.getDumpSynth() &&
+        res.asSatisfiabilityResult() == Result::UNSAT )
+    {
       g = new GetSynthSolutionCommand();
     }
-    if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) {
+
+    if( d_options.getDumpUnsatCores() &&
+        res.asSatisfiabilityResult() == Result::UNSAT )
+    {
       g = new GetUnsatCoreCommand();
     }
+
     if(g != NULL) {
       // set no time limit during dumping if applicable
-      if( d_options[options::forceNoLimitCpuWhileDump] ){
+      if( d_options.getForceNoLimitCpuWhileDump() ){
         setNoLimitCPU();
       }
       status = doCommandSingleton(g);
@@ -165,7 +179,9 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
     cmd->invoke(smt, *out);
   }
   // ignore the error if the command-verbosity is 0 for this command
-  if(smt->getOption(std::string("command-verbosity:") + cmd->getCommandName()).getIntegerValue() == 0) {
+  std::string commandName =
+      std::string("command-verbosity:") + cmd->getCommandName();
+  if(smt->getOption(commandName).getIntegerValue() == 0) {
     return true;
   }
   return !cmd->fail();
@@ -223,5 +239,51 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
   }
 }
 
+void CommandExecutor::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, ',');
+  }
+
+}
+
+void CommandExecutor::flushOutputStreams() {
+  if(d_options.getStatistics()) {
+    if(d_options.getStatsHideZeros() == false) {
+      flushStatistics(*(d_options.getErr()));
+    } else {
+      std::ostringstream ossStats;
+      flushStatistics(ossStats);
+      printStatsFilterZeros(*(d_options.getErr()), ossStats.str());
+    }
+  }
+
+  // make sure out and err streams are flushed too
+  d_options.flushOut();
+  d_options.flushErr();
+}
+
 }/* CVC4::main namespace */
 }/* CVC4 namespace */