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

2 files changed, 16 insertions, 10 deletions

diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 427ac577c..8cba51c8f 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -26,15 +26,16 @@
 
 using namespace std;
 
-using namespace CVC4;
-using namespace theory;
-using namespace idl;
-
-TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-                     Valuation valuation, const LogicInfo& logicInfo)
-: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo)
-, d_model(c)
-, d_assertionsDB(c)
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u,
+                     OutputChannel& out, Valuation valuation,
+                     const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals)
+    , d_model(c)
+    , d_assertionsDB(c)
 {}
 
 Node TheoryIdl::ppRewrite(TNode atom) {
@@ -148,3 +149,7 @@ bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
   // Everything fine, no conflict
   return true;
 }
+
+} /* namepsace CVC4::theory::idl */
+} /* namepsace CVC4::theory */
+} /* namepsace CVC4 */
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 7c879e722..aa7267eb7 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -45,7 +45,8 @@ public:
 
   /** Theory constructor. */
   TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
-            Valuation valuation, const LogicInfo& logicInfo);
+            Valuation valuation, const LogicInfo& logicInfo,
+            SmtGlobals* globals);
 
   /** Pre-processing of input atoms */
   Node ppRewrite(TNode atom);