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

1 files changed, 10 insertions, 2 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2185f22ff..adc4daeee 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -30,6 +30,7 @@
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
+#include "smt/smt_globals.h"
 #include "smt_util/command.h"
 #include "theory/atom_requests.h"
 #include "theory/bv/bv_to_bool.h"
@@ -206,6 +207,7 @@ class TheoryEngine {
    */
   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 
+
   /**
    * Statistics for a particular theory.
    */
@@ -476,10 +478,14 @@ class TheoryEngine {
   bool d_interrupted;
   ResourceManager* d_resourceManager;
 
+  /** Container for misc. globals. */
+  SmtGlobals* d_globals;
+
 public:
 
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic);
+  TheoryEngine(context::Context* context, context::UserContext* userContext,
+               RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -498,7 +504,9 @@ public:
   inline void addTheory(theory::TheoryId theoryId) {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo);
+    d_theoryTable[theoryId] =
+        new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
+                        theory::Valuation(this), d_logicInfo, d_globals);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {