From: Andrew Reynolds Date: Tue, 19 Apr 2022 19:35:40 +0000 (-0500) Subject: Simplify implementation of subtype methods in TypeNode (#8634) X-Git-Tag: cvc5-1.0.1~245 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36d3f481fbeecf09ff7330dc4fa30c175d6834b7;p=cvc5.git Simplify implementation of subtype methods in TypeNode (#8634) Also deletes unused data that was used for an inference schema involving subtypes in sets. --- diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index f48f5a320..d7b832c70 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -284,22 +284,34 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { if(*this == t) { return true; } - if(getKind() == kind::TYPE_CONSTANT) { - switch(getConst()) { - case INTEGER_TYPE: - return t.getKind() == kind::TYPE_CONSTANT && t.getConst() == REAL_TYPE; - default: - return false; - } + if (isInteger()) + { + return t.isReal(); } if (isFunction() && t.isFunction()) { - if (!isComparableTo(t)) + if (!getRangeType().isSubtypeOf(t.getRangeType())) + { + // range is not subtype, return false + return false; + } + // must have equal arguments + std::vector t0a = getArgTypes(); + std::vector t1a = t.getArgTypes(); + if (t0a.size() != t1a.size()) { - // incomparable, not subtype + // different arities return false; } - return getRangeType().isSubtypeOf(t.getRangeType()); + for (size_t i = 0, nargs = t0a.size(); i < nargs; i++) + { + if (t0a[i] != t1a[i]) + { + // an argument is different + return false; + } + } + return true; } // this should only return true for types T1, T2 where we handle equalities between T1 and T2 // (more cases go here, if we want to support such cases) @@ -307,18 +319,11 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { } bool TypeNode::isComparableTo(TypeNode t) const { - if(*this == t) { - return true; - } - if(isSubtypeOf(NodeManager::currentNM()->realType())) { - return t.isSubtypeOf(NodeManager::currentNM()->realType()); - } - if (isFunction() && t.isFunction()) + if (*this == t) { - // comparable if they have a common type node - return !leastCommonTypeNode(*this, t).isNull(); + return true; } - return false; + return isSubtypeOf(t) || t.isSubtypeOf(*this); } TypeNode TypeNode::getDatatypeTesterDomainType() const @@ -486,102 +491,19 @@ bool TypeNode::isParameterInstantiatedDatatype(size_t n) const } TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ - return commonTypeNode( t0, t1, true ); -} - -TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ - return commonTypeNode( t0, t1, false ); -} - -TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { - Assert(!t0.isNull()); - Assert(!t1.isNull()); - - if(__builtin_expect( (t0 == t1), true )) { + if (t0 == t1) + { return t0; } - - // t0 != t1 && - if(t0.getKind() == kind::TYPE_CONSTANT) { - switch(t0.getConst()) { - case INTEGER_TYPE: - if(t1.isInteger()) { - // t0 == IntegerType && t1.isInteger() - return t0; //IntegerType - } else if(t1.isReal()) { - // t0 == IntegerType && t1.isReal() && !t1.isInteger() - return isLeast ? t1 : t0; // RealType - } else { - return TypeNode(); // null type - } - case REAL_TYPE: - if(t1.isReal()) { - return isLeast ? t0 : t1; // RealType - } else { - return TypeNode(); // null type - } - default: - return TypeNode(); // null type - } - } else if(t1.getKind() == kind::TYPE_CONSTANT) { - return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases + if (t0.isSubtypeOf(t1)) + { + return t1; } - - // t0 != t1 && - // t0.getKind() == kind::TYPE_CONSTANT && - // t1.getKind() == kind::TYPE_CONSTANT - switch(t0.getKind()) { - case kind::FUNCTION_TYPE: - { - if (t1.getKind() != kind::FUNCTION_TYPE) - { - return TypeNode(); - } - // must have equal arguments - std::vector t0a = t0.getArgTypes(); - std::vector t1a = t1.getArgTypes(); - if (t0a.size() != t1a.size()) - { - // different arities - return TypeNode(); - } - for (unsigned i = 0, nargs = t0a.size(); i < nargs; i++) - { - if (t0a[i] != t1a[i]) - { - // an argument is different - return TypeNode(); - } - } - TypeNode t0r = t0.getRangeType(); - TypeNode t1r = t1.getRangeType(); - TypeNode tr = commonTypeNode(t0r, t1r, isLeast); - std::vector ftypes; - ftypes.insert(ftypes.end(), t0a.begin(), t0a.end()); - ftypes.push_back(tr); - return NodeManager::currentNM()->mkFunctionType(ftypes); - } - break; - case kind::BITVECTOR_TYPE: - case kind::FLOATINGPOINT_TYPE: - case kind::SORT_TYPE: - case kind::CONSTRUCTOR_TYPE: - case kind::SELECTOR_TYPE: - case kind::TESTER_TYPE: - case kind::ARRAY_TYPE: - case kind::DATATYPE_TYPE: - case kind::PARAMETRIC_DATATYPE: - case kind::SEQUENCE_TYPE: - case kind::SET_TYPE: - case kind::BAG_TYPE: - { - // we don't support subtyping except for built in types Int and Real. - return TypeNode(); // return null type - } - default: - Unimplemented() << "don't have a commonType for types `" << t0 - << "' and `" << t1 << "'"; + else if (t1.isSubtypeOf(t0)) + { + return t0; } + return TypeNode(); } /** Is this a sort kind */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9e1994729..314935da8 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -697,10 +697,8 @@ private: * a TypeNode such that isNull() is true is returned. */ static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); - static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); private: - static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); /** * Indents the given stream a given amount of spaces. diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ff68f19ec..6ac904ed0 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -198,8 +198,6 @@ void TheorySetsPrivate::fullEffortReset() Assert(d_equalityEngine->consistent()); d_fullCheckIncomplete = false; d_fullCheckIncompleteId = IncompleteId::UNKNOWN; - d_most_common_type.clear(); - d_most_common_type_term.clear(); d_card_enabled = false; d_rels_enabled = false; // reset the state object @@ -227,19 +225,9 @@ void TheorySetsPrivate::fullEffortCheck() while (!eqcs_i.isFinished()) { Node eqc = (*eqcs_i); - bool isSet = false; TypeNode tn = eqc.getType(); d_state.registerEqc(tn, eqc); eqcTypeCount[tn]++; - // common type node and term - TypeNode tnc; - Node tnct; - if (tn.isSet()) - { - isSet = true; - tnc = tn.getSetElementType(); - tnct = eqc; - } Trace("sets-eqc") << "[" << eqc << "] : "; eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine); while (!eqc_i.isFinished()) @@ -257,18 +245,6 @@ void TheorySetsPrivate::fullEffortCheck() } } TypeNode tnn = n.getType(); - if (isSet) - { - Assert(tnn.isSet()); - TypeNode tnnel = tnn.getSetElementType(); - tnc = TypeNode::mostCommonTypeNode(tnc, tnnel); - Assert(!tnc.isNull()); - // update the common type term - if (tnc == tnnel) - { - tnct = n; - } - } // register it with the state d_state.registerTerm(eqc, tnn, n); Kind nk = n.getKind(); @@ -312,12 +288,6 @@ void TheorySetsPrivate::fullEffortCheck() } ++eqc_i; } - if (isSet) - { - Assert(tnct.getType().getSetElementType() == tnc); - d_most_common_type[eqc] = tnc; - d_most_common_type_term[eqc] = tnct; - } Trace("sets-eqc") << std::endl; ++eqcs_i; } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index bfdf7a5c0..2a89b7933 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -119,8 +119,6 @@ class TheorySetsPrivate : protected EnvObj bool d_fullCheckIncomplete; /** The reason we set the above flag to true */ IncompleteId d_fullCheckIncompleteId; - std::map< Node, TypeNode > d_most_common_type; - std::map< Node, Node > d_most_common_type_term; public: