InteractiveShell: Remove redundant options argument. (#2244)

3 files changed, 27 insertions, 29 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 0d0ba3f90..898ffc6bd 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -282,7 +282,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 #endif /* PORTFOLIO_BUILD */
-      InteractiveShell shell(*exprMgr, opts);
+      InteractiveShell shell(*exprMgr);
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 473f7b039..f1220b961 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -88,14 +88,13 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBREADLINE */
 
-InteractiveShell::InteractiveShell(ExprManager& exprManager,
-                                   const Options& options)
-    : d_in(*options.getIn()),
-      d_out(*options.getOutConst()),
-      d_options(options),
+InteractiveShell::InteractiveShell(ExprManager& exprManager)
+    : d_options(exprManager.getOptions()),
+      d_in(*d_options.getIn()),
+      d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
+  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index b512fe5f0..203dfb766 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Tim King
+ **   Morgan Deters, Christopher L. Conway, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -32,11 +32,12 @@ namespace parser {
   class Parser;
 }/* CVC4::parser namespace */
 
-class CVC4_PUBLIC InteractiveShell {
+class CVC4_PUBLIC InteractiveShell
+{
+  const Options& d_options;
   std::istream& d_in;
   std::ostream& d_out;
   parser::Parser* d_parser;
-  const Options& d_options;
   bool d_quit;
   bool d_usingReadline;
 
@@ -46,25 +47,23 @@ class CVC4_PUBLIC InteractiveShell {
   static const unsigned s_historyLimit = 500;
 
 public:
-  InteractiveShell(ExprManager& exprManager, const Options& options);
-
-  /**
-   * Close out the interactive session.
-   */
-  ~InteractiveShell();
-
-  /**
-   * Read a command from the interactive shell. This will read as
-   * many lines as necessary to parse a well-formed command.
-   */
-  Command* readCommand();
-
-  /**
-   * Return the internal parser being used.
-   */
-  parser::Parser* getParser() {
-    return d_parser;
-  }
+ InteractiveShell(ExprManager& exprManager);
+
+ /**
+  * Close out the interactive session.
+  */
+ ~InteractiveShell();
+
+ /**
+  * Read a command from the interactive shell. This will read as
+  * many lines as necessary to parse a well-formed command.
+  */
+ Command* readCommand();
+
+ /**
+  * Return the internal parser being used.
+  */
+ parser::Parser* getParser() { return d_parser; }
 
 };/* class InteractiveShell */