summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/driver_unified.cpp2
-rw-r--r--src/main/interactive_shell.cpp11
-rw-r--r--src/main/interactive_shell.h43
-rw-r--r--test/unit/main/interactive_shell_black.h29
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<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 */
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 );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback