1 files changed, 106 insertions, 0 deletions
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 */