google test: api: Migrate op_black. (#5567)

3 files changed, 56 insertions, 73 deletions

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index b437146d9..59d914931 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -13,7 +13,7 @@
 
 cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_unit_test_black(grammar_black api)
-cvc4_add_cxx_unit_test_black(op_black api)
+cvc4_add_unit_test_black(op_black api)
 cvc4_add_unit_test_black(result_black api)
 cvc4_add_cxx_unit_test_black(solver_black api)
 cvc4_add_cxx_unit_test_black(sort_black api)
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.cpp
index da0bc8427..83ac768f1 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file op_black.h
+/*! \file op_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Makai Mann, Aina Niemetz
@@ -12,186 +12,169 @@
  ** \brief Black box testing of the Term class
  **/
 
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
+#include "test_api.h"
 
 using namespace CVC4::api;
 
-class OpBlack : public CxxTest::TestSuite
+class TestApiOpBlack : public TestApi
 {
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testGetKind();
-  void testIsNull();
-  void testOpFromKind();
-  void testGetIndicesString();
-  void testGetIndicesUint();
-  void testGetIndicesPairUint();
-
-  void testOpScopingToString();
-
- private:
-  Solver d_solver;
 };
 
-void OpBlack::testGetKind()
+TEST_F(TestApiOpBlack, getKind)
 {
   Op x;
   x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
-  TS_ASSERT_THROWS_NOTHING(x.getKind());
+  ASSERT_NO_THROW(x.getKind());
 }
 
-void OpBlack::testIsNull()
+TEST_F(TestApiOpBlack, isNull)
 {
   Op x;
-  TS_ASSERT(x.isNull());
+  ASSERT_TRUE(x.isNull());
   x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
-  TS_ASSERT(!x.isNull());
+  ASSERT_FALSE(x.isNull());
 }
 
-void OpBlack::testOpFromKind()
+TEST_F(TestApiOpBlack, opFromKind)
 {
   Op plus(&d_solver, PLUS);
-  TS_ASSERT(!plus.isIndexed());
-  TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
+  ASSERT_FALSE(plus.isIndexed());
+  ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
 
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkOp(PLUS));
-  TS_ASSERT_EQUALS(plus, d_solver.mkOp(PLUS));
-  TS_ASSERT_THROWS(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException&);
+  ASSERT_NO_THROW(d_solver.mkOp(PLUS));
+  EXPECT_EQ(plus, d_solver.mkOp(PLUS));
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
 }
 
-void OpBlack::testGetIndicesString()
+TEST_F(TestApiOpBlack, getIndicesString)
 {
   Op x;
-  TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&);
+  ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException);
 
   Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
-  TS_ASSERT(divisible_ot.isIndexed());
+  ASSERT_TRUE(divisible_ot.isIndexed());
   std::string divisible_idx = divisible_ot.getIndices<std::string>();
-  TS_ASSERT(divisible_idx == "4");
+  EXPECT_EQ(divisible_idx, "4");
 
   Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
   std::string record_update_idx = record_update_ot.getIndices<std::string>();
-  TS_ASSERT(record_update_idx == "test");
-  TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&);
+  EXPECT_EQ(record_update_idx, "test");
+  ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
 }
 
