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, 10 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index fd5aec7d0..c110ffa4f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -28,7 +28,6 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
-#include "expr/result.h"
 #include "expr/statistics_registry.h"
 #include "main/command_executor.h"
 
@@ -50,6 +49,7 @@
 #include "smt/smt_options_handler.h"
 #include "smt_util/command.h"
 #include "util/configuration.h"
+#include "util/result.h"
 
 using namespace std;
 using namespace CVC4;
@@ -285,11 +285,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       replayParserBuilder.withStreamInput(cin);
     }
     replayParser = replayParserBuilder.build();
-    opts.set(options::replayStream, new Parser::ExprStream(replayParser));
+    pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser));
   }
-  if( opts[options::replayLog] != NULL ) {
-    *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage])
-                              << expr::ExprSetDepth(-1);
+  if( pExecutor->globals()->getReplayLog() != NULL ) {
+    *(pExecutor->globals()->getReplayLog()) <<
+        language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1);
   }
 
   int returnValue = 0;
@@ -569,10 +569,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       delete parser;
     }
 
-    if( opts[options::replayStream] != NULL ) {
+    if( pExecutor->globals()->getReplayStream() != NULL ) {
+      ExprStream* replayStream = pExecutor->globals()->getReplayStream();
+      pExecutor->globals()->setReplayStream(NULL);
       // this deletes the expression parser too
-      delete opts[options::replayStream];
-      opts.set(options::replayStream, NULL);
+      delete replayStream;
     }
 
     Result result;
@@ -610,8 +611,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     }
 
     // make sure to flush replay output log before early-exit
-    if( opts[options::replayLog] != NULL ) {
-      *opts[options::replayLog] << flush;
+    if( pExecutor->globals()->getReplayLog() != NULL ) {
+      *(pExecutor->globals()->getReplayLog()) << flush;
     }
 
     // make sure out and err streams are flushed too