diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 25 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 57 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/main/signal_handlers.cpp | 18 |
4 files changed, 53 insertions, 49 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c5d89300c..2481eda10 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Driver for CVC4 executable (cvc4). + * Driver for cvc5 executable (cvc4). */ #include <stdio.h> @@ -78,11 +78,12 @@ TotalTimer::~TotalTimer() void printUsage(Options& opts, bool full) { stringstream ss; - ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" - << endl << endl - << "Without an input file, or with `-', CVC4 reads from standard input." - << endl << endl - << "CVC4 options:" << endl; + ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl + << endl + << "Without an input file, or with `-', cvc5 reads from standard input." + << endl + << endl + << "cvc5 options:" << endl; if(full) { Options::printUsage( ss.str(), *(opts.getOut()) ); } else { @@ -151,7 +152,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(opts.getInputLanguage() == language::input::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - opts.setInputLanguage(language::input::LANG_CVC4); + opts.setInputLanguage(language::input::LANG_CVC); } else { unsigned len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { @@ -161,7 +162,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.setInputLanguage(language::input::LANG_TPTP); } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts.setInputLanguage(language::input::LANG_CVC4); + opts.setInputLanguage(language::input::LANG_CVC); } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default @@ -211,17 +212,17 @@ int runCvc4(int argc, char* argv[], Options& opts) { InteractiveShell shell(pExecutor->getSolver(), pExecutor->getSymbolManager()); if(opts.getInteractivePrompt()) { - CVC4Message() << Configuration::getPackageName() << " " + CVC5Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); if(Configuration::isGitBuild()) { - CVC4Message() << " [" << Configuration::getGitId() << "]"; + CVC5Message() << " [" << Configuration::getGitId() << "]"; } - CVC4Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") + CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") << " assertions:" << (Configuration::isAssertionBuild() ? "on" : "off") << endl << endl; - CVC4Message() << Configuration::copyright() << endl; + CVC5Message() << Configuration::copyright() << endl; } while(true) { 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. // diff --git a/src/main/main.cpp b/src/main/main.cpp index 8532f9504..a4e70be89 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -38,7 +38,7 @@ using namespace cvc5::main; using namespace cvc5::language; /** - * CVC4's main() routine is just an exception-safe wrapper around CVC4. + * cvc5's main() routine is just an exception-safe wrapper around cvc5. * Please don't construct anything here. Even if the constructor is * inside the try { }, an exception during destruction can cause * problems. That's why main() wraps runCvc4() in the first place. diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index 1be6a7f35..9a6e34075 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -65,7 +65,7 @@ void print_statistics() void timeout_handler() { - safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n"); + safe_print(STDERR_FILENO, "cvc5 interrupted by timeout.\n"); print_statistics(); abort(); } @@ -83,7 +83,7 @@ void timeout_handler(int sig, siginfo_t* info, void*) { timeout_handler(); } /** Handler for SIGTERM. */ void sigterm_handler(int sig, siginfo_t* info, void*) { - safe_print(STDERR_FILENO, "CVC4 interrupted by SIGTERM.\n"); + safe_print(STDERR_FILENO, "cvc5 interrupted by SIGTERM.\n"); print_statistics(); abort(); } @@ -91,7 +91,7 @@ void sigterm_handler(int sig, siginfo_t* info, void*) /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { - safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n"); + safe_print(STDERR_FILENO, "cvc5 interrupted by user.\n"); print_statistics(); abort(); } @@ -103,7 +103,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize; uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr); #ifdef CVC5_DEBUG - safe_print(STDERR_FILENO, "CVC4 suffered a segfault in DEBUG mode.\n"); + safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); safe_print(STDERR_FILENO, "\n"); @@ -148,7 +148,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) } } #else /* CVC5_DEBUG */ - safe_print(STDERR_FILENO, "CVC4 suffered a segfault.\n"); + safe_print(STDERR_FILENO, "cvc5 suffered a segfault.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); safe_print(STDERR_FILENO, "\n"); @@ -175,7 +175,7 @@ void ill_handler(int sig, siginfo_t* info, void*) { #ifdef CVC5_DEBUG safe_print(STDERR_FILENO, - "CVC4 executed an illegal instruction in DEBUG mode.\n"); + "cvc5 executed an illegal instruction in DEBUG mode.\n"); if (!segvSpin) { print_statistics(); @@ -201,7 +201,7 @@ void ill_handler(int sig, siginfo_t* info, void*) } } #else /* CVC5_DEBUG */ - safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n"); + safe_print(STDERR_FILENO, "cvc5 executed an illegal instruction.\n"); print_statistics(); abort(); #endif /* CVC5_DEBUG */ @@ -221,14 +221,14 @@ void cvc4terminate() safe_print(STDERR_FILENO, "\n" - "CVC4 was terminated by the C++ runtime.\n" + "cvc5 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); print_statistics(); default_terminator(); #else /* CVC5_DEBUG */ safe_print(STDERR_FILENO, - "CVC4 was terminated by the C++ runtime.\n" + "cvc5 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); print_statistics(); default_terminator(); |