From 149134dfdb5a435ae4d1bea1a93ae3bde28fd646 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 1 Aug 2018 12:08:02 -0700 Subject: [PATCH] InteractiveShell: Remove redundant options argument. (#2244) --- src/main/driver_unified.cpp | 2 +- src/main/interactive_shell.cpp | 11 +++--- src/main/interactive_shell.h | 43 ++++++++++++------------ test/unit/main/interactive_shell_black.h | 29 ++++++++-------- 4 files changed, 42 insertions(+), 43 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 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 */ diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index e42172251..cf68b5465 100644 --- 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 ); } -- 2.30.2