summaryrefslogtreecommitdiff
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/check.cpp4
-rw-r--r--src/base/check.h14
-rw-r--r--src/base/configuration.cpp7
-rw-r--r--src/base/configuration.h4
-rw-r--r--src/base/configuration_private.h4
-rw-r--r--src/base/exception.cpp4
-rw-r--r--src/base/exception.h12
-rw-r--r--src/base/git_versioninfo.cpp.in8
-rw-r--r--src/base/listener.cpp5
-rw-r--r--src/base/listener.h4
-rw-r--r--src/base/map_util.h8
-rw-r--r--src/base/modal_exception.h8
-rw-r--r--src/base/output.cpp4
-rw-r--r--src/base/output.h63
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback