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}.

6 files changed, 343 insertions, 7 deletions

diff --git a/src/smt_util/Makefile.am b/src/smt_util/Makefile.am
index 3b457f641..ae1ea1f70 100644
--- a/src/smt_util/Makefile.am
+++ b/src/smt_util/Makefile.am
@@ -12,12 +12,14 @@ libsmtutil_la_SOURCES = \
 	boolean_simplification.h \
 	command.cpp \
 	command.h \
-	dump.h \
 	dump.cpp \
-	lemma_input_channel.h \
-	lemma_output_channel.h \
+	dump.h \
 	ite_removal.cpp \
 	ite_removal.h \
+	lemma_channels.cpp \
+	lemma_channels.h \
+	lemma_input_channel.h \
+	lemma_output_channel.h \
 	model.cpp \
 	model.h \
 	nary_builder.cpp \
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index 2732eaea7..27fdc3d28 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -35,8 +35,8 @@ namespace CVC4 {
  */
 class BooleanSimplification {
   // cannot construct one of these
-  BooleanSimplification() CVC4_UNUSED;
-  BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED;
+  BooleanSimplification() CVC4_UNDEFINED;
+  BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED;
 
   static bool push_back_associative_commute_recursive
     (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
diff --git a/src/smt_util/dump.cpp b/src/smt_util/dump.cpp
index 56313f4d8..218691bd0 100644
--- a/src/smt_util/dump.cpp
+++ b/src/smt_util/dump.cpp
@@ -21,4 +21,201 @@ namespace CVC4 {
 
 DumpC DumpChannel CVC4_PUBLIC;
 
+std::ostream& DumpC::setStream(std::ostream* os) {
+  DumpOut.setStream(os);
+  return *os;
+}
+std::ostream& DumpC::getStream() { return DumpOut.getStream(); }
+std::ostream* DumpC::getStreamPointer() { return DumpOut.getStreamPointer(); }
+
+
+void DumpC::setDumpFromString(const std::string& optarg) {
+#ifdef CVC4_DUMPING
+  char* optargPtr = strdup(optarg.c_str());
+  char* tokstr = optargPtr;
+  char* toksave;
+  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+    tokstr = NULL;
+    if(!strcmp(optargPtr, "benchmark")) {
+    } else if(!strcmp(optargPtr, "declarations")) {
+    } else if(!strcmp(optargPtr, "assertions")) {
+      Dump.on("assertions:post-everything");
+    } else if(!strncmp(optargPtr, "assertions:", 11)) {
+      const char* p = optargPtr + 11;
+      if(!strncmp(p, "pre-", 4)) {
+        p += 4;
+      } else if(!strncmp(p, "post-", 5)) {
+        p += 5;
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "boolean-terms")) {
+      } else if(!strcmp(p, "constrain-subtypes")) {
+      } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
+      } else if(!strcmp(p, "skolem-quant")) {
+      } else if(!strcmp(p, "simplify")) {
+      } else if(!strcmp(p, "static-learning")) {
+      } else if(!strcmp(p, "ite-removal")) {
+      } else if(!strcmp(p, "repeat-simplify")) {
+      } else if(!strcmp(p, "rewrite-apply-to-const")) {
+      } else if(!strcmp(p, "theory-preprocessing")) {
+      } else if(!strcmp(p, "nonclausal")) {
+      } else if(!strcmp(p, "theorypp")) {
+      } else if(!strcmp(p, "itesimp")) {
+      } else if(!strcmp(p, "unconstrained")) {
+      } else if(!strcmp(p, "repeatsimp")) {
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      Dump.on("assertions");
+    } else if(!strcmp(optargPtr, "skolems")) {
+    } else if(!strcmp(optargPtr, "clauses")) {
+    } else if(!strcmp(optargPtr, "t-conflicts") ||
+              !strcmp(optargPtr, "t-lemmas") ||
+              !strcmp(optargPtr, "t-explanations") ||
+              !strcmp(optargPtr, "bv-rewrites") ||
+              !strcmp(optargPtr, "theory::fullcheck")) {
+      // These are "non-state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is dumped, it will interfere with the validity
+      // of these generated queries.
+      if(Dump.isOn("state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("no-permit-state");
+      }
+    } else if(!strcmp(optargPtr, "state") ||
+              !strcmp(optargPtr, "missed-t-conflicts") ||
+              !strcmp(optargPtr, "t-propagations") ||
+              !strcmp(optargPtr, "missed-t-propagations")) {
+      // These are "state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is not dumped, it will interfere with the
+      // validity of these generated queries.
+      if(Dump.isOn("no-permit-state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "non-state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("state");
+      }
+    } else if(!strcmp(optargPtr, "help")) {
+      puts(s_dumpHelp.c_str());
+      exit(1);
+    } else if(!strcmp(optargPtr, "bv-abstraction")) {
+      Dump.on("bv-abstraction");
+    } else if(!strcmp(optargPtr, "bv-algebraic")) {
+      Dump.on("bv-algebraic");
+    } else {
+      throw OptionException(std::string("unknown option for --dump: `") +
+                            optargPtr + "'.  Try --dump help.");
+    }
+
+    Dump.on(optargPtr);
+    Dump.on("benchmark");
+    if(strcmp(optargPtr, "benchmark")) {
+      Dump.on("declarations");
+      if(strcmp(optargPtr, "declarations")) {
+        Dump.on("skolems");
+      }
+    }
+  }
+  free(optargPtr);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+
+const std::string DumpC::s_dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+  does not include any declarations or assertions.  Implied by all following\n\
+  modes.\n\
+\n\
+declarations\n\
++ Dump user declarations.  Implied by all following modes.\n\
+\n\
+skolems\n\
++ Dump internally-created skolem variable declarations.  These can\n\
+  arise from preprocessing simplifications, existential elimination,\n\
+  and a number of other things.  Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+  where PASS is one of the preprocessing passes: definition-expansion\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const theory-preprocessing.\n\
+  PASS can also be the special value \"everything\", in which case the\n\
+  assertions are printed before any preprocessing (with\n\
+  \"assertions:pre-everything\") or after all preprocessing completes\n\
+  (with \"assertions:post-everything\").\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+  output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+  Implied by all \"stateful\" modes below and conflicts with all\n\
+  non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+bv-abstraction [non-stateful]\n\
++ Output correctness queries for all bv abstraction \n\
+\n\
+bv-algebraic [non-stateful]\n\
++ Output correctness queries for bv algebraic solver. \n\
+\n\
+theory::fullcheck [non-stateful]\n                                      \
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
+one from the assertions category (either assertions or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations.  Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
 }/* CVC4 namespace */
diff --git a/src/smt_util/dump.h b/src/smt_util/dump.h
index 1f4efe640..19f9118e3 100644
--- a/src/smt_util/dump.h
+++ b/src/smt_util/dump.h
@@ -75,6 +75,8 @@ class CVC4_PUBLIC DumpC {
   std::set<std::string> d_tags;
   CommandSequence d_commands;
 
+  static const std::string s_dumpHelp;
+
 public:
   CVC4dumpstream operator()(const char* tag) {
     if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
@@ -83,6 +85,7 @@ public:
       return CVC4dumpstream();
     }
   }
+
   CVC4dumpstream operator()(std::string tag) {
     if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
       return CVC4dumpstream(getStream(), d_commands);
@@ -103,8 +106,11 @@ public:
   bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
   bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
 
-  std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; }
-  std::ostream& getStream() { return DumpOut.getStream(); }
+  std::ostream& setStream(std::ostream* os);
+  std::ostream& getStream();
+  std::ostream* getStreamPointer();
+
+  void setDumpFromString(const std::string& optarg);
 };/* class DumpC */
 
 /** The dump singleton */
diff --git a/src/smt_util/lemma_channels.cpp b/src/smt_util/lemma_channels.cpp
new file mode 100644
index 000000000..e75866c5e
--- /dev/null
+++ b/src/smt_util/lemma_channels.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file lemma_channels.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_util/lemma_channels.h"
+
+#include <cerrno>
+#include <iostream>
+#include <string>
+#include <utility>
+
+#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY
+#include "expr/expr_stream.h"
+#include "options/open_ostream.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"
+
+namespace CVC4 {
+
+LemmaChannels::LemmaChannels()
+    : d_lemmaInputChannel(NULL)
+    , d_lemmaOutputChannel(NULL)
+{}
+
+LemmaChannels::~LemmaChannels(){}
+
+void LemmaChannels::setLemmaInputChannel(LemmaInputChannel* in) {
+  d_lemmaInputChannel = in;
+}
+
+void LemmaChannels::setLemmaOutputChannel(LemmaOutputChannel* out) {
+  d_lemmaOutputChannel = out;
+}
+
+
+} /* namespace CVC4 */
diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h
new file mode 100644
index 000000000..6cd81795e
--- /dev/null
+++ b/src/smt_util/lemma_channels.h
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file lemma_channels.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 LemmaChannels is a light container for a pair of input and output
+ ** lemma channels.
+ **
+ ** LemmaChannels is a light container for a pair of input and output
+ ** lemma channels. These contain paramaters for the infrequently
+ ** used Portfolio mode. There should be exactly one of these per SmtEngine
+ ** with the same lifetime as the SmtEngine. The 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.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT_UTIL__LEMMA_CHANNELS_H
+#define __CVC4__SMT_UTIL__LEMMA_CHANNELS_H
+
+#include <iosfwd>
+#include <string>
+#include <utility>
+
+#include "options/option_exception.h"
+#include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
+
+namespace CVC4 {
+
+/**
+ * LemmaChannels is a wrapper around two pointers:
+ * - getLemmaInputChannel()
+ * - getLemmaOutputChannel()
+ *
+ * The user can directly set these and is responsible for handling the
+ * memory for these. These datastructures are used for Portfolio mode.
+ */
+class CVC4_PUBLIC LemmaChannels {
+ public:
+  /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */
+  LemmaChannels();
+  ~LemmaChannels();
+
+  void setLemmaInputChannel(LemmaInputChannel* in);
+  LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
+
+  void setLemmaOutputChannel(LemmaOutputChannel* out);
+  LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
+
+ private:
+  // Disable copy constructor.
+  LemmaChannels(const LemmaChannels&) CVC4_UNDEFINED;
+
+  // Disable assignment operator.
+  LemmaChannels& operator=(const LemmaChannels&) CVC4_UNDEFINED;
+
+  /** This captures the old options::lemmaInputChannel .*/
+  LemmaInputChannel* d_lemmaInputChannel;
+
+  /** This captures the old options::lemmaOutputChannel .*/
+  LemmaOutputChannel* d_lemmaOutputChannel;
+}; /* class LemmaChannels */
+
+} /* namespace CVC4 */
+
+#endif /* __CVC4__SMT_UTIL__LEMMA_CHANNELS_H */