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/interactive_shell.h | |
| 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/interactive_shell.h')
| -rw-r--r-- | src/main/interactive_shell.h | 8 |
1 files changed, 8 insertions, 0 deletions
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. */ |