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, 49 insertions, 45 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2863fad8a..ab57eb260 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -51,50 +51,52 @@ const bool d_solveWrite2 = false;
   //bool d_lazyRIntro1 = true;
   //bool d_eagerIndexSplitting = false;
 
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-  Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
-  d_numRow("theory::arrays::number of Row lemmas", 0),
-  d_numExt("theory::arrays::number of Ext lemmas", 0),
-  d_numProp("theory::arrays::number of propagations", 0),
-  d_numExplain("theory::arrays::number of explanations", 0),
-  d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
-  d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
-  d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
-  d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
-  d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
-  d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
-  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
-  d_ppFacts(u),
-  //  d_ppCache(u),
-  d_literalsToPropagate(c),
-  d_literalsToPropagateIndex(c, 0),
-  d_isPreRegistered(c),
-  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
-  d_conflict(c, false),
-  d_backtracker(c),
-  d_infoMap(c, &d_backtracker),
-  d_mergeQueue(c),
-  d_mergeInProgress(false),
-  d_RowQueue(c),
-  d_RowAlreadyAdded(u),
-  d_sharedArrays(c),
-  d_sharedOther(c),
-  d_sharedTerms(c, false),
-  d_reads(c),
-  d_constReadsList(c),
-  d_constReadsContext(new context::Context()),
-  d_contextPopper(c, d_constReadsContext),
-  d_skolemIndex(c, 0),
-  d_decisionRequests(c),
-  d_permRef(c),
-  d_modelConstraints(c),
-  d_lemmasSaved(c),
-  d_defValues(c),
-  d_readTableContext(new context::Context()),
-  d_arrayMerges(c),
-  d_inCheckModel(false)
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
+                           OutputChannel& out, Valuation valuation,
+                           const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals),
+      d_numRow("theory::arrays::number of Row lemmas", 0),
+      d_numExt("theory::arrays::number of Ext lemmas", 0),
+      d_numProp("theory::arrays::number of propagations", 0),
+      d_numExplain("theory::arrays::number of explanations", 0),
+      d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
+      d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
+      d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
+      d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
+      d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
+      d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
+      d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
+      d_ppFacts(u),
+      //      d_ppCache(u),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_isPreRegistered(c),
+      d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
+      d_conflict(c, false),
+      d_backtracker(c),
+      d_infoMap(c, &d_backtracker),
+      d_mergeQueue(c),
+      d_mergeInProgress(false),
+      d_RowQueue(c),
+      d_RowAlreadyAdded(u),
+      d_sharedArrays(c),
+      d_sharedOther(c),
+      d_sharedTerms(c, false),
+      d_reads(c),
+      d_constReadsList(c),
+      d_constReadsContext(new context::Context()),
+      d_contextPopper(c, d_constReadsContext),
+      d_skolemIndex(c, 0),
+      d_decisionRequests(c),
+      d_permRef(c),
+      d_modelConstraints(c),
+      d_lemmasSaved(c),
+      d_defValues(c),
+      d_readTableContext(new context::Context()),
+      d_arrayMerges(c),
+      d_inCheckModel(false)
 {
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 28d994835..98cba0420 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -126,7 +126,9 @@ class TheoryArrays : public Theory {
 
   public:
 
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
+               Valuation valuation, const LogicInfo& logicInfo,
+               SmtGlobals* globals);
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);