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

4 files changed, 21 insertions, 13 deletions

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index e705da409..bab71d8b2 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -155,7 +155,9 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_theoryEngine = d_smt->d_theoryEngine;
 
     d_satSolver = new FakeSatSolver();
-    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine), new context::Context());
+    d_cnfStream = new CVC4::prop::TseitinCnfStream(
+        d_satSolver, new theory::TheoryRegistrar(d_theoryEngine),
+        new context::Context(), d_smt->globals());
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index d8615eda7..4313a9b64 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -114,7 +114,8 @@ public:
     d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
     d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
 
-    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo);
+    d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
+                              d_logicInfo, d_smt->globals());
 
     preregistered = new std::set<Node>();
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 399feb43e..2ecb4e225 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -120,13 +120,14 @@ class FakeTheory : public Theory {
   // static std::deque<RewriteItem> s_expected;
 
 public:
-  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
+  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
+      Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, globals)
   { }
 
   /** Register an expected rewrite call */
-  static void expect(RewriteType type, FakeTheory* thy,
-                     TNode n, bool topLevel) throw() {
+  static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel)
+      throw()
+  {
     RewriteItem item = { type, thy, n, topLevel };
     //s_expected.push_back(item);
   }
@@ -224,7 +225,7 @@ public:
   void registerTerm(TNode) { Unimplemented(); }
   void check(Theory::Effort) { Unimplemented(); }
   void propagate(Theory::Effort) { Unimplemented(); }
-  void explain(TNode, Theory::Effort) { Unimplemented(); }
+  Node explain(TNode) { Unimplemented(); }
   Node getValue(TNode n) { return Node::null(); }
 };/* class FakeTheory */
 
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index c804ca307..429e72fc6 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -52,7 +52,9 @@ public:
 
   ~TestOutputChannel() {}
 
-  void safePoint() throw(Interrupted, AssertionException) {}
+  void safePoint(uint64_t amount)
+      throw(Interrupted, UnsafeInterruptException, AssertionException)
+  {}
 
   void conflict(TNode n)
     throw(AssertionException) {
@@ -119,9 +121,10 @@ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
-  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) {
-  }
+  DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out,
+              Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals)
+      : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, globals)
+  {}
 
   void registerTerm(TNode n) {
     // check that we registerTerm() a term only once
@@ -156,7 +159,7 @@ public:
   }
   void preRegisterTerm(TNode n) {}
   void propagate(Effort level) {}
-  void explain(TNode n, Effort level) {}
+  Node explain(TNode n) { return Node::null(); }
   Node getValue(TNode n) { return Node::null(); }
   string identify() const { return "DummyTheory"; }
 };/* class DummyTheory */
@@ -196,7 +199,8 @@ public:
     d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
     d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
 
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
+    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
+                              *d_logicInfo, d_smt->globals());
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);