diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/main | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/interactive_shell.cpp | 26 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 8 |
2 files changed, 34 insertions, 0 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 8f1d54a3a..1d1f447be 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -18,6 +18,7 @@ **/ #include <iostream> +#include <cstdlib> #include <vector> #include <string> #include <set> @@ -92,23 +93,38 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, if(d_in == cin) { ::rl_readline_name = "CVC4"; ::rl_completion_entry_function = commandGenerator; + ::using_history(); switch(OutputLanguage lang = toOutputLanguage(d_language)) { case output::LANG_CVC4: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; case output::LANG_SMTLIB: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib"; commandsBegin = smt_commands; commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands); break; case output::LANG_SMTLIB_V2: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); break; default: Unhandled(lang); } d_usingReadline = true; + int err = ::read_history(d_historyFilename.c_str()); + ::stifle_history(s_historyLimit); + if(Notice.isOn()) { + if(err == 0) { + Notice() << "Read " << ::history_length << " lines of history from " + << d_historyFilename << std::endl; + } else { + Notice() << "Could not read history from " << d_historyFilename + << ": " << strerror(err) << std::endl; + } + } } else { d_usingReadline = false; } @@ -117,6 +133,16 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, #endif /* HAVE_LIBREADLINE */ }/* InteractiveShell::InteractiveShell() */ +InteractiveShell::~InteractiveShell() { + int err = ::write_history(d_historyFilename.c_str()); + if(err == 0) { + Notice() << "Wrote " << ::history_length << " lines of history to " + << d_historyFilename << std::endl; + } else { + Notice() << "Could not write history to " << d_historyFilename + << ": " << strerror(err) << std::endl; + } +} Command* InteractiveShell::readCommand() { /* Don't do anything if the input is closed or if we've seen a diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index f6852b95b..65fea8494 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -40,12 +40,20 @@ class CVC4_PUBLIC InteractiveShell { bool d_quit; bool d_usingReadline; + std::string d_historyFilename; + static const std::string INPUT_FILENAME; + 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. */ |