From 78c0daa482b35b95c90dd058ee4dd8a981e1337f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 13 Jul 2020 19:48:07 -0700 Subject: [PATCH] Use TypeNode/Node in ArrayStoreAll (#4728) This commit changes ArrayStoreAll to use Node/TypeNode instead of Expr/Type. --- src/api/cvc4cpp.cpp | 8 +- src/expr/array_store_all.cpp | 57 ++++++----- src/expr/array_store_all.h | 21 ++--- src/expr/expr_template.cpp | 5 +- src/expr/type_node.h | 5 +- src/printer/cvc/cvc_printer.cpp | 5 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 6 +- src/theory/arrays/theory_arrays_rewriter.h | 8 +- src/theory/arrays/theory_arrays_type_rules.h | 5 +- src/theory/arrays/type_enumerator.h | 3 +- .../builtin/theory_builtin_rewriter.cpp | 5 +- test/unit/expr/expr_public.h | 78 ++++++++------- test/unit/theory/theory_black.h | 6 +- test/unit/theory/type_enumerator_white.h | 21 +++-- test/unit/util/CMakeLists.txt | 2 +- test/unit/util/array_store_all_black.h | 83 ---------------- test/unit/util/array_store_all_white.h | 94 +++++++++++++++++++ 18 files changed, 224 insertions(+), 190 deletions(-) delete mode 100644 test/unit/util/array_store_all_black.h create mode 100644 test/unit/util/array_store_all_white.h diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 550dd760b..3cca1a071 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1564,11 +1564,12 @@ bool Term::isConst() const Term Term::getConstArrayBase() const { + CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager())); CVC4_API_CHECK_NOT_NULL; // CONST_ARRAY kind maps to STORE_ALL internal kind CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL) << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; - return Term(d_solver, d_expr->getConst().getExpr()); + return Term(d_solver, d_expr->getConst().getValue().toExpr()); } std::vector Term::getConstSequenceElements() const @@ -3511,6 +3512,7 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const Term Solver::mkConstArray(Sort sort, Term val) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_ARG_CHECK_NOT_NULL(sort); CVC4_API_ARG_CHECK_NOT_NULL(val); CVC4_API_SOLVER_CHECK_SORT(sort); @@ -3518,8 +3520,8 @@ Term Solver::mkConstArray(Sort sort, Term val) const CVC4_API_CHECK(sort.isArray()) << "Not an array sort."; CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort())) << "Value does not match element sort."; - Term res = mkValHelper( - CVC4::ArrayStoreAll(*sort.d_type, *val.d_expr)); + Term res = mkValHelper(CVC4::ArrayStoreAll( + TypeNode::fromType(*sort.d_type), Node::fromExpr(*val.d_expr))); return res; CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 6655c7b61..0777bc1cf 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -21,15 +21,16 @@ #include #include "base/check.h" -#include "expr/expr.h" -#include "expr/type.h" +#include "expr/node.h" +#include "expr/type_node.h" using namespace std; namespace CVC4 { -ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) - : d_type(), d_expr() { +ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value) + : d_type(), d_value() +{ // this check is stronger than the assertion check in the expr manager that // ArrayTypes are actually array types // because this check is done in production builds too @@ -39,38 +40,41 @@ ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) type.toString().c_str()); PrettyCheckArgument( - expr.getType().isComparableTo(type.getConstituentType()), expr, + value.getType().isComparableTo(type.getArrayConstituentType()), + value, "expr type `%s' does not match constituent type of array type `%s'", - expr.getType().toString().c_str(), type.toString().c_str()); + value.getType().toString().c_str(), + type.toString().c_str()); - PrettyCheckArgument(expr.isConst(), expr, - "ArrayStoreAll requires a constant expression"); + PrettyCheckArgument( + value.isConst(), value, "ArrayStoreAll requires a constant expression"); - // Delay allocation until the checks above have been performed. If these fail, - // the memory for d_type and d_expr should not leak. The alternative is catch, - // delete and re-throw. - d_type.reset(new ArrayType(type)); - d_expr.reset(new Expr(expr)); + // Delay allocation until the checks above have been performed. If these + // fail, the memory for d_type and d_value should not leak. The alternative + // is catch, delete and re-throw. + d_type.reset(new TypeNode(type)); + d_value.reset(new Node(value)); } ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other) - : d_type(new ArrayType(other.getType())), - d_expr(new Expr(other.getExpr())) {} + : d_type(new TypeNode(other.getType())), d_value(new Node(other.getValue())) +{ +} ArrayStoreAll::~ArrayStoreAll() {} ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) { (*d_type) = other.getType(); - (*d_expr) = other.getExpr(); + (*d_value) = other.getValue(); return *this; } -const ArrayType& ArrayStoreAll::getType() const { return *d_type; } +const TypeNode& ArrayStoreAll::getType() const { return *d_type; } -const Expr& ArrayStoreAll::getExpr() const { return *d_expr; } +const Node& ArrayStoreAll::getValue() const { return *d_value; } bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const { - return getType() == asa.getType() && getExpr() == asa.getExpr(); + return getType() == asa.getType() && getValue() == asa.getValue(); } bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const @@ -80,14 +84,14 @@ bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const { - return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() < asa.getExpr()); + return (getType() < asa.getType()) + || (getType() == asa.getType() && getValue() < asa.getValue()); } bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const { - return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() <= asa.getExpr()); + return (getType() < asa.getType()) + || (getType() == asa.getType() && getValue() <= asa.getValue()); } bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const @@ -101,12 +105,13 @@ bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const } std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) { - return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() - << ')'; + return out << "__array_store_all__(" << asa.getType() << ", " + << asa.getValue() << ')'; } size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const { - return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); + return TypeNodeHashFunction()(asa.getType()) + * NodeHashFunction()(asa.getValue()); } } // namespace CVC4 diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 2d251257c..7fa25516c 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -24,29 +24,28 @@ #include #include -namespace CVC4 { -// messy; Expr needs ArrayStoreAll (because it's the payload of a -// CONSTANT-kinded expression), and ArrayStoreAll needs Expr. -class Expr; -class ArrayType; -} // namespace CVC4 namespace CVC4 { +template +class NodeTemplate; +typedef NodeTemplate Node; +class TypeNode; + class CVC4_PUBLIC ArrayStoreAll { public: /** * @throws IllegalArgumentException if `type` is not an array or if `expr` is * not a constant of type `type`. */ - ArrayStoreAll(const ArrayType& type, const Expr& expr); + ArrayStoreAll(const TypeNode& type, const Node& value); ~ArrayStoreAll(); ArrayStoreAll(const ArrayStoreAll& other); ArrayStoreAll& operator=(const ArrayStoreAll& other); - const ArrayType& getType() const; - const Expr& getExpr() const; + const TypeNode& getType() const; + const Node& getValue() const; bool operator==(const ArrayStoreAll& asa) const; bool operator!=(const ArrayStoreAll& asa) const; @@ -56,8 +55,8 @@ class CVC4_PUBLIC ArrayStoreAll { bool operator>=(const ArrayStoreAll& asa) const; private: - std::unique_ptr d_type; - std::unique_ptr d_expr; + std::unique_ptr d_type; + std::unique_ptr d_value; }; /* class ArrayStoreAll */ std::ostream& operator<<(std::ostream& out, diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 50884f715..132d4bfaa 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -694,8 +694,9 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v // for export so those don't matter. ExprManager* toEm = to->toExprManager(); const ArrayStoreAll& asa = n.getConst(); - return to->mkConst(ArrayStoreAll(asa.getType().exportTo(toEm, vmap), - asa.getExpr().exportTo(toEm, vmap))); + return to->mkConst(ArrayStoreAll( + TypeNode::fromType(asa.getType().toType().exportTo(toEm, vmap)), + Node::fromExpr(asa.getValue().toExpr().exportTo(toEm, vmap)))); } switch(n.getKind()) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5082fe1d3..12c96d307 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -409,7 +409,7 @@ public: * Convert this TypeNode into a Type using the currently-in-scope * manager. */ - inline Type toType(); + inline Type toType() const; /** * Convert a Type into a TypeNode. @@ -754,7 +754,8 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; namespace CVC4 { -inline Type TypeNode::toType() { +inline Type TypeNode::toType() const +{ return NodeManager::currentNM()->toType(*this); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 216fb0517..900651e1d 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -246,8 +246,9 @@ void CvcPrinter::toStream( case kind::STORE_ALL: { const ArrayStoreAll& asa = n.getConst(); - out << "ARRAY(" << asa.getType().getIndexType() << " OF " - << asa.getType().getConstituentType() << ") : " << asa.getExpr(); + out << "ARRAY(" << asa.getType().getArrayIndexType() << " OF " + << asa.getType().getArrayConstituentType() + << ") : " << asa.getValue(); break; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 3eedee600..49f786f78 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -237,7 +237,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STORE_ALL: { ArrayStoreAll asa = n.getConst(); - out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")"; + out << "((as const " << asa.getType() << ") " << asa.getValue() << ")"; break; } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 49f93286e..37443c070 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -808,7 +808,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) break; } ArrayStoreAll storeAll = node.getConst(); - Node defaultValue = Node::fromExpr(storeAll.getExpr()); + Node defaultValue = storeAll.getValue(); if (!defaultValue.isConst()) { throw LogicException("Array theory solver does not yet support non-constant default values for arrays"); } @@ -1230,7 +1230,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m) } // Build the STORE_ALL term with the default value - rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr())); + rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep)); /* } else { @@ -1904,7 +1904,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) TNode constArr = d_infoMap.getConstArr(a); if (!constArr.isNull()) { ArrayStoreAll storeAll = constArr.getConst(); - Node defValue = Node::fromExpr(storeAll.getExpr()); + Node defValue = storeAll.getValue(); Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i); if (!d_equalityEngine.hasTerm(selConst)) { preRegisterTermInternal(selConst); diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index e81b7d7c0..e8f03c1d0 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -93,7 +93,7 @@ class TheoryArraysRewriter : public TheoryRewriter } Assert(store.getKind() == kind::STORE_ALL); ArrayStoreAll storeAll = store.getConst(); - Node defaultValue = Node::fromExpr(storeAll.getExpr()); + Node defaultValue = storeAll.getValue(); NodeManager* nm = NodeManager::currentNM(); // Check if we are writing to default value - if so the store @@ -214,7 +214,7 @@ class TheoryArraysRewriter : public TheoryRewriter std::sort(newIndices.begin(), newIndices.end()); } - n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr())); + n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue)); std::vector::iterator itNew = newIndices.begin(), it_end = newIndices.end(); while (itNew != it_end || !indices.empty()) { if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) { @@ -267,7 +267,7 @@ class TheoryArraysRewriter : public TheoryRewriter if (store.getKind() == kind::STORE_ALL) { // select(store_all(v),i) = v ArrayStoreAll storeAll = store.getConst(); - n = Node::fromExpr(storeAll.getExpr()); + n = storeAll.getValue(); Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; Assert(n.isConst()); return RewriteResponse(REWRITE_DONE, n); @@ -432,7 +432,7 @@ class TheoryArraysRewriter : public TheoryRewriter if (store.getKind() == kind::STORE_ALL) { // select(store_all(v),i) = v ArrayStoreAll storeAll = store.getConst(); - n = Node::fromExpr(storeAll.getExpr()); + n = storeAll.getValue(); Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl; Assert(n.isConst()); return RewriteResponse(REWRITE_DONE, n); diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index e5681d50f..56c51d9bf 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -69,8 +69,7 @@ struct ArrayStoreTypeRule { else { Assert(n.getKind() == kind::STORE_ALL); ArrayStoreAll storeAll = n.getConst(); - ArrayType arrayType = storeAll.getType(); - return TypeNode::fromType(arrayType); + return storeAll.getType(); } } @@ -106,7 +105,7 @@ struct ArrayStoreTypeRule { } Assert(store.getKind() == kind::STORE_ALL); ArrayStoreAll storeAll = store.getConst(); - Node defaultValue = Node::fromExpr(storeAll.getExpr()); + Node defaultValue = storeAll.getValue(); if (value == defaultValue) { return false; } diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 3da793617..5894501b2 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -53,7 +53,8 @@ class ArrayEnumerator : public TypeEnumeratorBase { { d_indexVec.push_back(*d_index); d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); - d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr())); + d_arrayConst = + d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back())))); Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl; } diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 245e7cb8a..456b0cbca 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -185,7 +185,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( TNode a, TNode b } }else if( a.getKind()==kind::STORE_ALL ){ ArrayStoreAll storeAll = a.getConst(); - Node sa = Node::fromExpr(storeAll.getExpr()); + Node sa = storeAll.getValue(); // convert the default value recursively (bounded by the number of arguments in bvl) ret = getLambdaForArrayRepresentationRec( sa, bvl, bvlIndex+1, visited ); } @@ -448,8 +448,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n, } Trace("builtin-rewrite-debug2") << " make array store all " << curr.getType() << " annotated : " << array_type << std::endl; Assert(curr.getType().isSubtypeOf(array_type.getArrayConstituentType())); - curr = nm->mkConst( - ArrayStoreAll((ArrayType(array_type.toType())), curr.toExpr())); + curr = nm->mkConst(ArrayStoreAll(array_type, curr)); Trace("builtin-rewrite-debug2") << " build array..." << std::endl; // can only build if default value is constant (since array store all must be constant) Trace("builtin-rewrite-debug2") << " got constant base " << curr << std::endl; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 86de45fe9..f8ccd23d4 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -23,6 +23,9 @@ #include "base/exception.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/node.h" +#include "expr/type_node.h" #include "options/options.h" using namespace CVC4; @@ -85,7 +88,6 @@ class ExprPublic : public CxxTest::TestSuite { delete c_bool_and; delete b_bool; delete a_bool; - delete d_slv; } catch (Exception& e) @@ -369,40 +371,46 @@ class ExprPublic : public CxxTest::TestSuite { TS_ASSERT(cons_1_nil.isConst()); TS_ASSERT(cons_1_cons_2_nil.isConst()); - 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(arrType, 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(arrType, 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()); - + { + 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() { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 45d13d416..b1b79ec07 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -62,7 +62,7 @@ class TheoryBlack : public CxxTest::TestSuite { TypeNode arrType = d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); - Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr())); + Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero)); TS_ASSERT(storeAll.isConst()); Node arr = d_nm->mkNode(STORE, storeAll, zero, zero); @@ -85,7 +85,7 @@ class TheoryBlack : public CxxTest::TestSuite { arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(1), d_nm->mkBitVectorType(1)); zero = d_nm->mkConst(BitVector(1,unsigned(0))); one = d_nm->mkConst(BitVector(1,unsigned(1))); - storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr())); + storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero)); TS_ASSERT(storeAll.isConst()); arr = d_nm->mkNode(STORE, storeAll, zero, zero); @@ -113,7 +113,7 @@ class TheoryBlack : public CxxTest::TestSuite { one = d_nm->mkConst(BitVector(2,unsigned(1))); Node two = d_nm->mkConst(BitVector(2,unsigned(2))); Node three = d_nm->mkConst(BitVector(2,unsigned(3))); - storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), one.toExpr())); + storeAll = d_nm->mkConst(ArrayStoreAll(arrType, one)); TS_ASSERT(storeAll.isConst()); arr = d_nm->mkNode(STORE, storeAll, zero, zero); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index f8ce734ec..b996919ee 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -234,13 +234,20 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { TS_ASSERT( ! te.isFinished() ); // ensure that certain items were found - ArrayType arrayType(d_em->mkArrayType(d_em->integerType(), d_em->integerType())); - Node zeroes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(0)))); - Node ones = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(1)))); - Node twos = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(2)))); - Node threes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(3)))); - Node fours = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(4)))); - Node tens = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(10)))); + TypeNode arrayType = + d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()); + Node zeroes = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(0)))); + Node ones = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(1)))); + Node twos = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(2)))); + Node threes = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(3)))); + Node fours = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(4)))); + Node tens = + d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(10)))); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 0748e1059..5bccc9137 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -1,7 +1,7 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(array_store_all_black util) +cvc4_add_unit_test_white(array_store_all_white util) cvc4_add_unit_test_white(assert_white util) cvc4_add_unit_test_black(binary_heap_black util) cvc4_add_unit_test_black(bitvector_black util) diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h deleted file mode 100644 index bf0163317..000000000 --- a/test/unit/util/array_store_all_black.h +++ /dev/null @@ -1,83 +0,0 @@ -/********************* */ -/*! \file array_store_all_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of CVC4::ArrayStoreAll - ** - ** Black box testing of CVC4::ArrayStoreAll. - **/ - -#include - -#include "api/cvc4cpp.h" -#include "expr/array_store_all.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "expr/expr_manager_scope.h" -#include "expr/type.h" -#include "test_utils.h" - -using namespace CVC4; -using namespace std; - -class ArrayStoreAllBlack : public CxxTest::TestSuite { - public: - void setUp() override - { - d_slv = new api::Solver(); - d_em = d_slv->getExprManager(); - } - - void tearDown() override { delete d_slv; } - - void testStoreAll() { - Type usort = d_em->mkSort("U"); - ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), - d_em->mkConst(Rational(9, 2))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), - d_em->mkConst(UninterpretedConstant(usort, 0))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), - d_em->mkConst(Rational(0))); - ArrayStoreAll( - d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), - d_em->mkConst(Rational(0))); - } - - void testTypeErrors() - { - TS_ASSERT_THROWS(ArrayStoreAll(d_em->integerType(), - d_em->mkConst(UninterpretedConstant( - d_em->mkSort("U"), 0))), - IllegalArgumentException&); - TS_ASSERT_THROWS( - ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))), - IllegalArgumentException&); - TS_ASSERT_THROWS( - ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), - d_em->mkConst(Rational(9, 2))), - IllegalArgumentException&); - } - - void testConstError() { - Type usort = d_em->mkSort("U"); - TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( - d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort))); - TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( - d_em->integerType(), d_em->mkVar("x", d_em->integerType()))); - TS_ASSERT_THROWS_ANYTHING( - ArrayStoreAll(d_em->integerType(), - d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), - d_em->mkConst(Rational(0))))); - } - - private: - api::Solver* d_slv; - ExprManager* d_em; -}; /* class ArrayStoreAllBlack */ diff --git a/test/unit/util/array_store_all_white.h b/test/unit/util/array_store_all_white.h new file mode 100644 index 000000000..fb7857003 --- /dev/null +++ b/test/unit/util/array_store_all_white.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file array_store_all_white.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of CVC4::ArrayStoreAll + ** + ** Black box testing of CVC4::ArrayStoreAll. + **/ + +#include + +#include "api/cvc4cpp.h" +#include "expr/array_store_all.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "expr/type.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test_utils.h" + +using namespace CVC4; +using namespace std; + +class ArrayStoreAllWhite : public CxxTest::TestSuite +{ + public: + void setUp() override + { + d_slv = new api::Solver(); + d_scope = new smt::SmtScope(d_slv->getSmtEngine()); + d_nm = d_slv->getSmtEngine()->d_nodeManager; + } + + void tearDown() override + { + delete d_scope; + delete d_slv; + } + + void testStoreAll() + { + TypeNode usort = d_nm->mkSort("U"); + ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()), + d_nm->mkConst(Rational(9, 2))); + ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort), + d_nm->mkConst(UninterpretedConstant(usort.toType(), 0))); + ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()), + d_nm->mkConst(Rational(0))); + ArrayStoreAll( + d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()), + d_nm->mkConst(Rational(0))); + } + + void testTypeErrors() + { + TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(), + d_nm->mkConst(UninterpretedConstant( + d_nm->mkSort("U").toType(), 0))), + IllegalArgumentException&); + TS_ASSERT_THROWS( + ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))), + IllegalArgumentException&); + TS_ASSERT_THROWS( + ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")), + d_nm->mkConst(Rational(9, 2))), + IllegalArgumentException&); + } + + void testConstError() + { + TypeNode usort = d_nm->mkSort("U"); + TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( + d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort))); + TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( + d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType()))); + TS_ASSERT_THROWS_ANYTHING( + ArrayStoreAll(d_nm->integerType(), + d_nm->mkNode(kind::PLUS, + d_nm->mkConst(Rational(1)), + d_nm->mkConst(Rational(0))))); + } + + private: + api::Solver* d_slv; + smt::SmtScope* d_scope; + NodeManager* d_nm; +}; /* class ArrayStoreAllBlack */ -- 2.30.2