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, 51 insertions, 47 deletions

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 413b4941d..59bc859cb 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -23,9 +23,15 @@
 // Optional blocks below will be unconditionally included
 #define __CVC4_USE_MINISAT
 
+#include <iosfwd>
+
 #include "context/cdqueue.h"
+#include "expr/node.h"
 #include "expr/statistics_registry.h"
 #include "prop/sat_solver.h"
+#include "smt/smt_globals.h"
+#include "smt_util/lemma_output_channel.h"
+#include "smt_util/lemma_input_channel.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
@@ -42,40 +48,13 @@ class CnfStream;
  * The proxy class that allows the SatSolver to communicate with the theories
  */
 class TheoryProxy {
-
-  /** The prop engine we are using */
-  PropEngine* d_propEngine;
-
-  /** The CNF engine we are using */
-  CnfStream* d_cnfStream;
-
-  /** The decision engine we are using */
-  DecisionEngine* d_decisionEngine;
-
-  /** The theory engine we are using */
-  TheoryEngine* d_theoryEngine;
-
-  /** Queue of asserted facts */
-  context::CDQueue<TNode> d_queue;
-
-  /**
-   * Set of all lemmas that have been "shared" in the portfolio---i.e.,
-   * all imported and exported lemmas.
-   */
-  std::hash_set<Node, NodeHashFunction> d_shared;
-
-  /**
-   * Statistic: the number of replayed decisions (via --replay).
-   */
-  KEEP_STATISTIC(IntStat, d_replayedDecisions,
-                 "prop::theoryproxy::replayedDecisions", 0);
-
 public:
   TheoryProxy(PropEngine* propEngine,
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
-              CnfStream* cnfStream);
+              CnfStream* cnfStream,
+              SmtGlobals* globals);
 
   ~TheoryProxy();
 
@@ -117,25 +96,50 @@ public:
 
   SatValue getDecisionPolarity(SatVariable var);
 
-};/* class SatSolver */
+ private:
+  /** The prop engine we are using. */
+  PropEngine* d_propEngine;
 
-/* Functions that delegate to the concrete SAT solver. */
-
-inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
-                                TheoryEngine* theoryEngine,
-                                DecisionEngine* decisionEngine,
-                                context::Context* context,
-                                CnfStream* cnfStream) :
-  d_propEngine(propEngine),
-  d_cnfStream(cnfStream),
-  d_decisionEngine(decisionEngine),
-  d_theoryEngine(theoryEngine),
-  d_queue(context)
-{}
-
-inline TheoryProxy::~TheoryProxy() {
-  /* nothing to do for now */
-}
+  /** The CNF engine we are using. */
+  CnfStream* d_cnfStream;
+
+  /** The decision engine we are using. */
+  DecisionEngine* d_decisionEngine;
+
+  /** The theory engine we are using. */
+  TheoryEngine* d_theoryEngine;
+
+
+  /**
+   * Container for inputChannel, outputChannel, replayLog, and
+   * replayStream.
+   */
+  SmtGlobals* d_globals;
+
+  /** The lemma input channel we are using. */
+  LemmaInputChannel* inputChannel();
+
+  /** The lemma output channel we are using. */
+  LemmaOutputChannel* outputChannel();
+
+  std::ostream* replayLog();
+  ExprStream* replayStream();
+
+  /** Queue of asserted facts */
+  context::CDQueue<TNode> d_queue;
+
+  /**
+   * Set of all lemmas that have been "shared" in the portfolio---i.e.,
+   * all imported and exported lemmas.
+   */
+  std::hash_set<Node, NodeHashFunction> d_shared;
+
+  /**
+   * Statistic: the number of replayed decisions (via --replay).
+   */
+  KEEP_STATISTIC(IntStat, d_replayedDecisions,
+                 "prop::theoryproxy::replayedDecisions", 0);
+};/* class SatSolver */
 
 }/* CVC4::prop namespace */