Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

7 files changed, 69 insertions, 65 deletions

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index d109efdfd..745264b83 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,7 +18,7 @@
 
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 287704f39..e4a0dbb36 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -27,6 +27,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node_value.h"
+#include "test_utils.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -179,8 +180,8 @@ class NodeBlack : public CxxTest::TestSuite {
 
 #ifdef CVC4_ASSERTIONS
     // Basic bounds check on a node w/out children
-    TS_ASSERT_THROWS(Node::null()[-1], AssertionException&);
-    TS_ASSERT_THROWS(Node::null()[0], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(Node::null()[-1]);
+    TS_UTILS_EXPECT_ABORT(Node::null()[0]);
 #endif /* CVC4_ASSERTIONS */
 
     // Basic access check
@@ -198,8 +199,8 @@ class NodeBlack : public CxxTest::TestSuite {
 
 #ifdef CVC4_ASSERTIONS
     // Bounds check on a node with children
-    TS_ASSERT_THROWS(ite == ite[-1], AssertionException&);
-    TS_ASSERT_THROWS(ite == ite[4], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(ite == ite[-1]);
+    TS_UTILS_EXPECT_ABORT(ite == ite[4]);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -459,10 +460,10 @@ class NodeBlack : public CxxTest::TestSuite {
     }
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(testNaryExpForSize(AND, 0), AssertionException&);
-    TS_ASSERT_THROWS(testNaryExpForSize(AND, 1), AssertionException&);
-    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 0), AssertionException&);
-    TS_ASSERT_THROWS(testNaryExpForSize(NOT, 2), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 0));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 1));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 0));
+    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 2));
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2ece96cb8..473557e07 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -20,11 +20,12 @@
 #include <limits.h>
 #include <sstream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
+#include "test_utils.h"
 #include "util/rational.h"
 
 using namespace CVC4;
