rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to make it...

diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
index e18d9b9721b0c15ecfab26ca7bbea85fcb41191f..6b925cc3a3240e795c83eb5ec9c1511936946142 100644 (file)
--- 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 321a378bde1c519a184ce8d6fb5ad6f9525397ad..3967065bbb08562ecf9623da7b79f464b59c095e 100644 (file)
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -97,7 +97,7 @@
 #include <ext/hash_map>
 
 #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 7e15cf9eb2dc5958a039d784682c8d8d9a2d6677..544baed6b012ca6fcf78adfb9f8b42f644d35d22 100644 (file)
--- 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 4d8aea6cba623030030939ddb286d32b20391cb6..5f364897deabdb4ce00f4530fc39722c002a4aba 100644 (file)
--- 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 <boost/static_assert.hpp>
 

diff --git a/src/context/cdo.h b/src/context/cdo.h
index 1fc1eebe6fd7710c91b47913fbd6dd7141bfd797..a0f2bcd9d01057468a5876473dcf4dd12015407e 100644 (file)
--- 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 9464f416bac9df572d2ad0a4ebb2beb22de4cee5..24e214fbddaa3c10b563b863f6a673a433e87ae5 100644 (file)
--- 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 <vector>
 
 

diff --git a/src/context/context.cpp b/src/context/context.cpp
index da60a5bc4497b90cc5734552ff04e991602d9d97..358821023f111d37b550afaff5f2f72fe9f40cc7 100644 (file)
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -21,7 +21,7 @@
 #include <vector>
 
 #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 165c35c58c171eff94f5bb75d0b604ca83d5e2c4..2140451a7ef35e0138640d299879cc202ccfc9b9 100644 (file)
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -29,7 +29,7 @@
 #include <typeinfo>
 
 #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 aea2fe9c2f1cbe718d80ba966c2387b3a8d27cc5..4b4df1022277ed858aa17e3afe86dc257e82fe75 100644 (file)
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -22,7 +22,7 @@
 #include <deque>
 #include <new>
 #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 58f098713549edac95562ba2d1de8377c24ddc18..7d42f94848118a5f1be8f59c87cf2a39c4583b68 100644 (file)
--- 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 5070c852ffc52d5c23543f0ae5f67c0c0df459ed..f39c0e7eadcc714c53f89c9be98373ad923bf84f 100644 (file)
--- 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 <vector>
 #include <iterator>

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index dbaba664c113b0cc6cdbaae6cd71c787455fac26..f9091bdb12aa88e9130354c3e9e3a8940c134b33 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -24,7 +24,7 @@
 #include <iostream>
 
 #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 7108ba74a236937a9e0b90a3b33a42fe370ed3cd..b7c4b3ad8cc5a0f305604ecd8aa0ad1fa3265ae8 100644 (file)
--- 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 fa9b1c011a58cb54f8dec04c6131fd0ac62a944b..0c8ac40f8f531580210eac5be030efa68d35da7e 100644 (file)
--- 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 a669334701e29d141cdcd4456a006afeb5c57cbd..d7eda74375e3d8dfbb4bfb3da58a2979f3b3ec19 100644 (file)
--- 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 37c28ab079ecf0514a2f672b8911a82b56c232b5..b97d1ab14041c48cb645f2f6df0537a1cba64de9 100644 (file)
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -23,7 +23,7 @@
 
 #include <iterator>
 
