diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/main | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver.cpp | 2 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 2 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 18 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 2 |
4 files changed, 14 insertions, 10 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index fa42e0b28..eb70f5c93 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -259,7 +259,7 @@ int runCvc4(int argc, char* argv[], Options& options) { ParserBuilder parserBuilder(&exprMgr, filename, options); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parserBuilder.withLineBufferedStreamInput(cin); } Parser *parser = parserBuilder.build(); diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index d17d00c5d..363901c1d 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -428,7 +428,7 @@ int runCvc4(int argc, char *argv[], Options& options) { withOptions(options); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parserBuilder.withLineBufferedStreamInput(cin); } Parser *parser = parserBuilder.build(); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index a63d6c67b..d8e7df2f2 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -83,7 +83,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, const Options& options) : d_in(*options.in), d_out(*options.out), - d_language(options.inputLanguage), + d_options(options), d_quit(false) { ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options); /* Create parser with bogus input. */ @@ -95,7 +95,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, ::rl_completion_entry_function = commandGenerator; ::using_history(); - switch(OutputLanguage lang = toOutputLanguage(d_language)) { + switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) { case output::LANG_CVC4: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; @@ -166,7 +166,7 @@ Command* InteractiveShell::readCommand() { /* Prompt the user for input. */ if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline("CVC4> "); + lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -174,7 +174,9 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - d_out << "CVC4> " << flush; + if(d_options.verbosity >= 0) { + d_out << "CVC4> " << flush; + } /* Read a line */ d_in.get(sb,'\n'); @@ -229,7 +231,7 @@ Command* InteractiveShell::readCommand() { input[n] = '\n'; if(d_usingReadline) { #if HAVE_LIBREADLINE - lineBuf = ::readline("... > "); + lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -237,7 +239,9 @@ Command* InteractiveShell::readCommand() { free(lineBuf); #endif /* HAVE_LIBREADLINE */ } else { - d_out << "... > " << flush; + if(d_options.verbosity >= 0) { + d_out << "... > " << flush; + } /* Read a line */ d_in.get(sb,'\n'); @@ -250,7 +254,7 @@ Command* InteractiveShell::readCommand() { } } - d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME)); + d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME)); /* There may be more than one command in the input. Build up a sequence. */ diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 65fea8494..7f17b88d7 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -36,7 +36,7 @@ class CVC4_PUBLIC InteractiveShell { std::istream& d_in; std::ostream& d_out; parser::Parser* d_parser; - const InputLanguage d_language; + const Options& d_options; bool d_quit; bool d_usingReadline; |