Using Options in ParserBuilder and InteractiveShell

5 files changed, 87 insertions, 47 deletions

diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 6bd9db295..66c134ecd 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -21,6 +21,7 @@
 #include <string>
 
 #include "parser/parser_builder.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
@@ -34,11 +35,10 @@ class InteractiveShell {
   ParserBuilder d_parserBuilder;
 
 public:
-  InteractiveShell(std::istream& in, 
-                   std::ostream& out, 
-                   ParserBuilder& parserBuilder) : 
-    d_in(in),
-    d_out(out),
+  InteractiveShell(ParserBuilder& parserBuilder,
+                  const Options& options) : 
+    d_in(*options.in),
+    d_out(*options.out),
     d_parserBuilder(parserBuilder) {
   }
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 544c6fd29..8bca6190e 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -79,7 +79,7 @@ void printUsage() {
       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
       << endl
       << "CVC4 options:" << endl;
-  Options::printUsage( ss.str(), options.out );
+  Options::printUsage( ss.str(), *options.out );
 }
 
 /**
@@ -94,34 +94,34 @@ int main(int argc, char* argv[]) {
     return runCvc4(argc, argv);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
-    options.out << "unknown" << endl;
+    *options.out << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
     printUsage();
     exit(1);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
-    options.out << "unknown" << endl;
+    *options.out << "unknown" << endl;
 #endif
-    options.err << "CVC4 Error:" << endl << e << endl;
+    *options.err << "CVC4 Error:" << endl << e << endl;
     if(options.statistics) {
-      StatisticsRegistry::flushStatistics(options.err);
+      StatisticsRegistry::flushStatistics(*options.err);
     }
     exit(1);
   } catch(bad_alloc) {
 #ifdef CVC4_COMPETITION_MODE
-    options.out << "unknown" << endl;
+    *options.out << "unknown" << endl;
 #endif
-    options.err << "CVC4 ran out of memory." << endl;
+    *options.err << "CVC4 ran out of memory." << endl;
     if(options.statistics) {
-      StatisticsRegistry::flushStatistics(options.err);
+      StatisticsRegistry::flushStatistics(*options.err);
     }
     exit(1);
   } catch(...) {
 #ifdef CVC4_COMPETITION_MODE
-    options.out << "unknown" << endl;
+    *options.out << "unknown" << endl;
 #endif
-    options.err << "CVC4 threw an exception of unknown type." << endl;
+    *options.err << "CVC4 threw an exception of unknown type." << endl;
     exit(1);
   }
 }
@@ -143,10 +143,10 @@ int runCvc4(int argc, char* argv[]) {
     printUsage();
     exit(1);
   } else if( options.languageHelp ) {
-    Options::printLanguageHelp(options.out);
+    Options::printLanguageHelp(*options.out);
     exit(1);
   } else if( options.version ) {
-    options.out << Configuration::about().c_str() << flush;
+    *options.out << Configuration::about().c_str() << flush;
     exit(0);
   } 
 
@@ -154,7 +154,7 @@ int runCvc4(int argc, char* argv[]) {
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
-  options.out << unitbuf;
+  *options.out << unitbuf;
 #endif
 
   // We only accept one input file
@@ -230,12 +230,7 @@ int runCvc4(int argc, char* argv[]) {
   }
 
   ParserBuilder parserBuilder =
-      ParserBuilder(exprMgr, filename)
-        .withInputLanguage(options.inputLanguage)
-        .withMmap(options.memoryMap)
-        .withChecks(options.semanticChecks &&
-                    !Configuration::isMuzzledBuild() )
-        .withStrictMode( options.strictParsing );
+    ParserBuilder(exprMgr, filename, options);
 
   if( inputFromStdin ) {
     parserBuilder.withStreamInput(cin);
@@ -244,7 +239,7 @@ int runCvc4(int argc, char* argv[]) {
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    InteractiveShell shell(options.in,options.out,parserBuilder);
+    InteractiveShell shell(parserBuilder,options);
     while((cmd = shell.readCommand())) {
       doCommand(smt,cmd);
       delete cmd;
@@ -280,7 +275,7 @@ int runCvc4(int argc, char* argv[]) {
   StatisticsRegistry::registerStat(&s_statSatResult);
 
   if(options.statistics) {
-    StatisticsRegistry::flushStatistics(options.err);
+    StatisticsRegistry::flushStatistics(*options.err);
   }
 
   StatisticsRegistry::unregisterStat(&s_statSatResult);
@@ -304,11 +299,11 @@ void doCommand(SmtEngine& smt, Command* cmd) {
     }
   } else {
     if(options.verbosity > 0) {
-      options.out << "Invoking: " << *cmd << endl;
+      *options.out << "Invoking: " << *cmd << endl;
     }
 
     if(options.verbosity >= 0) {
-      cmd->invoke(&smt, options.out);
+      cmd->invoke(&smt, *options.out);
     } else {
       cmd->invoke(&smt);
     }
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 31f402df1..348fb6e6d 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -56,15 +56,36 @@ public:
   }
 };*/
 
-ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) :
-    d_inputType(FILE_INPUT),
-    d_lang(language::input::LANG_AUTO),
-    d_filename(filename),
-    d_streamInput(NULL),
-    d_exprManager(exprManager),
-    d_checksEnabled(true),
-    d_strictMode(false),
-    d_mmap(false) {
+ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename)//  :
+    // d_inputType(FILE_INPUT),
+    // d_lang(language::input::LANG_AUTO),
+  : d_filename(filename),
+    // d_streamInput(NULL),
+   d_exprManager(exprManager)
+    // d_checksEnabled(true),
+    // d_strictMode(false),
+    // d_mmap(false)
+{
+  init(exprManager,filename);
+}
+
+  ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename, const Options& options) :
+  d_filename(filename),
+   d_exprManager(exprManager)
+{
+  init(exprManager,filename);
+  withOptions(options);
+}
+
+  void ParserBuilder::init(ExprManager& exprManager, const std::string& filename) {
+  d_inputType = FILE_INPUT;
+  d_lang = language::input::LANG_AUTO;
+  d_filename = filename;
+  d_streamInput = NULL;
+  d_exprManager = exprManager;
+  d_checksEnabled = true;
+  d_strictMode = false;
+  d_mmap = false;
 }
 
 Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
