diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/check.cpp | 8 | ||||
| -rw-r--r-- | src/base/check.h | 64 | ||||
| -rw-r--r-- | src/base/configuration.cpp | 72 | ||||
| -rw-r--r-- | src/base/configuration.h | 2 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 110 | ||||
| -rw-r--r-- | src/base/exception.cpp | 8 | ||||
| -rw-r--r-- | src/base/exception.h | 15 | ||||
| -rw-r--r-- | src/base/output.h | 53 |
8 files changed, 162 insertions, 170 deletions
diff --git a/src/base/check.cpp b/src/base/check.cpp index 3ecdb0287..4bbe8df57 100644 --- a/src/base/check.cpp +++ b/src/base/check.cpp @@ -98,7 +98,7 @@ void AssertArgumentException::construct(const char* header, setMessage(std::string(buf)); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); if (buffer != NULL) { @@ -107,7 +107,7 @@ void AssertArgumentException::construct(const char* header, buffer->setContents(buf); } } -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ delete[] buf; } @@ -157,7 +157,7 @@ void AssertArgumentException::construct(const char* header, setMessage(std::string(buf)); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); if (buffer != NULL) { @@ -166,7 +166,7 @@ void AssertArgumentException::construct(const char* header, buffer->setContents(buf); } } -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ delete[] buf; } diff --git a/src/base/check.h b/src/base/check.h index 91184336b..19329f14f 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -22,7 +22,7 @@ ** Assert is a AlwaysAssert that is only enabled in debug builds. ** Assert(pointer != nullptr); ** - ** CVC4_FATAL() can be used to indicate unreachable code. + ** CVC5_FATAL() can be used to indicate unreachable code. ** ** The AlwaysAssert and Assert macros are not safe for use in ** signal-handling code. In future, a a signal-handling safe version of @@ -40,39 +40,39 @@ #include "base/exception.h" #include "cvc4_export.h" -// Define CVC4_NO_RETURN macro replacement for [[noreturn]]. +// Define CVC5_NO_RETURN macro replacement for [[noreturn]]. #if defined(SWIG) -#define CVC4_NO_RETURN +#define CVC5_NO_RETURN // SWIG does not yet support [[noreturn]] so emit nothing instead. #else -#define CVC4_NO_RETURN [[noreturn]] +#define CVC5_NO_RETURN [[noreturn]] // Not checking for whether the compiler supports [[noreturn]] using // __has_cpp_attribute as GCC 4.8 is too widespread and does not support this. // We instead assume this is C++11 (or later) and [[noreturn]] is available. #endif // defined(SWIG) -// Define CVC4_PREDICT_FALSE(x) that helps the compiler predict that x will be +// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be // false (if there is compiler support). #ifdef __has_builtin #if __has_builtin(__builtin_expect) -#define CVC4_PREDICT_FALSE(x) (__builtin_expect(x, false)) -#define CVC4_PREDICT_TRUE(x) (__builtin_expect(x, true)) +#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) +#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) #else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x #endif #else -#define CVC4_PREDICT_FALSE(x) x -#define CVC4_PREDICT_TRUE(x) x +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x #endif #ifdef __has_cpp_attribute #if __has_cpp_attribute(fallthrough) -#define CVC4_FALLTHROUGH [[fallthrough]] +#define CVC5_FALLTHROUGH [[fallthrough]] #endif // __has_cpp_attribute(fallthrough) #endif // __has_cpp_attribute -#ifndef CVC4_FALLTHROUGH -#define CVC4_FALLTHROUGH +#ifndef CVC5_FALLTHROUGH +#define CVC5_FALLTHROUGH #endif namespace cvc5 { @@ -96,7 +96,7 @@ class CVC4_EXPORT FatalStream { public: FatalStream(const char* function, const char* file, int line); - CVC4_NO_RETURN ~FatalStream(); + CVC5_NO_RETURN ~FatalStream(); std::ostream& stream(); @@ -114,7 +114,7 @@ class OstreamVoider void operator&(std::ostream&) {} }; -// CVC4_FATAL() always aborts a function and provides a convenient way of +// CVC5_FATAL() always aborts a function and provides a convenient way of // formatting error messages. This can be used instead of a return type. // // Example function that returns a type Foo: @@ -122,13 +122,13 @@ class OstreamVoider // switch(t.type()) { // ... // default: -// CVC4_FATAL() << "Unknown T type " << t.enum(); +// CVC5_FATAL() << "Unknown T type " << t.enum(); // } // } -#define CVC4_FATAL() \ +#define CVC5_FATAL() \ FatalStream(__PRETTY_FUNCTION__, __FILE__, __LINE__).stream() -/* GCC <= 9.2 ignores CVC4_NO_RETURN of ~FatalStream() if +/* GCC <= 9.2 ignores CVC5_NO_RETURN of ~FatalStream() if * used in template classes (e.g., CDHashMap::save()). As a workaround we * explicitly call abort() to let the compiler know that the * corresponding function call will not return. */ @@ -137,8 +137,8 @@ class OstreamVoider // If `cond` is true, log an error message and abort the process. // Otherwise, does nothing. This leaves a hanging std::ostream& that can be // inserted into. -#define CVC4_FATAL_IF(cond, function, file, line) \ - CVC4_PREDICT_FALSE(!(cond)) \ +#define CVC5_FATAL_IF(cond, function, file, line) \ + CVC5_PREDICT_FALSE(!(cond)) \ ? (void)0 : OstreamVoider() & FatalStream(function, file, line).stream() // If `cond` is false, log an error message and abort()'s the process. @@ -149,16 +149,16 @@ class OstreamVoider // AlwaysAssert(x >= 0) << "expected a positive value. Got " << x << " // instead"; #define AlwaysAssert(cond) \ - CVC4_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ + CVC5_FATAL_IF(!(cond), __PRETTY_FUNCTION__, __FILE__, __LINE__) \ << "Check failure\n\n " << #cond << "\n" // Assert is a variant of AlwaysAssert() that is only checked when -// CVC4_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. -#ifdef CVC4_ASSERTIONS +// CVC5_ASSERTIONS is defined. We rely on the optimizer to remove the deadcode. +#ifdef CVC5_ASSERTIONS #define Assert(cond) AlwaysAssert(cond) #else #define Assert(cond) \ - CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) + CVC5_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) #endif class AssertArgumentException : public Exception @@ -197,13 +197,13 @@ class AssertArgumentException : public Exception }; /* class AssertArgumentException */ -#define Unreachable() CVC4_FATAL() << "Unreachable code reached" +#define Unreachable() CVC5_FATAL() << "Unreachable code reached" -#define Unhandled() CVC4_FATAL() << "Unhandled case encountered" +#define Unhandled() CVC5_FATAL() << "Unhandled case encountered" -#define Unimplemented() CVC4_FATAL() << "Unimplemented code encountered" +#define Unimplemented() CVC5_FATAL() << "Unimplemented code encountered" -#define InternalError() CVC4_FATAL() << "Internal error detected" +#define InternalError() CVC5_FATAL() << "Internal error detected" #define IllegalArgument(arg, msg...) \ throw ::cvc5::IllegalArgumentException( \ @@ -235,15 +235,15 @@ class AssertArgumentException : public Exception } \ } while (0) -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS #define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ##msg) #define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ##msg) -#else /* ! CVC4_ASSERTIONS */ +#else /* ! CVC5_ASSERTIONS */ #define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true \ )*/ #define DebugCheckArgument( \ cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } // namespace cvc5 diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 561500a16..74bcdc57f 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -26,21 +26,19 @@ #include "cvc4autoconfig.h" #include "base/configuration_private.h" -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) # include "base/Debug_tags.h" -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ -#ifdef CVC4_TRACING +#ifdef CVC5_TRACING # include "base/Trace_tags.h" -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ using namespace std; namespace cvc5 { -string Configuration::getName() { - return CVC4_PACKAGE_NAME; -} +string Configuration::getName() { return CVC5_PACKAGE_NAME; } bool Configuration::isDebugBuild() { return IS_DEBUG_BUILD; @@ -82,36 +80,24 @@ bool Configuration::isCompetitionBuild() { bool Configuration::isStaticBuild() { -#if defined(CVC4_STATIC_BUILD) +#if defined(CVC5_STATIC_BUILD) return true; #else return false; #endif } -string Configuration::getPackageName() { - return CVC4_PACKAGE_NAME; -} +string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; } -string Configuration::getVersionString() { - return CVC4_RELEASE_STRING; -} +string Configuration::getVersionString() { return CVC5_RELEASE_STRING; } -unsigned Configuration::getVersionMajor() { - return CVC4_MAJOR; -} +unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; } -unsigned Configuration::getVersionMinor() { - return CVC4_MINOR; -} +unsigned Configuration::getVersionMinor() { return CVC5_MINOR; } -unsigned Configuration::getVersionRelease() { - return CVC4_RELEASE; -} +unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; } -std::string Configuration::getVersionExtra() { - return CVC4_EXTRAVERSION; -} +std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; } std::string Configuration::copyright() { std::stringstream ss; @@ -230,7 +216,7 @@ std::string Configuration::copyright() { std::string Configuration::about() { std::stringstream ss; - ss << "This is CVC4 version " << CVC4_RELEASE_STRING; + ss << "This is CVC4 version " << CVC5_RELEASE_STRING; if (Configuration::isGitBuild()) { ss << " [" << Configuration::getGitId() << "]"; } @@ -278,21 +264,21 @@ bool Configuration::isBuiltWithPoly() bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; } unsigned Configuration::getNumDebugTags() { -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) /* -1 because a NULL pointer is inserted as the last value */ return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1; -#else /* CVC4_DEBUG && CVC4_TRACING */ +#else /* CVC5_DEBUG && CVC5_TRACING */ return 0; -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ } char const* const* Configuration::getDebugTags() { -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) return Debug_tags; -#else /* CVC4_DEBUG && CVC4_TRACING */ +#else /* CVC5_DEBUG && CVC5_TRACING */ static char const* no_tags[] = { NULL }; return no_tags; -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ } int strcmpptr(const char **s1, const char **s2){ @@ -300,7 +286,7 @@ int strcmpptr(const char **s1, const char **s2){ } bool Configuration::isDebugTag(char const *tag){ -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) unsigned ntags = getNumDebugTags(); char const* const* tags = getDebugTags(); for (unsigned i = 0; i < ntags; ++ i) { @@ -308,30 +294,30 @@ bool Configuration::isDebugTag(char const *tag){ return true; } } -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ return false; } unsigned Configuration::getNumTraceTags() { -#if CVC4_TRACING +#if CVC5_TRACING /* -1 because a NULL pointer is inserted as the last value */ return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1; -#else /* CVC4_TRACING */ +#else /* CVC5_TRACING */ return 0; -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ } char const* const* Configuration::getTraceTags() { -#if CVC4_TRACING +#if CVC5_TRACING return Trace_tags; -#else /* CVC4_TRACING */ +#else /* CVC5_TRACING */ static char const* no_tags[] = { NULL }; return no_tags; -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ } bool Configuration::isTraceTag(char const * tag){ -#if CVC4_TRACING +#if CVC5_TRACING unsigned ntags = getNumTraceTags(); char const* const* tags = getTraceTags(); for (unsigned i = 0; i < ntags; ++ i) { @@ -339,7 +325,7 @@ bool Configuration::isTraceTag(char const * tag){ return true; } } -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ return false; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 6754923ed..3d30682fd 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -50,7 +50,7 @@ public: static constexpr bool isStatisticsBuild() { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON return true; #else return false; diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 754c8002f..ce6397682 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -24,101 +24,101 @@ namespace cvc5 { -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG # define IS_DEBUG_BUILD true -#else /* CVC4_DEBUG */ +#else /* CVC5_DEBUG */ # define IS_DEBUG_BUILD false -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ -#ifdef CVC4_TRACING +#ifdef CVC5_TRACING # define IS_TRACING_BUILD true -#else /* CVC4_TRACING */ +#else /* CVC5_TRACING */ # define IS_TRACING_BUILD false -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ -#ifdef CVC4_DUMPING +#ifdef CVC5_DUMPING # define IS_DUMPING_BUILD true -#else /* CVC4_DUMPING */ +#else /* CVC5_DUMPING */ # define IS_DUMPING_BUILD false -#endif /* CVC4_DUMPING */ +#endif /* CVC5_DUMPING */ -#ifdef CVC4_MUZZLE +#ifdef CVC5_MUZZLE # define IS_MUZZLED_BUILD true -#else /* CVC4_MUZZLE */ +#else /* CVC5_MUZZLE */ # define IS_MUZZLED_BUILD false -#endif /* CVC4_MUZZLE */ +#endif /* CVC5_MUZZLE */ -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS # define IS_ASSERTIONS_BUILD true -#else /* CVC4_ASSERTIONS */ +#else /* CVC5_ASSERTIONS */ # define IS_ASSERTIONS_BUILD false -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ -#ifdef CVC4_COVERAGE +#ifdef CVC5_COVERAGE # define IS_COVERAGE_BUILD true -#else /* CVC4_COVERAGE */ +#else /* CVC5_COVERAGE */ # define IS_COVERAGE_BUILD false -#endif /* CVC4_COVERAGE */ +#endif /* CVC5_COVERAGE */ -#ifdef CVC4_PROFILING +#ifdef CVC5_PROFILING # define IS_PROFILING_BUILD true -#else /* CVC4_PROFILING */ +#else /* CVC5_PROFILING */ # define IS_PROFILING_BUILD false -#endif /* CVC4_PROFILING */ +#endif /* CVC5_PROFILING */ -#ifdef CVC4_COMPETITION_MODE +#ifdef CVC5_COMPETITION_MODE # define IS_COMPETITION_BUILD true -#else /* CVC4_COMPETITION_MODE */ +#else /* CVC5_COMPETITION_MODE */ # define IS_COMPETITION_BUILD false -#endif /* CVC4_COMPETITION_MODE */ +#endif /* CVC5_COMPETITION_MODE */ -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP # define IS_GMP_BUILD true -#else /* CVC4_GMP_IMP */ +#else /* CVC5_GMP_IMP */ # define IS_GMP_BUILD false -#endif /* CVC4_GMP_IMP */ +#endif /* CVC5_GMP_IMP */ -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP # define IS_CLN_BUILD true -#else /* CVC4_CLN_IMP */ +#else /* CVC5_CLN_IMP */ # define IS_CLN_BUILD false -#endif /* CVC4_CLN_IMP */ +#endif /* CVC5_CLN_IMP */ -#if CVC4_USE_GLPK +#if CVC5_USE_GLPK # define IS_GLPK_BUILD true -#else /* CVC4_USE_GLPK */ +#else /* CVC5_USE_GLPK */ # define IS_GLPK_BUILD false -#endif /* CVC4_USE_GLPK */ +#endif /* CVC5_USE_GLPK */ -#if CVC4_USE_ABC +#if CVC5_USE_ABC # define IS_ABC_BUILD true -#else /* CVC4_USE_ABC */ +#else /* CVC5_USE_ABC */ # define IS_ABC_BUILD false -#endif /* CVC4_USE_ABC */ +#endif /* CVC5_USE_ABC */ -#if CVC4_USE_CADICAL +#if CVC5_USE_CADICAL #define IS_CADICAL_BUILD true -#else /* CVC4_USE_CADICAL */ +#else /* CVC5_USE_CADICAL */ #define IS_CADICAL_BUILD false -#endif /* CVC4_USE_CADICAL */ +#endif /* CVC5_USE_CADICAL */ -#if CVC4_USE_CRYPTOMINISAT +#if CVC5_USE_CRYPTOMINISAT # define IS_CRYPTOMINISAT_BUILD true -#else /* CVC4_USE_CRYPTOMINISAT */ +#else /* CVC5_USE_CRYPTOMINISAT */ # define IS_CRYPTOMINISAT_BUILD false -#endif /* CVC4_USE_CRYPTOMINISAT */ +#endif /* CVC5_USE_CRYPTOMINISAT */ -#if CVC4_USE_KISSAT +#if CVC5_USE_KISSAT #define IS_KISSAT_BUILD true -#else /* CVC4_USE_KISSAT */ +#else /* CVC5_USE_KISSAT */ #define IS_KISSAT_BUILD false -#endif /* CVC4_USE_KISSAT */ +#endif /* CVC5_USE_KISSAT */ -#if CVC4_USE_POLY +#if CVC5_USE_POLY #define IS_POLY_BUILD true -#else /* CVC4_USE_POLY */ +#else /* CVC5_USE_POLY */ #define IS_POLY_BUILD false -#endif /* CVC4_USE_POLY */ +#endif /* CVC5_USE_POLY */ #if HAVE_LIBEDITLINE #define IS_EDITLINE_BUILD true @@ -126,17 +126,17 @@ namespace cvc5 { #define IS_EDITLINE_BUILD false #endif /* HAVE_LIBEDITLINE */ -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #define IS_SYMFPU_BUILD true #else /* HAVE_SYMFPU_HEADERS */ #define IS_SYMFPU_BUILD false #endif /* HAVE_SYMFPU_HEADERS */ -#if CVC4_GPL_DEPS +#if CVC5_GPL_DEPS # define IS_GPL_BUILD true -#else /* CVC4_GPL_DEPS */ +#else /* CVC5_GPL_DEPS */ # define IS_GPL_BUILD false -#endif /* CVC4_GPL_DEPS */ +#endif /* CVC5_GPL_DEPS */ #define IS_ASAN_BUILD false @@ -154,11 +154,11 @@ namespace cvc5 { # endif /* __has_feature(address_sanitizer) */ #endif /* defined(__has_feature) */ -#ifdef CVC4_USE_UBSAN +#ifdef CVC5_USE_UBSAN #define IS_UBSAN_BUILD true -#else /* CVC4_USE_UBSAN */ +#else /* CVC5_USE_UBSAN */ #define IS_UBSAN_BUILD false -#endif /* CVC4_USE_UBSAN */ +#endif /* CVC5_USE_UBSAN */ #define IS_TSAN_BUILD false diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 3c5c21b46..c6fb03834 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -135,14 +135,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra, setMessage(string(buf)); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); if(buffer != nullptr){ if(buffer->getContents() == nullptr) { buffer->setContents(buf); } } -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ delete [] buf; } @@ -176,14 +176,14 @@ void IllegalArgumentException::construct(const char* header, const char* extra, setMessage(string(buf)); -#ifdef CVC4_DEBUG +#ifdef CVC5_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); if(buffer != nullptr){ if(buffer->getContents() == nullptr) { buffer->setContents(buf); } } -#endif /* CVC4_DEBUG */ +#endif /* CVC5_DEBUG */ delete [] buf; } diff --git a/src/base/exception.h b/src/base/exception.h index f3a5326fc..579a8cdad 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -119,18 +119,23 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) template <class T> inline void CheckArgument(bool cond, const T& arg, const char* tail); -template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED, - const char* tail CVC4_UNUSED) { +template <class T> +inline void CheckArgument(bool cond, + const T& arg CVC5_UNUSED, + const char* tail CVC5_UNUSED) +{ if(__builtin_expect( ( !cond ), false )) { throw ::cvc5::IllegalArgumentException("", "", tail); - } \ + } } template <class T> inline void CheckArgument(bool cond, const T& arg); -template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED) { +template <class T> +inline void CheckArgument(bool cond, const T& arg CVC5_UNUSED) +{ if(__builtin_expect( ( !cond ), false )) { throw ::cvc5::IllegalArgumentException("", "", ""); - } \ + } } class CVC4_EXPORT LastExceptionBuffer diff --git a/src/base/output.h b/src/base/output.h index 856b81333..acad7e40b 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -410,7 +410,7 @@ extern TraceC TraceChannel CVC4_EXPORT; /** The dump output singleton */ extern DumpOutC DumpOutChannel CVC4_EXPORT; -#ifdef CVC4_MUZZLE +#ifdef CVC5_MUZZLE #define Debug \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DebugChannel @@ -429,14 +429,14 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; #define DumpOut \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DumpOutChannel -#else /* CVC4_MUZZLE */ +#else /* CVC5_MUZZLE */ -# if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) #define Debug ::cvc5::DebugChannel -# else /* CVC4_DEBUG && CVC4_TRACING */ +#else /* CVC5_DEBUG && CVC5_TRACING */ #define Debug \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DebugChannel -# endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ #define Warning \ (!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullCvc4Stream \ : ::cvc5::WarningChannel @@ -453,35 +453,36 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; : ::cvc5::NoticeChannel #define Chat \ (!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullCvc4Stream : ::cvc5::ChatChannel -# ifdef CVC4_TRACING +#ifdef CVC5_TRACING #define Trace ::cvc5::TraceChannel -# else /* CVC4_TRACING */ +#else /* CVC5_TRACING */ #define Trace \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::TraceChannel -# endif /* CVC4_TRACING */ -# ifdef CVC4_DUMPING +#endif /* CVC5_TRACING */ +#ifdef CVC5_DUMPING #define DumpOut ::cvc5::DumpOutChannel -# else /* CVC4_DUMPING */ +#else /* CVC5_DUMPING */ #define DumpOut \ ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DumpOutChannel -# endif /* CVC4_DUMPING */ +#endif /* CVC5_DUMPING */ -#endif /* CVC4_MUZZLE */ +#endif /* CVC5_MUZZLE */ // Disallow e.g. !Debug("foo").isOn() forms // because the ! will apply before the ? . // If a compiler error has directed you here, // just parenthesize it e.g. !(Debug("foo").isOn()) class __cvc4_true { - void operator!() CVC4_UNUSED; - void operator~() CVC4_UNUSED; - void operator-() CVC4_UNUSED; - void operator+() CVC4_UNUSED; -public: + void operator!() CVC5_UNUSED; + void operator~() CVC5_UNUSED; + void operator-() CVC5_UNUSED; + void operator+() CVC5_UNUSED; + + public: inline operator bool() { return true; } };/* __cvc4_true */ -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) class ScopedDebug { @@ -509,7 +510,7 @@ public: } }; /* class ScopedDebug */ -#else /* CVC4_DEBUG && CVC4_TRACING */ +#else /* CVC5_DEBUG && CVC5_TRACING */ class ScopedDebug { @@ -517,9 +518,9 @@ class ScopedDebug ScopedDebug(std::string tag, bool newSetting = true) {} }; /* class ScopedDebug */ -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ -#ifdef CVC4_TRACING +#ifdef CVC5_TRACING class ScopedTrace { @@ -547,7 +548,7 @@ public: } }; /* class ScopedTrace */ -#else /* CVC4_TRACING */ +#else /* CVC5_TRACING */ class ScopedTrace { @@ -555,7 +556,7 @@ class ScopedTrace ScopedTrace(std::string tag, bool newSetting = true) {} }; /* class ScopedTrace */ -#endif /* CVC4_TRACING */ +#endif /* CVC5_TRACING */ /** * Pushes an indentation level on construction, pop on destruction. @@ -571,13 +572,13 @@ public: inline ~IndentedScope(); }; /* class IndentedScope */ -#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +#if defined(CVC5_DEBUG) && defined(CVC5_TRACING) inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } inline IndentedScope::~IndentedScope() { d_out << pop; } -#else /* CVC4_DEBUG && CVC4_TRACING */ +#else /* CVC5_DEBUG && CVC5_TRACING */ inline IndentedScope::IndentedScope(CVC4ostream out) {} inline IndentedScope::~IndentedScope() {} -#endif /* CVC4_DEBUG && CVC4_TRACING */ +#endif /* CVC5_DEBUG && CVC5_TRACING */ } // namespace cvc5 |