From: Aina Niemetz Date: Tue, 12 Jan 2021 16:55:56 +0000 (-0800) Subject: google test: Use ASSERT_* instead of EXPECT_*. (#5765) X-Git-Tag: cvc5-1.0.0~2383 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2835a8af8a83ba1d728b3cb65a6a56c75a97be0;p=cvc5.git google test: Use ASSERT_* instead of EXPECT_*. (#5765) Use ASSERT instead of EXPECT for consistency. There's no real benefit for us to use EXPECT -- the main difference is that within a test, EXPECT failures do not terminate the test, while ASSERT failures do. This further fixes a minor issue in theory_sets_type_rules_white.h (which is still not migrated to google test yet). --- diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index fad525655..858316971 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -38,7 +38,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSort) Datatype d = listSort.getDatatype(); DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; - EXPECT_THROW(d[2], CVC4ApiException); + ASSERT_THROW(d[2], CVC4ApiException); ASSERT_NO_THROW(consConstr.getConstructorTerm()); ASSERT_NO_THROW(nilConstr.getConstructorTerm()); } @@ -88,24 +88,24 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSorts) for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) { ASSERT_TRUE(dtsorts[i].isDatatype()); - EXPECT_FALSE(dtsorts[i].getDatatype().isFinite()); - EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); + ASSERT_FALSE(dtsorts[i].getDatatype().isFinite()); + ASSERT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); } // verify the resolution was correct Datatype dtTree = dtsorts[0].getDatatype(); DatatypeConstructor dtcTreeNode = dtTree[0]; - EXPECT_EQ(dtcTreeNode.getName(), "node"); + ASSERT_EQ(dtcTreeNode.getName(), "node"); DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; - EXPECT_EQ(dtsTreeNodeLeft.getName(), "left"); + ASSERT_EQ(dtsTreeNodeLeft.getName(), "left"); // argument type should have resolved to be recursive - EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); - EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); + ASSERT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); + ASSERT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); // fails due to empty datatype std::vector dtdeclsBad; DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); dtdeclsBad.push_back(emptyD); - EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); + ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); } TEST_F(TestApiDatatypeBlack, datatypeStructs) @@ -119,21 +119,21 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs) cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); Sort nullSort; - EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); + ASSERT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); - EXPECT_FALSE(dt.isCodatatype()); - EXPECT_FALSE(dt.isTuple()); - EXPECT_FALSE(dt.isRecord()); - EXPECT_FALSE(dt.isFinite()); - EXPECT_TRUE(dt.isWellFounded()); + ASSERT_FALSE(dt.isCodatatype()); + ASSERT_FALSE(dt.isTuple()); + ASSERT_FALSE(dt.isRecord()); + ASSERT_FALSE(dt.isFinite()); + ASSERT_TRUE(dt.isWellFounded()); // get constructor DatatypeConstructor dcons = dt[0]; Term consTerm = dcons.getConstructorTerm(); - EXPECT_EQ(dcons.getNumSelectors(), 2); + ASSERT_EQ(dcons.getNumSelectors(), 2); // create datatype sort to test DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); @@ -145,8 +145,8 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs) dtypeSpecEnum.addConstructor(cc); Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); Datatype dtEnum = dtypeSortEnum.getDatatype(); - EXPECT_FALSE(dtEnum.isTuple()); - EXPECT_TRUE(dtEnum.isFinite()); + ASSERT_FALSE(dtEnum.isTuple()); + ASSERT_TRUE(dtEnum.isFinite()); // create codatatype DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); @@ -157,29 +157,29 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs) dtypeSpecStream.addConstructor(consStream); Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); Datatype dtStream = dtypeSortStream.getDatatype(); - EXPECT_TRUE(dtStream.isCodatatype()); - EXPECT_FALSE(dtStream.isFinite()); + ASSERT_TRUE(dtStream.isCodatatype()); + ASSERT_FALSE(dtStream.isFinite()); // codatatypes may be well-founded - EXPECT_TRUE(dtStream.isWellFounded()); + ASSERT_TRUE(dtStream.isWellFounded()); // create tuple Sort tupSort = d_solver.mkTupleSort({boolSort}); Datatype dtTuple = tupSort.getDatatype(); - EXPECT_TRUE(dtTuple.isTuple()); - EXPECT_FALSE(dtTuple.isRecord()); - EXPECT_TRUE(dtTuple.isFinite()); - EXPECT_TRUE(dtTuple.isWellFounded()); + ASSERT_TRUE(dtTuple.isTuple()); + ASSERT_FALSE(dtTuple.isRecord()); + ASSERT_TRUE(dtTuple.isFinite()); + ASSERT_TRUE(dtTuple.isWellFounded()); // create record std::vector> fields = { std::make_pair("b", boolSort), std::make_pair("i", intSort)}; Sort recSort = d_solver.mkRecordSort(fields); - EXPECT_TRUE(recSort.isDatatype()); + ASSERT_TRUE(recSort.isDatatype()); Datatype dtRecord = recSort.getDatatype(); - EXPECT_FALSE(dtRecord.isTuple()); - EXPECT_TRUE(dtRecord.isRecord()); - EXPECT_FALSE(dtRecord.isFinite()); - EXPECT_TRUE(dtRecord.isWellFounded()); + ASSERT_FALSE(dtRecord.isTuple()); + ASSERT_TRUE(dtRecord.isRecord()); + ASSERT_FALSE(dtRecord.isFinite()); + ASSERT_TRUE(dtRecord.isWellFounded()); } TEST_F(TestApiDatatypeBlack, datatypeNames) @@ -189,7 +189,7 @@ TEST_F(TestApiDatatypeBlack, datatypeNames) // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); ASSERT_NO_THROW(dtypeSpec.getName()); - EXPECT_EQ(dtypeSpec.getName(), std::string("list")); + ASSERT_EQ(dtypeSpec.getName(), std::string("list")); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); @@ -198,22 +198,22 @@ TEST_F(TestApiDatatypeBlack, datatypeNames) dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); - EXPECT_EQ(dt.getName(), std::string("list")); + ASSERT_EQ(dt.getName(), std::string("list")); ASSERT_NO_THROW(dt.getConstructor("nil")); ASSERT_NO_THROW(dt["cons"]); ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException); ASSERT_THROW(dt.getConstructor(""), CVC4ApiException); DatatypeConstructor dcons = dt[0]; - EXPECT_EQ(dcons.getName(), std::string("cons")); + ASSERT_EQ(dcons.getName(), std::string("cons")); ASSERT_NO_THROW(dcons.getSelector("head")); ASSERT_NO_THROW(dcons["tail"]); ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException); // get selector DatatypeSelector dselTail = dcons[1]; - EXPECT_EQ(dselTail.getName(), std::string("tail")); - EXPECT_EQ(dselTail.getRangeSort(), dtypeSort); + ASSERT_EQ(dselTail.getName(), std::string("tail")); + ASSERT_EQ(dselTail.getRangeSort(), dtypeSort); // possible to construct null datatype declarations if not using solver ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); @@ -236,7 +236,7 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype) Sort pairType = d_solver.mkDatatypeSort(pairSpec); - EXPECT_TRUE(pairType.getDatatype().isParametric()); + ASSERT_TRUE(pairType.getDatatype().isParametric()); v.clear(); v.push_back(d_solver.getIntegerSort()); @@ -255,46 +255,46 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype) v.push_back(d_solver.getRealSort()); Sort pairIntReal = pairType.instantiate(v); - EXPECT_NE(pairIntInt, pairRealReal); - EXPECT_NE(pairIntReal, pairRealReal); - EXPECT_NE(pairRealInt, pairRealReal); - EXPECT_NE(pairIntInt, pairIntReal); - EXPECT_NE(pairIntInt, pairRealInt); - EXPECT_NE(pairIntReal, pairRealInt); - - EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal)); - EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal)); - EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal)); - EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal)); - EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt)); - EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt)); - EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt)); - EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt)); - EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal)); - EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal)); - EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal)); - EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal)); - EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt)); - EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt)); - EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt)); - EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt)); - - EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); - EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); - EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); - EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); - EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); - EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); - EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); - EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); - EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); - EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); - EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); - EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); - EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); - EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); - EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); - EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); + ASSERT_NE(pairIntInt, pairRealReal); + ASSERT_NE(pairIntReal, pairRealReal); + ASSERT_NE(pairRealInt, pairRealReal); + ASSERT_NE(pairIntInt, pairIntReal); + ASSERT_NE(pairIntInt, pairRealInt); + ASSERT_NE(pairIntReal, pairRealInt); + + ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal)); + ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal)); + ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal)); + ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal)); + ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt)); + ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt)); + ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt)); + ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt)); + ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal)); + ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal)); + ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal)); + ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal)); + ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt)); + ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt)); + ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt)); + ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt)); + + ASSERT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); + ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); + ASSERT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); + ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); + ASSERT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); + ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); + ASSERT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); + ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); + ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); + ASSERT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); + ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); + ASSERT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); + ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); + ASSERT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); + ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); + ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); } TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) @@ -346,12 +346,12 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) std::vector dtsorts; ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 3); - EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded()); - EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion()); - EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion()); - EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[2].getDatatype().isWellFounded()); + ASSERT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion()); + ASSERT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion()); + ASSERT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -378,10 +378,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 1); ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); - EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), + ASSERT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), dtsorts[0]); - EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -416,10 +416,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) // both are well-founded and have nested recursion ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 2); - EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); - EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -454,10 +454,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) // both are well-founded and have nested recursion ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 2); - EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); - EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -492,8 +492,8 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec) // well-founded and has nested recursion ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); ASSERT_EQ(dtsorts.size(), 1); - EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); - EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); } TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons) @@ -542,9 +542,9 @@ TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons) Term testConsTerm; // get the specialized constructor term for list[Int] ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); - EXPECT_NE(testConsTerm, nilc.getConstructorTerm()); + ASSERT_NE(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); + ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); } } // namespace test } // namespace CVC4 diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index ca64a322f..817662d67 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -46,7 +46,7 @@ TEST_F(TestApiOpBlack, opFromKind) ASSERT_THROW(plus.getIndices(), CVC4ApiException); ASSERT_NO_THROW(d_solver.mkOp(PLUS)); - EXPECT_EQ(plus, d_solver.mkOp(PLUS)); + ASSERT_EQ(plus, d_solver.mkOp(PLUS)); ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException); } @@ -58,11 +58,11 @@ TEST_F(TestApiOpBlack, getIndicesString) Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); ASSERT_TRUE(divisible_ot.isIndexed()); std::string divisible_idx = divisible_ot.getIndices(); - EXPECT_EQ(divisible_idx, "4"); + ASSERT_EQ(divisible_idx, "4"); Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); std::string record_update_idx = record_update_ot.getIndices(); - EXPECT_EQ(record_update_idx, "test"); + ASSERT_EQ(record_update_idx, "test"); ASSERT_THROW(record_update_ot.getIndices(), CVC4ApiException); } @@ -71,7 +71,7 @@ TEST_F(TestApiOpBlack, getIndicesUint) Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); ASSERT_TRUE(bitvector_repeat_ot.isIndexed()); uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices(); - EXPECT_EQ(bitvector_repeat_idx, 5); + ASSERT_EQ(bitvector_repeat_idx, 5); ASSERT_THROW( (bitvector_repeat_ot.getIndices>()), CVC4ApiException); @@ -79,40 +79,40 @@ TEST_F(TestApiOpBlack, getIndicesUint) Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); uint32_t bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices(); - EXPECT_EQ(bitvector_zero_extend_idx, 6); + ASSERT_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(); - EXPECT_EQ(bitvector_sign_extend_idx, 7); + ASSERT_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(); - EXPECT_EQ(bitvector_rotate_left_idx, 8); + ASSERT_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(); - EXPECT_EQ(bitvector_rotate_right_idx, 9); + ASSERT_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(); - EXPECT_EQ(int_to_bitvector_idx, 10); + ASSERT_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(); - EXPECT_EQ(floatingpoint_to_ubv_idx, 11); + ASSERT_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(); - EXPECT_EQ(floatingpoint_to_sbv_idx, 13); + ASSERT_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(); - EXPECT_EQ(tuple_update_idx, 5); + ASSERT_EQ(tuple_update_idx, 5); ASSERT_THROW(tuple_update_ot.getIndices(), CVC4ApiException); } @@ -180,7 +180,7 @@ TEST_F(TestApiOpBlack, opScopingToString) Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); std::string op_repr = bitvector_repeat_ot.toString(); Solver solver2; - EXPECT_EQ(bitvector_repeat_ot.toString(), op_repr); + ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr); } } // namespace test } // namespace CVC4 diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp index bb60ab7ac..52cb68b25 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/result_black.cpp @@ -50,8 +50,8 @@ TEST_F(TestApiResultBlack, eq) CVC4::api::Result res2 = d_solver.checkSat(); CVC4::api::Result res3 = d_solver.checkSat(); res = res2; - EXPECT_EQ(res, res2); - EXPECT_EQ(res3, res2); + ASSERT_EQ(res, res2); + ASSERT_EQ(res3, res2); } TEST_F(TestApiResultBlack, isSat) @@ -115,7 +115,7 @@ TEST_F(TestApiResultBlack, isEntailmentUnknown) CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x)); ASSERT_FALSE(res.isEntailed()); ASSERT_TRUE(res.isEntailmentUnknown()); - EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON"); + ASSERT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON"); } } // namespace test } // namespace CVC4 diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index e7610265e..5592c7d3d 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -343,11 +343,11 @@ TEST_F(TestApiSolverBlack, mkBitVector) ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException); ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException); ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException); - EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10)); - EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16)); - EXPECT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); - EXPECT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); - EXPECT_EQ(d_solver.mkBitVector(8, "-1", 10), + ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10)); + ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16)); + ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); + ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); + ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10), d_solver.mkBitVector(8, "FF", 16)); } @@ -672,9 +672,9 @@ TEST_F(TestApiSolverBlack, mkString) { ASSERT_NO_THROW(d_solver.mkString("")); ASSERT_NO_THROW(d_solver.mkString("asdfasdf")); - EXPECT_EQ(d_solver.mkString("asdf\\nasdf").toString(), + ASSERT_EQ(d_solver.mkString("asdf\\nasdf").toString(), "\"asdf\\u{5c}nasdf\""); - EXPECT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), + ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\""); } @@ -685,7 +685,7 @@ TEST_F(TestApiSolverBlack, mkChar) ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException); ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException); ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException); - EXPECT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC")); + ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC")); } TEST_F(TestApiSolverBlack, mkTerm) @@ -1237,8 +1237,8 @@ TEST_F(TestApiSolverBlack, uFIteration) uint32_t idx = 0; for (auto c : fxy) { - EXPECT_LT(idx, 3); - EXPECT_EQ(c, expected_children[idx]); + ASSERT_LT(idx, 3); + ASSERT_EQ(c, expected_children[idx]); idx++; } } @@ -1264,7 +1264,7 @@ TEST_F(TestApiSolverBlack, getOp) ASSERT_FALSE(a.hasOp()); ASSERT_THROW(a.getOp(), CVC4ApiException); ASSERT_TRUE(exta.hasOp()); - EXPECT_EQ(exta.getOp(), ext); + ASSERT_EQ(exta.getOp(), ext); // Test Datatypes -- more complicated DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list"); @@ -1287,13 +1287,13 @@ TEST_F(TestApiSolverBlack, getOp) Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1); ASSERT_TRUE(listnil.hasOp()); - EXPECT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); ASSERT_TRUE(listcons1.hasOp()); - EXPECT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); ASSERT_TRUE(listhead.hasOp()); - EXPECT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR)); + ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR)); } TEST_F(TestApiSolverBlack, getOption) @@ -1784,12 +1784,12 @@ TEST_F(TestApiSolverBlack, simplify) ASSERT_NO_THROW(d_solver.simplify(b)); Term x_eq_x = d_solver.mkTerm(EQUAL, x, x); ASSERT_NO_THROW(d_solver.simplify(x_eq_x)); - EXPECT_NE(d_solver.mkTrue(), x_eq_x); - EXPECT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x)); + ASSERT_NE(d_solver.mkTrue(), x_eq_x); + ASSERT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x)); Term x_eq_b = d_solver.mkTerm(EQUAL, x, b); ASSERT_NO_THROW(d_solver.simplify(x_eq_b)); - EXPECT_NE(d_solver.mkTrue(), x_eq_b); - EXPECT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b)); + ASSERT_NE(d_solver.mkTrue(), x_eq_b); + ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b)); Solver slv; ASSERT_THROW(slv.simplify(x), CVC4ApiException); @@ -1797,12 +1797,12 @@ TEST_F(TestApiSolverBlack, simplify) ASSERT_NO_THROW(d_solver.simplify(i1)); Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23")); ASSERT_NO_THROW(d_solver.simplify(i2)); - EXPECT_NE(i1, i2); - EXPECT_NE(i1, d_solver.simplify(i2)); + ASSERT_NE(i1, i2); + ASSERT_NE(i1, d_solver.simplify(i2)); Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0)); ASSERT_NO_THROW(d_solver.simplify(i3)); - EXPECT_NE(i1, i3); - EXPECT_EQ(i1, d_solver.simplify(i3)); + ASSERT_NE(i1, i3); + ASSERT_EQ(i1, d_solver.simplify(i3)); Datatype consList = consListSort.getDatatype(); Term dt1 = d_solver.mkTerm( diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index ea87441fe..16190b76d 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -56,7 +56,7 @@ TEST_F(TestApiSortBlack, datatypeSorts) dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); - EXPECT_FALSE(dtypeSort.isConstructor()); + ASSERT_FALSE(dtypeSort.isConstructor()); ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC4ApiException); ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC4ApiException); ASSERT_THROW(dtypeSort.getConstructorArity(), CVC4ApiException); @@ -65,30 +65,30 @@ TEST_F(TestApiSortBlack, datatypeSorts) DatatypeConstructor dcons = dt[0]; Term consTerm = dcons.getConstructorTerm(); Sort consSort = consTerm.getSort(); - EXPECT_TRUE(consSort.isConstructor()); - EXPECT_FALSE(consSort.isTester()); - EXPECT_FALSE(consSort.isSelector()); - EXPECT_EQ(consSort.getConstructorArity(), 2); + ASSERT_TRUE(consSort.isConstructor()); + ASSERT_FALSE(consSort.isTester()); + ASSERT_FALSE(consSort.isSelector()); + ASSERT_EQ(consSort.getConstructorArity(), 2); std::vector consDomSorts = consSort.getConstructorDomainSorts(); - EXPECT_EQ(consDomSorts[0], intSort); - EXPECT_EQ(consDomSorts[1], dtypeSort); - EXPECT_EQ(consSort.getConstructorCodomainSort(), dtypeSort); + ASSERT_EQ(consDomSorts[0], intSort); + ASSERT_EQ(consDomSorts[1], dtypeSort); + ASSERT_EQ(consSort.getConstructorCodomainSort(), dtypeSort); // get tester Term isConsTerm = dcons.getTesterTerm(); - EXPECT_TRUE(isConsTerm.getSort().isTester()); - EXPECT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); + ASSERT_TRUE(isConsTerm.getSort().isTester()); + ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); Sort booleanSort = d_solver.getBooleanSort(); - EXPECT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); + ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC4ApiException); ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC4ApiException); // get selector DatatypeSelector dselTail = dcons[1]; Term tailTerm = dselTail.getSelectorTerm(); - EXPECT_TRUE(tailTerm.getSort().isSelector()); - EXPECT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); - EXPECT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); + ASSERT_TRUE(tailTerm.getSort().isSelector()); + ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); + ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC4ApiException); ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException); } @@ -170,7 +170,7 @@ TEST_F(TestApiSortBlack, getSetElementSort) Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); ASSERT_NO_THROW(setSort.getSetElementSort()); Sort elementSort = setSort.getSetElementSort(); - EXPECT_EQ(elementSort, d_solver.getIntegerSort()); + ASSERT_EQ(elementSort, d_solver.getIntegerSort()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException); } @@ -180,7 +180,7 @@ TEST_F(TestApiSortBlack, getBagElementSort) Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort()); ASSERT_NO_THROW(bagSort.getBagElementSort()); Sort elementSort = bagSort.getBagElementSort(); - EXPECT_EQ(elementSort, d_solver.getIntegerSort()); + ASSERT_EQ(elementSort, d_solver.getIntegerSort()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException); } @@ -188,10 +188,10 @@ TEST_F(TestApiSortBlack, getBagElementSort) TEST_F(TestApiSortBlack, getSequenceElementSort) { Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); - EXPECT_TRUE(seqSort.isSequence()); + ASSERT_TRUE(seqSort.isSequence()); ASSERT_NO_THROW(seqSort.getSequenceElementSort()); Sort bvSort = d_solver.mkBitVectorSort(32); - EXPECT_FALSE(bvSort.isSequence()); + ASSERT_FALSE(bvSort.isSequence()); ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException); } @@ -206,7 +206,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortName) TEST_F(TestApiSortBlack, isUninterpretedSortParameterized) { Sort uSort = d_solver.mkUninterpretedSort("u"); - EXPECT_FALSE(uSort.isUninterpretedSortParameterized()); + ASSERT_FALSE(uSort.isUninterpretedSortParameterized()); Sort sSort = d_solver.mkSortConstructorSort("s", 1); Sort siSort = sSort.instantiate({uSort}); ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); @@ -220,7 +220,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts) ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts()); Sort sSort = d_solver.mkSortConstructorSort("s", 2); Sort siSort = sSort.instantiate({uSort, uSort}); - EXPECT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2); + ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException); } @@ -345,24 +345,24 @@ TEST_F(TestApiSortBlack, sortSubtyping) { Sort intSort = d_solver.getIntegerSort(); Sort realSort = d_solver.getRealSort(); - EXPECT_TRUE(intSort.isSubsortOf(realSort)); - EXPECT_FALSE(realSort.isSubsortOf(intSort)); - EXPECT_TRUE(intSort.isComparableTo(realSort)); - EXPECT_TRUE(realSort.isComparableTo(intSort)); + ASSERT_TRUE(intSort.isSubsortOf(realSort)); + ASSERT_FALSE(realSort.isSubsortOf(intSort)); + ASSERT_TRUE(intSort.isComparableTo(realSort)); + ASSERT_TRUE(realSort.isComparableTo(intSort)); Sort arraySortII = d_solver.mkArraySort(intSort, intSort); Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); - EXPECT_FALSE(arraySortII.isComparableTo(intSort)); + ASSERT_FALSE(arraySortII.isComparableTo(intSort)); // we do not support subtyping for arrays - EXPECT_FALSE(arraySortII.isComparableTo(arraySortIR)); + ASSERT_FALSE(arraySortII.isComparableTo(arraySortIR)); Sort setSortI = d_solver.mkSetSort(intSort); Sort setSortR = d_solver.mkSetSort(realSort); // we don't support subtyping for sets - EXPECT_FALSE(setSortI.isComparableTo(setSortR)); - EXPECT_FALSE(setSortI.isSubsortOf(setSortR)); - EXPECT_FALSE(setSortR.isComparableTo(setSortI)); - EXPECT_FALSE(setSortR.isSubsortOf(setSortI)); + ASSERT_FALSE(setSortI.isComparableTo(setSortR)); + ASSERT_FALSE(setSortI.isSubsortOf(setSortR)); + ASSERT_FALSE(setSortR.isComparableTo(setSortI)); + ASSERT_FALSE(setSortR.isSubsortOf(setSortI)); } TEST_F(TestApiSortBlack, sortScopedToString) @@ -370,11 +370,11 @@ TEST_F(TestApiSortBlack, sortScopedToString) std::string name = "uninterp-sort"; Sort bvsort8 = d_solver.mkBitVectorSort(8); Sort uninterp_sort = d_solver.mkUninterpretedSort(name); - EXPECT_EQ(bvsort8.toString(), "(_ BitVec 8)"); - EXPECT_EQ(uninterp_sort.toString(), name); + ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)"); + ASSERT_EQ(uninterp_sort.toString(), name); Solver solver2; - EXPECT_EQ(bvsort8.toString(), "(_ BitVec 8)"); - EXPECT_EQ(uninterp_sort.toString(), name); + ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)"); + ASSERT_EQ(uninterp_sort.toString(), name); } } // namespace test diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 6b032ebd6..50d67688d 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -46,10 +46,10 @@ TEST_F(TestApiTermBlack, getId) Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); ASSERT_NO_THROW(x.getId()); Term y = x; - EXPECT_EQ(x.getId(), y.getId()); + ASSERT_EQ(x.getId(), y.getId()); Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z"); - EXPECT_NE(x.getId(), z.getId()); + ASSERT_NE(x.getId(), z.getId()); } TEST_F(TestApiTermBlack, getKind) @@ -91,7 +91,7 @@ TEST_F(TestApiTermBlack, getKind) Sort seqSort = d_solver.mkSequenceSort(intSort); Term s = d_solver.mkConst(seqSort, "s"); Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s); - EXPECT_EQ(ss.getKind(), SEQ_CONCAT); + ASSERT_EQ(ss.getKind(), SEQ_CONCAT); } TEST_F(TestApiTermBlack, getSort) @@ -106,37 +106,37 @@ TEST_F(TestApiTermBlack, getSort) ASSERT_THROW(n.getSort(), CVC4ApiException); Term x = d_solver.mkVar(bvSort, "x"); ASSERT_NO_THROW(x.getSort()); - EXPECT_EQ(x.getSort(), bvSort); + ASSERT_EQ(x.getSort(), bvSort); Term y = d_solver.mkVar(bvSort, "y"); ASSERT_NO_THROW(y.getSort()); - EXPECT_EQ(y.getSort(), bvSort); + ASSERT_EQ(y.getSort(), bvSort); Term f = d_solver.mkVar(funSort1, "f"); ASSERT_NO_THROW(f.getSort()); - EXPECT_EQ(f.getSort(), funSort1); + ASSERT_EQ(f.getSort(), funSort1); Term p = d_solver.mkVar(funSort2, "p"); ASSERT_NO_THROW(p.getSort()); - EXPECT_EQ(p.getSort(), funSort2); + ASSERT_EQ(p.getSort(), funSort2); Term zero = d_solver.mkInteger(0); ASSERT_NO_THROW(zero.getSort()); - EXPECT_EQ(zero.getSort(), intSort); + ASSERT_EQ(zero.getSort(), intSort); Term f_x = d_solver.mkTerm(APPLY_UF, f, x); ASSERT_NO_THROW(f_x.getSort()); - EXPECT_EQ(f_x.getSort(), intSort); + ASSERT_EQ(f_x.getSort(), intSort); Term f_y = d_solver.mkTerm(APPLY_UF, f, y); ASSERT_NO_THROW(f_y.getSort()); - EXPECT_EQ(f_y.getSort(), intSort); + ASSERT_EQ(f_y.getSort(), intSort); Term sum = d_solver.mkTerm(PLUS, f_x, f_y); ASSERT_NO_THROW(sum.getSort()); - EXPECT_EQ(sum.getSort(), intSort); + ASSERT_EQ(sum.getSort(), intSort); Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero); ASSERT_NO_THROW(p_0.getSort()); - EXPECT_EQ(p_0.getSort(), boolSort); + ASSERT_EQ(p_0.getSort(), boolSort); Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y); ASSERT_NO_THROW(p_f_y.getSort()); - EXPECT_EQ(p_f_y.getSort(), boolSort); + ASSERT_EQ(p_f_y.getSort(), boolSort); } TEST_F(TestApiTermBlack, getOp) @@ -158,13 +158,13 @@ TEST_F(TestApiTermBlack, getOp) Term extb = d_solver.mkTerm(ext, b); ASSERT_TRUE(ab.hasOp()); - EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT)); + ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); ASSERT_FALSE(ab.getOp().isIndexed()); // can compare directly to a Kind (will invoke Op constructor) - EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT)); + ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); ASSERT_TRUE(extb.hasOp()); ASSERT_TRUE(extb.getOp().isIndexed()); - EXPECT_EQ(extb.getOp(), ext); + ASSERT_EQ(extb.getOp(), ext); Term f = d_solver.mkConst(funsort, "f"); Term fx = d_solver.mkTerm(APPLY_UF, f, x); @@ -172,10 +172,10 @@ TEST_F(TestApiTermBlack, getOp) ASSERT_FALSE(f.hasOp()); ASSERT_THROW(f.getOp(), CVC4ApiException); ASSERT_TRUE(fx.hasOp()); - EXPECT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF)); + ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF)); std::vector children(fx.begin(), fx.end()); // testing rebuild from op and children - EXPECT_EQ(fx, d_solver.mkTerm(fx.getOp(), children)); + ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children)); // Test Datatypes Ops Sort sort = d_solver.mkParamSort("T"); @@ -208,15 +208,15 @@ TEST_F(TestApiTermBlack, getOp) ASSERT_TRUE(headTerm.hasOp()); ASSERT_TRUE(tailTerm.hasOp()); - EXPECT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); - EXPECT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); - EXPECT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); - EXPECT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); + ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); + ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); // Test rebuilding children.clear(); children.insert(children.begin(), headTerm.begin(), headTerm.end()); - EXPECT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); + ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); } TEST_F(TestApiTermBlack, isNull) @@ -635,7 +635,7 @@ TEST_F(TestApiTermBlack, termAssignment) Term t1 = d_solver.mkInteger(1); Term t2 = t1; t2 = d_solver.mkInteger(2); - EXPECT_EQ(t1, d_solver.mkInteger(1)); + ASSERT_EQ(t1, d_solver.mkInteger(1)); } TEST_F(TestApiTermBlack, termCompare) @@ -654,8 +654,8 @@ TEST_F(TestApiTermBlack, termChildren) // simple term 2+3 Term two = d_solver.mkInteger(2); Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3)); - EXPECT_EQ(t1[0], two); - EXPECT_EQ(t1.getNumChildren(), 2); + ASSERT_EQ(t1[0], two); + ASSERT_EQ(t1.getNumChildren(), 2); Term tnull; ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException); @@ -666,8 +666,8 @@ TEST_F(TestApiTermBlack, termChildren) Term t2 = d_solver.mkTerm(APPLY_UF, f, two); // due to our higher-order view of terms, we treat f as a child of APPLY_UF ASSERT_EQ(t2.getNumChildren(), 2); - EXPECT_EQ(t2[0], f); - EXPECT_EQ(t2[1], two); + ASSERT_EQ(t2[0], f); + ASSERT_EQ(t2[1], two); ASSERT_THROW(tnull[0], CVC4ApiException); } @@ -685,64 +685,64 @@ TEST_F(TestApiTermBlack, getInteger) Term int10 = d_solver.mkInteger("18446744073709551615"); Term int11 = d_solver.mkInteger("18446744073709551616"); - EXPECT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() + ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() && !int1.isUInt64() && int1.isInteger()); - EXPECT_EQ(int1.getInteger(), "-18446744073709551616"); - EXPECT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64() + ASSERT_EQ(int1.getInteger(), "-18446744073709551616"); + ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64() && !int2.isUInt64() && int2.isInteger()); - EXPECT_EQ(int2.getInteger(), "-18446744073709551615"); - EXPECT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64() + ASSERT_EQ(int2.getInteger(), "-18446744073709551615"); + ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64() && !int3.isUInt64() && int3.isInteger()); - EXPECT_EQ(int3.getInt64(), -4294967296); - EXPECT_EQ(int3.getInteger(), "-4294967296"); - EXPECT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64() + ASSERT_EQ(int3.getInt64(), -4294967296); + ASSERT_EQ(int3.getInteger(), "-4294967296"); + ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64() && !int4.isUInt64() && int4.isInteger()); - EXPECT_EQ(int4.getInt64(), -4294967295); - EXPECT_EQ(int4.getInteger(), "-4294967295"); - EXPECT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64() + ASSERT_EQ(int4.getInt64(), -4294967295); + ASSERT_EQ(int4.getInteger(), "-4294967295"); + ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64() && !int5.isUInt64() && int5.isInteger()); - EXPECT_EQ(int5.getInt32(), -10); - EXPECT_EQ(int5.getInt64(), -10); - EXPECT_EQ(int5.getInteger(), "-10"); - EXPECT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64() + ASSERT_EQ(int5.getInt32(), -10); + ASSERT_EQ(int5.getInt64(), -10); + ASSERT_EQ(int5.getInteger(), "-10"); + ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64() && int6.isUInt64() && int6.isInteger()); - EXPECT_EQ(int6.getInt32(), 0); - EXPECT_EQ(int6.getUInt32(), 0); - EXPECT_EQ(int6.getInt64(), 0); - EXPECT_EQ(int6.getUInt64(), 0); - EXPECT_EQ(int6.getInteger(), "0"); - EXPECT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64() + ASSERT_EQ(int6.getInt32(), 0); + ASSERT_EQ(int6.getUInt32(), 0); + ASSERT_EQ(int6.getInt64(), 0); + ASSERT_EQ(int6.getUInt64(), 0); + ASSERT_EQ(int6.getInteger(), "0"); + ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64() && int7.isUInt64() && int7.isInteger()); - EXPECT_EQ(int7.getInt32(), 10); - EXPECT_EQ(int7.getUInt32(), 10); - EXPECT_EQ(int7.getInt64(), 10); - EXPECT_EQ(int7.getUInt64(), 10); - EXPECT_EQ(int7.getInteger(), "10"); - EXPECT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64() + ASSERT_EQ(int7.getInt32(), 10); + ASSERT_EQ(int7.getUInt32(), 10); + ASSERT_EQ(int7.getInt64(), 10); + ASSERT_EQ(int7.getUInt64(), 10); + ASSERT_EQ(int7.getInteger(), "10"); + ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64() && int8.isUInt64() && int8.isInteger()); - EXPECT_EQ(int8.getUInt32(), 4294967295); - EXPECT_EQ(int8.getInt64(), 4294967295); - EXPECT_EQ(int8.getUInt64(), 4294967295); - EXPECT_EQ(int8.getInteger(), "4294967295"); - EXPECT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64() + ASSERT_EQ(int8.getUInt32(), 4294967295); + ASSERT_EQ(int8.getInt64(), 4294967295); + ASSERT_EQ(int8.getUInt64(), 4294967295); + ASSERT_EQ(int8.getInteger(), "4294967295"); + ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64() && int9.isUInt64() && int9.isInteger()); - EXPECT_EQ(int9.getInt64(), 4294967296); - EXPECT_EQ(int9.getUInt64(), 4294967296); - EXPECT_EQ(int9.getInteger(), "4294967296"); - EXPECT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64() + ASSERT_EQ(int9.getInt64(), 4294967296); + ASSERT_EQ(int9.getUInt64(), 4294967296); + ASSERT_EQ(int9.getInteger(), "4294967296"); + ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64() && int10.isUInt64() && int10.isInteger()); - EXPECT_EQ(int10.getUInt64(), 18446744073709551615ull); - EXPECT_EQ(int10.getInteger(), "18446744073709551615"); - EXPECT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64() + ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull); + ASSERT_EQ(int10.getInteger(), "18446744073709551615"); + ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64() && !int11.isUInt64() && int11.isInteger()); - EXPECT_EQ(int11.getInteger(), "18446744073709551616"); + ASSERT_EQ(int11.getInteger(), "18446744073709551616"); } TEST_F(TestApiTermBlack, getString) { Term s1 = d_solver.mkString("abcde"); - EXPECT_TRUE(s1.isString()); - EXPECT_EQ(s1.getString(), L"abcde"); + ASSERT_TRUE(s1.isString()); + ASSERT_EQ(s1.getString(), L"abcde"); } TEST_F(TestApiTermBlack, substitute) @@ -753,8 +753,8 @@ TEST_F(TestApiTermBlack, substitute) Term xpx = d_solver.mkTerm(PLUS, x, x); Term onepone = d_solver.mkTerm(PLUS, one, one); - EXPECT_EQ(xpx.substitute(x, one), onepone); - EXPECT_EQ(onepone.substitute(one, x), xpx); + ASSERT_EQ(xpx.substitute(x, one), onepone); + ASSERT_EQ(onepone.substitute(one, x), xpx); // incorrect due to type ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException); @@ -768,7 +768,7 @@ TEST_F(TestApiTermBlack, substitute) rs.push_back(y); es.push_back(y); rs.push_back(one); - EXPECT_EQ(xpy.substitute(es, rs), xpone); + ASSERT_EQ(xpy.substitute(es, rs), xpone); // incorrect substitution due to arity rs.pop_back(); @@ -804,8 +804,8 @@ TEST_F(TestApiTermBlack, constArray) Term one = d_solver.mkInteger(1); Term constarr = d_solver.mkConstArray(arrsort, one); - EXPECT_EQ(constarr.getKind(), CONST_ARRAY); - EXPECT_EQ(constarr.getConstArrayBase(), one); + ASSERT_EQ(constarr.getKind(), CONST_ARRAY); + ASSERT_EQ(constarr.getConstArrayBase(), one); ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException); arrsort = @@ -825,7 +825,7 @@ TEST_F(TestApiTermBlack, constSequenceElements) Sort seqsort = d_solver.mkSequenceSort(realsort); Term s = d_solver.mkEmptySequence(seqsort); - EXPECT_EQ(s.getKind(), CONST_SEQUENCE); + ASSERT_EQ(s.getKind(), CONST_SEQUENCE); // empty sequence has zero elements std::vector cs = s.getConstSequenceElements(); ASSERT_TRUE(cs.empty()); @@ -840,9 +840,9 @@ TEST_F(TestApiTermBlack, termScopedToString) { Sort intsort = d_solver.getIntegerSort(); Term x = d_solver.mkConst(intsort, "x"); - EXPECT_EQ(x.toString(), "x"); + ASSERT_EQ(x.toString(), "x"); Solver solver2; - EXPECT_EQ(x.toString(), "x"); + ASSERT_EQ(x.toString(), "x"); } } // namespace test } // namespace CVC4 diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp index c8c98818f..6c0a2e3b5 100644 --- a/test/unit/base/map_util_black.cpp +++ b/test/unit/base/map_util_black.cpp @@ -66,13 +66,13 @@ TEST_F(TestMapBlack, map) ASSERT_TRUE(CVC4::ContainsKey(map, "key")); ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); if (std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); *found_value = "new value"; } - EXPECT_EQ(FindOrDie(map, "other"), "new value"); + ASSERT_EQ(FindOrDie(map, "other"), "new value"); } TEST_F(TestMapBlack, constant_map) @@ -83,10 +83,10 @@ TEST_F(TestMapBlack, constant_map) if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key."); } @@ -97,13 +97,13 @@ TEST_F(TestMapBlack, unordered_map) ASSERT_TRUE(CVC4::ContainsKey(map, "key")); ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); if (std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); *found_value = "new value"; } - EXPECT_EQ(FindOrDie(map, "other"), "new value"); + ASSERT_EQ(FindOrDie(map, "other"), "new value"); } TEST_F(TestMapBlack, const_unordered_map) @@ -115,10 +115,10 @@ TEST_F(TestMapBlack, const_unordered_map) if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key."); } @@ -155,10 +155,10 @@ TEST_F(TestMapBlack, CDHashMap) if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); } TEST_F(TestMapBlack, const_CDHashMap) @@ -173,10 +173,10 @@ TEST_F(TestMapBlack, const_CDHashMap) if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); } TEST_F(TestMapBlack, CDInsertHashMap) @@ -190,10 +190,10 @@ TEST_F(TestMapBlack, CDInsertHashMap) if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); } TEST_F(TestMapBlack, const_CDInsertHashMap) @@ -207,10 +207,10 @@ TEST_F(TestMapBlack, const_CDInsertHashMap) ASSERT_FALSE(CVC4::ContainsKey(map, "non key")); if (const std::string* found_value = FindOrNull(map, "other")) { - EXPECT_EQ(*found_value, "entry"); + ASSERT_EQ(*found_value, "entry"); } - EXPECT_EQ(FindOrNull(map, "non key"), nullptr); - EXPECT_EQ(FindOrDie(map, "other"), "entry"); + ASSERT_EQ(FindOrNull(map, "non key"), nullptr); + ASSERT_EQ(FindOrDie(map, "other"), "entry"); } } // namespace test } // namespace CVC4 diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index 71da10d0c..47db6c758 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -53,22 +53,22 @@ class TestContextCDListBlack : public TestContext ASSERT_TRUE(list.empty()); for (int32_t i = 0; i < n; ++i) { - EXPECT_EQ(list.size(), (uint32_t)i); + ASSERT_EQ(list.size(), (uint32_t)i); list.push_back(i); ASSERT_FALSE(list.empty()); - EXPECT_EQ(list.back(), i); + ASSERT_EQ(list.back(), i); int32_t i2 = 0; for (CDList::const_iterator j = list.begin(); j != list.end(); ++j) { - EXPECT_EQ(*j, i2++); + ASSERT_EQ(*j, i2++); } } - EXPECT_EQ(list.size(), (uint32_t)n); + ASSERT_EQ(list.size(), (uint32_t)n); for (int32_t i = 0; i < n; ++i) { - EXPECT_EQ(list[i], i); + ASSERT_EQ(list[i], i); } } }; @@ -114,25 +114,25 @@ TEST_F(TestContextCDListBlack, destructor_called) listF.push_back(shouldAlsoRemainFalseDSO); listF.push_back(aThirdFalseDSO); - EXPECT_EQ(shouldRemainFalse, false); - EXPECT_EQ(shouldFlipToTrue, false); - EXPECT_EQ(alsoFlipToTrue, false); - EXPECT_EQ(shouldAlsoRemainFalse, false); - EXPECT_EQ(aThirdFalse, false); + ASSERT_EQ(shouldRemainFalse, false); + ASSERT_EQ(shouldFlipToTrue, false); + ASSERT_EQ(alsoFlipToTrue, false); + ASSERT_EQ(shouldAlsoRemainFalse, false); + ASSERT_EQ(aThirdFalse, false); d_context->pop(); - EXPECT_EQ(shouldRemainFalse, false); - EXPECT_EQ(shouldFlipToTrue, true); - EXPECT_EQ(alsoFlipToTrue, true); - EXPECT_EQ(shouldAlsoRemainFalse, false); - EXPECT_EQ(aThirdFalse, false); + ASSERT_EQ(shouldRemainFalse, false); + ASSERT_EQ(shouldFlipToTrue, true); + ASSERT_EQ(alsoFlipToTrue, true); + ASSERT_EQ(shouldAlsoRemainFalse, false); + ASSERT_EQ(aThirdFalse, false); } TEST_F(TestContextCDListBlack, empty_iterator) { CDList* list = new (true) CDList(d_context.get()); - EXPECT_EQ(list->begin(), list->end()); + ASSERT_EQ(list->begin(), list->end()); list->deleteSelf(); } diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp index 440d95d40..cbf6a1cd9 100644 --- a/test/unit/context/cdo_black.cpp +++ b/test/unit/context/cdo_black.cpp @@ -37,14 +37,14 @@ TEST_F(TestContextCDOBlack, cdo) // Test that push/pop maintains the original value CDO a1(d_context.get()); a1 = 5; - EXPECT_EQ(d_context->getLevel(), 0); + ASSERT_EQ(d_context->getLevel(), 0); d_context->push(); a1 = 10; - EXPECT_EQ(d_context->getLevel(), 1); - EXPECT_EQ(a1, 10); + ASSERT_EQ(d_context->getLevel(), 1); + ASSERT_EQ(a1, 10); d_context->pop(); - EXPECT_EQ(d_context->getLevel(), 0); - EXPECT_EQ(a1, 5); + ASSERT_EQ(d_context->getLevel(), 0); + ASSERT_EQ(a1, 5); } } // namespace test diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp index 6dfdba0c3..7a8fa10a3 100644 --- a/test/unit/context/context_black.cpp +++ b/test/unit/context/context_black.cpp @@ -117,10 +117,10 @@ TEST_F(TestContextBlack, pre_post_notify) { MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false); - EXPECT_EQ(a.d_ncalls, 0); - EXPECT_EQ(b.d_ncalls, 0); - EXPECT_EQ(c.d_ncalls, 0); - EXPECT_EQ(d.d_ncalls, 0); + ASSERT_EQ(a.d_ncalls, 0); + ASSERT_EQ(b.d_ncalls, 0); + ASSERT_EQ(c.d_ncalls, 0); + ASSERT_EQ(d.d_ncalls, 0); MyContextObj w(d_context.get(), a); MyContextObj x(d_context.get(), b); @@ -134,15 +134,15 @@ TEST_F(TestContextBlack, pre_post_notify) y.makeCurrent(); z.makeCurrent(); - EXPECT_EQ(a.d_ncalls, 0); - EXPECT_EQ(b.d_ncalls, 0); - EXPECT_EQ(c.d_ncalls, 0); - EXPECT_EQ(d.d_ncalls, 0); + ASSERT_EQ(a.d_ncalls, 0); + ASSERT_EQ(b.d_ncalls, 0); + ASSERT_EQ(c.d_ncalls, 0); + ASSERT_EQ(d.d_ncalls, 0); - EXPECT_EQ(w.d_ncalls, 0); - EXPECT_EQ(x.d_ncalls, 0); - EXPECT_EQ(y.d_ncalls, 0); - EXPECT_EQ(z.d_ncalls, 0); + ASSERT_EQ(w.d_ncalls, 0); + ASSERT_EQ(x.d_ncalls, 0); + ASSERT_EQ(y.d_ncalls, 0); + ASSERT_EQ(z.d_ncalls, 0); d_context->push(); @@ -151,39 +151,39 @@ TEST_F(TestContextBlack, pre_post_notify) y.makeCurrent(); z.makeCurrent(); - EXPECT_EQ(a.d_ncalls, 0); - EXPECT_EQ(b.d_ncalls, 0); - EXPECT_EQ(c.d_ncalls, 0); - EXPECT_EQ(d.d_ncalls, 0); + ASSERT_EQ(a.d_ncalls, 0); + ASSERT_EQ(b.d_ncalls, 0); + ASSERT_EQ(c.d_ncalls, 0); + ASSERT_EQ(d.d_ncalls, 0); - EXPECT_EQ(w.d_ncalls, 0); - EXPECT_EQ(x.d_ncalls, 0); - EXPECT_EQ(y.d_ncalls, 0); - EXPECT_EQ(z.d_ncalls, 0); + ASSERT_EQ(w.d_ncalls, 0); + ASSERT_EQ(x.d_ncalls, 0); + ASSERT_EQ(y.d_ncalls, 0); + ASSERT_EQ(z.d_ncalls, 0); d_context->pop(); - EXPECT_EQ(a.d_ncalls, 1); - EXPECT_EQ(b.d_ncalls, 1); - EXPECT_EQ(c.d_ncalls, 1); - EXPECT_EQ(d.d_ncalls, 1); + ASSERT_EQ(a.d_ncalls, 1); + ASSERT_EQ(b.d_ncalls, 1); + ASSERT_EQ(c.d_ncalls, 1); + ASSERT_EQ(d.d_ncalls, 1); - EXPECT_EQ(w.d_ncalls, 1); - EXPECT_EQ(x.d_ncalls, 0); - EXPECT_EQ(y.d_ncalls, 1); - EXPECT_EQ(z.d_ncalls, 0); + ASSERT_EQ(w.d_ncalls, 1); + ASSERT_EQ(x.d_ncalls, 0); + ASSERT_EQ(y.d_ncalls, 1); + ASSERT_EQ(z.d_ncalls, 0); d_context->pop(); - EXPECT_EQ(a.d_ncalls, 2); - EXPECT_EQ(b.d_ncalls, 2); - EXPECT_EQ(c.d_ncalls, 2); - EXPECT_EQ(d.d_ncalls, 2); + ASSERT_EQ(a.d_ncalls, 2); + ASSERT_EQ(b.d_ncalls, 2); + ASSERT_EQ(c.d_ncalls, 2); + ASSERT_EQ(d.d_ncalls, 2); - EXPECT_EQ(w.d_ncalls, 2); - EXPECT_EQ(x.d_ncalls, 1); - EXPECT_EQ(y.d_ncalls, 2); - EXPECT_EQ(z.d_ncalls, 1); + ASSERT_EQ(w.d_ncalls, 2); + ASSERT_EQ(x.d_ncalls, 1); + ASSERT_EQ(y.d_ncalls, 2); + ASSERT_EQ(z.d_ncalls, 1); } catch (Exception& e) { @@ -211,28 +211,28 @@ TEST_F(TestContextBlack, top_scope_context_obj) MyContextObj x(true, d_context.get(), n); MyContextObj y(false, d_context.get(), n); - EXPECT_EQ(x.d_nsaves, 0); - EXPECT_EQ(y.d_nsaves, 0); + ASSERT_EQ(x.d_nsaves, 0); + ASSERT_EQ(y.d_nsaves, 0); x.makeCurrent(); y.makeCurrent(); - EXPECT_EQ(x.d_nsaves, 0); - EXPECT_EQ(y.d_nsaves, 1); + ASSERT_EQ(x.d_nsaves, 0); + ASSERT_EQ(y.d_nsaves, 1); d_context->push(); x.makeCurrent(); y.makeCurrent(); - EXPECT_EQ(x.d_nsaves, 1); - EXPECT_EQ(y.d_nsaves, 2); + ASSERT_EQ(x.d_nsaves, 1); + ASSERT_EQ(y.d_nsaves, 2); d_context->pop(); d_context->pop(); - EXPECT_EQ(x.d_nsaves, 1); - EXPECT_EQ(y.d_nsaves, 2); + ASSERT_EQ(x.d_nsaves, 1); + ASSERT_EQ(y.d_nsaves, 2); } } // namespace test diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp index c8ea59848..a6ea4d880 100644 --- a/test/unit/context/context_white.cpp +++ b/test/unit/context/context_white.cpp @@ -32,152 +32,152 @@ TEST_F(TestContextWhite, simple) { Scope* s = d_context->getTopScope(); - EXPECT_EQ(s, d_context->getBottomScope()); - EXPECT_EQ(d_context->getLevel(), 0); - EXPECT_EQ(d_context->d_scopeList.size(), 1); + ASSERT_EQ(s, d_context->getBottomScope()); + ASSERT_EQ(d_context->getLevel(), 0); + ASSERT_EQ(d_context->d_scopeList.size(), 1); - EXPECT_EQ(s->d_pContext, d_context.get()); - EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(s->d_level, 0); - EXPECT_EQ(s->d_pContextObjList, nullptr); + ASSERT_EQ(s->d_pContext, d_context.get()); + ASSERT_EQ(s->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(s->d_level, 0); + ASSERT_EQ(s->d_pContextObjList, nullptr); CDO a(d_context.get()); - EXPECT_EQ(s->d_pContext, d_context.get()); - EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(s->d_level, 0); - EXPECT_EQ(s->d_pContextObjList, &a); + ASSERT_EQ(s->d_pContext, d_context.get()); + ASSERT_EQ(s->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(s->d_level, 0); + ASSERT_EQ(s->d_pContextObjList, &a); - EXPECT_EQ(a.d_pScope, s); - EXPECT_EQ(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList); + ASSERT_EQ(a.d_pScope, s); + ASSERT_EQ(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList); CDO b(d_context.get()); - EXPECT_EQ(s->d_pContext, d_context.get()); - EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(s->d_level, 0); - EXPECT_EQ(s->d_pContextObjList, &b); + ASSERT_EQ(s->d_pContext, d_context.get()); + ASSERT_EQ(s->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(s->d_level, 0); + ASSERT_EQ(s->d_pContextObjList, &b); - EXPECT_EQ(a.d_pScope, s); - EXPECT_EQ(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + ASSERT_EQ(a.d_pScope, s); + ASSERT_EQ(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); - EXPECT_EQ(b.d_pScope, s); - EXPECT_EQ(b.d_pContextObjRestore, nullptr); - EXPECT_EQ(b.d_pContextObjNext, &a); - EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); + ASSERT_EQ(b.d_pScope, s); + ASSERT_EQ(b.d_pContextObjRestore, nullptr); + ASSERT_EQ(b.d_pContextObjNext, &a); + ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); d_context->push(); Scope* t = d_context->getTopScope(); - EXPECT_NE(s, t); + ASSERT_NE(s, t); - EXPECT_EQ(s, d_context->getBottomScope()); - EXPECT_EQ(d_context->getLevel(), 1); - EXPECT_EQ(d_context->d_scopeList.size(), 2); + ASSERT_EQ(s, d_context->getBottomScope()); + ASSERT_EQ(d_context->getLevel(), 1); + ASSERT_EQ(d_context->d_scopeList.size(), 2); - EXPECT_EQ(s->d_pContext, d_context.get()); - EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(s->d_level, 0); - EXPECT_EQ(s->d_pContextObjList, &b); + ASSERT_EQ(s->d_pContext, d_context.get()); + ASSERT_EQ(s->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(s->d_level, 0); + ASSERT_EQ(s->d_pContextObjList, &b); - EXPECT_EQ(t->d_pContext, d_context.get()); - EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(t->d_level, 1); - EXPECT_EQ(t->d_pContextObjList, nullptr); + ASSERT_EQ(t->d_pContext, d_context.get()); + ASSERT_EQ(t->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(t->d_level, 1); + ASSERT_EQ(t->d_pContextObjList, nullptr); - EXPECT_EQ(a.d_pScope, s); - EXPECT_EQ(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + ASSERT_EQ(a.d_pScope, s); + ASSERT_EQ(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); - EXPECT_EQ(b.d_pScope, s); - EXPECT_EQ(b.d_pContextObjRestore, nullptr); - EXPECT_EQ(b.d_pContextObjNext, &a); - EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); + ASSERT_EQ(b.d_pScope, s); + ASSERT_EQ(b.d_pContextObjRestore, nullptr); + ASSERT_EQ(b.d_pContextObjNext, &a); + ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); a = 5; - EXPECT_EQ(t->d_pContext, d_context.get()); - EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(t->d_level, 1); - EXPECT_EQ(t->d_pContextObjList, &a); + ASSERT_EQ(t->d_pContext, d_context.get()); + ASSERT_EQ(t->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(t->d_level, 1); + ASSERT_EQ(t->d_pContextObjList, &a); - EXPECT_EQ(a.d_pScope, t); - EXPECT_NE(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList); + ASSERT_EQ(a.d_pScope, t); + ASSERT_NE(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList); b = 3; - EXPECT_EQ(t->d_pContext, d_context.get()); - EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(t->d_level, 1); - EXPECT_EQ(t->d_pContextObjList, &b); + ASSERT_EQ(t->d_pContext, d_context.get()); + ASSERT_EQ(t->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(t->d_level, 1); + ASSERT_EQ(t->d_pContextObjList, &b); - EXPECT_EQ(a.d_pScope, t); - EXPECT_NE(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + ASSERT_EQ(a.d_pScope, t); + ASSERT_NE(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); - EXPECT_EQ(b.d_pScope, t); - EXPECT_NE(b.d_pContextObjRestore, nullptr); - EXPECT_EQ(b.d_pContextObjNext, &a); - EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); + ASSERT_EQ(b.d_pScope, t); + ASSERT_NE(b.d_pContextObjRestore, nullptr); + ASSERT_EQ(b.d_pContextObjNext, &a); + ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); d_context->push(); Scope* u = d_context->getTopScope(); - EXPECT_NE(u, t); - EXPECT_NE(u, s); + ASSERT_NE(u, t); + ASSERT_NE(u, s); CDO c(d_context.get()); c = 4; - EXPECT_EQ(c.d_pScope, u); - EXPECT_NE(c.d_pContextObjRestore, nullptr); - EXPECT_EQ(c.d_pContextObjNext, nullptr); - EXPECT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList); + ASSERT_EQ(c.d_pScope, u); + ASSERT_NE(c.d_pContextObjRestore, nullptr); + ASSERT_EQ(c.d_pContextObjNext, nullptr); + ASSERT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList); d_context->pop(); - EXPECT_EQ(t->d_pContext, d_context.get()); - EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(t->d_level, 1); - EXPECT_EQ(t->d_pContextObjList, &b); + ASSERT_EQ(t->d_pContext, d_context.get()); + ASSERT_EQ(t->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(t->d_level, 1); + ASSERT_EQ(t->d_pContextObjList, &b); - EXPECT_EQ(a.d_pScope, t); - EXPECT_NE(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + ASSERT_EQ(a.d_pScope, t); + ASSERT_NE(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); - EXPECT_EQ(b.d_pScope, t); - EXPECT_NE(b.d_pContextObjRestore, nullptr); - EXPECT_EQ(b.d_pContextObjNext, &a); - EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); + ASSERT_EQ(b.d_pScope, t); + ASSERT_NE(b.d_pContextObjRestore, nullptr); + ASSERT_EQ(b.d_pContextObjNext, &a); + ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); d_context->pop(); - EXPECT_EQ(s->d_pContext, d_context.get()); - EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); - EXPECT_EQ(s->d_level, 0); - EXPECT_EQ(s->d_pContextObjList, &c); - - EXPECT_EQ(a.d_pScope, s); - EXPECT_EQ(a.d_pContextObjRestore, nullptr); - EXPECT_EQ(a.d_pContextObjNext, nullptr); - EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); - - EXPECT_EQ(b.d_pScope, s); - EXPECT_EQ(b.d_pContextObjRestore, nullptr); - EXPECT_EQ(b.d_pContextObjNext, &a); - EXPECT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext); - - EXPECT_EQ(c.d_pScope, s); - EXPECT_EQ(c.d_pContextObjRestore, nullptr); - EXPECT_EQ(c.d_pContextObjNext, &b); - EXPECT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList); + ASSERT_EQ(s->d_pContext, d_context.get()); + ASSERT_EQ(s->d_pCMM, d_context->d_pCMM); + ASSERT_EQ(s->d_level, 0); + ASSERT_EQ(s->d_pContextObjList, &c); + + ASSERT_EQ(a.d_pScope, s); + ASSERT_EQ(a.d_pContextObjRestore, nullptr); + ASSERT_EQ(a.d_pContextObjNext, nullptr); + ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + ASSERT_EQ(b.d_pScope, s); + ASSERT_EQ(b.d_pContextObjRestore, nullptr); + ASSERT_EQ(b.d_pContextObjNext, &a); + ASSERT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext); + + ASSERT_EQ(c.d_pScope, s); + ASSERT_EQ(c.d_pContextObjRestore, nullptr); + ASSERT_EQ(c.d_pContextObjNext, &b); + ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList); } } // namespace test } // namespace CVC4 diff --git a/test/unit/expr/attribute_black.cpp b/test/unit/expr/attribute_black.cpp index cd2745a07..da15f6b63 100644 --- a/test/unit/expr/attribute_black.cpp +++ b/test/unit/expr/attribute_black.cpp @@ -64,7 +64,7 @@ TEST_F(TestExprBlackAttribute, ints) ASSERT_FALSE(node->getAttribute(attr, data0)); node->setAttribute(attr, val); ASSERT_TRUE(node->getAttribute(attr, data1)); - EXPECT_EQ(data1, val); + ASSERT_EQ(data1, val); delete node; } @@ -82,7 +82,7 @@ TEST_F(TestExprBlackAttribute, tnodes) ASSERT_FALSE(node->getAttribute(attr, data0)); node->setAttribute(attr, val); ASSERT_TRUE(node->getAttribute(attr, data1)); - EXPECT_EQ(data1, val); + ASSERT_EQ(data1, val); delete node; } @@ -100,7 +100,7 @@ TEST_F(TestExprBlackAttribute, strings) ASSERT_FALSE(node->getAttribute(attr, data0)); node->setAttribute(attr, val); ASSERT_TRUE(node->getAttribute(attr, data1)); - EXPECT_EQ(data1, val); + ASSERT_EQ(data1, val); delete node; } @@ -116,10 +116,10 @@ TEST_F(TestExprBlackAttribute, bools) BoolAttribute attr; ASSERT_TRUE(node->getAttribute(attr, data0)); - EXPECT_EQ(false, data0); + ASSERT_EQ(false, data0); node->setAttribute(attr, val); ASSERT_TRUE(node->getAttribute(attr, data1)); - EXPECT_EQ(data1, val); + ASSERT_EQ(data1, val); delete node; } diff --git a/test/unit/expr/attribute_white.cpp b/test/unit/expr/attribute_white.cpp index 1403fbe21..ab99b842f 100644 --- a/test/unit/expr/attribute_white.cpp +++ b/test/unit/expr/attribute_white.cpp @@ -80,33 +80,33 @@ TEST_F(TestExprWhiteAttribute, attribute_ids) // those that have already been assigned. unsigned lastId = attr::LastAttributeId::getId(); - EXPECT_LT(VarNameAttr::s_id, lastId); - EXPECT_LT(TestStringAttr1::s_id, lastId); - EXPECT_LT(TestStringAttr2::s_id, lastId); + ASSERT_LT(VarNameAttr::s_id, lastId); + ASSERT_LT(TestStringAttr1::s_id, lastId); + ASSERT_LT(TestStringAttr2::s_id, lastId); - EXPECT_NE(VarNameAttr::s_id, TestStringAttr1::s_id); - EXPECT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); - EXPECT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); + ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id); + ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); + ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); lastId = attr::LastAttributeId::getId(); - EXPECT_LT(TestFlag1::s_id, lastId); - EXPECT_LT(TestFlag2::s_id, lastId); - EXPECT_LT(TestFlag3::s_id, lastId); - EXPECT_LT(TestFlag4::s_id, lastId); - EXPECT_LT(TestFlag5::s_id, lastId); - EXPECT_NE(TestFlag1::s_id, TestFlag2::s_id); - EXPECT_NE(TestFlag1::s_id, TestFlag3::s_id); - EXPECT_NE(TestFlag1::s_id, TestFlag4::s_id); - EXPECT_NE(TestFlag1::s_id, TestFlag5::s_id); - EXPECT_NE(TestFlag2::s_id, TestFlag3::s_id); - EXPECT_NE(TestFlag2::s_id, TestFlag4::s_id); - EXPECT_NE(TestFlag2::s_id, TestFlag5::s_id); - EXPECT_NE(TestFlag3::s_id, TestFlag4::s_id); - EXPECT_NE(TestFlag3::s_id, TestFlag5::s_id); - EXPECT_NE(TestFlag4::s_id, TestFlag5::s_id); + ASSERT_LT(TestFlag1::s_id, lastId); + ASSERT_LT(TestFlag2::s_id, lastId); + ASSERT_LT(TestFlag3::s_id, lastId); + ASSERT_LT(TestFlag4::s_id, lastId); + ASSERT_LT(TestFlag5::s_id, lastId); + ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id); lastId = attr::LastAttributeId::getId(); - EXPECT_LT(TypeAttr::s_id, lastId); + ASSERT_LT(TypeAttr::s_id, lastId); } TEST_F(TestExprWhiteAttribute, attributes) @@ -305,25 +305,25 @@ TEST_F(TestExprWhiteAttribute, attributes) Debug("boolattr") << "set flag 5 on unnamed to T\n"; unnamed.setAttribute(TestFlag5(), true); - EXPECT_EQ(a.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(a.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(a.getAttribute(VarNameAttr()), ""); + ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); - EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); - EXPECT_EQ(b.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(b.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(b.getAttribute(VarNameAttr()), ""); + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); - EXPECT_NE(c.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); - EXPECT_EQ(c.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(c.getAttribute(VarNameAttr()), ""); + ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); - EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); @@ -386,25 +386,25 @@ TEST_F(TestExprWhiteAttribute, attributes) b.setAttribute(TestStringAttr1(), "bar"); c.setAttribute(TestStringAttr1(), "baz"); - EXPECT_EQ(a.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(a.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(a.getAttribute(VarNameAttr()), ""); + ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); - EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); - EXPECT_EQ(b.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(b.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(b.getAttribute(VarNameAttr()), ""); + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); - EXPECT_NE(c.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); - EXPECT_EQ(c.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(c.getAttribute(VarNameAttr()), ""); + ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); - EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); @@ -422,25 +422,25 @@ TEST_F(TestExprWhiteAttribute, attributes) b.setAttribute(VarNameAttr(), "c"); c.setAttribute(VarNameAttr(), "a"); - EXPECT_EQ(c.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(c.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(c.getAttribute(VarNameAttr()), ""); - - EXPECT_NE(a.getAttribute(VarNameAttr()), "a"); - EXPECT_EQ(a.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(a.getAttribute(VarNameAttr()), ""); - - EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(b.getAttribute(VarNameAttr()), "b"); - EXPECT_EQ(b.getAttribute(VarNameAttr()), "c"); - EXPECT_NE(b.getAttribute(VarNameAttr()), ""); - - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); - EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); - EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + ASSERT_EQ(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(a.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); } diff --git a/test/unit/expr/kind_black.cpp b/test/unit/expr/kind_black.cpp index 93b7c15cb..a5bba4d99 100644 --- a/test/unit/expr/kind_black.cpp +++ b/test/unit/expr/kind_black.cpp @@ -57,16 +57,16 @@ class TestExprBlackKind : public TestExprBlack TEST_F(TestExprBlackKind, equality) { - EXPECT_EQ(undefined, UNDEFINED_KIND); - EXPECT_EQ(last, LAST_KIND); + ASSERT_EQ(undefined, UNDEFINED_KIND); + ASSERT_EQ(last, LAST_KIND); } TEST_F(TestExprBlackKind, order) { - EXPECT_LT((int32_t)undefined, (int32_t)null); - EXPECT_LT((int32_t)null, (int32_t)last); - EXPECT_LT((int32_t)undefined, (int32_t)last); - EXPECT_LT((int32_t)last, (int32_t)unknown); + ASSERT_LT((int32_t)undefined, (int32_t)null); + ASSERT_LT((int32_t)null, (int32_t)last); + ASSERT_LT((int32_t)undefined, (int32_t)last); + ASSERT_LT((int32_t)last, (int32_t)unknown); } TEST_F(TestExprBlackKind, output) @@ -84,7 +84,7 @@ TEST_F(TestExprBlackKind, output_concat) << "NULL" << "LAST_KIND" << "?"; - EXPECT_EQ(act.str(), exp.str()); + ASSERT_EQ(act.str(), exp.str()); } } // namespace test } // namespace CVC4 diff --git a/test/unit/expr/node_algorithm_black.cpp b/test/unit/expr/node_algorithm_black.cpp index dd1982b1c..95018d9f1 100644 --- a/test/unit/expr/node_algorithm_black.cpp +++ b/test/unit/expr/node_algorithm_black.cpp @@ -43,8 +43,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1) Node n = d_nodeManager->mkNode(NOT, x); std::unordered_set syms; getSymbols(n, syms); - EXPECT_EQ(syms.size(), 1); - EXPECT_NE(syms.find(x), syms.end()); + ASSERT_EQ(syms.size(), 1); + ASSERT_NE(syms.find(x), syms.end()); } TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) @@ -74,10 +74,10 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) getSymbols(res, syms); // assertions - EXPECT_EQ(syms.size(), 2); - EXPECT_NE(syms.find(x), syms.end()); - EXPECT_NE(syms.find(y), syms.end()); - EXPECT_EQ(syms.find(var), syms.end()); + ASSERT_EQ(syms.size(), 2); + ASSERT_NE(syms.find(x), syms.end()); + ASSERT_NE(syms.find(y), syms.end()); + ASSERT_EQ(syms.find(var), syms.end()); } TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) @@ -104,34 +104,34 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) // Verify result // We should have only integer, bv and boolean as types - EXPECT_EQ(result.size(), 3); - EXPECT_NE(result.find(*d_intTypeNode), result.end()); - EXPECT_NE(result.find(*d_boolTypeNode), result.end()); - EXPECT_NE(result.find(*d_bvTypeNode), result.end()); + ASSERT_EQ(result.size(), 3); + ASSERT_NE(result.find(*d_intTypeNode), result.end()); + ASSERT_NE(result.find(*d_boolTypeNode), result.end()); + ASSERT_NE(result.find(*d_bvTypeNode), result.end()); // in integers, we should only have plus and mult as operators - EXPECT_EQ(result[*d_intTypeNode].size(), 2); - EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)), + ASSERT_EQ(result[*d_intTypeNode].size(), 2); + ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)), result[*d_intTypeNode].end()); - EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)), + ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)), result[*d_intTypeNode].end()); // in booleans, we should only have "=" and "and" as an operator. - EXPECT_EQ(result[*d_boolTypeNode].size(), 2); - EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)), + ASSERT_EQ(result[*d_boolTypeNode].size(), 2); + ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)), result[*d_boolTypeNode].end()); - EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)), + ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)), result[*d_boolTypeNode].end()); // in bv, we should only have "extract" as an operator. - EXPECT_EQ(result[*d_boolTypeNode].size(), 2); + ASSERT_EQ(result[*d_boolTypeNode].size(), 2); Node extractOp1 = d_nodeManager->mkConst(BitVectorExtract(1, 0)); Node extractOp2 = d_nodeManager->mkConst(BitVectorExtract(3, 2)); - EXPECT_NE(result[*d_bvTypeNode].find(extractOp1), + ASSERT_NE(result[*d_bvTypeNode].find(extractOp1), result[*d_bvTypeNode].end()); - EXPECT_NE(result[*d_bvTypeNode].find(extractOp2), + ASSERT_NE(result[*d_bvTypeNode].find(extractOp2), result[*d_bvTypeNode].end()); } @@ -150,15 +150,15 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) // check reflexivity ASSERT_TRUE(match(n1, n1, subs)); - EXPECT_EQ(subs.size(), 0); + ASSERT_EQ(subs.size(), 0); Node n2 = d_nodeManager->mkNode(MULT, two, a); subs.clear(); // check instance ASSERT_TRUE(match(n1, n2, subs)); - EXPECT_EQ(subs.size(), 1); - EXPECT_EQ(subs[x], a); + ASSERT_EQ(subs.size(), 1); + ASSERT_EQ(subs[x], a); // should return false for flipped arguments (match is not symmetric) ASSERT_FALSE(match(n2, n1, subs)); @@ -195,8 +195,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match) // implementation: check if the cache works correctly ASSERT_TRUE(match(n1, n2, subs)); - EXPECT_EQ(subs.size(), 1); - EXPECT_EQ(subs[x], a); + ASSERT_EQ(subs.size(), 1); + ASSERT_EQ(subs[x], a); } } // namespace test } // namespace CVC4 diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index 59f8186ac..4d60dea52 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -64,7 +64,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite // (singleton (singleton_op Int) 1) // (as emptyset (Set Real))) TS_ASSERT_THROWS(d_slv->mkTerm(UNION, singletonInt, emptyReal), - CVC4ApiException); + CVC4ApiException&); // (union // (singleton (singleton_op Real) 1) // (as emptyset (Set Real)))