diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
commit | 2b87789ee57a738cccd89dd9d2d81b065875dc29 (patch) | |
tree | f5376c532490088e5dcc7a37ed318127a0dc8c40 /src/util | |
parent | 7f5036bb37e13dbc7e176d4fa82ee0736d11e913 (diff) |
* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h index 8f03ecd45..3b42f2887 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -24,6 +24,8 @@ #include "cvc4_config.h" #include "config.h" +#include <cassert> + namespace CVC4 { class CVC4_PUBLIC AssertionException : public Exception { @@ -196,6 +198,8 @@ public: throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) +#define DtorAlwaysAssert(cond, msg...) \ + assert(EXPECT_TRUE( cond )) #define Unreachable(msg...) \ throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ @@ -215,9 +219,11 @@ public: #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) +# define DtorAssert(cond, msg...) assert(EXPECT_TRUE( cond )) # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +# define DtorAssert(cond, msg...) /*EXPECT_TRUE( cond )*/ # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ |