From 1b55d831e0952a9260997414b713e05002bf4526 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 May 2022 14:37:28 -0500 Subject: [PATCH] Eliminate use of subtypes from remainder of type rules (#8756) This PR should be added before the minor release that advertises our policy change for subtyping. --- src/expr/type_matcher.cpp | 12 ++++----- src/printer/smt2/smt2_printer.cpp | 2 +- src/theory/arith/theory_arith_type_rules.cpp | 10 ++----- .../arrays/theory_arrays_type_rules.cpp | 6 ++--- src/theory/bags/theory_bags_type_rules.cpp | 24 +++++++---------- .../datatypes/theory_datatypes_type_rules.cpp | 27 +++++++------------ src/theory/sets/theory_sets_type_rules.cpp | 16 +++++------ .../strings/theory_strings_type_rules.cpp | 4 +-- src/theory/uf/theory_uf_type_rules.cpp | 2 +- 9 files changed, 40 insertions(+), 63 deletions(-) diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index bfcce31d7..c5257b7e1 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -75,15 +75,13 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn) if (!d_match[index].isNull()) { Trace("typecheck-idt") - << "check subtype " << tn << " " << d_match[index] << std::endl; - TypeNode tnn = TypeNode::leastCommonTypeNode(tn, d_match[index]); - // recognize subtype relation - if (!tnn.isNull()) + << "check types " << tn << " " << d_match[index] << std::endl; + if (tn != d_match[index]) { - d_match[index] = tnn; - return true; + return false; } - return false; + d_match[index] = tn; + return true; } d_match[index] = tn; return true; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8f879916f..49e0ed525 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -94,7 +94,7 @@ static void toStreamRational(std::ostream& out, } else { - Assert (isReal); + Assert(isReal); out << "(/ "; if (neg) { diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index b709e2d6a..b60a9b8b8 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -110,18 +110,12 @@ TypeNode ArithRelationTypeRule::computeType(NodeManager* nodeManager, if (check) { Assert(n.getNumChildren() == 2); - TypeNode t1 = n[0].getType(check); - if (!t1.isRealOrInt()) + if (!n[0].getType(check).isRealOrInt() + || !n[1].getType(check).isRealOrInt()) { throw TypeCheckingExceptionPrivate( n, "expecting an arithmetic term for arithmetic relation"); } - TypeNode t2 = n[1].getType(check); - if (!t1.isComparableTo(t2)) - { - throw TypeCheckingExceptionPrivate( - n, "expecting arithmetic terms of comparable type"); - } } return nodeManager->booleanType(); } diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index a5ec7e15c..14987fbfe 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -40,7 +40,7 @@ TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager, "array select operating on non-array"); } TypeNode indexType = n[1].getType(check); - if (!indexType.isSubtypeOf(arrayType.getArrayIndexType())) + if (indexType != arrayType.getArrayIndexType()) { throw TypeCheckingExceptionPrivate( n, "array select not indexed with correct type for array"); @@ -197,13 +197,13 @@ TypeNode ArrayTableFunTypeRule::computeType(NodeManager* nodeManager, "array table fun arg 1 is non-array"); } TypeNode indexType = n[2].getType(check); - if (!indexType.isComparableTo(arrayType.getArrayIndexType())) + if (indexType != arrayType.getArrayIndexType()) { throw TypeCheckingExceptionPrivate( n, "array table fun arg 2 does not match type of array"); } indexType = n[3].getType(check); - if (!indexType.isComparableTo(arrayType.getArrayIndexType())) + if (indexType != arrayType.getArrayIndexType()) { throw TypeCheckingExceptionPrivate( n, "array table fun arg 3 does not match type of array"); diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 5ca0f0815..4e3da85f5 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -88,11 +88,8 @@ TypeNode SubBagTypeRule::computeType(NodeManager* nodeManager, TypeNode secondBagType = n[1].getType(check); if (secondBagType != bagType) { - if (!bagType.isComparableTo(secondBagType)) - { - throw TypeCheckingExceptionPrivate( - n, "BAG_SUBBAG operating on bags of different types"); - } + throw TypeCheckingExceptionPrivate( + n, "BAG_SUBBAG operating on bags of different types"); } } return nodeManager->booleanType(); @@ -114,12 +111,12 @@ TypeNode CountTypeRule::computeType(NodeManager* nodeManager, TypeNode elementType = n[0].getType(check); // e.g. (bag.count 1 (bag (BagMakeOp Real) 1.0 3))) is 3 whereas // (bag.count 1.0 (bag (BagMakeOp Int) 1 3)) throws a typing error - if (!elementType.isSubtypeOf(bagType.getBagElementType())) + if (elementType != bagType.getBagElementType()) { std::stringstream ss; ss << "member operating on bags of different types:\n" << "child type: " << elementType << "\n" - << "not subtype: " << bagType.getBagElementType() << "\n" + << "not type: " << bagType.getBagElementType() << "\n" << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -143,12 +140,12 @@ TypeNode MemberTypeRule::computeType(NodeManager* nodeManager, TypeNode elementType = n[0].getType(check); // e.g. (bag.member 1 (bag 1.0 1)) is true whereas // (bag.member 1.0 (bag 1 1)) throws a typing error - if (!elementType.isSubtypeOf(bagType.getBagElementType())) + if (elementType != bagType.getBagElementType()) { std::stringstream ss; ss << "member operating on bags of different types:\n" << "child type: " << elementType << "\n" - << "not subtype: " << bagType.getBagElementType() << "\n" + << "not type: " << bagType.getBagElementType() << "\n" << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -201,11 +198,11 @@ TypeNode BagMakeTypeRule::computeType(NodeManager* nm, TNode n, bool check) TypeNode actualElementType = n[0].getType(check); // the type of the element should be a subtype of the type of the operator // e.g. (bag (bag_op Real) 1 1) where 1 is an Int - if (!actualElementType.isSubtypeOf(expectedElementType)) + if (actualElementType != expectedElementType) { std::stringstream ss; ss << "The type '" << actualElementType - << "' of the element is not a subtype of '" << expectedElementType + << "' of the element is not type of '" << expectedElementType << "' in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -486,9 +483,8 @@ TypeNode BagPartitionTypeRule::computeType(NodeManager* nodeManager, } std::vector argTypes = functionType.getArgTypes(); TypeNode rangeType = functionType.getRangeType(); - if (!(argTypes.size() == 2 && elementType.isSubtypeOf(argTypes[0]) - && elementType.isSubtypeOf(argTypes[1]) - && rangeType == nm->booleanType())) + if (!(argTypes.size() == 2 && elementType == argTypes[0] + && elementType == argTypes[1] && rangeType == nm->booleanType())) { std::stringstream ss; ss << "Operator " << n.getKind() << " expects a function of type (-> " diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 94aebbc63..1a8c62225 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -87,12 +87,12 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager, Trace("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; - if (!childType.isSubtypeOf(argumentType)) + if (childType != argumentType) { std::stringstream ss; ss << "bad type for constructor argument:\n" << "child type: " << childType << "\n" - << "not subtype: " << argumentType << "\n" + << "not type: " << argumentType << "\n" << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -161,7 +161,7 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager, Trace("typecheck-idt") << "typecheck sel: " << n << std::endl; Trace("typecheck-idt") << "sel type: " << selType << std::endl; TypeNode childType = n[0].getType(check); - if (!selType[0].isComparableTo(childType)) + if (selType[0] != childType) { Trace("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl; @@ -203,7 +203,7 @@ TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager, { Trace("typecheck-idt") << "typecheck test: " << n << std::endl; Trace("typecheck-idt") << "test type: " << testType << std::endl; - if (!testType[0].isComparableTo(childType)) + if (testType[0] != childType) { throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); } @@ -238,12 +238,9 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager, "matching failed for update argument of parameterized datatype"); } } - else + else if (targ != childType) { - if (!targ.isComparableTo(childType)) - { - throw TypeCheckingExceptionPrivate(n, "bad type for update argument"); - } + throw TypeCheckingExceptionPrivate(n, "bad type for update argument"); } } } @@ -368,7 +365,7 @@ TypeNode DtSygusEvalTypeRule::computeType(NodeManager* nodeManager, { TypeNode vtype = svl[i].getType(check); TypeNode atype = n[i + 1].getType(check); - if (!vtype.isComparableTo(atype)) + if (vtype != atype) { throw TypeCheckingExceptionPrivate( n, @@ -464,14 +461,10 @@ TypeNode MatchTypeRule::computeType(NodeManager* nodeManager, { retType = currType; } - else + else if (retType != currType) { - retType = TypeNode::leastCommonTypeNode(retType, currType); - if (retType.isNull()) - { - throw TypeCheckingExceptionPrivate( - n, "incomparable types in match case list"); - } + throw TypeCheckingExceptionPrivate( + n, "incomparable types in match case list"); } } // it is mandatory to check this here to ensure the match is exhaustive diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index f97f7c7fc..fe10f303a 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -78,11 +78,8 @@ TypeNode SubsetTypeRule::computeType(NodeManager* nodeManager, TypeNode secondSetType = n[1].getType(check); if (secondSetType != setType) { - if (!setType.isComparableTo(secondSetType)) - { - throw TypeCheckingExceptionPrivate( - n, "set subset operating on sets of different types"); - } + throw TypeCheckingExceptionPrivate( + n, "set subset operating on sets of different types"); } } return nodeManager->booleanType(); @@ -104,12 +101,12 @@ TypeNode MemberTypeRule::computeType(NodeManager* nodeManager, TypeNode elementType = n[0].getType(check); // e.g. (member 1 (singleton 1.0)) is true whereas // (member 1.0 (singleton 1)) throws a typing error - if (!elementType.isSubtypeOf(setType.getSetElementType())) + if (elementType != setType.getSetElementType()) { std::stringstream ss; ss << "member operating on sets of different types:\n" << "child type: " << elementType << "\n" - << "not subtype: " << setType.getSetElementType() << "\n" + << "not type: " << setType.getSetElementType() << "\n" << "in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -129,13 +126,12 @@ TypeNode SingletonTypeRule::computeType(NodeManager* nodeManager, if (check) { TypeNode type2 = n[0].getType(check); - TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2); // the type of the element should be a subtype of the type of the operator // e.g. (set.singleton (SetSingletonOp Real) 1) where 1 is an Int - if (leastCommonType.isNull() || leastCommonType != type1) + if (type1 != type2) { std::stringstream ss; - ss << "The type '" << type2 << "' of the element is not a subtype of '" + ss << "The type '" << type2 << "' of the element is not a type of '" << type1 << "' in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index 5e47283a4..01adb7e3a 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -336,10 +336,10 @@ TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, TypeNode argType = n[0].getType(check); // the type of the element should be a subtype of the type of the operator // e.g. (seq.unit (SeqUnitOp Real) 1) where 1 is an Int - if (!argType.isSubtypeOf(otype)) + if (argType != otype) { std::stringstream ss; - ss << "The type '" << argType << "' of the element is not a subtype of '" + ss << "The type '" << argType << "' of the element is not the type of '" << otype << "' in term : " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 84a54025f..9a0a66a3f 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -131,7 +131,7 @@ TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager, if (check) { TypeNode aType = n[1].getType(check); - if (!aType.isSubtypeOf(fType[0])) + if (aType != fType[0]) { throw TypeCheckingExceptionPrivate( n, "argument does not match function type"); -- 2.30.2