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());
}
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<DatatypeDecl> 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)
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");
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);
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<std::pair<std::string, Sort>> 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)
// 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");
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);
Sort pairType = d_solver.mkDatatypeSort(pairSpec);
- EXPECT_TRUE(pairType.getDatatype().isParametric());
+ ASSERT_TRUE(pairType.getDatatype().isParametric());
v.clear();
v.push_back(d_solver.getIntegerSort());
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)
std::vector<Sort> 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
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
// 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
// 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
// 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)
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
ASSERT_THROW(plus.getIndices<uint32_t>(), 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);
}
Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
ASSERT_TRUE(divisible_ot.isIndexed());
std::string divisible_idx = divisible_ot.getIndices<std::string>();
- 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<std::string>();
- EXPECT_EQ(record_update_idx, "test");
+ ASSERT_EQ(record_update_idx, "test");
ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
}
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<uint32_t>();
- EXPECT_EQ(bitvector_repeat_idx, 5);
+ ASSERT_EQ(bitvector_repeat_idx, 5);
ASSERT_THROW(
(bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
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>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- EXPECT_EQ(tuple_update_idx, 5);
+ ASSERT_EQ(tuple_update_idx, 5);
ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
}
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
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)
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
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));
}
{
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\"");
}
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)
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++;
}
}
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");
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)
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);
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(
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);
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<Sort> 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);
}
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);
}
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);
}
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);
}
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());
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);
}
{
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)
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
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)
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)
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)
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);
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<Term> 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");
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)
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)
// 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);
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);
}
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)
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);
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();
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 =
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<Term> cs = s.getConstSequenceElements();
ASSERT_TRUE(cs.empty());
{
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
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)
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.");
}
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)
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.");
}
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)
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)
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)
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
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<int32_t>::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);
}
}
};
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<int>* list = new (true) CDList<int>(d_context.get());
- EXPECT_EQ(list->begin(), list->end());
+ ASSERT_EQ(list->begin(), list->end());
list->deleteSelf();
}
// Test that push/pop maintains the original value
CDO<int> 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
{
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);
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();
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)
{
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
{
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<int> 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<int> 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<int> 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
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;
}
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;
}
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;
}
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;
}
// those that have already been assigned.
unsigned lastId = attr::LastAttributeId<std::string, false>::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<bool, false>::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<TypeNode, false>::getId();
- EXPECT_LT(TypeAttr::s_id, lastId);
+ ASSERT_LT(TypeAttr::s_id, lastId);
}
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()));
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()));
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()));
}
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)
<< "NULL"
<< "LAST_KIND"
<< "?";
- EXPECT_EQ(act.str(), exp.str());
+ ASSERT_EQ(act.str(), exp.str());
}
} // namespace test
} // namespace CVC4
Node n = d_nodeManager->mkNode(NOT, x);
std::unordered_set<Node, NodeHashFunction> 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)
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)
// 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>(BitVectorExtract(1, 0));
Node extractOp2 =
d_nodeManager->mkConst<BitVectorExtract>(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());
}
// 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));
// 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
// (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)))