-#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 1de8f2cf7635a3e2383fdd92b90b75e31c42e932..b31442b7fb87658c9cfd15159f67994a29c344d6 100644 (file)
--- 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 14477f3cdbb9000336b5f8c16157fa6ad5827aec..a41db794db536e32133c0ebd09aa1f9aa9c0a817 100644 (file)
--- 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 a0397e0bd80f937f854e729b3b74dcc86c8eb558..fa1d6cdaa147ce0230d3a911437013b53d12f8e2 100644 (file)
--- 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 ee7a93144a7bb7d56a055921cbb871875f26ebcd..ea18122786101e3f6b1634bc1b63b73aa06ab968 100644 (file)
--- 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 4191d1046d0c993edbb9b574a04100e14518bd7f..2dee07dabf1be01e4e633012383f891d3662ec40 100644 (file)
--- 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 9fb825e4709de0f31543558bfb1ff3cc197b16dc..0f1161a068b21541e14951cae0452cf461926b98 100644 (file)
--- 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 d9f3f798ad0a18f877a3392c6258d1ae668e9c72..f115aa6d0b7962bcdd0c78b2864dbd8f1b46aedf 100644 (file)
--- 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 926d3507bf60d0cba2897ad488a59812ec741a34..60091a5fbd29472d78f82234c9e5a0089bbaf8c6 100644 (file)
--- 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 dfa32418f1f1ef2de67a643ced488245f67e5963..8e4335213869ab8f3e749585f72beaa21edbbf40 100644 (file)
--- a/src/theory/arrays/static_fact_manager.cpp
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -21,7 +21,7 @@
 #include <iostream>
 
 #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 57fd412e4462e4f612525f1f79bde0f942d05481..408bb64ac565d2b6175b309cea3ad1105a1c518d 100644 (file)
--- a/src/theory/arrays/union_find.cpp
+++ b/src/theory/arrays/union_find.cpp
@@ -21,7 +21,7 @@
 #include <iostream>
 
 #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 3305b88d8628ec95aa2955eb756eb9a5fc22f252..f1c8fd657309bb4de90ef894a99cbe054e9bc032 100644 (file)
--- 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 c4ae81927c6065094574a286108e38fe5fadd91e..79fcaaebd21242b6522580160f7ba8829e633e0e 100644 (file)
--- 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 8ddf809b63bb93b0a6d6e61f995773c267260d86..760cc1f4dc5afb6371e5fa17fd957d9454bdb226 100644 (file)
--- 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 c45626dd925ca2904b9fc8f6e2b5634b1882c5bc..16c9764757709d2d513a6993cfcd1a716d9af264 100644 (file)
--- 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 79e4f6a36b830db77d3a7b5c79bf321e93b2f333..1ae9edb73466109383fd3ff6337fb3a28f5d47f3 100644 (file)
--- 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 ee7b4cf2dd20e2cb93470ad34166eb9c6b0f2d60..9a5df133adef8bf4bd9d38478e79663d1cb6fc70 100644 (file)
--- 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 7b097ac77a783a954acfdabae0652c6182188cdd..fa7334697ee23f9154b86a6fb078f1453866e210 100644 (file)
--- 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 0619a900f20db21259c903f45056f3fb4e08bc36..cb0fadc76aa1c9f3bad4c0cf30d8fb328e2f7407 100644 (file)
--- 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 (file)
index e299bef..0000000
--- 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 <new>
-#include <cstdarg>
-#include <cstdio>
-
-#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 (file)
index 4a6fe4d..0000000
--- 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 <string>
-#include <sstream>
-#include <cstdio>
-#include <cstdlib>
-#include <cstdarg>
-
-#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 <class T>
-  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 (file)
index b43c365..0000000
--- 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 fcbadf490a1ec7af6478d3947f0edc9eee2c0751..1848ef7644602ff4e78a22ada70a3e3156a0a07d 100644 (file)
--- 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 a5a6462319e7a69ea29c7a5c208b91ed144ceb7b..fcdb111810c0fac58cb5d5cd38f4f16d0ba39e71 100644 (file)
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -25,7 +25,7 @@
 #include <algorithm>
 
 #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 (file)
index 0000000..ea70cc2
--- /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 <new>
+#include <cstdarg>
+#include <cstdio>
+
+#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 (file)
index 0000000..4a6fe4d
--- /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 <string>
+#include <sstream>
+#include <cstdio>
+#include <cstdlib>
+#include <cstdarg>
+
+#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 <class T>
+  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 (file)
index 0000000..45d7631
--- /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 ee9c4e406a17b8e606e67c7c3ec6f9f77a2ecd46..a5be71da2823ebf47c2a80faba55d3807084b00c 100644 (file)
--- 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 2c8b842e44bdf8b8b345d19fb3939715cd9c57c2..9f1fed565c757a6585e144624ab25dbe21ee963e 100644 (file)
--- 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 4241fb1f106ac0e4bbc47cad5ad37baaa8c3bdc6..184a214533edbdddee24ecbfa047f62a2fbb6871 100644 (file)
--- 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 871fe528fe4516a002bf390fe2a90fdd67dd158f..abee47c9aca86f80f6861f86339ca9d05fcacff3 100644 (file)
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -25,7 +25,7 @@
 #include <string>
 #include <vector>
 #include <map>
