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, 22 insertions, 6 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index be2a89dbc..60716146e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -104,7 +104,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
                            const LogicInfo& logicInfo,
-                           SmtGlobals* globals)
+                           LemmaChannels* channels)
 : d_propEngine(NULL),
   d_decisionEngine(NULL),
   d_context(context),
@@ -133,16 +133,20 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_false(),
   d_interrupted(false),
   d_resourceManager(NodeManager::currentResourceManager()),
-  d_globals(globals),
+  d_channels(channels),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
   d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
   d_bvToBoolPreprocessor(),
+  d_theoryAlternatives(),
+  d_attr_handle(),
   d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 {
-  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
+      ++ theoryId)
+  {
     d_theoryTable[theoryId] = NULL;
     d_theoryOut[theoryId] = NULL;
   }
@@ -155,7 +159,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  PROOF (ProofManager::currentPM()->initTheoryProofEngine(d_globals); );
+  PROOF (ProofManager::currentPM()->initTheoryProofEngine(); );
 
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 
@@ -1398,8 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // Share with other portfolio threads
-  if(d_globals->getLemmaOutputChannel() != NULL) {
-    d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
+  if(d_channels->getLemmaOutputChannel() != NULL) {
+    d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
   // Run theory preprocessing, maybe
@@ -1769,6 +1773,18 @@ void TheoryEngine::spendResource(unsigned ammount) {
   d_resourceManager->spendResource(ammount);
 }
 
+void TheoryEngine::enableTheoryAlternative(const std::string& name){
+  Debug("TheoryEngine::enableTheoryAlternative")
+      << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
+
+  d_theoryAlternatives.insert(name);
+}
+
+bool TheoryEngine::useTheoryAlternative(const std::string& name) {
+  return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
+}
+
+
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
     conflicts(mkName("theory<", theory, ">::conflicts"), 0),
     propagations(mkName("theory<", theory, ">::propagations"), 0),