diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/util/Assert.h | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/util/Assert.h')
-rw-r--r-- | src/util/Assert.h | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h new file mode 100644 index 000000000..8fd970c6c --- /dev/null +++ b/src/util/Assert.h @@ -0,0 +1,111 @@ +/********************* -*- C++ -*- */ +/** assert.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Assertion utility classes, functions, and exceptions. + **/ + +#ifndef __CVC4__ASSERT_H +#define __CVC4__ASSERT_H + +#include <string> +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" + +namespace CVC4 { + +class CVC4_PUBLIC AssertionException : public Exception { +public: + AssertionException() : Exception() {} + AssertionException(std::string msg) : Exception(msg) {} + AssertionException(const char* msg) : Exception(msg) {} +};/* class AssertionException */ + +class CVC4_PUBLIC UnreachableCodeException : public AssertionException { +public: + UnreachableCodeException() : AssertionException() {} + UnreachableCodeException(std::string msg) : AssertionException(msg) {} + UnreachableCodeException(const char* msg) : AssertionException(msg) {} +};/* class UnreachableCodeException */ + +class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { +public: + UnhandledCaseException() : UnreachableCodeException() {} + UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {} + UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {} +};/* class UnhandledCaseException */ + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg) +#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg) + +#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg) +#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg) + +inline void AssertImpl(const char* info, bool cond, std::string msg) { + if(EXPECT_FALSE( ! cond )) + throw AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond, const char* msg) { + if(EXPECT_FALSE( ! cond )) + throw AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond) { + if(EXPECT_FALSE( ! cond )) + throw AssertionException(info); +} + +#ifdef __GNUC__ +inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnreachableImpl(const char* info, std::string msg) { + throw UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info, const char* msg) { + throw UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info) { + throw UnreachableCodeException(info); +} + +#ifdef __GNUC__ +inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnhandledImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnhandledImpl(const char* info, std::string msg) { + throw UnhandledCaseException(std::string(info) + "\n" + msg); +} + +inline void UnhandledImpl(const char* info, const char* msg) { + throw UnhandledCaseException(std::string(info) + "\n" + msg); +} + +inline void UnhandledImpl(const char* info) { + throw UnhandledCaseException(info); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__ASSERT_H */ |