InteractiveShell: Remove redundant options argument. (#2244)

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 0d0ba3f90ba13260b9eb24db515bbc614e87645a..898ffc6bdc8aaea9f3ef1adce96653ee005696b9 100644 (file)
--- 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 473f7b039b4405e1e6ce917fbc08cbc164f06bff..f1220b961c20f873a3a40c1f0fd23e4d03d3012f 100644 (file)
--- 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 b512fe5f0fe0a6aa0c7fdcdc04fc88bf4febf99f..203dfb766fab82512b41d9740cd7a35ddce86ad5 100644 (file)
--- 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 */
 

diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index e4217225179826517e2805880c6dd075f167fb60..cf68b5465b614ec3e1bd66c73b8c7fc0cbf3359d 100644 (file)
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -38,13 +38,14 @@ private:
   stringstream* d_sin;
   stringstream* d_sout;
 
-  /** Read up to maxCommands+1 from the shell and throw an assertion
-      error if it's fewer than minCommands and more than maxCommands.
-      Note that an empty string followed by EOF may be returned as an
-      empty command, and not NULL (subsequent calls to readCommand()
-      should return NULL). E.g., "CHECKSAT;\n" may return two
-      commands: the CHECKSAT, followed by an empty command, followed
-      by NULL. */
+  /**
+   * Read up to maxCommands+1 from the shell and throw an assertion error if
+   * it's fewer than minCommands and more than maxCommands.
+   * Note that an empty string followed by EOF may be returned as an empty
+   * command, and not NULL (subsequent calls to readCommand() should return
+   * NULL). E.g., "CHECKSAT;\n" may return two commands: the CHECKSAT,
+   * followed by an empty command, followed by NULL.
+   */
   void countCommands(InteractiveShell& shell, 
                      int minCommands, 
                      int maxCommands) {
@@ -60,12 +61,12 @@ private:
 
  public:
   void setUp() {
-    d_exprManager = new ExprManager;
     d_sin = new stringstream;
     d_sout = new stringstream;
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
+    d_exprManager = new ExprManager(d_options);
   }
 
   void tearDown() {
@@ -76,18 +77,18 @@ private:
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
     /* readCommand may return a sequence, so we can't say for sure
        whether it will return 1 or 2... */
@@ -95,7 +96,7 @@ private:
   }
 
   void testDefUse2() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -105,14 +106,14 @@ private:
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }