diff options
Diffstat (limited to 'src/main/interactive_shell.cpp')
| -rw-r--r-- | src/main/interactive_shell.cpp | 57 |
1 files changed, 30 insertions, 27 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 904cba276..127b2c14d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -101,7 +101,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) #if HAVE_LIBEDITLINE if(&d_in == &cin) { - ::rl_readline_name = const_cast<char*>("CVC4"); + ::rl_readline_name = const_cast<char*>("cvc5"); #if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP ::rl_completion_entry_function = commandGenerator; #else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */ @@ -111,30 +111,32 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage()); switch(lang) { - 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_TPTP: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; - commandsBegin = tptp_commands; - commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); - break; - default: - if (language::isOutputLang_smt2(lang)) - { - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; - commandsBegin = smt2_commands; + case output::LANG_CVC: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; + commandsBegin = cvc_commands; commandsEnd = - smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); - } - else - { - std::stringstream ss; - ss << "internal error: unhandled language " << lang; - throw Exception(ss.str()); - } + cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); + break; + case output::LANG_TPTP: + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; + commandsBegin = tptp_commands; + commandsEnd = + tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); + break; + default: + if (language::isOutputLang_smt2(lang)) + { + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; + commandsBegin = smt2_commands; + commandsEnd = + smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); + } + else + { + std::stringstream ss; + ss << "internal error: unhandled language " << lang; + throw Exception(ss.str()); + } } d_usingEditline = true; int err = ::read_history(d_historyFilename.c_str()); @@ -194,7 +196,8 @@ restart: { #if HAVE_LIBEDITLINE lineBuf = ::readline(d_options.getInteractivePrompt() - ? (line == "" ? "CVC4> " : "... > ") : ""); + ? (line == "" ? "cvc5> " : "... > ") + : ""); if(lineBuf != NULL && lineBuf[0] != '\0') { ::add_history(lineBuf); } @@ -206,7 +209,7 @@ restart: { if(d_options.getInteractivePrompt()) { if(line == "") { - d_out << "CVC4> " << flush; + d_out << "cvc5> " << flush; } else { d_out << "... > " << flush; } @@ -367,7 +370,7 @@ restart: // because the parse error might be for the second command on the // line. The first ones haven't yet been executed by the SmtEngine, // but the parser state has already made the variables and the mappings - // in the symbol table. So unfortunately, either we exit CVC4 entirely, + // in the symbol table. So unfortunately, either we exit cvc5 entirely, // or we commit to the current line up to the command with the parse // error. // |