diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/check.cpp | 4 | ||||
-rw-r--r-- | src/base/check.h | 14 | ||||
-rw-r--r-- | src/base/configuration.cpp | 7 | ||||
-rw-r--r-- | src/base/configuration.h | 4 | ||||
-rw-r--r-- | src/base/configuration_private.h | 4 | ||||
-rw-r--r-- | src/base/exception.cpp | 4 | ||||
-rw-r--r-- | src/base/exception.h | 12 | ||||
-rw-r--r-- | src/base/git_versioninfo.cpp.in | 8 | ||||
-rw-r--r-- | src/base/listener.cpp | 5 | ||||
-rw-r--r-- | src/base/listener.h | 4 | ||||
-rw-r--r-- | src/base/map_util.h | 8 | ||||
-rw-r--r-- | src/base/modal_exception.h | 8 | ||||
-rw-r--r-- | src/base/output.cpp | 4 | ||||
-rw-r--r-- | src/base/output.h | 63 |
14 files changed, 84 insertions, 65 deletions
diff --git a/src/base/check.cpp b/src/base/check.cpp index c19b30f6a..4aa6bfce0 100644 --- a/src/base/check.cpp +++ b/src/base/check.cpp @@ -19,7 +19,7 @@ #include <cstdlib> #include <iostream> -namespace CVC4 { +namespace CVC5 { FatalStream::FatalStream(const char* function, const char* file, int line) { @@ -209,4 +209,4 @@ AssertArgumentException::AssertArgumentException(const char* condStr, line); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/base/check.h b/src/base/check.h index 70c5c9016..1e46ea85c 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -75,7 +75,7 @@ #define CVC4_FALLTHROUGH #endif -namespace CVC4 { +namespace CVC5 { // Implementation notes: // To understand FatalStream and OStreamVoider, it is useful to understand @@ -206,11 +206,11 @@ class AssertArgumentException : public Exception #define InternalError() CVC4_FATAL() << "Internal error detected" #define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException( \ + throw ::CVC5::IllegalArgumentException( \ "", \ #arg, \ __PRETTY_FUNCTION__, \ - ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); + ::CVC5::IllegalArgumentException::formatVariadic(msg).c_str()); // This cannot use check argument directly as this forces // CheckArgument to use a va_list. This is unsupported in Swig. #define PrettyCheckArgument(cond, arg, msg...) \ @@ -218,11 +218,11 @@ class AssertArgumentException : public Exception { \ if (__builtin_expect((!(cond)), false)) \ { \ - throw ::CVC4::IllegalArgumentException( \ + throw ::CVC5::IllegalArgumentException( \ #cond, \ #arg, \ __PRETTY_FUNCTION__, \ - ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ + ::CVC5::IllegalArgumentException::formatVariadic(msg).c_str()); \ } \ } while (0) #define AlwaysAssertArgument(cond, arg, msg...) \ @@ -230,7 +230,7 @@ class AssertArgumentException : public Exception { \ if (__builtin_expect((!(cond)), false)) \ { \ - throw ::CVC4::AssertArgumentException( \ + throw ::CVC5::AssertArgumentException( \ #cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ##msg); \ } \ } while (0) @@ -245,6 +245,6 @@ class AssertArgumentException : public Exception cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/ #endif /* CVC4_ASSERTIONS */ -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__CHECK_H */ diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 39284227a..1b8be7bf9 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -36,7 +36,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { string Configuration::getName() { return CVC4_PACKAGE_NAME; @@ -375,7 +375,8 @@ std::string Configuration::getGitId() { stringstream ss; ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8) - << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" ); + << (::CVC5::Configuration::hasGitModifications() ? " (with modifications)" + : ""); return ss.str(); } @@ -398,4 +399,4 @@ std::string Configuration::getCompiledDateTime() { return __DATE__ " " __TIME__; } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/base/configuration.h b/src/base/configuration.h index ec8cc879b..c6cf3b229 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -25,7 +25,7 @@ #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { /** * Represents the (static) configuration of CVC4. @@ -135,6 +135,6 @@ public: }; /* class Configuration */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__CONFIGURATION_H */ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index cc1983734..7de4f0e97 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -22,7 +22,7 @@ #include "base/configuration.h" -namespace CVC4 { +namespace CVC5 { #ifdef CVC4_DEBUG # define IS_DEBUG_BUILD true @@ -182,6 +182,6 @@ namespace CVC4 { #endif /* __has_feature(thread_sanitizer) */ #endif /* defined(__has_feature) */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__CONFIGURATION_PRIVATE_H */ diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 43227cce5..631f1cc35 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -27,7 +27,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { std::string Exception::toString() const { @@ -187,4 +187,4 @@ void IllegalArgumentException::construct(const char* header, const char* extra, delete [] buf; } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/base/exception.h b/src/base/exception.h index d9bf83f44..a0ad0819c 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -25,7 +25,7 @@ #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { class Exception : public std::exception { @@ -121,15 +121,15 @@ 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) { - if(__builtin_expect( ( !cond ), false )) { \ - throw ::CVC4::IllegalArgumentException("", "", tail); \ + 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) { - if(__builtin_expect( ( !cond ), false )) { \ - throw ::CVC4::IllegalArgumentException("", "", ""); \ + if(__builtin_expect( ( !cond ), false )) { + throw ::CVC5::IllegalArgumentException("", "", ""); } \ } @@ -159,6 +159,6 @@ private: static thread_local LastExceptionBuffer* s_currentBuffer; }; /* class LastExceptionBuffer */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__EXCEPTION_H */ diff --git a/src/base/git_versioninfo.cpp.in b/src/base/git_versioninfo.cpp.in index 78f9115b0..333564b97 100644 --- a/src/base/git_versioninfo.cpp.in +++ b/src/base/git_versioninfo.cpp.in @@ -16,7 +16,7 @@ **/ #include "base/configuration.h" -const bool ::CVC4::Configuration::IS_GIT_BUILD = @GIT_BUILD@; -const char* const ::CVC4::Configuration::GIT_BRANCH_NAME = "@GIT_BRANCH@"; -const char* const ::CVC4::Configuration::GIT_COMMIT = "@GIT_SHA1@"; -const bool ::CVC4::Configuration::GIT_HAS_MODIFICATIONS = @GIT_IS_DIRTY@; +const bool ::CVC5::Configuration::IS_GIT_BUILD = @GIT_BUILD@; +const char* const ::CVC5::Configuration::GIT_BRANCH_NAME = "@GIT_BRANCH@"; +const char* const ::CVC5::Configuration::GIT_COMMIT = "@GIT_SHA1@"; +const bool ::CVC5::Configuration::GIT_HAS_MODIFICATIONS = @GIT_IS_DIRTY@; diff --git a/src/base/listener.cpp b/src/base/listener.cpp index 02a052a09..b7d92e6a3 100644 --- a/src/base/listener.cpp +++ b/src/base/listener.cpp @@ -16,10 +16,9 @@ #include "base/listener.h" -namespace CVC4 { +namespace CVC5 { Listener::Listener(){} Listener::~Listener(){} - -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/base/listener.h b/src/base/listener.h index 4205aca01..0bb81e63a 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -20,7 +20,7 @@ #ifndef CVC4__LISTENER_H #define CVC4__LISTENER_H -namespace CVC4 { +namespace CVC5 { /** * Listener interface class. @@ -37,6 +37,6 @@ class Listener virtual void notify() = 0; }; -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__LISTENER_H */ diff --git a/src/base/map_util.h b/src/base/map_util.h index 2af0113b5..f428a9943 100644 --- a/src/base/map_util.h +++ b/src/base/map_util.h @@ -16,8 +16,8 @@ ** new code. Supports: ** - std::map ** - std::unordered_map - ** - CVC4::context::CDHashmap - ** - CVC4::context::CDInsertHashmap + ** - CVC5::context::CDHashmap + ** - CVC5::context::CDInsertHashmap ** The ContainsKey function is also compatible with std::[unordered_]set. ** ** Currently implemented classes of functions: @@ -40,7 +40,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { // Returns true if the `map` contains the `key`. // @@ -92,6 +92,6 @@ const MapMappedTypeT<M>& FindOrDie(const M& map, const MapKeyTypeT<M>& key) return (*it).second; } -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__BASE__MAP_UTIL_H */ diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h index bfd5c9469..eab6c66b1 100644 --- a/src/base/modal_exception.h +++ b/src/base/modal_exception.h @@ -24,9 +24,9 @@ #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { -class ModalException : public CVC4::Exception +class ModalException : public CVC5::Exception { public: ModalException() : @@ -50,7 +50,7 @@ class ModalException : public CVC4::Exception * TODO(#1108): This exception should not be needed anymore in future versions * of the public API. */ -class RecoverableModalException : public CVC4::ModalException +class RecoverableModalException : public CVC5::ModalException { public: RecoverableModalException(const std::string& msg) : ModalException(msg) {} @@ -58,6 +58,6 @@ class RecoverableModalException : public CVC4::ModalException RecoverableModalException(const char* msg) : ModalException(msg) {} }; /* class RecoverableModalException */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__SMT__MODAL_EXCEPTION_H */ diff --git a/src/base/output.cpp b/src/base/output.cpp index 93ebf2a70..7876f0fbe 100644 --- a/src/base/output.cpp +++ b/src/base/output.cpp @@ -20,7 +20,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { /* Definitions of the declared globals from output.h... */ @@ -41,4 +41,4 @@ TraceC TraceChannel(&cout); std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer DumpOutC DumpOutChannel(&DumpOutC::dump_cout); -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/base/output.h b/src/base/output.h index 5791d6f8f..b1f15d98b 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -28,7 +28,7 @@ #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { template <class T, class U> std::ostream& operator<<(std::ostream& out, @@ -412,39 +412,58 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; #ifdef CVC4_MUZZLE -# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel -# define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel -# define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +#define Debug \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::DebugChannel +#define Warning \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::WarningChannel +#define WarningOnce \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::WarningChannel #define CVC4Message \ - ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel -# define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel -# define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel -# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel -# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::MessageChannel +#define Notice \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::NoticeChannel +#define Chat \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::ChatChannel +#define Trace \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::TraceChannel +#define DumpOut \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::DumpOutChannel #else /* CVC4_MUZZLE */ # if defined(CVC4_DEBUG) && defined(CVC4_TRACING) -# define Debug ::CVC4::DebugChannel +#define Debug ::CVC5::DebugChannel # else /* CVC4_DEBUG && CVC4_TRACING */ -# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel +#define Debug \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::DebugChannel # endif /* CVC4_DEBUG && CVC4_TRACING */ -# define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel -# define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel +#define Warning \ + (!::CVC5::WarningChannel.isOn()) ? ::CVC5::nullCvc4Stream \ + : ::CVC5::WarningChannel +#define WarningOnce \ + (!::CVC5::WarningChannel.isOn() \ + || !::CVC5::WarningChannel.warnOnce(__FILE__, __LINE__)) \ + ? ::CVC5::nullCvc4Stream \ + : ::CVC5::WarningChannel #define CVC4Message \ - (!::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream \ - : ::CVC4::MessageChannel -# define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel -# define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel + (!::CVC5::MessageChannel.isOn()) ? ::CVC5::nullCvc4Stream \ + : ::CVC5::MessageChannel +#define Notice \ + (!::CVC5::NoticeChannel.isOn()) ? ::CVC5::nullCvc4Stream \ + : ::CVC5::NoticeChannel +#define Chat \ + (!::CVC5::ChatChannel.isOn()) ? ::CVC5::nullCvc4Stream : ::CVC5::ChatChannel # ifdef CVC4_TRACING -# define Trace ::CVC4::TraceChannel +#define Trace ::CVC5::TraceChannel # else /* CVC4_TRACING */ -# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel +#define Trace \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::TraceChannel # endif /* CVC4_TRACING */ # ifdef CVC4_DUMPING -# define DumpOut ::CVC4::DumpOutChannel +#define DumpOut ::CVC5::DumpOutChannel # else /* CVC4_DUMPING */ -# define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel +#define DumpOut \ + ::CVC5::__cvc4_true() ? ::CVC5::nullCvc4Stream : ::CVC5::DumpOutChannel # endif /* CVC4_DUMPING */ #endif /* CVC4_MUZZLE */ @@ -560,6 +579,6 @@ inline IndentedScope::IndentedScope(CVC4ostream out) {} inline IndentedScope::~IndentedScope() {} #endif /* CVC4_DEBUG && CVC4_TRACING */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__OUTPUT_H */ |