From 319caf1bf9bff1e02dbdce037a1fe41064470fe0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 29 Mar 2022 17:22:40 -0700 Subject: [PATCH] TypeNode: Rename isSort() and getSortConstructorArity(). (#8446) Names of these two functions were slightly confusing with respect to API terminology. This renames isSort() to isUninterpretedSort() and getSortConstructorArity() to getUninterpretedSortConstructorArity() for more consistency and clarity. --- src/api/cpp/cvc5.cpp | 19 +++++++++------- src/expr/cardinality_constraint.cpp | 2 +- src/expr/dtype.cpp | 2 +- src/expr/dtype_cons.cpp | 5 +++-- src/expr/node_manager_template.cpp | 4 ++-- src/expr/symbol_table.cpp | 13 ++++++----- src/expr/type_node.cpp | 22 +++++++++++-------- src/expr/type_node.h | 6 ++--- src/preprocessing/passes/ackermann.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 8 ++++--- src/proof/lfsc/lfsc_node_converter.cpp | 2 +- src/proof/lfsc/lfsc_printer.cpp | 2 +- src/smt/print_benchmark.cpp | 4 ++-- src/smt/solver_engine.cpp | 2 +- src/theory/quantifiers/equality_query.cpp | 3 ++- src/theory/quantifiers/first_order_model.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 2 +- .../quantifiers/fmf/full_model_check.cpp | 20 ++++++++++++----- src/theory/quantifiers/fmf/model_engine.cpp | 9 +++++--- .../quantifiers/quant_bound_inference.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 4 ++-- src/theory/quantifiers/term_util.cpp | 3 ++- src/theory/sep/theory_sep.cpp | 7 ++++-- src/theory/sort_inference.cpp | 6 ++--- src/theory/theory_model.cpp | 4 ++-- src/theory/theory_model_builder.cpp | 10 ++++----- src/theory/uf/cardinality_extension.cpp | 9 ++++---- src/theory/uf/theory_uf_type_rules.cpp | 2 +- src/util/uninterpreted_sort_value.cpp | 2 +- test/unit/node/node_manager_black.cpp | 10 ++++----- 30 files changed, 108 insertions(+), 80 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c4b912825..aea5add41 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1405,7 +1405,7 @@ bool Sort::isUninterpretedSort() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isSort(); + return d_type->isUninterpretedSort(); //////// CVC5_API_TRY_CATCH_END; } @@ -1414,7 +1414,7 @@ bool Sort::isUninterpretedSortConstructor() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isSortConstructor(); + return d_type->isUninterpretedSortConstructor(); //////// CVC5_API_TRY_CATCH_END; } @@ -1445,13 +1445,15 @@ Sort Sort::instantiate(const std::vector& params) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_DOMAIN_SORTS(params); - CVC5_API_CHECK(d_type->isParametricDatatype() || d_type->isSortConstructor()) + CVC5_API_CHECK(d_type->isParametricDatatype() + || d_type->isUninterpretedSortConstructor()) << "Expected parametric datatype or sort constructor sort."; CVC5_API_CHECK(!d_type->isParametricDatatype() || d_type->getNumChildren() == params.size() + 1) << "Arity mismatch for instantiated parametric datatype"; - CVC5_API_CHECK(!d_type->isSortConstructor() - || d_type->getSortConstructorArity() == params.size()) + CVC5_API_CHECK(!d_type->isUninterpretedSortConstructor() + || d_type->getUninterpretedSortConstructorArity() + == params.size()) << "Arity mismatch for instantiated sort constructor"; //////// all checks before this line std::vector tparams = sortVectorToTypeNodes(params); @@ -1459,7 +1461,7 @@ Sort Sort::instantiate(const std::vector& params) const { return Sort(d_solver, d_type->instantiateParametricDatatype(tparams)); } - Assert(d_type->isSortConstructor()); + Assert(d_type->isUninterpretedSortConstructor()); return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams)); //////// CVC5_API_TRY_CATCH_END; @@ -1710,9 +1712,10 @@ size_t Sort::getUninterpretedSortConstructorArity() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(d_type->isSortConstructor()) << "Not a sort constructor sort."; + CVC5_API_CHECK(d_type->isUninterpretedSortConstructor()) + << "Not a sort constructor sort."; //////// all checks before this line - return d_type->getSortConstructorArity(); + return d_type->getUninterpretedSortConstructorArity(); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/expr/cardinality_constraint.cpp b/src/expr/cardinality_constraint.cpp index a470dfb3a..5f6c33dbf 100644 --- a/src/expr/cardinality_constraint.cpp +++ b/src/expr/cardinality_constraint.cpp @@ -25,7 +25,7 @@ CardinalityConstraint::CardinalityConstraint(const TypeNode& type, const Integer& ub) : d_type(new TypeNode(type)), d_ubound(ub) { - AlwaysAssert(type.isSort()) + AlwaysAssert(type.isUninterpretedSort()) << "Unexpected cardinality constraints for " << type; } diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 4375ac6e3..5fbceee64 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -446,7 +446,7 @@ bool DType::computeCardinalityRecSingleton( TypeNode tc = d_constructors[0]->getArgType(i); // if it is an uninterpreted sort, then we depend on it having cardinality // one - if (tc.isSort()) + if (tc.isUninterpretedSort()) { if (std::find(u_assume.begin(), u_assume.end(), tc) == u_assume.end()) { diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 71ec23f8d..8cde888d6 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -310,7 +310,7 @@ bool DTypeConstructor::involvesUninterpretedType() const { for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++) { - if (!getArgType(i).isSort()) + if (!getArgType(i).isUninterpretedSort()) { return true; } @@ -645,7 +645,8 @@ TypeNode DTypeConstructor::doParametricSubstitution( } for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i) { - if (paramTypes[i].getSortConstructorArity() == origChildren.size()) + if (paramTypes[i].getUninterpretedSortConstructorArity() + == origChildren.size()) { TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren); if (range == tn) diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 9f8e8885a..6bd665f26 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -645,14 +645,14 @@ std::vector NodeManager::mkMutualDatatypeTypes( // unresolved SortType used as a placeholder in complex types) // with "(*resolver).second" (the TypeNode we created in the // first step, above). - if (ut.isSort()) + if (ut.isUninterpretedSort()) { placeholders.push_back(ut); replacements.push_back((*resolver).second); } else { - Assert(ut.isSortConstructor()); + Assert(ut.isUninterpretedSortConstructor()); paramTypes.push_back(ut); paramReplacements.push_back((*resolver).second); } diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 8c0bd44dc..7280c5902 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -490,11 +490,13 @@ cvc5::Sort SymbolTable::Implementation::lookupType( "expected parametric datatype"); return p.second.instantiate(params); } - bool isSortConstructor = p.second.isUninterpretedSortConstructor(); + bool isUninterpretedSortConstructor = + p.second.isUninterpretedSortConstructor(); if (TraceIsOn("sort")) { Trace("sort") << "instantiating using a sort " - << (isSortConstructor ? "constructor" : "substitution") + << (isUninterpretedSortConstructor ? "constructor" + : "substitution") << std::endl; Trace("sort") << "have formals ["; copy(p.first.begin(), @@ -508,10 +510,9 @@ cvc5::Sort SymbolTable::Implementation::lookupType( << "type ctor " << name << std::endl << "type is " << p.second << std::endl; } - cvc5::Sort instantiation = isSortConstructor - ? p.second.instantiate(params) - : p.second.substitute(p.first, params); - + cvc5::Sort instantiation = isUninterpretedSortConstructor + ? p.second.instantiate(params) + : p.second.substitute(p.first, params); Trace("sort") << "instance is " << instantiation << std::endl; return instantiation; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 5fa22a1a9..2f92e9233 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -96,7 +96,7 @@ CardinalityClass TypeNode::getCardinalityClass() getAttribute(TypeCardinalityClassAttr())); } CardinalityClass ret = CardinalityClass::INFINITE; - if (isSort()) + if (isUninterpretedSort()) { ret = CardinalityClass::INTERPRETED_ONE; } @@ -217,7 +217,8 @@ bool TypeNode::isClosedEnumerable() if (!getAttribute(IsClosedEnumerableComputedAttr())) { bool ret = true; - if (isArray() || isSort() || isCodatatype() || isFunction() || isRegExp()) + if (isArray() || isUninterpretedSort() || isCodatatype() || isFunction() + || isRegExp()) { ret = false; } @@ -424,7 +425,7 @@ bool TypeNode::isInstantiatedDatatype() const { bool TypeNode::isInstantiated() const { return isInstantiatedDatatype() - || (isSort() && getNumChildren() > 0); + || (isUninterpretedSort() && getNumChildren() > 0); } TypeNode TypeNode::instantiateParametricDatatype( @@ -443,22 +444,23 @@ TypeNode TypeNode::instantiateParametricDatatype( return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); } -uint64_t TypeNode::getSortConstructorArity() const +uint64_t TypeNode::getUninterpretedSortConstructorArity() const { - Assert(isSortConstructor() && hasAttribute(expr::SortArityAttr())); + Assert(isUninterpretedSortConstructor() + && hasAttribute(expr::SortArityAttr())); return getAttribute(expr::SortArityAttr()); } std::string TypeNode::getName() const { - Assert(isSort() || isSortConstructor()); + Assert(isUninterpretedSort() || isUninterpretedSortConstructor()); return getAttribute(expr::VarNameAttr()); } TypeNode TypeNode::instantiateSortConstructor( const std::vector& params) const { - Assert(isSortConstructor()); + Assert(isUninterpretedSortConstructor()); return NodeManager::currentNM()->mkSort(*this, params); } @@ -570,12 +572,14 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { } /** Is this a sort kind */ -bool TypeNode::isSort() const { +bool TypeNode::isUninterpretedSort() const +{ return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); } /** Is this a sort constructor kind */ -bool TypeNode::isSortConstructor() const { +bool TypeNode::isUninterpretedSortConstructor() const +{ return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8c6e98ddb..584c64554 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -650,13 +650,13 @@ private: uint32_t getBitVectorSize() const; /** Is this a sort kind */ - bool isSort() const; + bool isUninterpretedSort() const; /** Is this a sort constructor kind */ - bool isSortConstructor() const; + bool isUninterpretedSortConstructor() const; /** Get sort constructor arity */ - uint64_t getSortConstructorArity() const; + uint64_t getUninterpretedSortConstructorArity() const; /** * Get name, for uninterpreted sorts and uninterpreted sort constructors. diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index f1b1e2257..4788e57f5 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -239,7 +239,7 @@ std::unordered_set getVarsWithUSorts(AssertionPipeline* assertions) for (const TNode& var : vars) { - if (var.getType().isSort()) + if (var.getType().isUninterpretedSort()) { res.insert(var); } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f7ef49c88..583567e98 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1387,7 +1387,7 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, TypeNode tn, const std::vector& elements) const { - if (!tn.isSort()) + if (!tn.isUninterpretedSort()) { out << "ERROR: don't know how to print non uninterpreted sort in model: " << tn << std::endl; @@ -1651,8 +1651,10 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( void Smt2Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const { - Assert(type.isSort() || type.isSortConstructor()); - size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0; + Assert(type.isUninterpretedSort() || type.isUninterpretedSortConstructor()); + size_t arity = type.isUninterpretedSortConstructor() + ? type.getUninterpretedSortConstructorArity() + : 0; out << "(declare-sort " << type << " " << arity << ")" << std::endl; } diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 9a2453eb6..4259dde07 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -562,7 +562,7 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) std::stringstream ss; options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6); tn.toStream(ss); - if (tn.isSort() || (tn.isDatatype() && !tn.isTuple())) + if (tn.isUninterpretedSort() || (tn.isDatatype() && !tn.isTuple())) { std::stringstream sss; sss << LfscNodeConverter::getNameForUserName(ss.str()); diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index 52b64fe5b..bba0fad22 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -242,7 +242,7 @@ void LfscPrinter::printTypeDefinition( return; } processed.insert(tn); - if (tn.isSort()) + if (tn.isUninterpretedSort()) { os << "(declare "; printType(os, tn); diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp index fa9a50a78..a02cc4b19 100644 --- a/src/smt/print_benchmark.cpp +++ b/src/smt/print_benchmark.cpp @@ -56,7 +56,7 @@ void PrintBenchmark::printAssertions(std::ostream& out, std::vector datatypeBlock; for (const TypeNode& ctn : connectedTypes) { - if (ctn.isSort()) + if (ctn.isUninterpretedSort()) { d_printer->toStreamCmdDeclareType(out, ctn); } @@ -183,7 +183,7 @@ void PrintBenchmark::getConnectedSubfieldTypes( return; } processed.insert(tn); - if (tn.isSort()) + if (tn.isUninterpretedSort()) { connectedTypes.push_back(tn); } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 247950476..59264ee70 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1010,7 +1010,7 @@ std::vector SolverEngine::getValues(const std::vector& exprs) const std::vector SolverEngine::getModelDomainElements(TypeNode tn) const { - Assert(tn.isSort()); + Assert(tn.isUninterpretedSort()); TheoryModel* m = getAvailableModel("getModelDomainElements"); return m->getDomainElements(tn); } diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 2bc208fa3..ac58a4d9f 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -63,7 +63,8 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) r = tr; r = d_qstate.getRepresentative(r); }else{ - if( r.getType().isSort() ){ + if (r.getType().isUninterpretedSort()) + { Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; //should never happen : UF constants should never escape model Assert(false); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index f707c952c..57be2d8d4 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -157,7 +157,7 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn) { RepSet* rs = d_model->getRepSetPtr(); - if (tn.isSort()) + if (tn.isUninterpretedSort()) { // must ensure uninterpreted type is non-empty. if (!rs->hasType(tn)) diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 96f33ed5d..464e67257 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -438,7 +438,7 @@ void BoundedIntegers::checkOwnership(Node f) for( unsigned i=0; id_type_reps.end(); ++it) { - if( it->first.isSort() ){ + if (it->first.isUninterpretedSort()) + { Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; for( size_t a=0; asecond.size(); a++ ){ Node r = m->getRepresentative(it->second[a]); @@ -613,13 +615,16 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { else { TypeNode tn = n.getType(); - if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){ + if (tn.isUninterpretedSort() && d_rep_ids.find(tn) != d_rep_ids.end()) + { if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) { Trace(tr) << d_rep_ids[tn][n]; }else{ Trace(tr) << n; } - }else{ + } + else + { Trace(tr) << n; } } @@ -1059,7 +1064,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def d.addEntry(fm, mkCond(cond), d_true); }else{ TypeNode tn = eq[0].getType(); - if( tn.isSort() ){ + if (tn.isUninterpretedSort()) + { int j = fm->getVariableId(f, eq[0]); int k = fm->getVariableId(f, eq[1]); const RepSet* rs = fm->getRepSet(); @@ -1076,7 +1082,9 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def d.addEntry( fm, mkCond(cond), d_true); } d.addEntry( fm, mkCondDefault(fm, f), d_false); - }else{ + } + else + { d.addEntry( fm, mkCondDefault(fm, f), Node::null()); } } diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 86e4a8778..2c4db6ae7 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -139,7 +139,8 @@ void ModelEngine::registerQuantifier( Node f ){ bool canHandle = true; for( unsigned i=0; igetRepSetPtr()->d_type_reps.end(); ++it) { - if( it->first.isSort() ){ - Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + if (it->first.isUninterpretedSort()) + { + Trace("model-engine") << "Cardinality( " << it->first << " )" + << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " Reps : "; for( size_t i=0; isecond.size(); i++ ){ Trace("model-engine-debug") << it->second[i] << " "; diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index effe91475..0552e1d29 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -73,7 +73,7 @@ bool QuantifiersBoundInference::isFiniteBound(Node q, Node v) return true; } TypeNode tn = v.getType(); - if (tn.isSort() && d_isFmf) + if (tn.isUninterpretedSort() && d_isFmf) { return true; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 510f2b38f..3d9c67b92 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -533,7 +533,7 @@ bool CegGrammarConstructor::isHandledType(TypeNode t) collectSygusGrammarTypesFor(t, types); for (const TypeNode& tn : types) { - if (tn.isSort() || tn.isFloatingPoint()) + if (tn.isUninterpretedSort() || tn.isFloatingPoint()) { return false; } @@ -1050,7 +1050,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(cop, dt[l].getName(), cargsCons); } } - else if (types[i].isSort() || types[i].isFunction() + else if (types[i].isUninterpretedSort() || types[i].isFunction() || types[i].isRoundingMode()) { // do nothing diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index a4f897860..4209bf250 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -214,7 +214,8 @@ int TermUtil::getTermDepth( Node n ) { bool TermUtil::containsUninterpretedConstant( Node n ) { if (!n.hasAttribute(ContainsUConstAttribute()) ){ bool ret = false; - if (n.getKind() == UNINTERPRETED_SORT_VALUE && n.getType().isSort()) + if (n.getKind() == UNINTERPRETED_SORT_VALUE + && n.getType().isUninterpretedSort()) { ret = true; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index b26354467..df161616a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1197,10 +1197,13 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { //check whether monotonic (elements can be added to tn without effecting satisfiability) bool tn_is_monotonic = true; - if( tn.isSort() ){ + if (tn.isUninterpretedSort()) + { //TODO: use monotonicity inference tn_is_monotonic = !logicInfo().isQuantified(); - }else{ + } + else + { tn_is_monotonic = tn.getCardinality().isInfinite(); } //add a reference type for maximum occurrences of empty in a constraint diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 3c4cf6487..b4c0c07c7 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -381,7 +381,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< //apply sort inference to quantified variables for( size_t i=0; i TheoryModel::getDomainElements(TypeNode tn) const { // must be an uninterpreted sort - Assert(tn.isSort()); + Assert(tn.isUninterpretedSort()); std::vector elements; const std::vector* type_refs = d_rep_set.getTypeRepsOrNull(tn); if (type_refs == nullptr || type_refs->empty()) @@ -171,7 +171,7 @@ bool TheoryModel::isModelCoreSymbol(Node s) const Cardinality TheoryModel::getCardinality(TypeNode tn) const { //for now, we only handle cardinalities for uninterpreted sorts - if (!tn.isSort()) + if (!tn.isUninterpretedSort()) { Trace("model-getvalue-debug") << "Get cardinality other sort, unknown." << std::endl; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 6938f7bf0..942374a47 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -282,7 +282,7 @@ bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r) bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const { - if (tn.isSort()) + if (tn.isUninterpretedSort()) { return true; } @@ -316,7 +316,7 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( { visited[v] = true; TypeNode tn = v.getType(); - if (tn.isSort()) + if (tn.isUninterpretedSort()) { Trace("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl; @@ -608,7 +608,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // count the number of equivalence classes of sorts in finite model finding if (options().quantifiers.finiteModelFind) { - if (eqct.isSort()) + if (eqct.isUninterpretedSort()) { eqc_usort_count[eqct]++; } @@ -889,7 +889,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) bool isUSortFiniteRestricted = false; if (options().quantifiers.finiteModelFind) { - isUSortFiniteRestricted = !t.isSort() && involvesUSort(t); + isUSortFiniteRestricted = !t.isUninterpretedSort() && involvesUSort(t); } #endif @@ -960,7 +960,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) n = itAssigner->second.getNextAssignment(); Assert(!n.isNull()); } - else if (t.isSort() || !d_env.isFiniteType(t)) + else if (t.isUninterpretedSort() || !d_env.isFiniteType(t)) { // If its interpreted as infinite, we get a fresh value that does // not occur in the model. diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 8c75a407d..b193adfde 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1346,7 +1346,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) const CardinalityConstraint& cc = lit.getOperator().getConst(); TypeNode tn = cc.getType(); - Assert(tn.isSort()); + Assert(tn.isUninterpretedSort()); Assert(d_rep_model[tn]); uint32_t nCard = cc.getUpperBound().getUnsignedInt(); Trace("uf-ss-debug") << "...check cardinality constraint : " << tn @@ -1525,7 +1525,8 @@ void CardinalityExtension::check(Theory::Effort level) while( !eqcs_i.isFinished() ){ Node a = *eqcs_i; TypeNode tn = a.getType(); - if( tn.isSort() ){ + if (tn.isUninterpretedSort()) + { if( type_proc.find( tn )==type_proc.end() ){ std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn ); if( itel!=eqc_list.end() ){ @@ -1610,7 +1611,7 @@ void CardinalityExtension::preRegisterTerm(TNode n) { tn = n.getType(); } - if (!tn.isSort()) + if (!tn.isUninterpretedSort()) { return; } @@ -1618,7 +1619,7 @@ void CardinalityExtension::preRegisterTerm(TNode n) if (it == d_rep_model.end()) { SortModel* rm = nullptr; - if (tn.isSort()) + if (tn.isUninterpretedSort()) { Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl; rm = new SortModel(d_env, tn, d_state, d_im, this); diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 7f15f1c57..bdea5057a 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -73,7 +73,7 @@ TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager, if (check) { const CardinalityConstraint& cc = n.getConst(); - if (!cc.getType().isSort()) + if (!cc.getType().isUninterpretedSort()) { throw TypeCheckingExceptionPrivate( n, "cardinality constraint must apply to uninterpreted sort"); diff --git a/src/util/uninterpreted_sort_value.cpp b/src/util/uninterpreted_sort_value.cpp index b2fde93f3..4a1c86f41 100644 --- a/src/util/uninterpreted_sort_value.cpp +++ b/src/util/uninterpreted_sort_value.cpp @@ -35,7 +35,7 @@ UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type, const Integer& index) : d_type(new TypeNode(type)), d_index(index) { - PrettyCheckArgument(type.isSort(), + PrettyCheckArgument(type.isUninterpretedSort(), type, "uninterpreted constants can only be created for " "uninterpreted sorts, not `%s'", diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index 0eb03ca42..cfdffe116 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -162,7 +162,7 @@ TEST_F(TestNodeBlackNodeManager, booleanType) ASSERT_FALSE(t.isFunction()); ASSERT_FALSE(t.isNull()); ASSERT_FALSE(t.isPredicate()); - ASSERT_FALSE(t.isSort()); + ASSERT_FALSE(t.isUninterpretedSort()); ASSERT_EQ(t, t2); ASSERT_NE(t, t3); @@ -180,7 +180,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool) ASSERT_TRUE(t.isFunction()); ASSERT_FALSE(t.isNull()); ASSERT_TRUE(t.isPredicate()); - ASSERT_FALSE(t.isSort()); + ASSERT_FALSE(t.isUninterpretedSort()); ASSERT_EQ(t, t2); @@ -208,7 +208,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type) ASSERT_TRUE(t.isFunction()); ASSERT_FALSE(t.isNull()); ASSERT_FALSE(t.isPredicate()); - ASSERT_FALSE(t.isSort()); + ASSERT_FALSE(t.isUninterpretedSort()); ASSERT_EQ(t, t2); @@ -238,7 +238,7 @@ TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments) ASSERT_TRUE(t.isFunction()); ASSERT_FALSE(t.isNull()); ASSERT_FALSE(t.isPredicate()); - ASSERT_FALSE(t.isSort()); + ASSERT_FALSE(t.isUninterpretedSort()); ASSERT_EQ(t, t2); @@ -269,7 +269,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType) ASSERT_TRUE(t.isFunction()); ASSERT_FALSE(t.isNull()); ASSERT_TRUE(t.isPredicate()); - ASSERT_FALSE(t.isSort()); + ASSERT_FALSE(t.isUninterpretedSort()); ASSERT_EQ(t, t2); -- 2.30.2