Add SmtGlobals Class

- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

6 files changed, 238 insertions, 29 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c1d49d8c8..3571ae0cb 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -724,7 +724,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_private(NULL),
   d_smtAttributes(NULL),
   d_statisticsRegistry(NULL),
-  d_stats(NULL) {
+  d_stats(NULL),
+  d_globals(new SmtGlobals())
+{
 
   SmtScope smts(this);
   d_smtAttributes = new expr::attr::SmtAttributes(d_context);
@@ -734,7 +736,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed);
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
+  d_theoryEngine = new TheoryEngine(d_context, d_userContext,
+                                    d_private->d_iteRemover,
+                                    const_cast<const LogicInfo&>(d_logic),
+                                    d_globals);
 
   // Add the theories
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
@@ -764,7 +769,8 @@ void SmtEngine::finishInit() {
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_decisionEngine->init();   // enable appropriate strategies
 
-  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext);
+  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
+                                d_userContext, d_globals);
 
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
@@ -907,6 +913,9 @@ SmtEngine::~SmtEngine() throw() {
     delete d_context;
     d_context = NULL;
 
+    delete d_globals;
+    d_globals = NULL;
+
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c94646c40..3f049e392 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,15 +28,16 @@
 #include "context/cdlist_forward.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "expr/result.h"
 #include "expr/sexpr.h"
 #include "expr/statistics.h"
 #include "options/options.h"
 #include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
+#include "smt/smt_globals.h"
 #include "theory/logic_info.h"
 #include "util/hash.h"
 #include "util/proof.h"
+#include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
@@ -385,6 +386,8 @@ class CVC4_PUBLIC SmtEngine {
 
   smt::SmtEngineStatistics* d_stats;
 
+  SmtGlobals* d_globals;
+
   /**
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
@@ -729,6 +732,8 @@ public:
    * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized.
    */
   static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException);
+
+  SmtGlobals* globals() { return d_globals; }
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_globals.cpp b/src/smt/smt_globals.cpp
new file mode 100644
index 000000000..4c1b0dc72
--- /dev/null
+++ b/src/smt/smt_globals.cpp
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \file smt_globals.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This class is a light container for globals that used to live
+ ** in options. This is NOT a good long term solution, but is a reasonable
+ ** stop gap.
+ **
+ ** This class is a light container for globals that used to live
+ ** in options. This is NOT a good long term solution, but is a reasonable
+ ** stop gap.
+ **/
+
+#include "smt/smt_globals.h"
+
+#include <cerrno>
+#include <iostream>
+#include <string>
+#include <utility>
+
+#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY
+#include "expr/expr_stream.h"
+#include "options/option_exception.h"
+#include "options/parser_options.h"
+#include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
+#include "smt/smt_options_handler.h"
+
+namespace CVC4 {
+
+SmtGlobals::SmtGlobals()
+    : d_gcReplayLog(false)
+    , d_replayLog(NULL)
+    , d_replayStream(NULL)
+    , d_lemmaInputChannel(NULL)
+    , d_lemmaOutputChannel(NULL)
+{}
+
+SmtGlobals::~SmtGlobals(){
+  if(d_gcReplayLog){
+    delete d_replayLog;
+    d_gcReplayLog = false;
+    d_replayLog = NULL;
+  }
+}
+
+void SmtGlobals::setReplayLog(std::ostream* log){
+  d_replayLog = log;
+}
+
+void SmtGlobals::setReplayStream(ExprStream* stream) {
+  d_replayStream = stream;
+}
+
+void SmtGlobals::setLemmaInputChannel(LemmaInputChannel* in) {
+  d_lemmaInputChannel = in;
+}
+
+void SmtGlobals::setLemmaOutputChannel(LemmaOutputChannel* out) {
+  d_lemmaOutputChannel = out;
+}
+
+void SmtGlobals::parseReplayLog(std::string optarg) throw (OptionException) {
+  if(d_gcReplayLog){
+    delete d_replayLog;
+    d_gcReplayLog = false;
+    d_replayLog = NULL;
+  }
+
+  std::pair<bool, std::ostream*> checkResult = checkReplayLogFilename(optarg);
+  d_gcReplayLog = checkResult.first;
+  d_replayLog = checkResult.second;
+}
+
+#warning "TODO: Move checkReplayLogFilename back into options and has calling setReplayLog as a side effect."
+std::pair<bool, std::ostream*> SmtGlobals::checkReplayLogFilename(std::string optarg)
+    throw (OptionException)
+{
+#ifdef CVC4_REPLAY
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --replay-log"));
+  } else if(optarg == "-") {
+    return std::make_pair(false, &std::cout);
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
+  } else {
+    errno = 0;
+    std::ios_base::openmode out_trunc = std::ofstream::out | std::ofstream::trunc;
+    std::ostream* replayLog = new std::ofstream(optarg.c_str(), out_trunc);
+    if(replayLog == NULL || !*replayLog) {
+      std::stringstream ss;
+      ss << "Cannot open replay-log file: `" << optarg << "': "
+         << smt::SmtOptionsHandler::__cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
+    return std::make_pair(true, replayLog);
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+
+} /* namespace CVC4 */
diff --git a/src/smt/smt_globals.h b/src/smt/smt_globals.h
new file mode 100644
index 000000000..00b90a703
--- /dev/null
+++ b/src/smt/smt_globals.h
@@ -0,0 +1,106 @@
+/*********************                                                        */
+/*! \file smt_globals.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SmtGlobals is a light container for psuedo-global datastructures
+ ** that are set by the user.
+ **
+ ** SmtGlobals is a light container for psuedo-global datastructures
+ ** that are set by the user. These contain paramaters for infrequently
+ ** used modes: Portfolio and Replay. There should be exactly one of these
+ ** per SmtEngine with the same lifetime as the SmtEngine.
+ ** A user directly passes these as pointers and is resonsible for cleaning up
+ ** the memory.
+ **
+ ** Basically, the problem this class is solving is that previously these were
+ ** using smt_options.h and the Options class as globals for these same
+ ** datastructures.
+ **
+ ** This class is NOT a good long term solution, but is a reasonable stop gap.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SMT_GLOBALS_H
+#define __CVC4__SMT__SMT_GLOBALS_H
+
+#include <iosfwd>
+#include <string>
+#include <utility>
+
+#include "expr/expr_stream.h"
+#include "options/option_exception.h"
+#include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
+
+namespace CVC4 {
+
+/**
+ * SmtGlobals is a wrapper around 4 pointers:
+ * - getReplayLog()
+ * - getReplayStream()
+ * - getLemmaInputChannel()
+ * - getLemmaOutputChannel()
+ *
+ * The user can directly set these and is responsible for handling the
+ * memory for these. These datastructures are used for the Replay and Portfolio
+ * modes.
+ */
+class CVC4_PUBLIC SmtGlobals {
+ public:
+  /** Creates an empty SmtGlobals with all 4 pointers initially NULL. */
+  SmtGlobals();
+  ~SmtGlobals();
+
+  /** This setsReplayLog based on --replay-log */
+  void parseReplayLog(std::string optarg) throw (OptionException);
+  void setReplayLog(std::ostream*);
+  std::ostream* getReplayLog() { return d_replayLog; }
+
+  void setReplayStream(ExprStream* stream);
+  ExprStream* getReplayStream() { return d_replayStream; }
+
+  void setLemmaInputChannel(LemmaInputChannel* in);
+  LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
+
+  void setLemmaOutputChannel(LemmaOutputChannel* out);
+  LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
+
+ private:
+  // Disable copy constructor.
+  SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED;
+
+  // Disable assignment operator.
+  SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED;
+
+  static std::pair<bool, std::ostream*>
+      checkReplayLogFilename(std::string optarg) throw (OptionException);
+
+  /**
+   * d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog.
+   */
+  bool d_gcReplayLog;
+
+  /** This captures the old options::replayLog .*/
+  std::ostream* d_replayLog;
+
+  /** This captures the old options::replayStream .*/
+  ExprStream* d_replayStream;
+
+  /** This captures the old options::lemmaInputChannel .*/
+  LemmaInputChannel* d_lemmaInputChannel;
+
+  /** This captures the old options::lemmaOutputChannel .*/
+  LemmaOutputChannel* d_lemmaOutputChannel;
+}; /* class SmtGlobals */
+
+} /* namespace CVC4 */
+
+#endif /* __CVC4__SMT__SMT_GLOBALS_H */
diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp
index e1a19d48b..147a53368 100644
--- a/src/smt/smt_options_handler.cpp
+++ b/src/smt/smt_options_handler.cpp
@@ -1308,7 +1308,7 @@ void SmtOptionsHandler::setDiagnosticOutputChannel(std::string option, std::stri
 std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
 #ifdef CVC4_REPLAY
   if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --replay"));
+    throw OptionException (std::string("Bad file name for --replay"));
   } else {
     return optarg;
   }
@@ -1317,28 +1317,6 @@ std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::stri
 #endif /* CVC4_REPLAY */
 }
 
-std::ostream* SmtOptionsHandler::checkReplayLogFilename(std::string option, std::string optarg) {
-#ifdef CVC4_REPLAY
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --replay-log"));
-  } else if(optarg == "-") {
-    return &std::cout;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(replayLog == NULL || !*replayLog) {
-      std::stringstream ss;
-      ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-    return replayLog;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
 
 void SmtOptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) {
 #ifndef CVC4_STATISTICS_ON
diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h
index c4d27a722..f8e2ac155 100644
--- a/src/smt/smt_options_handler.h
+++ b/src/smt/smt_options_handler.h
@@ -124,7 +124,6 @@ public:
   virtual void setRegularOutputChannel(std::string option, std::string optarg);
   virtual void setDiagnosticOutputChannel(std::string option, std::string optarg);
   virtual std::string checkReplayFilename(std::string option, std::string optarg);
-  virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg);
   virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException);
   virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException);
   virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
@@ -152,13 +151,14 @@ public:
   virtual void addDebugTag(std::string option, std::string optarg);
   virtual void setPrintSuccess(std::string option, bool value);
 
+  static std::string __cvc4_errno_failreason();
+
 private:
   SmtEngine* d_smtEngine;
 
   /* Helper utilities */
   static std::string suggestTags(char const* const* validTags, std::string inputTag,
                                  char const* const* additionalTags = NULL);
-  static std::string __cvc4_errno_failreason();
 
   /* Help strings */
   static const std::string s_bitblastingModeHelp;