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

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 */
 }