-#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 748e818c33450e4fee7eb86125b150c26ad9e0d8..5805e5c668b3fa22353c6929557d98665a9ba1ce 100644 (file)
--- 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 1146a4429fab4fe431d62e0cda97f231ba826cc8..fe849842f0d299bfa173147ee90233c537cfa19a 100644 (file)
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -77,7 +77,7 @@
 #include <ext/hash_set>
 #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 84e422c1915d3485cddf7c8719d7ba81b2b1c71b..63d1ff8438bc1886e97b991a925dadeff81ee17c 100644 (file)
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -22,7 +22,7 @@
 #include <cctype>
 
 #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 f90426fab515d9b0e3f99f26824dede185e1f578..a5034a36c05ae18803837fe1957aa1611fa1ae27 100644 (file)
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -20,7 +20,7 @@
 #include <vector>
 
 #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 ba289080cb7e385d225713d20c72214325fa3f32..7a70807aaf9ae8173b76deefdde3297e711417c2 100644 (file)
--- 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 db940f3ea6233d5c7947f308cf37cdca26ed18f0..0ff896f91f0c6c3ea658c61634403b7bf99ae7fb 100644 (file)
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -19,7 +19,7 @@
 #include <cxxtest/TestSuite.h>
 
 #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 6d40a0fb173b62c014a18d3e2f5ba22d1a84c28d..67ca2bfa9fa5bc9c69e0a7cd9e9560db1f12f968 100644 (file)
--- 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 1a50d0637de4c0b06997cd64cb6a3293e0e7bf8d..e47ba39506824e391ef2b0697e213c73462f9616 100644 (file)
--- 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 9fb94097db193f4e34335cdcbaacac3f6592031a..5fdcbf5c9237f120088c580175457d25ffd29720 100644 (file)
--- 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 0fe0e93f0bf9e2cfae1cfc516f42048332bfdc29..eed826a4ec2bd08b3ad81e43220c098d486e6778 100644 (file)
--- 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 97abddc00dafba48acd00a6cbb0b602b3b08f9b2..426477bc50b10eb10188b77e06a472aa61870ecf 100644 (file)
--- 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 a042b17529df388a5450fd4f5962a7a8591fbd70..0860f735a73e6903c2fde011031a54466f52bb48 100644 (file)
--- 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 89fbf42e897e0643f0af4b9e6f798b8dcb94d82a..486872b0b081c2b203cc9b8c21bfe80fdd27c81a 100644 (file)
--- 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 19b45c05dce1e6ea2d3e32cd644cf5086de1f30a..3c9fd0afa70fa0d78d72848665a87b9757b51e58 100644 (file)
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -31,7 +31,7 @@
 #include <sys/time.h>
 #include <sys/resource.h>
 
-#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 cc7ea9bf65a727aa8f50558921cc05c947036e7a..81f108fb26d5e5c56be12a1dff1e53abba949fb4 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -20,7 +20,7 @@
 /* #include <gmock/gmock.h> */
 /* #include <gtest/gtest.h> */
 
-#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 2a176e3d9efb7979cbd4d4a92a6b07aad1cf04b6..17185899d46022b8340e5966c81bdb86ce108ecf 100644 (file)
--- 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 54c77b1651989ecf00395fae86c07e41b68aeef3..2f86feaeafd0e37f5fb564bcdbdde6e5868accb8 100644 (file)
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -21,7 +21,7 @@
 #include <string>
 #include <cstring>
 
-#include "util/Assert.h"
+#include "util/cvc4_assert.h"
 
 using namespace CVC4;
 using namespace std;