summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/driver_unified.cpp25
-rw-r--r--src/main/interactive_shell.cpp57
-rw-r--r--src/main/main.cpp2
-rw-r--r--src/main/signal_handlers.cpp18
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback