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

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 57ff3c5c0..dfa84ef14 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,10 +25,11 @@
 
 #include "base/modal_exception.h"
 #include "expr/node.h"
-#include "expr/result.h"
 #include "options/options.h"
 #include "proof/proof_manager.h"
+#include "smt/smt_globals.h"
 #include "util/unsafe_interrupt_exception.h"
+#include "util/result.h"
 
 namespace CVC4 {
 
@@ -91,12 +92,15 @@ class PropEngine {
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
 
+  /** Container for misc. globals. */
+  SmtGlobals* d_globals;
+
 public:
 
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext);
+  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext, SmtGlobals* global);
 
   /**
    * Destructor.