@@ -90,9 +91,9 @@ private:
     NodeBuilder<> def;
     TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(def.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(def.begin(), AssertionException&);
-    TS_ASSERT_THROWS(def.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(def.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(def.begin());
+    TS_UTILS_EXPECT_ABORT(def.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(specKind);
@@ -104,9 +105,9 @@ private:
     NodeBuilder<> from_nm(d_nm);
     TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(from_nm.begin(), AssertionException&);
-    TS_ASSERT_THROWS(from_nm.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(from_nm.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(from_nm.begin());
+    TS_UTILS_EXPECT_ABORT(from_nm.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
@@ -120,9 +121,9 @@ private:
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(ws.begin(), AssertionException&);
-    TS_ASSERT_THROWS(ws.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(ws.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(ws.begin());
+    TS_UTILS_EXPECT_ABORT(ws.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_kind(specKind);
@@ -134,9 +135,9 @@ private:
     NodeBuilder<K> ws_from_nm(d_nm);
     TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException&);
-    TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(ws_from_nm.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(ws_from_nm.begin());
+    TS_UTILS_EXPECT_ABORT(ws_from_nm.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
@@ -158,33 +159,33 @@ private:
     NodeBuilder<> copy(def);
     TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(copy.begin(), AssertionException&);
-    TS_ASSERT_THROWS(copy.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(copy.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(copy.begin());
+    TS_UTILS_EXPECT_ABORT(copy.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> cp_ws(ws);
     TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(cp_ws.begin(), AssertionException&);
-    TS_ASSERT_THROWS(cp_ws.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(cp_ws.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_ws.begin());
+    TS_UTILS_EXPECT_ABORT(cp_ws.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K-10> cp_from_larger(ws);
     TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException&);
-    TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(cp_from_larger.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_from_larger.begin());
+    TS_UTILS_EXPECT_ABORT(cp_from_larger.end());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K+10> cp_from_smaller(ws);
     TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException&);
-    TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(cp_from_smaller.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(cp_from_smaller.begin());
+    TS_UTILS_EXPECT_ABORT(cp_from_smaller.end());
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -282,7 +283,7 @@ private:
     Node n = noKind;
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(noKind.getKind(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(noKind.getKind());
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(PLUS);
@@ -297,7 +298,7 @@ private:
 
     NodeBuilder<> nb;
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
     nb << PLUS << x << x;
 
@@ -309,7 +310,7 @@ private:
     Node n = nb;// avoid warning on clear()
     nb.clear();
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
     nb.clear(PLUS);
     TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
@@ -321,16 +322,16 @@ private:
     TS_ASSERT_EQUALS(nb.getNumChildren(), 6u);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << PLUS);
     n = nb;
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
 #endif /* CVC4_ASSERTIONS */
   }
 
   void testOperatorSquare() {
     /*
       Node operator[](int i) const {
-      Assert(i >= 0 && i < d_ev->getNumChildren());
+      TS_ASSERT(i >= 0 && i < d_ev->getNumChildren());
       return Node(d_ev->d_children[i]);
       }
     */
@@ -341,8 +342,8 @@ private:
     Node i_K = d_nm->mkNode(NOT, i_0);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(arr[-1], AssertionException&);
-    TS_ASSERT_THROWS(arr[0], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(arr[-1]);
+    TS_UTILS_EXPECT_ABORT(arr[0]);
 #endif /* CVC4_ASSERTIONS */
 
     arr << i_0;
@@ -375,7 +376,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = arr;
-    TS_ASSERT_THROWS(arr[0], AssertionException&);
+    TS_UTILS_EXPECT_ABORT(arr[0]);
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -385,9 +386,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
-    TS_ASSERT_THROWS(nb.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -402,9 +403,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
-    TS_ASSERT_THROWS(nb.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
@@ -427,9 +428,9 @@ private:
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&);
-    TS_ASSERT_THROWS(nb.begin(), AssertionException&);
-    TS_ASSERT_THROWS(nb.end(), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.getNumChildren());
+    TS_UTILS_EXPECT_ABORT(nb.begin());
+    TS_UTILS_EXPECT_ABORT(nb.end());
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -438,7 +439,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> spec(specKind);
-    TS_ASSERT_THROWS(spec << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(spec << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> noSpec;
@@ -457,12 +458,12 @@ private:
     nb.clear(PLUS);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(n = nb, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(n = nb);
     nb.clear(PLUS);
 #endif /* CVC4_ASSERTIONS */
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testRef;
@@ -470,7 +471,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     NodeBuilder<> testTwo;
-    TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(testTwo << specKind << PLUS);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> testMixOrder1;
@@ -494,7 +495,7 @@ private:
 
 #ifdef CVC4_ASSERTIONS
     Node n = nb;
-    TS_ASSERT_THROWS(nb << n, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb << n);
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> overflow(specKind);
@@ -527,7 +528,7 @@ private:
     Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(d_nm->mkNode(XOR, y, x, x));
 #endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> b(specKind);
@@ -588,7 +589,7 @@ private:
     TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K);
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(Node blah = implicit, AssertionException&);
+    TS_UTILS_EXPECT_ABORT(Node blah = implicit);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e568fc9df..4b9c42bd0 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -22,6 +22,7 @@
 #include "base/output.h"
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
+#include "test_utils.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -300,7 +301,7 @@ class NodeManagerBlack : public CxxTest::TestSuite {
   void testMkNodeTooFew() {
 #ifdef CVC4_ASSERTIONS
     Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
-    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, x), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, x));
 #endif
   }
 
@@ -319,7 +320,7 @@ class NodeManagerBlack : public CxxTest::TestSuite {
       vars.push_back(skolem_j);
       vars.push_back(orNode);
     }
-    TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, vars));
 #endif
   }
 };
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index c2888a708..6f7729f74 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,6 +19,7 @@
 #include <string>
 
 #include "expr/node_manager.h"
+#include "test_utils.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
@@ -57,7 +58,7 @@ class NodeManagerWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS_NOTHING(nb.realloc(25));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(256));
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.realloc(100), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.realloc(100));
 #endif /* CVC4_ASSERTIONS */
     TS_ASSERT_THROWS_NOTHING(nb.realloc(257));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(4000));
@@ -67,7 +68,7 @@ class NodeManagerWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS_NOTHING(nb.realloc(65536));
     TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863));
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&);
+    TS_UTILS_EXPECT_ABORT(nb.realloc(67108863));
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index e9a3112cf..c95c46e02 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -18,7 +18,7 @@
 
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index ef65e8773..1ac1fa315 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,7 +19,7 @@
 #include <sstream>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/exception.h"
 #include "context/context.h"
 #include "expr/expr.h"