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, 122 insertions, 0 deletions

diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
new file mode 100644
index 000000000..9e0100786
--- /dev/null
+++ b/src/smt/update_ostream.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file update_ostream.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-2016  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UPDATE_OSTREAM_H
+#define __CVC4__UPDATE_OSTREAM_H
+
+#include <ostream>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "expr/expr_iomanip.h"
+#include "options/language.h"
+#include "options/set_language.h"
+#include "options/base_options.h"
+#include "smt_util/dump.h"
+
+namespace CVC4 {
+
+class ChannelSettings {
+ public:
+  ChannelSettings(std::ostream& out)
+      : d_dagSetting(expr::ExprDag::getDag(out)),
+        d_exprDepthSetting(expr::ExprSetDepth::getDepth(out)),
+        d_printtypesSetting(expr::ExprPrintTypes::getPrintTypes(out)),
+        d_languageSetting(language::SetLanguage::getLanguage(out))
+  {}
+
+  void apply(std::ostream& out) {
+    out << expr::ExprDag(d_dagSetting);
+    out << expr::ExprSetDepth(d_exprDepthSetting);
+    out << expr::ExprPrintTypes(d_printtypesSetting);
+    out << language::SetLanguage(d_languageSetting);
+  }
+
+ private:
+  const int d_dagSetting;
+  const size_t d_exprDepthSetting;
+  const bool d_printtypesSetting;
+  const OutputLanguage d_languageSetting;
+}; /* class ChannelSettings */
+
+class OstreamUpdate {
+public:
+  virtual std::ostream& get() = 0;
+  virtual void set(std::ostream* setTo) = 0;
+
+  void apply(std::ostream* setTo) {
+    PrettyCheckArgument(setTo != NULL, setTo);
+
+    ChannelSettings initialSettings(get());
+    set(setTo);
+    initialSettings.apply(get());
+  }
+}; /* class OstreamUpdate */
+
+class OptionsErrOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return *(options::err()); }
+  virtual void set(std::ostream* setTo) { return options::err.set(setTo); }
+};  /* class OptionsErrOstreamUpdate */
+
+class DumpOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Dump.getStream(); }
+  virtual void set(std::ostream* setTo) { Dump.setStream(setTo); }
+};  /* class DumpOstreamUpdate */
+
+class DebugOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Debug.getStream(); }
+  virtual void set(std::ostream* setTo) { Debug.setStream(setTo); }
+};  /* class DebugOstreamUpdate */
+
+class WarningOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Warning.getStream(); }
+  virtual void set(std::ostream* setTo) { Warning.setStream(setTo); }
+};  /* class WarningOstreamUpdate */
+
+class MessageOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Message.getStream(); }
+  virtual void set(std::ostream* setTo) { Message.setStream(setTo); }
+};  /* class MessageOstreamUpdate */
+
+class NoticeOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Notice.getStream(); }
+  virtual void set(std::ostream* setTo) { Notice.setStream(setTo); }
+};  /* class NoticeOstreamUpdate */
+
+class ChatOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Chat.getStream(); }
+  virtual void set(std::ostream* setTo) { Chat.setStream(setTo); }
+};  /* class ChatOstreamUpdate */
+
+class TraceOstreamUpdate : public OstreamUpdate {
+ public:
+  virtual std::ostream& get() { return Trace.getStream(); }
+  virtual void set(std::ostream* setTo) { Trace.setStream(setTo); }
+};  /* class TraceOstreamUpdate */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UPDATE_OSTREAM_H */