From 01ff626de4261af83f69552eaba038399c428882 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 23 Nov 2021 21:53:01 -0800 Subject: [PATCH] Remove dependency of `TypeNode` on `Node` (#7690) This is further work towards breaking cyclic dependencies in the `expr` folder. --- src/expr/CMakeLists.txt | 12 ++++ src/expr/dtype.cpp | 3 +- src/expr/dtype_cons.cpp | 2 +- src/expr/node_converter.cpp | 2 +- src/expr/node_manager.h | 30 +++++++++ src/expr/node_manager_template.cpp | 13 ++++ src/expr/type_node.cpp | 62 ++++--------------- src/expr/type_node.h | 39 ------------ src/expr/type_properties_template.cpp | 51 +++++++++++++++ src/expr/type_properties_template.h | 30 +-------- .../arrays/theory_arrays_type_rules.cpp | 3 +- src/theory/datatypes/datatypes_rewriter.cpp | 3 +- src/theory/datatypes/proof_checker.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 5 +- .../candidate_rewrite_database.cpp | 3 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 6 +- .../quantifiers/sygus/sygus_reconstruct.cpp | 3 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 3 +- src/theory/smt_engine_subsolver.cpp | 3 +- src/theory/strings/sequences_rewriter.cpp | 3 +- src/theory/theory_model.cpp | 3 +- src/theory/uf/theory_uf_type_rules.cpp | 2 +- test/unit/util/datatype_black.cpp | 54 +++++++++------- 23 files changed, 179 insertions(+), 158 deletions(-) create mode 100644 src/expr/type_properties_template.cpp diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index a6a7c04e9..9a89dfbe6 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -105,6 +105,7 @@ libcvc5_add_sources(GENERATED metakind.h node_manager.cpp type_checker.cpp + type_properties.cpp type_properties.h ) @@ -146,6 +147,16 @@ add_custom_command( DEPENDS mkkind type_properties_template.h ${KINDS_FILES} ) +add_custom_command( + OUTPUT type_properties.cpp + COMMAND + ${mkkind_script} + ${CMAKE_CURRENT_LIST_DIR}/type_properties_template.cpp + ${KINDS_FILES} + > ${CMAKE_CURRENT_BINARY_DIR}/type_properties.cpp + DEPENDS mkkind type_properties_template.cpp type_properties.h ${KINDS_FILES} +) + add_custom_command( OUTPUT metakind.h COMMAND @@ -194,5 +205,6 @@ add_custom_target(gen-expr metakind.h node_manager.cpp type_checker.cpp + type_properties.cpp type_properties.h ) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index a5719a7ff..5b2503454 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -278,7 +278,8 @@ void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) if (!hasConstant) { // add an arbitrary one - Node op = st.mkGroundTerm(); + NodeManager* nm = NodeManager::currentNM(); + Node op = nm->mkGroundTerm(st); // use same naming convention as SygusDatatype std::stringstream ss; ss << getName() << "_" << getNumConstructors() << "_" << op; diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index f23cfa4f9..6ba3970c9 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -410,7 +410,7 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t, else { // call mkGroundValue or mkGroundTerm based on isValue - arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm(); + arg = isValue ? nm->mkGroundValue(selType) : nm->mkGroundTerm(selType); } if (arg.isNull()) { diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp index b72aa99f6..3b165ded8 100644 --- a/src/expr/node_converter.cpp +++ b/src/expr/node_converter.cpp @@ -199,7 +199,7 @@ TypeNode NodeConverter::convertType(TypeNode tn) if (ret.getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator - nb << ret.getOperator(); + nb << NodeManager::operatorFromType(ret); } for (TypeNode::const_iterator j = ret.begin(), iend = ret.end(); j != iend; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5b74b04e1..6435c488a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -73,6 +73,18 @@ class NodeManager */ static bool isNAryKind(Kind k); + /** + * Returns a node representing the operator of this `TypeNode`. + * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) have an + * operator. "Little-p parameterized" types (like Array), are OPERATORs, not + * PARAMETERIZEDs. + */ + static Node operatorFromType(const TypeNode& tn) + { + Assert(tn.getMetaKind() == kind::metakind::PARAMETERIZED); + return Node(tn.d_nv->getOperator()); + } + private: /** * Instead of creating an instance using the constructor, @@ -448,6 +460,24 @@ class NodeManager Node mkBoundVar(const TypeNode& type); + /** + * Construct and return a ground term of a given type. If the type is not + * well founded, this function throws an exception. + * + * @param tn The type + * @return a ground term of the type + */ + Node mkGroundTerm(const TypeNode& tn); + + /** + * Construct and return a ground value of a given type. If the type is not + * well founded, this function throws an exception. + * + * @param tn The type + * @return a ground value of the type + */ + Node mkGroundValue(const TypeNode& tn); + /** get the canonical bound variable list for function type tn */ Node getBoundVarListForFunctionType( TypeNode tn ); diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 06f5bcfb6..a3e267d95 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -29,8 +29,10 @@ #include "expr/node_manager_attributes.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" +#include "expr/type_properties.h" #include "theory/bags/bag_make_op.h" #include "theory/sets/singleton_op.h" +#include "theory/type_enumerator.h" #include "util/abstract_value.h" #include "util/bitvector.h" #include "util/rational.h" @@ -1216,6 +1218,17 @@ NodeClass NodeManager::mkConstInternal(Kind k, const T& val) return NodeClass(nv); } +Node NodeManager::mkGroundTerm(const TypeNode& tn) +{ + return kind::mkGroundTerm(tn); +} + +Node NodeManager::mkGroundValue(const TypeNode& tn) +{ + theory::TypeEnumerator te(tn); + return *te; +} + bool NodeManager::safeToReclaimZombies() const { // FIXME multithreading diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e94d4733e..8358facac 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -264,16 +264,6 @@ bool TypeNode::isWellFounded() const { return kind::isWellFounded(*this); } -Node TypeNode::mkGroundTerm() const { - return kind::mkGroundTerm(*this); -} - -Node TypeNode::mkGroundValue() const -{ - theory::TypeEnumerator te(*this); - return *te; -} - bool TypeNode::isStringLike() const { return isString() || isSequence(); } // !!! Note that this will change to isReal() || isInteger() when subtyping is @@ -560,47 +550,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { } } -Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { - TypeNode ntn = n.getType(); - Assert(ntn.isComparableTo(tn)); - if( !ntn.isSubtypeOf( tn ) ){ - if( tn.isInteger() ){ - if( tn.isSubtypeOf( ntn ) ){ - return NodeManager::currentNM()->mkNode( kind::IS_INTEGER, n ); - } - }else if( tn.isDatatype() && ntn.isDatatype() ){ - if( tn.isTuple() && ntn.isTuple() ){ - const DType& dt1 = tn.getDType(); - const DType& dt2 = ntn.getDType(); - NodeManager* nm = NodeManager::currentNM(); - if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){ - std::vector< Node > conds; - for( unsigned i=0; imkNode( - kind::APPLY_SELECTOR_TOTAL, dt2[0][i].getSelector(), n); - Node etc = getEnsureTypeCondition(s, dt1[0][i].getRangeType()); - if( etc.isNull() ){ - return Node::null(); - }else{ - conds.push_back( etc ); - } - } - if( conds.empty() ){ - return nm->mkConst(true); - }else if( conds.size()==1 ){ - return conds[0]; - }else{ - return nm->mkNode(kind::AND, conds); - } - } - } - } - return Node::null(); - }else{ - return NodeManager::currentNM()->mkConst( true ); - } -} - /** Is this a sort kind */ bool TypeNode::isSort() const { return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); @@ -698,6 +647,17 @@ uint32_t TypeNode::getBitVectorSize() const return getConst(); } +TypeNode TypeNode::getRangeType() const +{ + if (isTester()) + { + return NodeManager::currentNM()->booleanType(); + } + Assert(isFunction() || isConstructor() || isSelector()) + << "Cannot get range type of " << *this; + return (*this)[getNumChildren() - 1]; +} + } // namespace cvc5 namespace std { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 33d698163..9882c7fc5 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -217,16 +217,6 @@ private: return TypeNode(d_nv->getChild(i)); } - /** - * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these) - * have an operator. "Little-p parameterized" types (like Array), - * are OPERATORs, not PARAMETERIZEDs. - */ - inline Node getOperator() const { - Assert(getMetaKind() == kind::metakind::PARAMETERIZED); - return Node(d_nv->getOperator()); - } - /** * Returns the unique id of this node * @@ -442,22 +432,6 @@ private: */ bool isWellFounded() const; - /** - * Construct and return a ground term of this type. If the type is - * not well founded, this function throws an exception. - * - * @return a ground term of the type - */ - Node mkGroundTerm() const; - - /** - * Construct and return a ground value of this type. If the type is - * not well founded, this function throws an exception. - * - * @return a ground value of the type - */ - Node mkGroundValue() const; - /** * Is this type a subtype of the given type? */ @@ -699,10 +673,6 @@ private: static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); - /** get ensure type condition - * Return value is a condition that implies that n has type tn. - */ - static Node getEnsureTypeCondition( Node n, TypeNode tn ); private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); @@ -975,15 +945,6 @@ inline bool TypeNode::isPredicateLike() const { return isFunctionLike() && getRangeType().isBoolean(); } -inline TypeNode TypeNode::getRangeType() const { - if(isTester()) { - return NodeManager::currentNM()->booleanType(); - } - Assert(isFunction() || isConstructor() || isSelector()) - << "Cannot get range type of " << *this; - return (*this)[getNumChildren() - 1]; -} - /** Is this a floating-point type of with exp exponent bits and sig significand bits */ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { diff --git a/src/expr/type_properties_template.cpp b/src/expr/type_properties_template.cpp new file mode 100644 index 000000000..1ad2572d7 --- /dev/null +++ b/src/expr/type_properties_template.cpp @@ -0,0 +1,51 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Template for the Type properties source file. + */ + +#include "expr/type_properties.h" + +namespace cvc5 { +namespace kind { + +Node mkGroundTerm(TypeConstant tc) +{ + switch (tc) + { + // clang-format off +${type_constant_groundterms} + // clang-format on + default: + InternalError() << "No ground term known for type constant: " << tc; + } +} + +Node mkGroundTerm(TypeNode typeNode) +{ + AssertArgument(!typeNode.isNull(), typeNode); + switch (Kind k = typeNode.getKind()) + { + case TYPE_CONSTANT: + return mkGroundTerm(typeNode.getConst()); + // clang-format off +${type_groundterms} + // clang-format on + default: + InternalError() << "A theory kinds file did not provide a ground term " + << "or ground term computer for type:\n" + << typeNode << "\nof kind " << k; + } +} + +} // namespace kind +} // namespace cvc5 diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 40ead9a5e..3ce3391dc 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -97,34 +97,8 @@ ${type_wellfoundednesses} } }/* isWellFounded(TypeNode) */ -inline Node mkGroundTerm(TypeConstant tc) -{ - switch (tc) - { - // clang-format off -${type_constant_groundterms} - // clang-format on - default: - InternalError() << "No ground term known for type constant: " << tc; - } -} /* mkGroundTerm(TypeConstant) */ - -inline Node mkGroundTerm(TypeNode typeNode) -{ - AssertArgument(!typeNode.isNull(), typeNode); - switch (Kind k = typeNode.getKind()) - { - case TYPE_CONSTANT: - return mkGroundTerm(typeNode.getConst()); - // clang-format off -${type_groundterms} - // clang-format on - default: - InternalError() << "A theory kinds file did not provide a ground term " - << "or ground term computer for type:\n" - << typeNode << "\nof kind " << k; - } -} /* mkGroundTerm(TypeNode) */ +Node mkGroundTerm(TypeConstant tc); +Node mkGroundTerm(TypeNode typeNode); } // namespace kind } // namespace cvc5 diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index a389c6efb..7ba98000a 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -251,8 +251,9 @@ bool ArraysProperties::isWellFounded(TypeNode type) Node ArraysProperties::mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::ARRAY_TYPE); + NodeManager* nm = NodeManager::currentNM(); TypeNode elemType = type.getArrayConstituentType(); - Node elem = elemType.mkGroundTerm(); + Node elem = nm->mkGroundTerm(elemType); if (elem.isConst()) { return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem)); diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 4cda9f728..903a08bb4 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -441,7 +441,8 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) else if (k == kind::APPLY_SELECTOR_TOTAL) { // evaluates to the first ground value of type tn. - Node gt = tn.mkGroundValue(); + NodeManager* nm = NodeManager::currentNM(); + Node gt = nm->mkGroundValue(tn); Assert(!gt.isNull()); if (tn.isDatatype() && !tn.isInstantiatedDatatype()) { diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index cfeb72b5c..69153ef00 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -93,7 +93,7 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id, const DTypeConstructor& dtc = dt[constructorIndex]; int selectorIndex = dtc.getSelectorIndexInternal(selector); Node r = - selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex]; + selectorIndex < 0 ? nm->mkGroundTerm(t.getType()) : t[0][selectorIndex]; return t.eqNode(r); } else if (id == PfRule::DT_SPLIT) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b19eb53af..a9f0c3198 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1007,10 +1007,11 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { // uninterpreted sorts and arrays, where the solver does not fully // handle values of the sort. The call to mkGroundTerm does not introduce // values for these sorts. - rrs = r.getType().mkGroundTerm(); + NodeManager* nm = NodeManager::currentNM(); + rrs = nm->mkGroundTerm(r.getType()); Trace("datatypes-wrong-sel") << "Bad apply " << r << " term = " << rrs - << ", value = " << r.getType().mkGroundValue() << std::endl; + << ", value = " << nm->mkGroundValue(r.getType()) << std::endl; } else { diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 5a5d97064..5f129f3fc 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -150,6 +150,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, if (r.asSatisfiabilityResult().isSat() == Result::SAT) { Trace("rr-check") << "...rewrite does not hold for: " << std::endl; + NodeManager* nm = NodeManager::currentNM(); is_unique_term = true; std::vector vars; d_sampler->getVariables(vars); @@ -166,7 +167,7 @@ Node CandidateRewriteDatabase::addTerm(Node sol, if (itf == d_fv_to_skolem.end()) { // not in conjecture, can use arbitrary value - val = v.getType().mkGroundTerm(); + val = nm->mkGroundTerm(v.getType()); } else { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a05b64249..438afbe82 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -437,7 +437,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, else if (type.isArray() || type.isSet()) { // generate constant array over the first element of the constituent type - Node c = type.mkGroundTerm(); + Node c = nm->mkGroundTerm(type); // note that c should never contain an uninterpreted constant Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); @@ -1065,8 +1065,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { // if there are not constructors yet by this point, which can happen, // e.g. for unimplemented types that have no variables in the argument - // list of the function-to-synthesize, create a fresh ground term - sdts[i].addConstructor(types[i].mkGroundTerm(), "", {}); + // list of the function-to-synthesize, create a fresh ground term + sdts[i].addConstructor(nm->mkGroundTerm(types[i]), "", {}); } // always add ITE diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 6167f7474..bd71de283 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -442,9 +442,10 @@ Node SygusReconstruct::mkGround(Node n) const std::unordered_map subs; // generate a ground value for each one of those variables + NodeManager* nm = NodeManager::currentNM(); for (const TNode& var : vars) { - subs.emplace(var, var.getType().mkGroundValue()); + subs.emplace(var, nm->mkGroundValue(var.getType())); } // substitute the variables with ground values diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 6b023075b..d1f29d207 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -609,7 +609,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) { if (sol_templ_children[j].isNull()) { - sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm(); + sol_templ_children[j] = + nm->mkGroundTerm(cop_to_sks[cop][j].getType()); } } sol_templ_children.insert(sol_templ_children.begin(), cop); diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index d22bde370..3e4a69dc9 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -116,9 +116,10 @@ Result checkWithSubsolver(Node query, if (r.asSatisfiabilityResult().isSat() == Result::SAT) { // default model + NodeManager* nm = NodeManager::currentNM(); for (const Node& v : vars) { - modelVals.push_back(v.getType().mkGroundTerm()); + modelVals.push_back(nm->mkGroundTerm(v.getType())); } } return r; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 69cd790e8..1d82f9abd 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1757,7 +1757,8 @@ Node SequencesRewriter::rewriteSeqNth(Node node) if (node.getKind() == SEQ_NTH_TOTAL) { // return arbitrary term - Node ret = s.getType().getSequenceElementType().mkGroundValue(); + NodeManager* nm = NodeManager::currentNM(); + Node ret = nm->mkGroundValue(s.getType().getSequenceElementType()); return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB); } else diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a91a185a0..079683116 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -124,7 +124,8 @@ std::vector TheoryModel::getDomainElements(TypeNode tn) const { // This is called when t is a sort that does not occur in this model. // Sorts are always interpreted as non-empty, thus we add a single element. - elements.push_back(tn.mkGroundTerm()); + NodeManager* nm = NodeManager::currentNM(); + elements.push_back(nm->mkGroundTerm(tn)); return elements; } return *type_refs; diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index a05c76d4c..2c0dcd763 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -264,7 +264,7 @@ Node FunctionProperties::mkGroundTerm(TypeNode type) { NodeManager* nm = NodeManager::currentNM(); Node bvl = nm->getBoundVarListForFunctionType(type); - Node ret = type.getRangeType().mkGroundTerm(); + Node ret = nm->mkGroundTerm(type.getRangeType()); return nm->mkNode(kind::LAMBDA, bvl, ret); } diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 15dde0cc2..336190b8e 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -71,8 +71,9 @@ TEST_F(TestUtilBlackDatatype, enumeration) ASSERT_TRUE(colorsType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << colorsType.getDType().getName() << std::endl - << " is " << colorsType.mkGroundTerm() << std::endl; - ASSERT_EQ(colorsType.mkGroundTerm().getType(), colorsType); + << " is " << d_nodeManager->mkGroundTerm(colorsType) + << std::endl; + ASSERT_EQ(d_nodeManager->mkGroundTerm(colorsType).getType(), colorsType); } TEST_F(TestUtilBlackDatatype, nat) @@ -103,8 +104,9 @@ TEST_F(TestUtilBlackDatatype, nat) ASSERT_TRUE(natType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << natType.getDType().getName() << std::endl - << " is " << natType.mkGroundTerm() << std::endl; - ASSERT_TRUE(natType.mkGroundTerm().getType() == natType); + << " is " << d_nodeManager->mkGroundTerm(natType) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(natType).getType() == natType); } TEST_F(TestUtilBlackDatatype, tree) @@ -135,8 +137,9 @@ TEST_F(TestUtilBlackDatatype, tree) ASSERT_TRUE(treeType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << treeType.getDType().getName() << std::endl - << " is " << treeType.mkGroundTerm() << std::endl; - ASSERT_TRUE(treeType.mkGroundTerm().getType() == treeType); + << " is " << d_nodeManager->mkGroundTerm(treeType) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).getType() == treeType); } TEST_F(TestUtilBlackDatatype, list_int) @@ -166,8 +169,9 @@ TEST_F(TestUtilBlackDatatype, list_int) ASSERT_TRUE(listType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDType().getName() << std::endl - << " is " << listType.mkGroundTerm() << std::endl; - ASSERT_TRUE(listType.mkGroundTerm().getType() == listType); + << " is " << d_nodeManager->mkGroundTerm(listType) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType); } TEST_F(TestUtilBlackDatatype, list_real) @@ -196,8 +200,9 @@ TEST_F(TestUtilBlackDatatype, list_real) ASSERT_TRUE(listType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDType().getName() << std::endl - << " is " << listType.mkGroundTerm() << std::endl; - ASSERT_TRUE(listType.mkGroundTerm().getType() == listType); + << " is " << d_nodeManager->mkGroundTerm(listType) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType); } TEST_F(TestUtilBlackDatatype, list_boolean) @@ -226,8 +231,9 @@ TEST_F(TestUtilBlackDatatype, list_boolean) ASSERT_TRUE(listType.getDType().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDType().getName() << std::endl - << " is " << listType.mkGroundTerm() << std::endl; - ASSERT_TRUE(listType.mkGroundTerm().getType() == listType); + << " is " << d_nodeManager->mkGroundTerm(listType) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(listType).getType() == listType); } TEST_F(TestUtilBlackDatatype, listIntUpdate) @@ -248,7 +254,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) TypeNode listType = d_nodeManager->mkDatatypeType(list); const DType& ldt = listType.getDType(); Node updater = ldt[0][0].getUpdater(); - Node gt = listType.mkGroundTerm(); + Node gt = d_nodeManager->mkGroundTerm(listType); Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term @@ -322,8 +328,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees1) ASSERT_TRUE(dtts[0].getDType().isWellFounded()); Debug("groundterms") << "ground term of " << dtts[0].getDType().getName() << std::endl - << " is " << dtts[0].mkGroundTerm() << std::endl; - ASSERT_TRUE(dtts[0].mkGroundTerm().getType() == dtts[0]); + << " is " << d_nodeManager->mkGroundTerm(dtts[0]) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[0]).getType() == dtts[0]); ASSERT_FALSE(dtts[1].getDType().isFinite()); ASSERT_TRUE(dtts[1].getDType().getCardinality().compare(Cardinality::INTEGERS) @@ -331,8 +338,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees1) ASSERT_TRUE(dtts[1].getDType().isWellFounded()); Debug("groundterms") << "ground term of " << dtts[1].getDType().getName() << std::endl - << " is " << dtts[1].mkGroundTerm() << std::endl; - ASSERT_TRUE(dtts[1].mkGroundTerm().getType() == dtts[1]); + << " is " << d_nodeManager->mkGroundTerm(dtts[1]) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts[1]).getType() == dtts[1]); } TEST_F(TestUtilBlackDatatype, mutual_list_trees2) @@ -388,8 +396,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees2) ASSERT_TRUE(dtts2[0].getDType().isWellFounded()); Debug("groundterms") << "ground term of " << dtts2[0].getDType().getName() << std::endl - << " is " << dtts2[0].mkGroundTerm() << std::endl; - ASSERT_TRUE(dtts2[0].mkGroundTerm().getType() == dtts2[0]); + << " is " << d_nodeManager->mkGroundTerm(dtts2[0]) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[0]).getType() == dtts2[0]); ASSERT_FALSE(dtts2[1].getDType().isParametric()); ASSERT_FALSE(dtts2[1].getDType().isFinite()); @@ -399,8 +408,9 @@ TEST_F(TestUtilBlackDatatype, mutual_list_trees2) ASSERT_TRUE(dtts2[1].getDType().isWellFounded()); Debug("groundterms") << "ground term of " << dtts2[1].getDType().getName() << std::endl - << " is " << dtts2[1].mkGroundTerm() << std::endl; - ASSERT_TRUE(dtts2[1].mkGroundTerm().getType() == dtts2[1]); + << " is " << d_nodeManager->mkGroundTerm(dtts2[1]) + << std::endl; + ASSERT_TRUE(d_nodeManager->mkGroundTerm(dtts2[1]).getType() == dtts2[1]); } TEST_F(TestUtilBlackDatatype, not_so_well_founded) @@ -423,7 +433,7 @@ TEST_F(TestUtilBlackDatatype, not_so_well_founded) treeType.getDType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); ASSERT_FALSE(treeType.getDType().isWellFounded()); - ASSERT_TRUE(treeType.mkGroundTerm().isNull()); + ASSERT_TRUE(d_nodeManager->mkGroundTerm(treeType).isNull()); ASSERT_TRUE(treeType.getDType().mkGroundTerm(treeType).isNull()); } -- 2.30.2