-void OpBlack::testGetIndicesUint()
+TEST_F(TestApiOpBlack, getIndicesUint)
 {
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
-  TS_ASSERT(bitvector_repeat_ot.isIndexed());
+  ASSERT_TRUE(bitvector_repeat_ot.isIndexed());
   uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
-  TS_ASSERT(bitvector_repeat_idx == 5);
-  TS_ASSERT_THROWS(
+  EXPECT_EQ(bitvector_repeat_idx, 5);
+  ASSERT_THROW(
       (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
-      CVC4ApiException&);
+      CVC4ApiException);
 
   Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
   uint32_t bitvector_zero_extend_idx =
       bitvector_zero_extend_ot.getIndices<uint32_t>();
-  TS_ASSERT(bitvector_zero_extend_idx == 6);
+  EXPECT_EQ(bitvector_zero_extend_idx, 6);
 
   Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
   uint32_t bitvector_sign_extend_idx =
       bitvector_sign_extend_ot.getIndices<uint32_t>();
-  TS_ASSERT(bitvector_sign_extend_idx == 7);
+  EXPECT_EQ(bitvector_sign_extend_idx, 7);
 
   Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
   uint32_t bitvector_rotate_left_idx =
       bitvector_rotate_left_ot.getIndices<uint32_t>();
-  TS_ASSERT(bitvector_rotate_left_idx == 8);
+  EXPECT_EQ(bitvector_rotate_left_idx, 8);
 
   Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
   uint32_t bitvector_rotate_right_idx =
       bitvector_rotate_right_ot.getIndices<uint32_t>();
-  TS_ASSERT(bitvector_rotate_right_idx == 9);
+  EXPECT_EQ(bitvector_rotate_right_idx, 9);
 
   Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
   uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
-  TS_ASSERT(int_to_bitvector_idx == 10);
+  EXPECT_EQ(int_to_bitvector_idx, 10);
 
   Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
   uint32_t floatingpoint_to_ubv_idx =
       floatingpoint_to_ubv_ot.getIndices<uint32_t>();
-  TS_ASSERT(floatingpoint_to_ubv_idx == 11);
+  EXPECT_EQ(floatingpoint_to_ubv_idx, 11);
 
   Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
   uint32_t floatingpoint_to_sbv_idx =
       floatingpoint_to_sbv_ot.getIndices<uint32_t>();
-  TS_ASSERT(floatingpoint_to_sbv_idx == 13);
+  EXPECT_EQ(floatingpoint_to_sbv_idx, 13);
 
   Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
   uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
-  TS_ASSERT(tuple_update_idx == 5);
-  TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(),
-                   CVC4ApiException&);
+  EXPECT_EQ(tuple_update_idx, 5);
+  ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
 }
 
-void OpBlack::testGetIndicesPairUint()
+TEST_F(TestApiOpBlack, getIndicesPairUint)
 {
   Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
-  TS_ASSERT(bitvector_extract_ot.isIndexed());
+  ASSERT_TRUE(bitvector_extract_ot.isIndexed());
   std::pair<uint32_t, uint32_t> bitvector_extract_indices =
       bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
+  ASSERT_TRUE(
+      (bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
 
   Op floatingpoint_to_fp_ieee_bitvector_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
       floatingpoint_to_fp_ieee_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_TRUE((floatingpoint_to_fp_ieee_bitvector_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_floatingpoint_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
       floatingpoint_to_fp_floatingpoint_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_TRUE((floatingpoint_to_fp_floatingpoint_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_real_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
       floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_real_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_TRUE((floatingpoint_to_fp_real_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_signed_bitvector_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
       floatingpoint_to_fp_signed_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_TRUE((floatingpoint_to_fp_signed_bitvector_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_unsigned_bitvector_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
       floatingpoint_to_fp_unsigned_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_TRUE((floatingpoint_to_fp_unsigned_bitvector_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_generic_ot =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
       floatingpoint_to_fp_generic_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
-  TS_ASSERT((floatingpoint_to_fp_generic_indices
-             == std::pair<uint32_t, uint32_t>{4, 25}));
-  TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
-                   CVC4ApiException&);
+  ASSERT_TRUE((floatingpoint_to_fp_generic_indices
+               == std::pair<uint32_t, uint32_t>{4, 25}));
+  ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
+               CVC4ApiException);
 }
 
-void OpBlack::testOpScopingToString()
+TEST_F(TestApiOpBlack, opScopingToString)
 {
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   std::string op_repr = bitvector_repeat_ot.toString();
   Solver solver2;
-  TS_ASSERT_EQUALS(bitvector_repeat_ot.toString(), op_repr);
+  EXPECT_EQ(bitvector_repeat_ot.toString(), op_repr);
 }
diff --git a/test/unit/test_api.h b/test/unit/test_api.h
index 72d0658a7..83e48f8ab 100644
--- a/test/unit/test_api.h
+++ b/test/unit/test_api.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file datatype_api_black.h
+/*! \file test_api.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Aina Niemetz