@@ -135,6 +156,14 @@ ParserBuilder& ParserBuilder::withMmap(bool flag) {
   return *this;
 }
 
+ParserBuilder& ParserBuilder::withOptions(const Options& options) {
+  return 
+    withInputLanguage(options.inputLanguage)
+      .withMmap(options.memoryMap)
+      .withChecks(options.semanticChecks)
+      .withStrictMode(options.strictParsing);
+  }
+
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
   d_strictMode = flag;
   return *this;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 2e0af677e..4e8c06f78 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -23,8 +23,10 @@
 
 #include <string>
 
-#include "parser/input.h"
-#include "parser/parser_options.h"
+#include "input.h"
+#include "parser_options.h"
+
+#include "util/options.h"
 
 namespace CVC4 {
 
@@ -87,11 +89,16 @@ class CVC4_PUBLIC ParserBuilder {
   /** Should we memory-map a file input? */
   bool d_mmap;
 
+  void init(ExprManager& exprManager, const std::string& filename);
+
 public:
 
   /** Create a parser builder using the given ExprManager and filename. */
   ParserBuilder(ExprManager& exprManager, const std::string& filename);
 
+  ParserBuilder(ExprManager& exprManager, const std::string& filename,
+                const Options& options);
+
   /** Build the parser, using the current settings. */
   Parser *build() throw (InputStreamException,AssertionException);
 
@@ -118,6 +125,9 @@ public:
    * the parser will have a file input. (Default: no) */
   ParserBuilder& withMmap(bool flag = true);
 
+  /** Derive settings from the given options. */
+  ParserBuilder& withOptions(const Options& options);
+
   /** Should the parser use strict mode? (Default: no) */
   ParserBuilder& withStrictMode(bool flag = true);
 
diff --git a/src/util/options.h b/src/util/options.h
index b56741fba..e232176b5 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -27,6 +27,12 @@
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
 #endif /* CVC4_DEBUG */
 
+#ifdef CVC4_MUZZLED
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif
+
 #include <iostream>
 #include <string>
 
@@ -49,9 +55,9 @@ struct CVC4_PUBLIC Options {
 
   bool statistics;
 
-  std::istream& in;
-  std::ostream& out;
-  std::ostream& err;
+  std::istream* in;
+  std::ostream* out;
+  std::ostream* err;
 
   /* -1 means no output */
   /* 0 is normal (and default) -- warnings only */
@@ -120,14 +126,14 @@ struct CVC4_PUBLIC Options {
   Options() :
     binary_name(),
     statistics(false),
-    in(std::cin),
-    out(std::cout),
-    err(std::cerr),
+    in(&std::cin),
+    out(&std::cout),
+    err(&std::cerr),
     verbosity(0),
     inputLanguage(language::input::LANG_AUTO),
     uf_implementation(MORGAN),
     parseOnly(false),
-    semanticChecks(true),
+    semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
     memoryMap(false),
     strictParsing(false),
     lazyDefinitionExpansion(false),
@@ -136,7 +142,7 @@ struct CVC4_PUBLIC Options {
     segvNoSpin(false),
     produceModels(false),
     produceAssignments(false),
-    typeChecking(true),
+    typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
     earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
   }