diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/datatype_api_black.h | 2 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 10 | ||||
-rw-r--r-- | test/unit/api/sort_black.h | 12 | ||||
-rw-r--r-- | test/unit/expr/expr_public.h | 2 | ||||
-rw-r--r-- | test/unit/theory/type_enumerator_white.h | 6 | ||||
-rw-r--r-- | test/unit/util/datatype_black.h | 24 |
6 files changed, 28 insertions, 28 deletions
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index 6a5f3eb7b..b9c671a30 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -38,7 +38,7 @@ void DatatypeBlack::tearDown() {} void DatatypeBlack::testMkDatatypeSort() { - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); cons.addSelector(head); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 92313ac3c..2831b840d 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -179,7 +179,7 @@ void SolverBlack::testMkFloatingPointSort() void SolverBlack::testMkDatatypeSort() { - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); cons.addSelector(head); @@ -187,7 +187,7 @@ void SolverBlack::testMkDatatypeSort() DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec)); - DatatypeDecl throwsDtypeSpec("list"); + DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list"); TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); } @@ -627,7 +627,7 @@ void SolverBlack::testMkTermFromOp() // list datatype Sort sort = d_solver->mkParamSort("T"); - DatatypeDecl listDecl("paramlist", sort); + DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); DatatypeSelectorDecl head("head", sort); @@ -930,7 +930,7 @@ void SolverBlack::testGetOp() TS_ASSERT_EQUALS(exta.getOp(), ext); // Test Datatypes -- more complicated - DatatypeDecl consListSpec("list"); + DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); @@ -1036,7 +1036,7 @@ 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"); + DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 73eb3df88..4ea29b8d7 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -58,7 +58,7 @@ void SortBlack::tearDown() {} void SortBlack::testGetDatatype() { // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); cons.addSelector(head); @@ -76,7 +76,7 @@ void SortBlack::testInstantiate() { // instantiate parametric datatype, check should not fail Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); DatatypeSelectorDecl paramHead("head", sort); @@ -87,7 +87,7 @@ void SortBlack::testInstantiate() TS_ASSERT_THROWS_NOTHING( paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()})); // instantiate non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); cons.addSelector(head); @@ -222,7 +222,7 @@ void SortBlack::testGetDatatypeParamSorts() { // create parametric datatype, check should not fail Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); DatatypeSelectorDecl paramHead("head", sort); @@ -232,7 +232,7 @@ void SortBlack::testGetDatatypeParamSorts() Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); // create non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); cons.addSelector(head); @@ -246,7 +246,7 @@ void SortBlack::testGetDatatypeParamSorts() void SortBlack::testGetDatatypeArity() { // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); cons.addSelector(head); diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 82cf10a9b..da9434d79 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -370,7 +370,7 @@ private: TS_ASSERT(!null->isConst()); // more complicated "constants" exist in datatypes and arrays theories - Datatype list("list"); + Datatype list(d_em, "list"); DatatypeConstructor consC("cons"); consC.addArg("car", d_em->integerType()); consC.addArg("cdr", DatatypeSelfType()); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 2c3f09ce0..da915b7ee 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -146,7 +146,7 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { } void testDatatypesFinite() { - Datatype dt("Colors"); + Datatype dt(d_em, "Colors"); dt.addConstructor(DatatypeConstructor("red")); dt.addConstructor(DatatypeConstructor("orange")); dt.addConstructor(DatatypeConstructor("yellow")); @@ -167,7 +167,7 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { } void testDatatypesInfinite1() { - Datatype colors("Colors"); + Datatype colors(d_em, "Colors"); colors.addConstructor(DatatypeConstructor("red")); colors.addConstructor(DatatypeConstructor("orange")); colors.addConstructor(DatatypeConstructor("yellow")); @@ -175,7 +175,7 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { colors.addConstructor(DatatypeConstructor("blue")); colors.addConstructor(DatatypeConstructor("violet")); TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors)); - Datatype listColors("ListColors"); + Datatype listColors(d_em, "ListColors"); DatatypeConstructor consC("cons"); consC.addArg("car", colorsType.toType()); consC.addArg("cdr", DatatypeSelfType()); diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 6df18fd44..e81caf36f 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -47,7 +47,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testEnumeration() { - Datatype colors("colors"); + Datatype colors(d_em, "colors"); DatatypeConstructor yellow("yellow", "is_yellow"); DatatypeConstructor blue("blue", "is_blue"); @@ -85,7 +85,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testNat() { - Datatype nat("nat"); + Datatype nat(d_em, "nat"); DatatypeConstructor succ("succ", "is_succ"); succ.addArg("pred", DatatypeSelfType()); @@ -112,7 +112,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testTree() { - Datatype tree("tree"); + Datatype tree(d_em, "tree"); Type integerType = d_em->integerType(); DatatypeConstructor node("node", "is_node"); @@ -144,7 +144,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testListInt() { - Datatype list("list"); + Datatype list(d_em, "list"); Type integerType = d_em->integerType(); DatatypeConstructor cons("cons", "is_cons"); @@ -169,7 +169,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testListReal() { - Datatype list("list"); + Datatype list(d_em, "list"); Type realType = d_em->realType(); DatatypeConstructor cons("cons", "is_cons"); @@ -194,7 +194,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testListBoolean() { - Datatype list("list"); + Datatype list(d_em, "list"); Type booleanType = d_em->booleanType(); DatatypeConstructor cons("cons", "is_cons"); @@ -226,7 +226,7 @@ class DatatypeBlack : public CxxTest::TestSuite { * list = cons(car: tree, cdr: list) | nil * END; */ - Datatype tree("tree"); + Datatype tree(d_em, "tree"); DatatypeConstructor node("node", "is_node"); node.addArg("left", DatatypeSelfType()); node.addArg("right", DatatypeSelfType()); @@ -238,7 +238,7 @@ class DatatypeBlack : public CxxTest::TestSuite { Debug("datatypes") << tree << std::endl; - Datatype list("list"); + Datatype list(d_em, "list"); DatatypeConstructor cons("cons", "is_cons"); cons.addArg("car", DatatypeUnresolvedType("tree")); cons.addArg("cdr", DatatypeSelfType()); @@ -280,7 +280,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testMutualListTrees2() { - Datatype tree("tree"); + Datatype tree(d_em, "tree"); DatatypeConstructor node("node", "is_node"); node.addArg("left", DatatypeSelfType()); node.addArg("right", DatatypeSelfType()); @@ -290,7 +290,7 @@ class DatatypeBlack : public CxxTest::TestSuite { leaf.addArg("leaf", DatatypeUnresolvedType("list")); tree.addConstructor(leaf); - Datatype list("list"); + Datatype list(d_em, "list"); DatatypeConstructor cons("cons", "is_cons"); cons.addArg("car", DatatypeUnresolvedType("tree")); cons.addArg("cdr", DatatypeSelfType()); @@ -327,7 +327,7 @@ class DatatypeBlack : public CxxTest::TestSuite { } void testNotSoWellFounded() { - Datatype tree("tree"); + Datatype tree(d_em, "tree"); DatatypeConstructor node("node", "is_node"); node.addArg("left", DatatypeSelfType()); @@ -351,7 +351,7 @@ class DatatypeBlack : public CxxTest::TestSuite { Type t1, t2; v.push_back(t1 = d_em->mkSort("T1")); v.push_back(t2 = d_em->mkSort("T2")); - Datatype pair("pair", v); + Datatype pair(d_em, "pair", v); DatatypeConstructor mkpair("mk-pair"); mkpair.addArg("first", t1); |