From 0cccfea1233b918c18ec2e1268fd786983074261 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Aug 2020 15:56:24 -0500 Subject: [PATCH] Update Expr-level unit tests that depend on datatypes to Node (#4860) In preparation for eliminating the Expr-level datatype. --- test/unit/expr/expr_public.h | 74 ------------------ test/unit/expr/node_black.h | 78 ++++++++++++++++++- test/unit/expr/type_cardinality_public.h | 22 ++++-- .../theory_sets_type_enumerator_white.h | 25 +++--- 4 files changed, 103 insertions(+), 96 deletions(-) diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index f8ccd23d4..0e17ab1e8 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -339,80 +339,6 @@ class ExprPublic : public CxxTest::TestSuite { TS_ASSERT(null->isNull()); } - void testIsConst() { - /* bool isConst() const; */ - - //Debug.on("isConst"); - - TS_ASSERT(!a_bool->isConst()); - TS_ASSERT(!b_bool->isConst()); - TS_ASSERT(!c_bool_and->isConst()); - TS_ASSERT(and_op->isConst()); - TS_ASSERT(plus_op->isConst()); - TS_ASSERT(!d_apply_fun_bool->isConst()); - TS_ASSERT(!null->isConst()); - - // more complicated "constants" exist in datatypes and arrays theories - Datatype list(d_em, "list"); - DatatypeConstructor consC("cons"); - consC.addArg("car", d_em->integerType()); - consC.addArg("cdr", DatatypeSelfType()); - list.addConstructor(consC); - list.addConstructor(DatatypeConstructor("nil")); - DatatypeType listType = d_em->mkDatatypeType(list); - Expr cons = listType.getDatatype().getConstructor("cons"); - Expr nil = listType.getDatatype().getConstructor("nil"); - Expr x = d_em->mkVar("x", d_em->integerType()); - Expr cons_x_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, x, d_em->mkExpr(APPLY_CONSTRUCTOR, nil)); - Expr cons_1_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil)); - Expr cons_1_cons_2_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(2)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil))); - TS_ASSERT(d_em->mkExpr(APPLY_CONSTRUCTOR, nil).isConst()); - TS_ASSERT(!cons_x_nil.isConst()); - TS_ASSERT(cons_1_nil.isConst()); - TS_ASSERT(cons_1_cons_2_nil.isConst()); - - { - ExprManagerScope ems(*d_em); - ArrayType arrType = - d_em->mkArrayType(d_em->integerType(), d_em->integerType()); - Expr zero = d_em->mkConst(Rational(0)); - Expr one = d_em->mkConst(Rational(1)); - Expr storeAll = d_em->mkConst( - ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero))); - TS_ASSERT(storeAll.isConst()); - - Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero); - TS_ASSERT(!arr.isConst()); - arr = d_em->mkExpr(STORE, storeAll, zero, one); - TS_ASSERT(arr.isConst()); - Expr arr2 = d_em->mkExpr(STORE, arr, one, zero); - TS_ASSERT(!arr2.isConst()); - arr2 = d_em->mkExpr(STORE, arr, one, one); - TS_ASSERT(arr2.isConst()); - arr2 = d_em->mkExpr(STORE, arr, zero, one); - TS_ASSERT(!arr2.isConst()); - - arrType = - d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1)); - zero = d_em->mkConst(BitVector(1, unsigned(0))); - one = d_em->mkConst(BitVector(1, unsigned(1))); - storeAll = d_em->mkConst( - ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero))); - TS_ASSERT(storeAll.isConst()); - - arr = d_em->mkExpr(STORE, storeAll, zero, zero); - TS_ASSERT(!arr.isConst()); - arr = d_em->mkExpr(STORE, storeAll, zero, one); - TS_ASSERT(arr.isConst()); - arr2 = d_em->mkExpr(STORE, arr, one, zero); - TS_ASSERT(!arr2.isConst()); - arr2 = d_em->mkExpr(STORE, arr, one, one); - TS_ASSERT(!arr2.isConst()); - arr2 = d_em->mkExpr(STORE, arr, zero, one); - TS_ASSERT(!arr2.isConst()); - } - } - void testGetConst() { /* template const T& getConst() const; */ diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 91242322a..182f742b0 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -23,13 +23,15 @@ #include #include "api/cvc4cpp.h" -#include "smt/smt_engine.h" +#include "expr/dtype.h" #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node_value.h" +#include "smt/smt_engine.h" #include "test_utils.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace CVC4::kind; @@ -706,6 +708,80 @@ class NodeBlack : public CxxTest::TestSuite { std::equal(children.begin(), children.end(), skolems.begin())); } + void testIsConst() + { + // more complicated "constants" exist in datatypes and arrays theories + DType list("list"); + std::shared_ptr consC = + std::make_shared("cons"); + consC->addArg("car", d_nodeManager->integerType()); + consC->addArgSelf("cdr"); + list.addConstructor(consC); + list.addConstructor(std::make_shared("nil")); + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const std::vector >& lcons = + listType.getDType().getConstructors(); + Node cons = lcons[0]->getConstructor(); + Node nil = lcons[1]->getConstructor(); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node cons_x_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + x, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_cons_2_nil = d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); + TS_ASSERT(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); + TS_ASSERT(!cons_x_nil.isConst()); + TS_ASSERT(cons_1_nil.isConst()); + TS_ASSERT(cons_1_cons_2_nil.isConst()); + + TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + TS_ASSERT(storeAll.isConst()); + + Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + TS_ASSERT(!arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + TS_ASSERT(arr.isConst()); + Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + TS_ASSERT(!arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), + d_nodeManager->mkBitVectorType(1)); + zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); + one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + TS_ASSERT(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + TS_ASSERT(!arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + TS_ASSERT(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + TS_ASSERT(!arr2.isConst()); + } + // This Test is designed to fail in a way that will cause a segfault, // so it is commented out. // This is for demonstrating what a certain type of user error looks like. diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 49d6bd9fd..ba236fdf2 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -23,6 +23,7 @@ #include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "expr/kind.h" +#include "expr/node_manager.h" #include "expr/type.h" #include "util/cardinality.h" @@ -36,6 +37,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { { d_slv = new api::Solver(); d_em = d_slv->getExprManager(); + d_nm = d_slv->getNodeManager(); } void tearDown() override { delete d_slv; } @@ -180,15 +182,20 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { } void testTernaryFunctions() { - vector boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); - vector boolboolbool = boolbool; boolboolbool.push_back(d_em->booleanType()); + vector boolbool; + boolbool.push_back(d_nm->booleanType()); + boolbool.push_back(d_nm->booleanType()); + vector boolboolbool = boolbool; + boolboolbool.push_back(d_nm->booleanType()); - Type boolboolTuple = d_em->mkTupleType(boolbool); - Type boolboolboolTuple = d_em->mkTupleType(boolboolbool); + TypeNode boolboolTuple = d_nm->mkTupleType(boolbool); + TypeNode boolboolboolTuple = d_nm->mkTupleType(boolboolbool); - Type boolboolboolToBool = d_em->mkFunctionType(boolboolbool, d_em->booleanType()); - Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple); - Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple); + TypeNode boolboolboolToBool = + d_nm->mkFunctionType(boolboolbool, d_nm->booleanType()); + TypeNode boolboolToBoolbool = d_nm->mkFunctionType(boolbool, boolboolTuple); + TypeNode boolToBoolboolbool = + d_nm->mkFunctionType(d_nm->booleanType(), boolboolboolTuple); TS_ASSERT( boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8) == Cardinality::EQUAL ); TS_ASSERT( boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4) == Cardinality::EQUAL ); @@ -232,4 +239,5 @@ class TypeCardinalityPublic : public CxxTest::TestSuite { private: api::Solver* d_slv; ExprManager* d_em; + NodeManager* d_nm; };/* TypeCardinalityPublic */ diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 0a97f4c42..b6726e540 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -18,6 +18,7 @@ #include +#include "expr/dtype.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/sets/theory_sets_type_enumerator.h" @@ -135,24 +136,20 @@ class SetEnumeratorWhite : public CxxTest::TestSuite void testSetOfFiniteDatatype() { - Datatype dt(d_em, "Colors"); - dt.addConstructor(DatatypeConstructor("red")); - dt.addConstructor(DatatypeConstructor("green")); - dt.addConstructor(DatatypeConstructor("blue")); - TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt)); + DType dt("Colors"); + dt.addConstructor(std::make_shared("red")); + dt.addConstructor(std::make_shared("green")); + dt.addConstructor(std::make_shared("blue")); + TypeNode datatype = d_nm->mkDatatypeType(dt); + const std::vector >& dtcons = + datatype.getDType().getConstructors(); SetEnumerator setEnumerator(d_nm->mkSetType(datatype)); - Node red = d_nm->mkNode( - APPLY_CONSTRUCTOR, - DatatypeType(datatype.toType()).getDatatype().getConstructor("red")); + Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()); - Node green = d_nm->mkNode( - APPLY_CONSTRUCTOR, - DatatypeType(datatype.toType()).getDatatype().getConstructor("green")); + Node green = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()); - Node blue = d_nm->mkNode( - APPLY_CONSTRUCTOR, - DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")); + Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()); Node actual0 = *setEnumerator; Node expected0 = -- 2.30.2