From: Andrew Reynolds Date: Wed, 18 May 2022 06:01:20 +0000 (-0500) Subject: Eliminate subtypes (#8783) X-Git-Tag: cvc5-1.0.1~119 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d886ae8bb345dae281b95ec152aee2106137831;p=cvc5.git Eliminate subtypes (#8783) --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1bbc1bede..35be11a64 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -6303,11 +6303,7 @@ Term Solver::defineFun(const std::string& symbol, CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort); CVC5_API_SOLVER_CHECK_TERM(term); - // We are permissive with subtypes so that integers are allowed to define - // the body of a function whose codomain is real. This is to accomodate - // SMT-LIB inputs in the Reals theory, where NUMERAL can be used to specify - // reals. Instead of making our parser for numerals dependent on the logic, - // we instead allow integers here in this case. + // the sort of the body must match the return sort CVC5_API_CHECK(term.d_node->getType() == *sort.d_type) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -6352,7 +6348,6 @@ Term Solver::defineFunRec(const std::string& symbol, CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort); - // we are permissive with subtypes, similar to defineFun CVC5_API_CHECK(term.d_node->getType() == *sort.d_type) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -6402,7 +6397,6 @@ Term Solver::defineFunRec(const Term& fun, std::vector domain_sorts = fun.getSort().getFunctionDomainSorts(); CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts); Sort codomain = fun.getSort().getFunctionCodomainSort(); - // we are permissive with subtypes, similar to defineFun CVC5_API_CHECK(*codomain.d_type == term.d_node->getType()) << "Invalid sort of function body '" << term << "', expected '" << codomain << "'"; diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp index fe3a54c45..446997898 100644 --- a/src/expr/match_trie.cpp +++ b/src/expr/match_trie.cpp @@ -129,7 +129,7 @@ bool MatchTrie::getMatches(Node n, NotifyMatch* ntm) recurse = false; } } - else if (!var.getType().isSubtypeOf(cn.getType())) + else if (var.getType() != cn.getType()) { recurse = false; } diff --git a/src/expr/nary_match_trie.cpp b/src/expr/nary_match_trie.cpp index d094c3dd3..ce8f420ed 100644 --- a/src/expr/nary_match_trie.cpp +++ b/src/expr/nary_match_trie.cpp @@ -165,8 +165,8 @@ bool NaryMatchTrie::getMatches(Node n, NotifyMatch* ntm) const { currChildren.push_back(next); syms.pop_back(); - // check subtyping in the (non-list) case - if (!var.getType().isSubtypeOf(next.getType())) + // check types in the (non-list) case + if (var.getType() != next.getType()) { next = Node::null(); } diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 212f1feb3..27d34e332 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -800,7 +800,7 @@ bool match(Node x, Node y, std::unordered_map& subs) visited.insert(curr); if (curr.first.getNumChildren() == 0) { - if (!curr.first.getType().isComparableTo(curr.second.getType())) + if (curr.first.getType() != curr.second.getType()) { // the two subterms have different types return false; diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index cebff11c5..130308730 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -71,7 +71,7 @@ void Subs::add(const std::vector& vs) void Subs::add(const Node& v, const Node& s) { - Assert(s.isNull() || v.getType().isComparableTo(s.getType())); + Assert(s.isNull() || v.getType() == s.getType()); d_vars.push_back(v); d_subs.push_back(s); } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 4afbd04aa..350ea6968 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -273,58 +273,22 @@ bool TypeNode::isWellFounded() const { return kind::isWellFounded(*this); } -bool TypeNode::isStringLike() const { return isString() || isSequence(); } - -// !!! Note that this will change to isReal() || isInteger() when subtyping is -// eliminated -bool TypeNode::isRealOrInt() const { return isReal(); } - -bool TypeNode::isSubtypeOf(TypeNode t) const { - if(*this == t) { - return true; - } - if (isInteger()) - { - return t.isReal(); - } - if (isFunction() && t.isFunction()) - { - 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()) - { - // different arities - return false; - } - 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) - return false; +bool TypeNode::isInteger() const +{ + return getKind() == kind::TYPE_CONSTANT + && getConst() == INTEGER_TYPE; } -bool TypeNode::isComparableTo(TypeNode t) const { - if (*this == t) - { - return true; - } - return isSubtypeOf(t) || t.isSubtypeOf(*this); +bool TypeNode::isReal() const +{ + return getKind() == kind::TYPE_CONSTANT + && getConst() == REAL_TYPE; } +bool TypeNode::isStringLike() const { return isString() || isSequence(); } + +bool TypeNode::isRealOrInt() const { return isReal() || isInteger(); } + TypeNode TypeNode::getDatatypeTesterDomainType() const { Assert(isDatatypeTester()); @@ -483,22 +447,6 @@ bool TypeNode::isParameterInstantiatedDatatype(size_t n) const return dt.getParameter(n) != (*this)[n + 1]; } -TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ - if (t0 == t1) - { - return t0; - } - if (t0.isSubtypeOf(t1)) - { - return t1; - } - else if (t1.isSubtypeOf(t0)) - { - return t0; - } - return TypeNode(); -} - /** Is this a sort kind */ bool TypeNode::isUninterpretedSort() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d20ad0bc2..db46fc71e 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -432,17 +432,6 @@ private: */ bool isWellFounded() const; - /** - * Is this type a subtype of the given type? - */ - bool isSubtypeOf(TypeNode t) const; - - /** - * Is this type comparable to the given type (i.e., do they share - * a common ancestor in the subtype tree)? - */ - bool isComparableTo(TypeNode t) const; - /** Is this the Boolean type? */ bool isBoolean() const; @@ -688,13 +677,6 @@ private: */ TypeNode getUninterpretedSortConstructor() const; - /** - * Returns the leastUpperBound in the extended type lattice of the two types. - * If this is \top, i.e. there is no inhabited type that contains both, - * a TypeNode such that isNull() is true is returned. - */ - static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); - private: /** @@ -874,17 +856,6 @@ inline bool TypeNode::isBoolean() const { ( getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE ); } -inline bool TypeNode::isInteger() const { - return - ( getKind() == kind::TYPE_CONSTANT && getConst() == INTEGER_TYPE ); -} - -inline bool TypeNode::isReal() const { - return - ( getKind() == kind::TYPE_CONSTANT && getConst() == REAL_TYPE ) || - isInteger(); -} - inline bool TypeNode::isString() const { return getKind() == kind::TYPE_CONSTANT && getConst() == STRING_TYPE; diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 3b80d9f88..e8ec68b88 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -49,7 +49,8 @@ bool childrenTypesChanged(Node n, NodeMap& cache) { for (Node child : n) { TypeNode originalType = child.getType(); TypeNode newType = cache[child].getType(); - if (! newType.isSubtypeOf(originalType)) { + if (newType != originalType) + { return true; } } diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 3f2a9d9ed..a3e09aafe 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -255,7 +255,7 @@ void UnconstrainedSimplifier::processUnconstrained() if (parent[0].getType() != parent[1].getType()) { TNode other = (parent[0] == current) ? parent[1] : parent[0]; - if (current.getType().isSubtypeOf(other.getType())) + if (current.getType() == other.getType()) { break; } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 6c7b3d419..d0b0ccb87 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -499,7 +499,7 @@ void SolverEngine::debugCheckFunctionBody(Node formula, if (formals.size() > 0) { TypeNode rangeType = funcType.getRangeType(); - if (!formulaType.isComparableTo(rangeType)) + if (formulaType != rangeType) { stringstream ss; ss << "Type of defined function does not match its declaration\n" @@ -512,7 +512,7 @@ void SolverEngine::debugCheckFunctionBody(Node formula, } else { - if (!formulaType.isComparableTo(funcType)) + if (formulaType != funcType) { stringstream ss; ss << "Declared type of defined constant does not match its definition\n" @@ -1043,10 +1043,7 @@ Node SolverEngine::getValue(const Node& ex) const Trace("smt") << "--- expected type " << expectedType << endl; // type-check the result we got - // Notice that lambdas have function type, which does not respect the subtype - // relation, so we ignore them here. - Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA - || resultNode.getType().isSubtypeOf(expectedType)) + Assert(resultNode.isNull() || resultNode.getType() == expectedType) << "Run with -t smt for details."; // Ensure it's a value (constant or const-ish like real algebraic diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index a9ef66b03..5b302369a 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -109,7 +109,7 @@ parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root p operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" -operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real)" +operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term)" typerule ADD ::cvc5::internal::theory::arith::ArithOperatorTypeRule typerule MULT ::cvc5::internal::theory::arith::ArithOperatorTypeRule diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index f2e6a5dd7..4dcade099 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -325,8 +325,8 @@ bool NlModel::addSubstitution(TNode v, TNode s) bool NlModel::addBound(TNode v, TNode l, TNode u) { - Assert(l.getType().isSubtypeOf(v.getType())); - Assert(u.getType().isSubtypeOf(v.getType())); + Assert(l.getType() == v.getType()); + Assert(u.getType() == v.getType()); Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " " << u << "]" << std::endl; if (l == u) @@ -467,7 +467,7 @@ bool NlModel::solveEqualitySimple(Node eq, // We also ensure types are correct here, which avoids substituting // a term of non-integer type for a variable of integer type. if (veqc.isNull() && !expr::hasSubterm(slv, uv) - && slv.getType().isSubtypeOf(uv.getType())) + && slv.getType() == uv.getType()) { Trace("nl-ext-cm") << "check-model-subs : " << uv << " -> " << slv << std::endl; diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 14987fbfe..c5853de6b 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -65,12 +65,12 @@ TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager, } TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); - if (!indexType.isSubtypeOf(arrayType.getArrayIndexType())) + if (indexType != arrayType.getArrayIndexType()) { throw TypeCheckingExceptionPrivate( n, "array store not indexed with correct type for array"); } - if (!valueType.isSubtypeOf(arrayType.getArrayConstituentType())) + if (valueType != arrayType.getArrayConstituentType()) { Trace("array-types") << "array type: " << arrayType.getArrayConstituentType() @@ -306,12 +306,12 @@ TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager, TypeNode indexType = n0_type.getArrayIndexType(); TypeNode indexRangeType1 = n[2].getType(check); TypeNode indexRangeType2 = n[3].getType(check); - if (!indexRangeType1.isSubtypeOf(indexType)) + if (indexRangeType1 != indexType) { throw TypeCheckingExceptionPrivate( n, "eqrange lower index type does not match array index type"); } - if (!indexRangeType2.isSubtypeOf(indexType)) + if (indexRangeType2 != indexType) { throw TypeCheckingExceptionPrivate( n, "eqrange upper index type does not match array index type"); diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 1379b1ef8..0987bccfc 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -900,8 +900,8 @@ Node BagsUtils::constructProductTuple(TNode n, TNode e1, TNode e2) Node B = n[1]; TypeNode typeA = A.getType().getBagElementType(); TypeNode typeB = B.getType().getBagElementType(); - Assert(e1.getType().isSubtypeOf(typeA)); - Assert(e2.getType().isSubtypeOf(typeB)); + Assert(e1.getType() == typeA); + Assert(e2.getType() == typeB); TypeNode productTupleType = n.getType().getBagElementType(); Node tuple = TupleUtils::concatTuples(productTupleType, e1, e2); diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 715c32662..8d8ee22c5 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -73,7 +73,7 @@ void InferenceGenerator::registerCardinalityTerm(Node n) InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e) { Assert(n.getType().isBag()); - Assert(e.getType().isSubtypeOf(n.getType().getBagElementType())); + Assert(e.getType() == n.getType().getBagElementType()); InferInfo inferInfo(d_im, InferenceId::BAGS_NON_NEGATIVE_COUNT); Node count = d_nm->mkNode(BAG_COUNT, e, n); @@ -114,7 +114,7 @@ InferInfo InferenceGenerator::bagMake(Node n) InferInfo InferenceGenerator::bagMake(Node n, Node e) { Assert(n.getKind() == BAG_MAKE); - Assert(e.getType().isSubtypeOf(n.getType().getBagElementType())); + Assert(e.getType() == n.getType().getBagElementType()); /* * (ite (and (= e x) (>= c 1)) @@ -191,7 +191,7 @@ Node InferenceGenerator::registerAndAssertSkolemLemma(Node& n, InferInfo InferenceGenerator::empty(Node n, Node e) { Assert(n.getKind() == BAG_EMPTY); - Assert(e.getType().isSubtypeOf(n.getType().getBagElementType())); + Assert(e.getType() == n.getType().getBagElementType()); InferInfo inferInfo(d_im, InferenceId::BAGS_EMPTY); Node skolem = registerAndAssertSkolemLemma(n, "skolem_bag"); @@ -205,7 +205,7 @@ InferInfo InferenceGenerator::empty(Node n, Node e) InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) { Assert(n.getKind() == BAG_UNION_DISJOINT && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -227,7 +227,7 @@ InferInfo InferenceGenerator::unionDisjoint(Node n, Node e) InferInfo InferenceGenerator::unionMax(Node n, Node e) { Assert(n.getKind() == BAG_UNION_MAX && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -250,7 +250,7 @@ InferInfo InferenceGenerator::unionMax(Node n, Node e) InferInfo InferenceGenerator::intersection(Node n, Node e) { Assert(n.getKind() == BAG_INTER_MIN && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -271,7 +271,7 @@ InferInfo InferenceGenerator::intersection(Node n, Node e) InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) { Assert(n.getKind() == BAG_DIFFERENCE_SUBTRACT && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -293,7 +293,7 @@ InferInfo InferenceGenerator::differenceSubtract(Node n, Node e) InferInfo InferenceGenerator::differenceRemove(Node n, Node e) { Assert(n.getKind() == BAG_DIFFERENCE_REMOVE && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -315,7 +315,7 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e) InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e) { Assert(n.getKind() == BAG_DUPLICATE_REMOVAL && n[0].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[0].getType().getBagElementType())); + Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL); @@ -536,7 +536,7 @@ InferInfo InferenceGenerator::mapUp( InferInfo InferenceGenerator::filterDownwards(Node n, Node e) { Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType())); + Assert(e.getType() == n[1].getType().getBagElementType()); Node P = n[0]; Node A = n[1]; @@ -558,7 +558,7 @@ InferInfo InferenceGenerator::filterDownwards(Node n, Node e) InferInfo InferenceGenerator::filterUpwards(Node n, Node e) { Assert(n.getKind() == BAG_FILTER && n[1].getType().isBag()); - Assert(e.getType().isSubtypeOf(n[1].getType().getBagElementType())); + Assert(e.getType() == n[1].getType().getBagElementType()); Node P = n[0]; Node A = n[1]; @@ -606,7 +606,7 @@ InferInfo InferenceGenerator::productUp(Node n, Node e1, Node e2) InferInfo InferenceGenerator::productDown(Node n, Node e) { Assert(n.getKind() == TABLE_PRODUCT); - Assert(e.getType().isSubtypeOf(n.getType().getBagElementType())); + Assert(e.getType() == n.getType().getBagElementType()); Node A = n[0]; Node B = n[1]; @@ -676,7 +676,7 @@ InferInfo InferenceGenerator::joinUp(Node n, Node e1, Node e2) InferInfo InferenceGenerator::joinDown(Node n, Node e) { Assert(n.getKind() == TABLE_JOIN); - Assert(e.getType().isSubtypeOf(n.getType().getBagElementType())); + Assert(e.getType() == n.getType().getBagElementType()); Node A = n[0]; Node B = n[1]; diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 1bfd6fc17..f57fc1206 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -43,7 +43,7 @@ void SolverState::registerBag(TNode n) void SolverState::registerCountTerm(Node bag, Node element, Node skolem) { Assert(bag.getType().isBag() && bag == getRepresentative(bag)); - Assert(element.getType().isSubtypeOf(bag.getType().getBagElementType()) + Assert(element.getType() == bag.getType().getBagElementType() && element == getRepresentative(element)); Assert(skolem.isVar() && skolem.getType().isInteger()); std::pair pair = std::make_pair(element, skolem); diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 9c9178514..94614b00a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -90,10 +90,10 @@ Node TheoryBuiltinRewriter::rewriteWitness(TNode node) Trace("builtin-rewrite") << "Witness rewrite: " << node << " --> " << node[1][1 - i] << std::endl; // also must be a legal elimination: the other side of the equality - // cannot contain the variable, and it must be a subtype of the + // cannot contain the variable, and it must be the same type as the // variable if (!expr::hasSubterm(node[1][1 - i], node[0][0]) - && node[1][i].getType().isSubtypeOf(node[0][0].getType())) + && node[1][i].getType() == node[0][0].getType()) { return node[1][1 - i]; } diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp index 1c348a071..e4d990902 100644 --- a/src/theory/bv/int_blaster.cpp +++ b/src/theory/bv/int_blaster.cpp @@ -822,7 +822,7 @@ bool IntBlaster::childrenTypesChanged(Node n) { TypeNode originalType = child.getType(); TypeNode newType = d_intblastCache[child].get().getType(); - if (!newType.isSubtypeOf(originalType)) + if (newType != originalType) { result = true; break; @@ -836,7 +836,7 @@ Node IntBlaster::castToType(Node n, TypeNode tn) { // If there is no reason to cast, return the // original node. - if (n.getType().isSubtypeOf(tn)) + if (n.getType() == tn) { return n; } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 307e7cb61..3837e1d21 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -147,7 +147,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) Node ret = sygusToBuiltinEval(ev, args); Trace("dt-sygus-util") << "...got " << ret << "\n"; Trace("dt-sygus-util") << "Type is " << ret.getType() << std::endl; - Assert(in.getType().isComparableTo(ret.getType())); + Assert(in.getType() == ret.getType()); return RewriteResponse(REWRITE_AGAIN_FULL, ret); } } diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 5bc715c2f..de7e08d37 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -989,7 +989,7 @@ Node SygusExtension::registerSearchValue(Node a, bool isVarAgnostic, bool doSym) { - Assert(n.getType().isComparableTo(nv.getType())); + Assert(n.getType() == nv.getType()); TypeNode tn = n.getType(); if (!tn.isDatatype()) { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 0696edc4e..61cbeb6f6 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -126,11 +126,10 @@ class DtSygusEvalTypeRule * - The head is a datatype T, * - The remaining children are either MATCH_BIND_CASE or MATCH_CASE, * - The patterns for the cases are over the same datatype as the head term, - * - The return types for the cases are comparable, + * - The return types for the cases are the same, * - The patterns specified by the children are exhaustive for T. * - * The type rule returns the (least common subtype) of the return types of the - * cases. + * The type rule returns the return type of the cases. */ class MatchTypeRule { diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 96b5468d8..3bcd9d1ce 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -245,7 +245,7 @@ bool CandidateRewriteFilter::notify(Node s, { // By using internal representation of terms, we ensure polymorphism is // handled correctly. - Assert(vars[i].getType().isComparableTo(subs[i].getType())); + Assert(vars[i].getType() == subs[i].getType()); } #endif // must convert the inferred substitution to original form diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 6d0f41aa1..f49bfc035 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1092,7 +1092,7 @@ bool CegInstantiator::doAddInstantiation(std::vector& vars, Node n = it->second; Trace("cegqi-inst-debug") << " " << d_input_vars[i] << " -> " << n << std::endl; - Assert(n.getType().isComparableTo(d_input_vars[i].getType())); + Assert(n.getType() == d_input_vars[i].getType()); subs.push_back( n ); } } @@ -1104,7 +1104,7 @@ bool CegInstantiator::doAddInstantiation(std::vector& vars, Node v = d_input_vars[i]; Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : " << v << " -> " << subs[i] << std::endl; - Assert(subs[i].getType().isComparableTo(v.getType())); + Assert(subs[i].getType() == v.getType()); } } Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl; @@ -1153,7 +1153,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; for( unsigned i=0; i " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; - Assert(subs[i].getType().isSubtypeOf(vars[i].getType())); + Assert(subs[i].getType() == vars[i].getType()); } } Node nret; @@ -1233,7 +1233,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node v = msum_term[it->first]; if (!v.isNull()) { - Assert(v.getType().isComparableTo(type)); + Assert(v.getType() == type); c = nm->mkNode(MULT, c, v); } children.push_back( c ); diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index ca092c4fa..9e0a4597d 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -177,8 +177,7 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ Node n = (*d_eqc_false); ++d_eqc_false; if( n.getKind()==d_match_pattern.getKind() ){ - if (n[0].getType().isComparableTo(d_match_pattern_type) - && isLegalCandidate(n)) + if (n[0].getType() == d_match_pattern_type && isLegalCandidate(n)) { //found an iff or equality, try to match it //DO_THIS: cache to avoid redundancies? @@ -212,7 +211,8 @@ Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ TNode n = (*d_eq); ++d_eq; - if( n.getType().isComparableTo( d_match_pattern_type ) ){ + if (n.getType() == d_match_pattern_type) + { TNode nh = tdb->getEligibleTermInEqc(n); if( !nh.isNull() ){ if (options::instMaxLevel() != -1) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index c3d3e17c0..88db6ff31 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -519,7 +519,7 @@ int InstMatchGenerator::getNextMatch(InstMatch& m) //if t not null, try to fit it into match m if( !t.isNull() ){ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){ - Assert(t.getType().isComparableTo(d_match_pattern_type)); + Assert(t.getType() == d_match_pattern_type); Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl; success = getMatch(t, m); if( d_independent_gen && success<0 ){ diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index dd22f9a06..a8ec669fb 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -166,7 +166,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, { Node t = tt.first; // using representatives, just check if equal - Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex])); + Assert(t.getType() == d_match_pattern_arg_types[argIndex]); bool wasSet = !m.get(v).isNull(); if (!m.set(v, t)) { diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 81a980046..8ac8239fe 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -57,7 +57,6 @@ int VarMatchGeneratorTermSubs::getNextMatch(InstMatch& m) Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; d_eq_class = Node::null(); - // if( s.getType().isSubtypeOf( d_var_type ) ){ d_rm_prev = m.get(index).isNull(); if (!m.set(index, s)) { diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 917633234..475f1e619 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -128,7 +128,7 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << " and type " << r_best.getType() << std::endl; - Assert(r_best.getType().isSubtypeOf(v_tn)); + Assert(r_best.getType() == v_tn); v_int_rep[r] = r_best; if (TraceIsOn("internal-rep-debug")) { @@ -172,7 +172,7 @@ int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) { // reject return -2; } - else if (!n.getType().isSubtypeOf(v_tn)) + else if (n.getType() != v_tn) { // reject if incorrect type return -2; } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 7ca9f6965..336f8b99a 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -73,7 +73,7 @@ class FirstOrderModel : protected EnvObj * Choose a term that is equivalent to a in the current context that is the * best term for instantiating the index^th variable of quantified formula q. * If no legal term can be found, we return null. This can occur if: - * - a's type is not a subtype of the type of the index^th variable of q, + * - a's type is not the type of the index^th variable of q, * - a is in an equivalent class with all terms that are restricted not to * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample * guided instantiation. diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index bc0b2ba97..842357f68 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -760,7 +760,6 @@ Node Instantiate::ensureType(Node n, TypeNode tn) { Trace("inst-add-debug2") << "Ensure " << n << " : " << tn << std::endl; TypeNode ntn = n.getType(); - Assert(ntn.isComparableTo(tn)); if (ntn == tn) { return n; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c677d744a..7df5caf92 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1946,7 +1946,7 @@ bool MatchGen::doMatching() { d_qni.push_back(it); // set the match - if (it->first.getType().isComparableTo(d_qi->d_var_types[repVar]) + if (it->first.getType() == d_qi->d_var_types[repVar] && d_qi->setMatch(d_qni_bound[index], it->first, true, true)) { Trace("qcf-match-debug") diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp index df82df96b..e9e55c4c2 100644 --- a/src/theory/quantifiers/quantifiers_macros.cpp +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -274,7 +274,7 @@ Node QuantifiersMacros::solveEq(Node n, Node ndef) } TNode op = n.getOperator(); TNode fdeft = fdef; - Assert(op.getType().isComparableTo(fdef.getType())); + Assert(op.getType() == fdef.getType()); return op.eqNode(fdef); } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 5c5cbf4d0..55ed145cf 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -835,7 +835,7 @@ Node QuantifiersRewriter::computeCondSplit(Node body, bool QuantifiersRewriter::isVarElim(Node v, Node s) { Assert(v.getKind() == BOUND_VARIABLE); - return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); + return !expr::hasSubterm(s, v) && s.getType() == v.getType(); } Node QuantifiersRewriter::getVarElimEq(Node lit, @@ -1124,7 +1124,7 @@ bool QuantifiersRewriter::getVarElimLit(Node body, << "Variable eliminate based on theory-specific solving : " << var << " -> " << slv << std::endl; Assert(!expr::hasSubterm(slv, var)); - Assert(slv.getType().isSubtypeOf(var.getType())); + Assert(slv.getType() == var.getType()); vars.push_back(var); subs.push_back(slv); args.erase(ita); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 278eef1a9..7263ece48 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -81,7 +81,7 @@ class QuantifiersRewriter : public TheoryRewriter //-------------------------------------variable elimination utilities /** is variable elimination * - * Returns true if v is not a subterm of s, and the type of s is a subtype of + * Returns true if v is not a subterm of s, and the type of s is the same as * the type of v. */ static bool isVarElim(Node v, Node s); diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index a3ed6d8a3..fc1e6b549 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -173,7 +173,7 @@ void RelevantDomain::compute(){ TypeNode expectedType = d.first[0][dd.first].getType(); for (const Node& t : r->d_terms) { - if (!t.getType().isComparableTo(expectedType)) + if (t.getType() != expectedType) { Unhandled() << "Relevant domain: bad type " << t.getType() << ", expected " << expectedType; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 5a88b218b..ac1445761 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -608,7 +608,7 @@ bool Cegis::checkRefinementEvalLemmas(const std::vector& vs, for (unsigned j = 0, psize = vsProc.size(); j < psize; j++) { evalVisited[vsProc[j]] = msProc[j]; - Assert(vsProc[j].getType().isComparableTo(msProc[j].getType())); + Assert(vsProc[j].getType() == msProc[j].getType()); } } } diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index b39a98a8a..0cef62892 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -51,7 +51,7 @@ void EnumStreamPermutation::reset(Node value) TypeNode tn = value.getType(); Node var_list = tn.getDType().getSygusVarList(); NodeManager* nm = NodeManager::currentNM(); - // get subtypes in value's type + // get subfield types in value's type SygusTypeInfo& ti = d_tds->getTypeInfo(tn); std::vector sf_types; ti.getSubfieldTypes(sf_types); @@ -59,7 +59,7 @@ void EnumStreamPermutation::reset(Node value) std::map cons_var; for (const Node& v : var_list) { - // collect constructors for variable in all subtypes + // collect constructors for variable in all subfield types for (const TypeNode& stn : sf_types) { const DType& dt = stn.getDType(); @@ -337,7 +337,7 @@ void EnumStreamSubstitution::initialize(TypeNode tn) d_tn = tn; // get variables in value's type Node var_list = tn.getDType().getSygusVarList(); - // get subtypes in value's type + // get subfield types in value's type NodeManager* nm = NodeManager::currentNM(); SygusTypeInfo& ti = d_tds->getTypeInfo(tn); std::vector sf_types; @@ -345,7 +345,7 @@ void EnumStreamSubstitution::initialize(TypeNode tn) // associate variables with constructors in all subfield types for (const Node& v : var_list) { - // collect constructors for variable in all subtypes + // collect constructors for variable in all subfield types for (const TypeNode& stn : sf_types) { const DType& dt = stn.getDType(); diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index 59fe30450..667d73a5e 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.cpp +++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp @@ -57,7 +57,7 @@ Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv) { clearEvaluationCache(bv); } - Assert(ret.getType().isComparableTo(bv.getType())); + Assert(ret.getType() == bv.getType()); return ret; } diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 83b4fca5e..5283eeba9 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -131,7 +131,7 @@ void SygusExplain::getExplanationForEquality(Node n, { // since builtin types occur in grammar, types are comparable but not // necessarily equal - Assert(n.getType().isComparableTo(n.getType())); + Assert(n.getType() == vn.getType()); if (n == vn) { return; @@ -189,7 +189,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, int& sz) { Assert(vnr.isNull() || vn != vnr); - Assert(n.getType().isComparableTo(vn.getType())); + Assert(n.getType() == vn.getType()); TypeNode ntn = n.getType(); if (!ntn.isDatatype()) { diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index cc4d9e815..c088dcaf5 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -62,8 +62,7 @@ bool SynthConjectureProcessFun::checkMatch( ++it) { Assert(it->first < d_arg_vars.size()); - Assert( - it->second.getType().isComparableTo(d_arg_vars[it->first].getType())); + Assert(it->second.getType() == d_arg_vars[it->first].getType()); vars.push_back(d_arg_vars[it->first]); subs.push_back(it->second); } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 9a6740082..872ed64b5 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -953,12 +953,12 @@ bool SynthConjecture::getSynthSolutions( // since we don't have function subtyping, this assertion should only // check the return type Assert(fvar.getType().isFunction()); - Assert(fvar.getType().getRangeType().isComparableTo(bsol.getType())); + Assert(fvar.getType().getRangeType() == bsol.getType()); bsol = nm->mkNode(LAMBDA, bvl, bsol); } else { - Assert(fvar.getType().isComparableTo(bsol.getType())); + Assert(fvar.getType() == bsol.getType()); } // store in map smc[fvar] = bsol; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 2a5943317..732570141 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -160,7 +160,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) { Assert(tn.isDatatype()); Assert(tn.getDType().isSygus()); - Assert(tn.getDType().getSygusType().isComparableTo(c.getType())); + Assert(tn.getDType().getSygusType() == c.getType()); std::map::iterator it = d_proxy_vars[tn].find(c); if (it == d_proxy_vars[tn].end()) @@ -291,7 +291,7 @@ Node TermDbSygus::canonizeBuiltin(Node n, std::map& var_count) } Trace("sygus-db-canon") << " ...normalized " << n << " --> " << ret << std::endl; - Assert(ret.getType().isComparableTo(n.getType())); + Assert(ret.getType() == n.getType()); return ret; } @@ -308,7 +308,7 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) // if its a constant, we use the datatype utility version return datatypes::utils::sygusToBuiltin(n); } - Assert(n.getType().isComparableTo(tn)); + Assert(n.getType() == tn); if (!tn.isDatatype()) { return n; @@ -405,7 +405,7 @@ void TermDbSygus::registerEnumerator(Node e, Trace("sygus-db") << " registering symmetry breaking clauses..." << std::endl; // depending on if we are using symbolic constructors, introduce symmetry - // breaking lemma templates for each relevant subtype of the grammar + // breaking lemma templates for each relevant subfield type of the grammar SygusTypeInfo& eti = getTypeInfo(et); std::vector sf_types; eti.getSubfieldTypes(sf_types); diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 9d2f276f3..6fd10e9e6 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -171,7 +171,7 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) // terms, so the term created by mkGeneric will also be well-typed here. Node g = tds->mkGeneric(dt, i); TypeNode gtn = g.getType(); - AlwaysAssert(gtn.isSubtypeOf(btn)) + AlwaysAssert(gtn == btn) << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl << "Due to " << g << " of type " << gtn << std::endl; diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp index faa6d7b58..2148e9e38 100644 --- a/src/theory/quantifiers/term_pools.cpp +++ b/src/theory/quantifiers/term_pools.cpp @@ -84,7 +84,7 @@ void TermPools::registerPool(Node p, const std::vector& initValue) d.initialize(); for (const Node& i : initValue) { - Assert(i.getType().isComparableTo(p.getType().getSetElementType())); + Assert(i.getType() == p.getType().getSetElementType()); d.add(i); } } diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index cf5235f9c..9c914b9d8 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -298,7 +298,7 @@ void TermTupleEnumeratorBase::next(/*out*/ std::vector& terms) terms[variableIx] = t; Trace("inst-alg-rd") << t << " "; Assert(!t.isNull()); - Assert(t.getType().isComparableTo(d_quantifier[0][variableIx].getType())) + Assert(t.getType() == d_quantifier[0][variableIx].getType()) << "Bad type: " << t << " " << t.getType() << " " << d_quantifier[0][variableIx].getType(); } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index fb421a997..8656f741a 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -97,7 +97,7 @@ void RepSet::add( TypeNode tn, Node n ){ } } Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl; - Assert(n.getType().isSubtypeOf(tn)); + Assert(n.getType() == tn); d_tmap[ n ] = (int)d_type_reps[tn].size(); d_type_reps[tn].push_back( n ); } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d924c57e3..8e930bea6 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1103,8 +1103,8 @@ void TheorySep::ensureHeapTypesFor(Node atom) const TypeNode tn1 = atom[0].getType(); TypeNode tn2 = atom[1].getType(); // already declared, ensure compatible - if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref)) - || (!tn2.isNull() && !tn2.isComparableTo(d_type_data))) + if ((!tn1.isNull() && tn1 != d_type_ref) + || (!tn2.isNull() && tn2 != d_type_data)) { std::stringstream ss; ss << "ERROR: the separation logic heap type has already been set to " diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 6c23fe74c..52a333cc3 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -605,9 +605,12 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); // if no sort was inferred for this node, return original - if( tn.isNull() || tn.isComparableTo( old.getType() ) ){ + if (tn.isNull() || tn == old.getType()) + { return old; - }else if( old.isConst() ){ + } + else if (old.isConst()) + { //must make constant of type tn if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ std::stringstream ss; @@ -618,7 +621,9 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ "constant created during sort inference"); // use mkConst??? } return d_const_map[tn][ old ]; - }else if( old.getKind()==kind::BOUND_VARIABLE ){ + } + else if (old.getKind() == kind::BOUND_VARIABLE) + { std::stringstream ss; ss << "b_" << old; return nm->mkBoundVar(ss.str(), tn); @@ -714,7 +719,8 @@ Node SortInference::simplifyNode( }else if( n.getKind()==kind::EQUAL ){ TypeNode tn1 = children[0].getType(); TypeNode tn2 = children[1].getType(); - if( !tn1.isComparableTo( tn2 ) ){ + if (tn1 != tn2) + { Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl; Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; Assert(false); @@ -756,7 +762,7 @@ Node SortInference::simplifyNode( { TypeNode tn = children[i+1].getType(); TypeNode tna = getTypeForId( d_op_arg_types[op][i] ); - if (!tn.isSubtypeOf(tna)) + if (tn != tna) { Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl; Assert(false); diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 0e77034f0..08f0cee77 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -123,7 +123,7 @@ void BaseSolver::checkInit() { // (seq.unit x) = (seq.unit y) => x=y, or // (seq.unit x) = (seq.unit c) => x=c - Assert(s.getType().isComparableTo(t.getType())); + Assert(s.getType() == t.getType()); d_im.sendInference(exp, s.eqNode(t), InferenceId::STRINGS_UNIT_INJ); } } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index f46bb4aba..a32e9a4df 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2014,7 +2014,7 @@ void CoreSolver::processDeq(Node ni, Node nj) Assert(v.getKind() == SEQ_UNIT); vc = v[0]; } - Assert(u[0].getType().isComparableTo(vc.getType())); + Assert(u[0].getType() == vc.getType()); // if already disequal, we are done if (d_state.areDisequal(u[0], vc)) { diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp index 886995684..d25c41218 100644 --- a/src/theory/strings/eager_solver.cpp +++ b/src/theory/strings/eager_solver.cpp @@ -126,7 +126,7 @@ bool EagerSolver::checkForMergeConflict(Node a, EqcInfo* eb) { Assert(eb != nullptr && ea != nullptr); - Assert(a.getType().isComparableTo(b.getType())) + Assert(a.getType() == b.getType()) << "bad types for merge " << a << ", " << b; // usages of isRealOrInt are only due to subtyping, where seq.nth for // sequences of Real are merged to integer equivalence classes diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 165fedb51..5858af78e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -753,7 +753,7 @@ Node TheoryStrings::mkSkeletonFor(Node c) TypeNode etn = c.getType().getSequenceElementType(); for (const Node& snv : snvec) { - Assert(snv.getType().isSubtypeOf(etn)); + Assert(snv.getType() == etn); Node v = bvm->mkBoundVar(snv, etn); // use a skolem, not a bound variable Node kv = sm->mkPurifySkolem(v, "smv"); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 46f09cc9d..d5df7084a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -320,8 +320,10 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!val.getType().isSubtypeOf(x.getType())) + if (val.getType() != x.getType()) { + Assert(false) << "isLegalElimination for disequal typed terms " << x + << " -> " << val; return false; } if (!options().smt.produceModels || options().smt.modelVarElimUneval) diff --git a/src/theory/theory.h b/src/theory/theory.h index 45bd81296..1001db7ee 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -215,7 +215,7 @@ class Theory : protected EnvObj * * The following criteria imply that x -> val is *not* a legal elimination: * (1) If x is contained in val, - * (2) If the type of val is not a subtype of the type of x, + * (2) If the type of val is not the same as the type of x, * (3) If val contains an operator that cannot be evaluated, and * produceModels is true. For example, x -> sqrt(2) is not a legal * elimination if we are producing models. This is because we care about the diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 8d9f5c0d3..c29d89fde 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1167,7 +1167,7 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) Node n = *eqc_i; static int repCheckInstance = 0; ++repCheckInstance; - AlwaysAssert(rep.getType().isSubtypeOf(n.getType())) + AlwaysAssert(rep.getType() == n.getType()) << "Representative " << rep << " of " << n << " violates type constraints (" << rep.getType() << " and " << n.getType() << ")"; @@ -1351,7 +1351,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) Node hni = m->getRepresentative(hn[1]); Trace("model-builder-debug2") << " get rep : " << hn[0] << " returned " << hni << std::endl; - Assert(hni.getType().isSubtypeOf(args[0].getType())); + Assert(hni.getType() == args[0].getType()); hni = rewrite(args[0].eqNode(hni)); Node hnv = m->getRepresentative(hn); Trace("model-builder-debug2") << " get rep val : " << hn @@ -1371,8 +1371,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) largs.begin(), largs.end(), apply_args.begin(), apply_args.end()); hnv = rewrite(hnv); } - Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType()) - .isNull()); + Assert(hnv.getType() == curr.getType()); curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr); } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 05f55e11b..d2f6b242f 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1233,7 +1233,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, if (!c1.isNull() && !c2.isNull()) { simpTrans = false; - Assert(c1.getType().isComparableTo(c2.getType())); + Assert(c1.getType() == c2.getType()); std::shared_ptr eqpmc = std::make_shared(); eqpmc->d_id = MERGED_THROUGH_CONSTANTS; eqpmc->d_node = c1.eqNode(c2).eqNode(d_false); diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp index 8167bcca0..27b39018a 100644 --- a/src/theory/uf/function_const.cpp +++ b/src/theory/uf/function_const.cpp @@ -79,11 +79,8 @@ Node FunctionConst::getLambdaForArrayRepresentationRec( a[2], bvl, bvlIndex + 1, visited); if (!val.isNull()) { - Assert(!TypeNode::leastCommonTypeNode(a[1].getType(), - bvl[bvlIndex].getType()) - .isNull()); - Assert(!TypeNode::leastCommonTypeNode(val.getType(), body.getType()) - .isNull()); + Assert(a[1].getType() == bvl[bvlIndex].getType()); + Assert(val.getType() == body.getType()); Node cond = bvl[bvlIndex].eqNode(a[1]); ret = NodeManager::currentNM()->mkNode(kind::ITE, cond, val, body); } @@ -369,7 +366,7 @@ Node FunctionConst::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())); + Assert(curr.getType() == array_type.getArrayConstituentType()); 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 @@ -382,7 +379,7 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n, for (size_t i = 0, numCond = conds.size(); i < numCond; i++) { size_t ii = (numCond - 1) - i; - Assert(conds[ii].getType().isSubtypeOf(first_arg.getType())); + Assert(conds[ii].getType() == first_arg.getType()); curr = nm->mkNode(kind::STORE, curr, conds[ii], vals[ii]); // normalize it using the array rewriter utility, which must be done at // each iteration of this loop diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 9a0a66a3f..f339a28d5 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -53,11 +53,11 @@ TypeNode UfTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) if (currentArgument != currentArgumentType) { std::stringstream ss; - ss << "argument type is not a subtype of the function's argument " + ss << "argument type is not the type of the function's argument " << "type:\n" << "argument: " << *argument_it << "\n" << "has type: " << (*argument_it).getType() << "\n" - << "not subtype: " << *argument_type_it << "\n" + << "not type: " << *argument_type_it << "\n" << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index b2ea12bb4..9a5f082e8 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -57,36 +57,6 @@ TEST_F(TestNodeWhiteTypeNode, sub_types) std::vector formals; formals.push_back(x); d_slvEngine->defineFunction(lambda, formals, xPos); - - ASSERT_FALSE(realType.isComparableTo(booleanType)); - ASSERT_TRUE(realType.isComparableTo(integerType)); - ASSERT_TRUE(realType.isComparableTo(realType)); - ASSERT_FALSE(realType.isComparableTo(arrayType)); - ASSERT_FALSE(realType.isComparableTo(bvType)); - - ASSERT_FALSE(booleanType.isComparableTo(integerType)); - ASSERT_FALSE(booleanType.isComparableTo(realType)); - ASSERT_TRUE(booleanType.isComparableTo(booleanType)); - ASSERT_FALSE(booleanType.isComparableTo(arrayType)); - ASSERT_FALSE(booleanType.isComparableTo(bvType)); - - ASSERT_TRUE(integerType.isComparableTo(realType)); - ASSERT_TRUE(integerType.isComparableTo(integerType)); - ASSERT_FALSE(integerType.isComparableTo(booleanType)); - ASSERT_FALSE(integerType.isComparableTo(arrayType)); - ASSERT_FALSE(integerType.isComparableTo(bvType)); - - ASSERT_FALSE(arrayType.isComparableTo(booleanType)); - ASSERT_FALSE(arrayType.isComparableTo(integerType)); - ASSERT_FALSE(arrayType.isComparableTo(realType)); - ASSERT_TRUE(arrayType.isComparableTo(arrayType)); - ASSERT_FALSE(arrayType.isComparableTo(bvType)); - - ASSERT_FALSE(bvType.isComparableTo(booleanType)); - ASSERT_FALSE(bvType.isComparableTo(integerType)); - ASSERT_FALSE(bvType.isComparableTo(realType)); - ASSERT_FALSE(bvType.isComparableTo(arrayType)); - ASSERT_TRUE(bvType.isComparableTo(bvType)); } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index d7a03364c..8c54a36a9 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -30,16 +30,6 @@ class TestTheoryWhiteSetsTypeRuleInternal : public TestNode { }; -TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to) -{ - TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType()); - TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType()); - ASSERT_FALSE(setIntType.isComparableTo(setRealType)); - ASSERT_FALSE(setIntType.isSubtypeOf(setRealType)); - ASSERT_FALSE(setRealType.isComparableTo(setIntType)); - ASSERT_FALSE(setRealType.isComparableTo(setIntType)); -} - TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term) { Sort realSort = d_solver.getRealSort(); diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index ad7ccc0f4..4182cecee 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -464,64 +464,6 @@ TEST_F(TestUtilBlackDatatype, parametric_DType) ASSERT_NE(pairIntInt, pairIntReal); ASSERT_NE(pairIntInt, pairRealInt); ASSERT_NE(pairIntReal, pairRealInt); - - ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal)); - ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal)); - ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal)); - ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal)); - ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt)); - ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt)); - ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt)); - ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt)); - ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal)); - ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal)); - ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal)); - ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal)); - ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt)); - ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt)); - ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt)); - ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt)); - - ASSERT_TRUE(pairRealReal.isSubtypeOf(pairRealReal)); - ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealReal)); - ASSERT_FALSE(pairRealInt.isSubtypeOf(pairRealReal)); - ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealReal)); - ASSERT_FALSE(pairRealReal.isSubtypeOf(pairRealInt)); - ASSERT_FALSE(pairIntReal.isSubtypeOf(pairRealInt)); - ASSERT_TRUE(pairRealInt.isSubtypeOf(pairRealInt)); - ASSERT_FALSE(pairIntInt.isSubtypeOf(pairRealInt)); - ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntReal)); - ASSERT_TRUE(pairIntReal.isSubtypeOf(pairIntReal)); - ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntReal)); - ASSERT_FALSE(pairIntInt.isSubtypeOf(pairIntReal)); - ASSERT_FALSE(pairRealReal.isSubtypeOf(pairIntInt)); - ASSERT_FALSE(pairIntReal.isSubtypeOf(pairIntInt)); - ASSERT_FALSE(pairRealInt.isSubtypeOf(pairIntInt)); - ASSERT_TRUE(pairIntInt.isSubtypeOf(pairIntInt)); - - ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealReal, pairRealReal), - pairRealReal); - ASSERT_TRUE( - TypeNode::leastCommonTypeNode(pairIntReal, pairRealReal).isNull()); - ASSERT_TRUE( - TypeNode::leastCommonTypeNode(pairRealInt, pairRealReal).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealReal).isNull()); - ASSERT_TRUE( - TypeNode::leastCommonTypeNode(pairRealReal, pairRealInt).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairRealInt).isNull()); - ASSERT_EQ(TypeNode::leastCommonTypeNode(pairRealInt, pairRealInt), - pairRealInt); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairRealInt).isNull()); - ASSERT_TRUE( - TypeNode::leastCommonTypeNode(pairRealReal, pairIntReal).isNull()); - ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntReal, pairIntReal), - pairIntReal); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntReal).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntInt, pairIntReal).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealReal, pairIntInt).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairIntReal, pairIntInt).isNull()); - ASSERT_TRUE(TypeNode::leastCommonTypeNode(pairRealInt, pairIntInt).isNull()); - ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt); } } // namespace test } // namespace cvc5::internal