diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/main/interactive_shell.cpp | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r-- | src/main/interactive_shell.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 719c8f61d..4f75779af 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -37,6 +37,7 @@ #include "util/language.h" #include <string.h> +#include <cassert> #if HAVE_LIBREADLINE # include <readline/readline.h> @@ -121,7 +122,9 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); break; default: - Unhandled(lang); + std::stringstream ss; + ss << "internal error: unhandled language " << lang; + throw Exception(ss.str()); } d_usingReadline = true; int err = ::read_history(d_historyFilename.c_str()); @@ -195,12 +198,12 @@ Command* InteractiveShell::readCommand() { while(true) { Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; - Assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); + assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); /* Check for failure. */ if(d_in.fail() && !d_in.eof()) { /* This should only happen if the input line was empty. */ - Assert( line.empty() ); + assert( line.empty() ); d_in.clear(); } @@ -229,7 +232,7 @@ Command* InteractiveShell::readCommand() { if(!d_usingReadline) { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - Assert( c == '\n' ); + assert( c == '\n' ); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } |