From: Morgan Deters Date: Fri, 28 Sep 2012 20:14:40 +0000 (+0000) Subject: rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it... X-Git-Tag: cvc5-1.0.0~7769 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c49dd8a78fcceeef058126797e6bbe44d23b6804;p=cvc5.git rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds --- diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h index e18d9b972..6b925cc3a 100644 --- a/src/context/cdchunk_list.h +++ b/src/context/cdchunk_list.h @@ -28,7 +28,7 @@ #include "context/context.h" #include "context/context_mm.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace context { diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 321a378bd..3967065bb 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -97,7 +97,7 @@ #include #include "context/context.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "context/cdhashmap_forward.h" namespace CVC4 { diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index 7e15cf9eb..544baed6b 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -24,7 +24,7 @@ #include "context/context.h" #include "context/cdhashset_forward.h" #include "context/cdhashmap.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace context { diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 4d8aea6cb..5f364897d 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -30,7 +30,7 @@ #include "context/context.h" #include "context/context_mm.h" #include "context/cdlist_forward.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include diff --git a/src/context/cdo.h b/src/context/cdo.h index 1fc1eebe6..a0f2bcd9d 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -22,7 +22,7 @@ #define __CVC4__CONTEXT__CDO_H #include "context/context.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace context { diff --git a/src/context/cdvector.h b/src/context/cdvector.h index 9464f416b..24e214fbd 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -24,7 +24,7 @@ #include "context/context.h" #include "context/cdlist.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include diff --git a/src/context/context.cpp b/src/context/context.cpp index da60a5bc4..358821023 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -21,7 +21,7 @@ #include #include "context/context.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace context { diff --git a/src/context/context.h b/src/context/context.h index 165c35c58..2140451a7 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -29,7 +29,7 @@ #include #include "context/context_mm.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace context { diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index aea2fe9c2..4b4df1022 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -22,7 +22,7 @@ #include #include #include "context/context_mm.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/output.h" namespace CVC4 { diff --git a/src/cvc4.i b/src/cvc4.i index 58f098713..7d42f9484 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -146,7 +146,6 @@ using namespace CVC4; %include "util/output.i" %include "util/result.i" %include "util/configuration.i" -%include "util/Assert.i" %include "util/bitvector.i" %include "util/subrange_bound.i" %include "util/array.i" diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 5070c852f..f39c0e7ea 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include #include diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index dbaba664c..f9091bdb1 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -24,7 +24,7 @@ #include #include "expr/kind.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/expr/node.h b/src/expr/node.h index 7108ba74a..b7c4b3ad8 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -36,7 +36,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/configuration.h" #include "util/output.h" #include "util/exception.h" diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index fa9b1c011..0c8ac40f8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -173,7 +173,7 @@ namespace CVC4 { #include "expr/kind.h" #include "expr/metakind.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node_value.h" #include "util/output.h" diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a66933470..d7eda7437 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -20,7 +20,7 @@ #include "expr/node_manager.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "options/options.h" #include "util/statistics_registry.h" #include "util/tls.h" diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 37c28ab07..b97d1ab14 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -23,7 +23,7 @@ #include -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index 1de8f2cf7..b31442b7f 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -31,7 +31,7 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 14477f3cd..a41db794d 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -30,7 +30,7 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" #include "util/output.h" diff --git a/src/expr/type_node.h b/src/expr/type_node.h index a0397e0bd..fa1d6cdaa 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -31,7 +31,7 @@ #include "expr/kind.h" #include "expr/metakind.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/cardinality.h" namespace CVC4 { diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index ee7a93144..ea1812278 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -24,7 +24,7 @@ #line 25 "${template}" #include "expr/type_node.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/expr.h" #include "util/language.h" diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 4191d1046..2dee07dab 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -21,7 +21,7 @@ #include "util/proof.h" #include "proof/sat_proof.h" #include "proof/cnf_proof.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9fb825e47..0f1161a06 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -23,7 +23,7 @@ #include "theory/theory_engine.h" #include "theory/theory.h" #include "expr/node.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/output.h" #include "expr/command.h" #include "expr/expr.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index d9f3f798a..f115aa6d0 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -26,7 +26,7 @@ #include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "options/options.h" #include "smt/options.h" #include "main/options.h" diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 926d3507b..60091a5fb 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -21,7 +21,7 @@ #include "smt/smt_engine.h" #include "util/tls.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node_manager.h" #include "util/output.h" diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index dfa32418f..8e4335213 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -21,7 +21,7 @@ #include #include "theory/arrays/static_fact_manager.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node.h" using namespace std; diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index 57fd412e4..408bb64ac 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -21,7 +21,7 @@ #include #include "theory/arrays/union_find.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node.h" using namespace std; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3305b88d8..f1c8fd657 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -21,7 +21,7 @@ #include "theory/valuation.h" #include "expr/kind.h" #include "util/datatype.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "theory/datatypes/theory_datatypes_instantiator.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/model.h" diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index c4ae81927..79fcaaebd 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -24,7 +24,7 @@ #include "expr/kind.h" #include "theory/logic_info.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4::theory; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 8ddf809b6..760cc1f4d 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -21,7 +21,7 @@ #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "theory/interrupted.h" namespace CVC4 { diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index c45626dd9..16c976475 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -23,7 +23,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/model_engine.h" #include "expr/kind.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "theory/quantifiers/theory_quantifiers_instantiator.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 79e4f6a36..1ae9edb73 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,7 +17,7 @@ **/ #include "theory/theory.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/instantiator_default.h" diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index ee7b4cf2d..9a5df133a 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -21,7 +21,7 @@ #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H #define __CVC4__THEORY__THEORY_TEST_UTILS_H -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node.h" #include "theory/output_channel.h" #include "theory/interrupted.h" diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 7b097ac77..fa7334697 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -24,7 +24,7 @@ #include "util/exception.h" #include "expr/node.h" #include "expr/type_node.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace theory { diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index 0619a900f..cb0fadc76 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -21,7 +21,7 @@ #include "theory/type_enumerator.h" #include "expr/kind.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" ${type_enumerator_includes} #line 28 "${template}" diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp deleted file mode 100644 index e299bef1d..000000000 --- a/src/util/Assert.cpp +++ /dev/null @@ -1,167 +0,0 @@ -/********************* */ -/*! \file Assert.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): acsys - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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.\endverbatim - ** - ** \brief Assertion utility classes, functions, and exceptions. - ** - ** Assertion utility classes, functions, and exceptions. Implementation. - **/ - -#include -#include -#include - -#include "util/Assert.h" - -using namespace std; - -namespace CVC4 { - -#ifdef CVC4_DEBUG -CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; -#endif /* CVC4_DEBUG */ - -void AssertionException::construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, - va_list args) { - // try building the exception msg with a smallish buffer first, - // then with a larger one if sprintf tells us to. - int n = 512; - char* buf; - - for(;;) { - buf = new char[n]; - - int size; - if(extra == NULL) { - size = snprintf(buf, n, "%s\n%s\n%s:%d\n", - header, function, file, line); - } else { - size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", - header, function, file, line, extra); - } - - if(size < n) { - va_list args_copy; - va_copy(args_copy, args); - size += vsnprintf(buf + size, n - size, fmt, args_copy); - va_end(args_copy); - - if(size < n) { - break; - } - } - - if(size >= n) { - // try again with a buffer that's large enough - n = size + 1; - delete [] buf; - } - } - - setMessage(string(buf)); - -#ifdef CVC4_DEBUG - if(s_debugLastException == NULL) { - // we leak buf[] but only in debug mode with assertions failing - s_debugLastException = buf; - } -#else /* CVC4_DEBUG */ - delete [] buf; -#endif /* CVC4_DEBUG */ -} - -void AssertionException::construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line) { - // try building the exception msg with a smallish buffer first, - // then with a larger one if sprintf tells us to. - int n = 256; - char* buf; - - for(;;) { - buf = new char[n]; - - int size; - if(extra == NULL) { - size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", - header, function, file, line); - } else { - size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", - header, function, file, line, extra); - } - - if(size < n) { - break; - } else { - // try again with a buffer that's large enough - n = size + 1; - delete [] buf; - } - } - - setMessage(string(buf)); - -#ifdef CVC4_DEBUG - // we leak buf[] but only in debug mode with assertions failing - if(s_debugLastException == NULL) { - s_debugLastException = buf; - } -#else /* CVC4_DEBUG */ - delete [] buf; -#endif /* CVC4_DEBUG */ -} - -#ifdef CVC4_DEBUG - -/** - * Special assertion failure handling in debug mode; in non-debug - * builds, the exception is thrown from the macro. We factor out this - * additional logic so as not to bloat the code at every Assert() - * expansion. - * - * Note this name is prefixed with "debug" because it is included in - * debug builds only; in debug builds, it handles all assertion - * failures (even those that exist in non-debug builds). - */ -void debugAssertionFailed(const AssertionException& thisException, - const char* propagatingException) { - static CVC4_THREADLOCAL(bool) alreadyFired = false; - - if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) { - throw thisException; - } - - alreadyFired = true; - - // propagatingException is the propagating exception, but can be - // NULL if the propagating exception is not a CVC4::Exception. - Warning() << "===========================================" << std::endl - << "An assertion failed during stack unwinding:" << std::endl; - if(propagatingException != NULL) { - Warning() << "The propagating exception is:" << std::endl - << propagatingException << std::endl - << "===========================================" << std::endl; - Warning() << "The newly-thrown exception is:" << std::endl; - } else { - Warning() << "The propagating exception is unknown." << std::endl; - } - Warning() << thisException << std::endl - << "===========================================" << std::endl; - - terminate(); -} - -#endif /* CVC4_DEBUG */ - -}/* CVC4 namespace */ diff --git a/src/util/Assert.h b/src/util/Assert.h deleted file mode 100644 index 4a6fe4d3a..000000000 --- a/src/util/Assert.h +++ /dev/null @@ -1,311 +0,0 @@ -/********************* */ -/*! \file Assert.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): acsys - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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.\endverbatim - ** - ** \brief Assertion utility classes, functions, exceptions, and macros. - ** - ** Assertion utility classes, functions, exceptions, and macros. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__ASSERT_H -#define __CVC4__ASSERT_H - -#include -#include -#include -#include -#include - -#include "util/exception.h" -#include "util/tls.h" - -// output.h not strictly needed for this header, but it _is_ needed to -// actually _use_ anything in this header, so let's include it. -#include "util/output.h" - -namespace CVC4 { - -class AssertionException : public Exception { -protected: - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, ...) { - va_list args; - va_start(args, fmt); - construct(header, extra, function, file, line, fmt, args); - va_end(args); - } - - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line, const char* fmt, va_list args); - - void construct(const char* header, const char* extra, - const char* function, const char* file, - unsigned line); - - AssertionException() : Exception() {} - -public: - AssertionException(const char* extra, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : - Exception() { - va_list args; - va_start(args, fmt); - construct("Assertion failure", extra, function, file, line, fmt, args); - va_end(args); - } - - AssertionException(const char* extra, const char* function, - const char* file, unsigned line) : - Exception() { - construct("Assertion failure", extra, function, file, line); - } -};/* class AssertionException */ - -class UnreachableCodeException : public AssertionException { -protected: - UnreachableCodeException() : AssertionException() {} - -public: - UnreachableCodeException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Unreachable code reached", - NULL, function, file, line, fmt, args); - va_end(args); - } - - UnreachableCodeException(const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Unreachable code reached", NULL, function, file, line); - } -};/* class UnreachableCodeException */ - -class UnhandledCaseException : public UnreachableCodeException { -protected: - UnhandledCaseException() : UnreachableCodeException() {} - -public: - UnhandledCaseException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - UnreachableCodeException() { - va_list args; - va_start(args, fmt); - construct("Unhandled case encountered", - NULL, function, file, line, fmt, args); - va_end(args); - } - - template - UnhandledCaseException(const char* function, const char* file, - unsigned line, T theCase) : - UnreachableCodeException() { - std::stringstream sb; - sb << theCase; - construct("Unhandled case encountered", - NULL, function, file, line, "The case was: %s", sb.str().c_str()); - } - - UnhandledCaseException(const char* function, const char* file, - unsigned line) : - UnreachableCodeException() { - construct("Unhandled case encountered", NULL, function, file, line); - } -};/* class UnhandledCaseException */ - -class UnimplementedOperationException : public AssertionException { -protected: - UnimplementedOperationException() : AssertionException() {} - -public: - UnimplementedOperationException(const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Unimplemented code encountered", - NULL, function, file, line, fmt, args); - va_end(args); - } - - UnimplementedOperationException(const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Unimplemented code encountered", NULL, function, file, line); - } -};/* class UnimplementedOperationException */ - -class AssertArgumentException : public AssertionException { -protected: - AssertArgumentException() : AssertionException() {} - -public: - AssertArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line, - const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), - function, file, line, fmt, args); - va_end(args); - } - - AssertArgumentException(const char* argDesc, const char* function, - const char* file, unsigned line) : - AssertionException() { - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), - function, file, line); - } - - AssertArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line, const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument; expected " + - condStr + " to hold" ).c_str(), - function, file, line, fmt, args); - va_end(args); - } - - AssertArgumentException(const char* condStr, const char* argDesc, - const char* function, const char* file, - unsigned line) : - AssertionException() { - construct("Illegal argument detected", - ( std::string("`") + argDesc + "' is a bad argument; expected " + - condStr + " to hold" ).c_str(), - function, file, line); - } -};/* class AssertArgumentException */ - -class InternalErrorException : public AssertionException { -protected: - InternalErrorException() : AssertionException() {} - -public: - InternalErrorException(const char* function, const char* file, unsigned line) : - AssertionException() { - construct("Internal error detected", "", - function, file, line); - } - - InternalErrorException(const char* function, const char* file, unsigned line, - const char* fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Internal error detected", "", - function, file, line, fmt, args); - va_end(args); - } - - InternalErrorException(const char* function, const char* file, unsigned line, - std::string fmt, ...) : - AssertionException() { - va_list args; - va_start(args, fmt); - construct("Internal error detected", "", - function, file, line, fmt.c_str(), args); - va_end(args); - } - -};/* class InternalErrorException */ - -#ifdef CVC4_DEBUG - -extern CVC4_THREADLOCAL(const char*) s_debugLastException; - -/** - * Special assertion failure handling in debug mode; in non-debug - * builds, the exception is thrown from the macro. We factor out this - * additional logic so as not to bloat the code at every Assert() - * expansion. - * - * Note this name is prefixed with "debug" because it is included in - * debug builds only; in debug builds, it handles all assertion - * failures (even those that exist in non-debug builds). - */ -void debugAssertionFailed(const AssertionException& thisException, const char* lastException); - -// If we're currently handling an exception, print a warning instead; -// otherwise std::terminate() is called by the runtime and we lose -// details of the exception -# define AlwaysAssert(cond, msg...) \ - do { \ - if(EXPECT_FALSE( ! (cond) )) { \ - /* save the last assertion failure */ \ - const char* lastException = ::CVC4::s_debugLastException; \ - ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - ::CVC4::debugAssertionFailed(exception, lastException); \ - } \ - } while(0) - -#else /* CVC4_DEBUG */ -// These simpler (but less useful) versions for non-debug builds fails -// will terminate() if thrown during stack unwinding. -# define AlwaysAssert(cond, msg...) \ - do { \ - if(EXPECT_FALSE( ! (cond) )) { \ - throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - } \ - } while(0) -#endif /* CVC4_DEBUG */ - -#define Unreachable(msg...) \ - throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define Unhandled(msg...) \ - throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define Unimplemented(msg...) \ - throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define InternalError(msg...) \ - throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) -#define IllegalArgument(arg, msg...) \ - throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) -#define CheckArgument(cond, arg, msg...) \ - do { \ - if(EXPECT_FALSE( ! (cond) )) { \ - throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ - } \ - } while(0) -#define AlwaysAssertArgument(cond, arg, msg...) \ - do { \ - if(EXPECT_FALSE( ! (cond) )) { \ - throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - } \ - } while(0) - -#ifdef CVC4_ASSERTIONS -# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) -# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) -# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) -#else /* ! CVC4_ASSERTIONS */ -# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ -# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ -# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ -#endif /* CVC4_ASSERTIONS */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__ASSERT_H */ diff --git a/src/util/Assert.i b/src/util/Assert.i deleted file mode 100644 index b43c36520..000000000 --- a/src/util/Assert.i +++ /dev/null @@ -1,8 +0,0 @@ -%{ -#include "util/Assert.h" -%} - -%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; -%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...); - -%include "util/Assert.h" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index fcbadf490..1848ef764 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -20,8 +20,8 @@ libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_F # configured at the time of the "make dist", which (1) may not be the # configuration that the user wants, and (2) might cause link errors. libutil_la_SOURCES = \ - Assert.h \ - Assert.cpp \ + cvc4_assert.h \ + cvc4_assert.cpp \ backtrackable.h \ Makefile.am \ Makefile.in \ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index a5a646231..fcdb11181 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -25,7 +25,7 @@ #include #include "expr/node.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp new file mode 100644 index 000000000..ea70cc24e --- /dev/null +++ b/src/util/cvc4_assert.cpp @@ -0,0 +1,167 @@ +/********************* */ +/*! \file Assert.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): acsys + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Assertion utility classes, functions, and exceptions. + ** + ** Assertion utility classes, functions, and exceptions. Implementation. + **/ + +#include +#include +#include + +#include "util/cvc4_assert.h" + +using namespace std; + +namespace CVC4 { + +#ifdef CVC4_DEBUG +CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; +#endif /* CVC4_DEBUG */ + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, + va_list args) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 512; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + va_list args_copy; + va_copy(args_copy, args); + size += vsnprintf(buf + size, n - size, fmt, args_copy); + va_end(args_copy); + + if(size < n) { + break; + } + } + + if(size >= n) { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + +#ifdef CVC4_DEBUG + if(s_debugLastException == NULL) { + // we leak buf[] but only in debug mode with assertions failing + s_debugLastException = buf; + } +#else /* CVC4_DEBUG */ + delete [] buf; +#endif /* CVC4_DEBUG */ +} + +void AssertionException::construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line) { + // try building the exception msg with a smallish buffer first, + // then with a larger one if sprintf tells us to. + int n = 256; + char* buf; + + for(;;) { + buf = new char[n]; + + int size; + if(extra == NULL) { + size = snprintf(buf, n, "%s.\n%s\n%s:%d\n", + header, function, file, line); + } else { + size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n %s\n", + header, function, file, line, extra); + } + + if(size < n) { + break; + } else { + // try again with a buffer that's large enough + n = size + 1; + delete [] buf; + } + } + + setMessage(string(buf)); + +#ifdef CVC4_DEBUG + // we leak buf[] but only in debug mode with assertions failing + if(s_debugLastException == NULL) { + s_debugLastException = buf; + } +#else /* CVC4_DEBUG */ + delete [] buf; +#endif /* CVC4_DEBUG */ +} + +#ifdef CVC4_DEBUG + +/** + * Special assertion failure handling in debug mode; in non-debug + * builds, the exception is thrown from the macro. We factor out this + * additional logic so as not to bloat the code at every Assert() + * expansion. + * + * Note this name is prefixed with "debug" because it is included in + * debug builds only; in debug builds, it handles all assertion + * failures (even those that exist in non-debug builds). + */ +void debugAssertionFailed(const AssertionException& thisException, + const char* propagatingException) { + static CVC4_THREADLOCAL(bool) alreadyFired = false; + + if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) { + throw thisException; + } + + alreadyFired = true; + + // propagatingException is the propagating exception, but can be + // NULL if the propagating exception is not a CVC4::Exception. + Warning() << "===========================================" << std::endl + << "An assertion failed during stack unwinding:" << std::endl; + if(propagatingException != NULL) { + Warning() << "The propagating exception is:" << std::endl + << propagatingException << std::endl + << "===========================================" << std::endl; + Warning() << "The newly-thrown exception is:" << std::endl; + } else { + Warning() << "The propagating exception is unknown." << std::endl; + } + Warning() << thisException << std::endl + << "===========================================" << std::endl; + + terminate(); +} + +#endif /* CVC4_DEBUG */ + +}/* CVC4 namespace */ diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h new file mode 100644 index 000000000..4a6fe4d3a --- /dev/null +++ b/src/util/cvc4_assert.h @@ -0,0 +1,311 @@ +/********************* */ +/*! \file Assert.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): acsys + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Assertion utility classes, functions, exceptions, and macros. + ** + ** Assertion utility classes, functions, exceptions, and macros. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ASSERT_H +#define __CVC4__ASSERT_H + +#include +#include +#include +#include +#include + +#include "util/exception.h" +#include "util/tls.h" + +// output.h not strictly needed for this header, but it _is_ needed to +// actually _use_ anything in this header, so let's include it. +#include "util/output.h" + +namespace CVC4 { + +class AssertionException : public Exception { +protected: + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, ...) { + va_list args; + va_start(args, fmt); + construct(header, extra, function, file, line, fmt, args); + va_end(args); + } + + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line, const char* fmt, va_list args); + + void construct(const char* header, const char* extra, + const char* function, const char* file, + unsigned line); + + AssertionException() : Exception() {} + +public: + AssertionException(const char* extra, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + Exception() { + va_list args; + va_start(args, fmt); + construct("Assertion failure", extra, function, file, line, fmt, args); + va_end(args); + } + + AssertionException(const char* extra, const char* function, + const char* file, unsigned line) : + Exception() { + construct("Assertion failure", extra, function, file, line); + } +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +protected: + UnreachableCodeException() : AssertionException() {} + +public: + UnreachableCodeException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unreachable code reached", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnreachableCodeException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unreachable code reached", NULL, function, file, line); + } +};/* class UnreachableCodeException */ + +class UnhandledCaseException : public UnreachableCodeException { +protected: + UnhandledCaseException() : UnreachableCodeException() {} + +public: + UnhandledCaseException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + UnreachableCodeException() { + va_list args; + va_start(args, fmt); + construct("Unhandled case encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + template + UnhandledCaseException(const char* function, const char* file, + unsigned line, T theCase) : + UnreachableCodeException() { + std::stringstream sb; + sb << theCase; + construct("Unhandled case encountered", + NULL, function, file, line, "The case was: %s", sb.str().c_str()); + } + + UnhandledCaseException(const char* function, const char* file, + unsigned line) : + UnreachableCodeException() { + construct("Unhandled case encountered", NULL, function, file, line); + } +};/* class UnhandledCaseException */ + +class UnimplementedOperationException : public AssertionException { +protected: + UnimplementedOperationException() : AssertionException() {} + +public: + UnimplementedOperationException(const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Unimplemented code encountered", + NULL, function, file, line, fmt, args); + va_end(args); + } + + UnimplementedOperationException(const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Unimplemented code encountered", NULL, function, file, line); + } +};/* class UnimplementedOperationException */ + +class AssertArgumentException : public AssertionException { +protected: + AssertArgumentException() : AssertionException() {} + +public: + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), + function, file, line, fmt, args); + va_end(args); + } + + AssertArgumentException(const char* argDesc, const char* function, + const char* file, unsigned line) : + AssertionException() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), + function, file, line); + } + + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line, const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold" ).c_str(), + function, file, line, fmt, args); + va_end(args); + } + + AssertArgumentException(const char* condStr, const char* argDesc, + const char* function, const char* file, + unsigned line) : + AssertionException() { + construct("Illegal argument detected", + ( std::string("`") + argDesc + "' is a bad argument; expected " + + condStr + " to hold" ).c_str(), + function, file, line); + } +};/* class AssertArgumentException */ + +class InternalErrorException : public AssertionException { +protected: + InternalErrorException() : AssertionException() {} + +public: + InternalErrorException(const char* function, const char* file, unsigned line) : + AssertionException() { + construct("Internal error detected", "", + function, file, line); + } + + InternalErrorException(const char* function, const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt, args); + va_end(args); + } + + InternalErrorException(const char* function, const char* file, unsigned line, + std::string fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt.c_str(), args); + va_end(args); + } + +};/* class InternalErrorException */ + +#ifdef CVC4_DEBUG + +extern CVC4_THREADLOCAL(const char*) s_debugLastException; + +/** + * Special assertion failure handling in debug mode; in non-debug + * builds, the exception is thrown from the macro. We factor out this + * additional logic so as not to bloat the code at every Assert() + * expansion. + * + * Note this name is prefixed with "debug" because it is included in + * debug builds only; in debug builds, it handles all assertion + * failures (even those that exist in non-debug builds). + */ +void debugAssertionFailed(const AssertionException& thisException, const char* lastException); + +// If we're currently handling an exception, print a warning instead; +// otherwise std::terminate() is called by the runtime and we lose +// details of the exception +# define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + /* save the last assertion failure */ \ + const char* lastException = ::CVC4::s_debugLastException; \ + ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + ::CVC4::debugAssertionFailed(exception, lastException); \ + } \ + } while(0) + +#else /* CVC4_DEBUG */ +// These simpler (but less useful) versions for non-debug builds fails +// will terminate() if thrown during stack unwinding. +# define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) +#endif /* CVC4_DEBUG */ + +#define Unreachable(msg...) \ + throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unhandled(msg...) \ + throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define Unimplemented(msg...) \ + throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define InternalError(msg...) \ + throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define IllegalArgument(arg, msg...) \ + throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg) +#define CheckArgument(cond, arg, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \ + } \ + } while(0) +#define AlwaysAssertArgument(cond, arg, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) AlwaysAssert(cond, ## msg) +# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) +# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__ASSERT_H */ diff --git a/src/util/cvc4_assert.i b/src/util/cvc4_assert.i new file mode 100644 index 000000000..45d76312d --- /dev/null +++ b/src/util/cvc4_assert.i @@ -0,0 +1,8 @@ +%{ +#include "util/cvc4_assert.h" +%} + +%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; +%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...); + +%include "util/cvc4_assert.h" diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index ee9c4e406..a5be71da2 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -28,7 +28,7 @@ #include "expr/node.h" #include "util/recursion_breaker.h" #include "util/matcher.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h index 2c8b842e4..9f1fed565 100644 --- a/src/util/dynamic_array.h +++ b/src/util/dynamic_array.h @@ -22,7 +22,7 @@ #ifndef __CVC4__UTIL__DYNAMIC_ARRAY_H #define __CVC4__UTIL__DYNAMIC_ARRAY_H -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/util/exception.h b/src/util/exception.h index 4241fb1f1..184a21453 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -131,7 +131,7 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { }/* CVC4 namespace */ #if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) -# include "util/Assert.h" +# include "util/cvc4_assert.h" #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */ namespace CVC4 { diff --git a/src/util/matcher.h b/src/util/matcher.h index 871fe528f..abee47c9a 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -25,7 +25,7 @@ #include #include #include -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/node.h" #include "expr/type_node.h" diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp index 748e818c3..5805e5c66 100644 --- a/src/util/predicate.cpp +++ b/src/util/predicate.cpp @@ -20,7 +20,7 @@ #include "expr/expr.h" #include "util/predicate.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h index 1146a4429..fe849842f 100644 --- a/src/util/recursion_breaker.h +++ b/src/util/recursion_breaker.h @@ -77,7 +77,7 @@ #include #include "util/hash.h" #include "util/tls.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/util/result.cpp b/src/util/result.cpp index 84e422c19..63d1ff843 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -22,7 +22,7 @@ #include #include "util/result.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "printer/printer.h" using namespace std; diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index f90426fab..a5034a36c 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -20,7 +20,7 @@ #include #include "util/sexpr.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "printer/printer.h" #include "expr/expr.h" diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index ba289080c..7a70807aa 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -18,7 +18,7 @@ #include "util/trans_closure.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index db940f3ea..0ff896f91 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -19,7 +19,7 @@ #include #include "context/cdhashmap.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index 6d40a0fb1..67ca2bfa9 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -23,7 +23,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdo.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 1a50d0637..e47ba3950 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -23,7 +23,7 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdo.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 9fb94097d..5fdcbf5c9 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -20,7 +20,7 @@ #include "context/context.h" #include "context/cdo.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 0fe0e93f0..eed826a4e 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -29,7 +29,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 97abddc00..426477bc5 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "expr/kind.h" #include "context/context.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/rational.h" using namespace CVC4; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index a042b1752..0860f735a 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -25,7 +25,7 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "context/context.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 89fbf42e8..486872b0b 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -26,7 +26,7 @@ #include "expr/expr_manager.h" #include "expr/expr.h" #include "expr/type.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "util/exception.h" using namespace CVC4; diff --git a/test/unit/memory.h b/test/unit/memory.h index 19b45c05d..3c9fd0afa 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -31,7 +31,7 @@ #include #include -#include "util/Assert.h" +#include "util/cvc4_assert.h" namespace CVC4 { namespace test { diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index cc7ea9bf6..81f108fb2 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -20,7 +20,7 @@ /* #include */ /* #include */ -#include "util/Assert.h" +#include "util/cvc4_assert.h" #include "expr/expr_manager.h" #include "expr/node_manager.h" diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 2a176e3d9..17185899d 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -39,7 +39,7 @@ #include "util/rational.h" #include "util/integer.h" #include "options/options.h" -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 54c77b165..2f86feaea 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -21,7 +21,7 @@ #include #include -#include "util/Assert.h" +#include "util/cvc4_assert.h" using namespace CVC4; using namespace std;