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, 11 insertions, 9 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3649a86..8ded63c28 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/statistics_registry.h"
+#include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
@@ -35,10 +36,10 @@ namespace bv {
 class CoreSolver;
 class InequalitySolver;
 class AlgebraicSolver;
-class BitblastSolver; 
+class BitblastSolver;
 
 class EagerBitblastSolver;
-  
+
 class AbstractionModule;
 
 class TheoryBV : public Theory {
@@ -49,14 +50,14 @@ class TheoryBV : public Theory {
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-  
-  std::vector<SubtheorySolver*> d_subtheories;
-  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 
+  std::vector<SubtheorySolver*> d_subtheories;
+  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+
   ~TheoryBV();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -80,13 +81,14 @@ public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   void enableCoreTheorySlicer();
-  
+
   Node ppRewrite(TNode t);
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
-  
+
   void presolve();
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
 private:
 
   class Statistics {