From f87f038c5f0821d0fefb01cea00bfdec6004da91 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 9 Apr 2021 17:22:07 -0700 Subject: Rename CVC4_ macros to CVC5_. (#6327) --- src/main/driver_unified.cpp | 26 +++++++++++++------------- src/main/interactive_shell.cpp | 2 +- src/main/main.cpp | 4 ++-- src/main/main.h | 2 +- src/main/signal_handlers.cpp | 22 +++++++++++----------- 5 files changed, 28 insertions(+), 28 deletions(-) (limited to 'src/main') diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index ec141d13a..9488b5c6d 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -121,9 +121,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { segvSpin = opts.getSegvSpin(); // If in competition mode, set output stream option to flush immediately -#ifdef CVC4_COMPETITION_MODE +#ifdef CVC5_COMPETITION_MODE *(opts.getOut()) << unitbuf; -#endif /* CVC4_COMPETITION_MODE */ +#endif /* CVC5_COMPETITION_MODE */ // We only accept one input file if(filenames.size() > 1) { @@ -260,11 +260,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts); if( inputFromStdin ) { -#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) +#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK) parserBuilder.withStreamInput(cin); -#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ +#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ parserBuilder.withLineBufferedStreamInput(cin); -#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ +#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ } vector< vector > allCommands; @@ -416,11 +416,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts); if( inputFromStdin ) { -#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) +#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK) parserBuilder.withStreamInput(cin); -#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ +#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ parserBuilder.withLineBufferedStreamInput(cin); -#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ +#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ } std::unique_ptr parser(parserBuilder.build()); @@ -461,26 +461,26 @@ int runCvc4(int argc, char* argv[], Options& opts) { returnValue = 1; } -#ifdef CVC4_COMPETITION_MODE +#ifdef CVC5_COMPETITION_MODE opts.flushOut(); // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors // or other on_exit/atexit stuff. _exit(returnValue); -#endif /* CVC4_COMPETITION_MODE */ +#endif /* CVC5_COMPETITION_MODE */ totalTime.reset(); pExecutor->flushOutputStreams(); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) { _exit(returnValue); } -#else /* CVC4_DEBUG */ +#else /* CVC5_DEBUG */ if(opts.getEarlyExit()) { _exit(returnValue); } -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ } pExecutor.reset(); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 0ddd8707a..e6ae7ad5d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -261,7 +261,7 @@ restart: if (!d_usingEditline) { /* Extract the newline delimiter from the stream too */ - int c CVC4_UNUSED = d_in.get(); + int c CVC5_UNUSED = d_in.get(); Assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; diff --git a/src/main/main.cpp b/src/main/main.cpp index 2a8bc7ab2..37c122732 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -50,14 +50,14 @@ int main(int argc, char* argv[]) { try { return runCvc4(argc, argv, opts); } catch(OptionException& e) { -#ifdef CVC4_COMPETITION_MODE +#ifdef CVC5_COMPETITION_MODE *opts.getOut() << "unknown" << endl; #endif cerr << "(error \"" << e << "\")" << endl << endl << "Please use --help to get help on command-line options." << endl; } catch(Exception& e) { -#ifdef CVC4_COMPETITION_MODE +#ifdef CVC5_COMPETITION_MODE *opts.getOut() << "unknown" << endl; #endif if (language::isOutputLang_smt2(opts.getOutputLanguage())) diff --git a/src/main/main.h b/src/main/main.h index 3f35a9ad4..c263e9d7a 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -54,7 +54,7 @@ class TotalTimer extern std::unique_ptr totalTime; /** - * If true, will not spin on segfault even when CVC4_DEBUG is on. + * If true, will not spin on segfault even when CVC5_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs * etc. See util.cpp. */ diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index 02544c7e3..a29872c95 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -47,7 +47,7 @@ namespace cvc5 { namespace main { /** - * If true, will not spin on segfault even when CVC4_DEBUG is on. + * If true, will not spin on segfault even when CVC5_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs * etc. */ @@ -103,7 +103,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) { uintptr_t extent = reinterpret_cast(cvc4StackBase) - cvc4StackSize; uintptr_t addr = reinterpret_cast(info->si_addr); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG safe_print(STDERR_FILENO, "CVC4 suffered a segfault in DEBUG mode.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); @@ -148,7 +148,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) sleep(60); } } -#else /* CVC4_DEBUG */ +#else /* CVC5_DEBUG */ safe_print(STDERR_FILENO, "CVC4 suffered a segfault.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); @@ -167,14 +167,14 @@ void segv_handler(int sig, siginfo_t* info, void* c) } print_statistics(); abort(); -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ } #endif /* HAVE_SIGALTSTACK */ /** Handler for SIGILL (illegal instruction). */ void ill_handler(int sig, siginfo_t* info, void*) { -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if (!segvSpin) @@ -201,11 +201,11 @@ void ill_handler(int sig, siginfo_t* info, void*) sleep(60); } } -#else /* CVC4_DEBUG */ +#else /* CVC5_DEBUG */ safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n"); print_statistics(); abort(); -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ } #endif /* __WIN32__ */ @@ -215,7 +215,7 @@ static terminate_handler default_terminator; void cvc4terminate() { set_terminate(default_terminator); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer* current = LastExceptionBuffer::getCurrent(); LastExceptionBuffer::setCurrent(NULL); delete current; @@ -227,18 +227,18 @@ void cvc4terminate() "(Don't do that.)\n"); print_statistics(); default_terminator(); -#else /* CVC4_DEBUG */ +#else /* CVC5_DEBUG */ safe_print(STDERR_FILENO, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); print_statistics(); default_terminator(); -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ } void install() { -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer::setCurrent(new LastExceptionBuffer()); #endif -- cgit v1.2.3