diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/api/solver_black.h | 18 | ||||
| -rw-r--r-- | test/unit/util/datatype_black.h | 32 |
2 files changed, 36 insertions, 14 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 41c4a86dd..374a3ff2a 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -624,6 +624,7 @@ void SolverBlack::testMkTermFromOpTerm() OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); // list datatype + Sort sort = d_solver->mkParamSort("T"); DatatypeDecl listDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); @@ -776,17 +777,21 @@ void SolverBlack::testMkConstArray() void SolverBlack::testDeclareDatatype() { - DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); std::vector<DatatypeConstructorDecl> ctors1 = {nil}; - std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil}; - std::vector<DatatypeConstructorDecl> ctors3; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil2("nil"); + std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2)); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3), + DatatypeConstructorDecl cons2("cons"); + DatatypeConstructorDecl nil3("nil"); + std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3}; + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3)); + std::vector<DatatypeConstructorDecl> ctors4; + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors4), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3), + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4), CVC4ApiException&); } @@ -983,7 +988,6 @@ void SolverBlack::testSimplify() Sort uSort = d_solver->mkUninterpretedSort("u"); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); - DatatypeDecl consListSpec("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index e48d04a7f..6df18fd44 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -277,21 +277,39 @@ class DatatypeBlack : public CxxTest::TestSuite { Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl << " is " << dtts[1].mkGroundTerm() << endl; TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]); + } + void testMutualListTrees2() + { + Datatype tree("tree"); + DatatypeConstructor node("node", "is_node"); + node.addArg("left", DatatypeSelfType()); + node.addArg("right", DatatypeSelfType()); + tree.addConstructor(node); + + DatatypeConstructor leaf("leaf", "is_leaf"); + leaf.addArg("leaf", DatatypeUnresolvedType("list")); + tree.addConstructor(leaf); + + Datatype list("list"); + DatatypeConstructor cons("cons", "is_cons"); + cons.addArg("car", DatatypeUnresolvedType("tree")); + cons.addArg("cdr", DatatypeSelfType()); + list.addConstructor(cons); + + DatatypeConstructor nil("nil", "is_nil"); + list.addConstructor(nil); // add another constructor to list datatype resulting in an // "otherNil-list" DatatypeConstructor otherNil("otherNil", "is_otherNil"); - dts[1].addConstructor(otherNil); + list.addConstructor(otherNil); + vector<Datatype> dts; + dts.push_back(tree); + dts.push_back(list); // remake the types vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts); - TS_ASSERT_DIFFERS(dtts, dtts2); - TS_ASSERT_DIFFERS(dtts[1], dtts2[1]); - - // tree is also different because it's a tree of otherNil-lists - TS_ASSERT_DIFFERS(dtts[0], dtts2[0]); - TS_ASSERT(! dtts2[0].getDatatype().isFinite()); TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts2[0].getDatatype().isWellFounded()); |