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

6 files changed, 141 insertions, 87 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ffbc67cc4..b3666875d 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -45,21 +45,26 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
-  d_satSolver(satSolver),
-  d_booleanVariables(context),
-  d_nodeToLiteralMap(context),
-  d_literalToNodeMap(context),
-  d_fullLitToNodeMap(fullLitToNodeMap),
-  d_convertAndAssertCounter(0),
-  d_registrar(registrar),
-  d_assertionTable(context),
-  d_removable(false) {
+CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
+                     context::Context* context, SmtGlobals* globals,
+                     bool fullLitToNodeMap)
+    : d_satSolver(satSolver),
+      d_booleanVariables(context),
+      d_nodeToLiteralMap(context),
+      d_literalToNodeMap(context),
+      d_fullLitToNodeMap(fullLitToNodeMap),
+      d_convertAndAssertCounter(0),
+      d_registrar(registrar),
+      d_assertionTable(context),
+      d_globals(globals),
+      d_removable(false) {
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
-  CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
-}
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
+                                   context::Context* context,
+                                   SmtGlobals* globals, bool fullLitToNodeMap)
+    : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap)
+{}
 
 void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
   Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl;
@@ -184,7 +189,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
 
   // If it's a theory literal, need to store it for back queries
   if ( isTheoryAtom || d_fullLitToNodeMap ||
-       ( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
+       ( CVC4_USE_REPLAY && d_globals->getReplayLog() != NULL ) ||
        (Dump.isOn("clauses")) ) {
 
     d_literalToNodeMap.insert_safe(lit, node);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index d5d01d126..cfab216fe 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -25,14 +25,15 @@
 #ifndef __CVC4__PROP__CNF_STREAM_H
 #define __CVC4__PROP__CNF_STREAM_H
 
+#include <ext/hash_map>
+
+#include "context/cdinsert_hashmap.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
-#include "prop/theory_proxy.h"
-#include "prop/registrar.h"
 #include "proof/proof_manager.h"
-#include "context/cdlist.h"
-#include "context/cdinsert_hashmap.h"
-
-#include <ext/hash_map>
+#include "prop/registrar.h"
+#include "prop/theory_proxy.h"
+#include "smt/smt_globals.h"
 
 namespace CVC4 {
 namespace prop {
@@ -86,6 +87,9 @@ protected:
   /** A table of assertions, used for regenerating proofs. */
   context::CDList<Node> d_assertionTable;
 
+  /** Container for misc. globals. */
+  SmtGlobals* d_globals;
+
   /**
    * How many literals were already mapped at the top-level when we
    * tried to convertAndAssert() something.  This
@@ -191,7 +195,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
+  CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -291,7 +295,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
+  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
 
 private:
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2a1b05619..96ca7480f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -25,7 +25,6 @@
 #include "decision/decision_engine.h"
 #include "expr/expr.h"
 #include "expr/resource_manager.h"
-#include "expr/result.h"
 #include "options/base_options.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"
@@ -40,7 +39,7 @@
 #include "smt_util/command.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
-
+#include "util/result.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -68,7 +67,7 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) :
+PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) :
   d_inCheckSat(false),
   d_theoryEngine(te),
   d_decisionEngine(de),
@@ -78,7 +77,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
   d_registrar(NULL),
   d_cnfStream(NULL),
   d_interrupted(false),
-  d_resourceManager(NodeManager::currentResourceManager()) {
+  d_resourceManager(NodeManager::currentResourceManager()),
+  d_globals(globals)
+{
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
@@ -86,14 +87,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream
-    (d_satSolver, d_registrar,
-     userContext,
+    (d_satSolver, d_registrar, userContext, d_globals,
      // fullLitToNode Map =
      options::threads() > 1 ||
      options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
      );
 
-  d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream);
+  d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals);
   d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 57ff3c5c0..dfa84ef14 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,10 +25,11 @@
 
 #include "base/modal_exception.h"
 #include "expr/node.h"
-#include "expr/result.h"
 #include "options/options.h"
 #include "proof/proof_manager.h"
+#include "smt/smt_globals.h"
 #include "util/unsafe_interrupt_exception.h"
+#include "util/result.h"
 
 namespace CVC4 {
 
@@ -91,12 +92,15 @@ class PropEngine {
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
 
+  /** Container for misc. globals. */
+  SmtGlobals* d_globals;
+
 public:
 
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext);
+  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext, SmtGlobals* global);
 
   /**
    * Destructor.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 386b12391..d0830b9a5 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -31,6 +31,43 @@
 namespace CVC4 {
 namespace prop {
 
+TheoryProxy::TheoryProxy(PropEngine* propEngine,
+                         TheoryEngine* theoryEngine,
+                         DecisionEngine* decisionEngine,
+                         context::Context* context,
+                         CnfStream* cnfStream,
+                         SmtGlobals* globals)
+    : d_propEngine(propEngine),
+      d_cnfStream(cnfStream),
+      d_decisionEngine(decisionEngine),
+      d_theoryEngine(theoryEngine),
+      d_globals(globals),
+      d_queue(context)
+{}
+
+TheoryProxy::~TheoryProxy() {
+  /* nothing to do for now */
+}
+
+/** The lemma input channel we are using. */
+LemmaInputChannel* TheoryProxy::inputChannel() {
+  return d_globals->getLemmaInputChannel();
+}
+
+/** The lemma output channel we are using. */
+LemmaOutputChannel* TheoryProxy::outputChannel() {
+  return d_globals->getLemmaOutputChannel();
+}
+
+std::ostream* TheoryProxy::replayLog() {
+  return d_globals->getReplayLog();
+}
+
+ExprStream* TheoryProxy::replayStream() {
+  return d_globals->getReplayStream();
+}
+
+
 void TheoryProxy::variableNotify(SatVariable var) {
   d_theoryEngine->preRegister(getNode(SatLiteral(var)));
 }
@@ -108,10 +145,10 @@ void TheoryProxy::notifyRestart() {
 
   static uint32_t lemmaCount = 0;
 
-  if(options::lemmaInputChannel() != NULL) {
-    while(options::lemmaInputChannel()->hasNewLemma()) {
+  if(inputChannel() != NULL) {
+    while(inputChannel()->hasNewLemma()) {
       Debug("shared") << "shared" << std::endl;
-      Expr lemma = options::lemmaInputChannel()->getNewLemma();
+      Expr lemma = inputChannel()->getNewLemma();
       Node asNode = lemma.getNode();
       asNode = theory::Rewriter::rewrite(asNode);
 
@@ -135,7 +172,7 @@ void TheoryProxy::notifyRestart() {
 
 void TheoryProxy::notifyNewLemma(SatClause& lemma) {
   Assert(lemma.size() > 0);
-  if(options::lemmaOutputChannel() != NULL) {
+  if(outputChannel() != NULL) {
     if(lemma.size() == 1) {
       // cannot share units yet
       //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
@@ -148,7 +185,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
       if(d_shared.find(n) == d_shared.end()) {
         d_shared.insert(n);
-        options::lemmaOutputChannel()->notifyNewLemma(n.toExpr());
+        outputChannel()->notifyNewLemma(n.toExpr());
       } else {
         Debug("shared") <<"drop new " << n << std::endl;
       }
@@ -158,8 +195,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) {
 
 SatLiteral TheoryProxy::getNextReplayDecision() {
 #ifdef CVC4_REPLAY
-  if(options::replayStream() != NULL) {
-    Expr e = options::replayStream()->nextExpr();
+  if(replayStream() != NULL) {
+    Expr e = replayStream()->nextExpr();
     if(!e.isNull()) { // we get null node when out of decisions to replay
       // convert & return
       ++d_replayedDecisions;
@@ -172,9 +209,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
 
 void TheoryProxy::logDecision(SatLiteral lit) {
 #ifdef CVC4_REPLAY
-  if(options::replayLog() != NULL) {
+  if(replayLog() != NULL) {
     Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
-    *options::replayLog() << d_cnfStream->getNode(lit) << std::endl;
+    (*replayLog()) << d_cnfStream->getNode(lit) << std::endl;
   }
 #endif /* CVC4_REPLAY */
 }
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 */