From: mudathirmahgoub Date: Tue, 6 Oct 2020 00:49:32 +0000 (-0500) Subject: Remove subtyping for sets (#5205) X-Git-Tag: cvc5-1.0.0~2752 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cedeef257a8031bcfb16aa6e6f500121348458bf;p=cvc5.git Remove subtyping for sets (#5205) Removed subtyping for sets in type_node.h Fixes #4502, fixes #4631. --- diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index cbfb57747..659b1eef2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -318,9 +318,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const { return false; } } - if(isSet() && t.isSet()) { - return getSetElementType().isSubtypeOf(t.getSetElementType()); - } if (isFunction() && t.isFunction()) { if (!isComparableTo(t)) @@ -342,9 +339,6 @@ bool TypeNode::isComparableTo(TypeNode t) const { if(isSubtypeOf(NodeManager::currentNM()->realType())) { return t.isSubtypeOf(NodeManager::currentNM()->realType()); } - if(isSet() && t.isSet()) { - return getSetElementType().isComparableTo(t.getSetElementType()); - } if (isFunction() && t.isFunction()) { // comparable if they have a common type node @@ -583,24 +577,15 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::SEQUENCE_TYPE: return TypeNode(); case kind::SET_TYPE: { - // take the least common subtype of element types - TypeNode elementType; - if (t1.isSet() - && !(elementType = commonTypeNode(t0[0], t1[0], isLeast)).isNull()) - { - return NodeManager::currentNM()->mkSetType(elementType); - } - else - { - return TypeNode(); - } + // we don't support subtyping for sets + return TypeNode(); // return null type } - case kind::SEXPR_TYPE: - Unimplemented() - << "haven't implemented leastCommonType for symbolic expressions yet"; - default: - Unimplemented() << "don't have a commonType for types `" << t0 << "' and `" - << t1 << "'"; + case kind::SEXPR_TYPE: + Unimplemented() + << "haven't implemented leastCommonType for symbolic expressions yet"; + default: + Unimplemented() << "don't have a commonType for types `" << t0 + << "' and `" << t1 << "'"; } } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 18df43e9f..db2f3f22f 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -361,8 +361,6 @@ void TheorySetsPrivate::fullEffortCheck() Trace("sets-mem") << std::endl; } } - // check subtypes - checkSubtypes(); d_im.doPendingLemmas(); if (d_im.hasSent()) { @@ -418,49 +416,6 @@ void TheorySetsPrivate::fullEffortCheck() << std::endl; } -void TheorySetsPrivate::checkSubtypes() -{ - Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl; - const std::vector& sec = d_state.getSetsEqClasses(); - for (const Node& s : sec) - { - TypeNode mct = d_most_common_type[s]; - Assert(!mct.isNull()); - const std::map& smems = d_state.getMembers(s); - if (!smems.empty()) - { - for (const std::pair& it2 : smems) - { - Trace("sets") << " check subtype " << it2.first << " " << it2.second - << std::endl; - Trace("sets") << " types : " << it2.first.getType() << " " << mct - << std::endl; - if (!it2.first.getType().isSubtypeOf(mct)) - { - Node mctt = d_most_common_type_term[s]; - Assert(!mctt.isNull()); - Trace("sets") << " most common type term is " << mctt << std::endl; - std::vector exp; - exp.push_back(it2.second); - Assert(d_state.areEqual(mctt, it2.second[1])); - exp.push_back(mctt.eqNode(it2.second[1])); - Node tc_k = d_treg.getTypeConstraintSkolem(it2.first, mct); - if (!tc_k.isNull()) - { - Node etc = tc_k.eqNode(it2.first); - d_im.assertInference(etc, exp, "subtype-clash"); - if (d_state.isInConflict()) - { - return; - } - } - } - } - } - } - Trace("sets") << "TheorySetsPrivate: finished." << std::endl; -} - void TheorySetsPrivate::checkDownwardsClosure() { Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 5ac40515a..8247d4940 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -61,19 +61,6 @@ class TheorySetsPrivate { * Reset the information for a full effort check. */ void fullEffortReset(); - /** - * This ensures that subtype constraints are met for all set terms. In - * particular, for a set equivalence class E, let Set(T) be the most - * common type among the types of terms in that class. In other words, - * if E contains two terms of Set(Int) and Set(Real), then Set(Int) is the - * most common type. Then, for each membership x in S where S is a set in - * this equivalence class, we ensure x has type T by asserting: - * x = k - * for a fresh constant k of type T. This is done only if the type of x is not - * a subtype of Int (e.g. if x is of type Real). We call k the "type - * constraint skolem for x of type Int". - */ - void checkSubtypes(); /** * This implements an inference schema based on the "downwards closure" of * set membership. This roughly corresponds to the rules UNION DOWN I and II, diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 20e5e57e2..c5e86f10c 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -84,33 +84,26 @@ struct SubsetTypeRule { } };/* struct SetSubsetTypeRule */ -struct MemberTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) +struct MemberTypeRule +{ + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { Assert(n.getKind() == kind::MEMBER); TypeNode setType = n[1].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "checking for membership in a non-set"); } TypeNode elementType = n[0].getType(check); - // TODO : still need to be flexible here due to situations like: - // - // T : (Set Int) - // S : (Set Real) - // (= (as T (Set Real)) S) - // (member 0.5 S) - // ...where (member 0.5 T) is inferred - // - // or - // - // S : (Set Real) - // (not (member 0.5 s)) - // (member 0.0 s) - // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0))) - // - if(!elementType.isComparableTo(setType.getSetElementType())) { - //if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing + // e.g. (member 1 (singleton 1.0)) is true whereas + // (member 1.0 (singleton 1)) throws a typing error + if (!elementType.isSubtypeOf(setType.getSetElementType())) + { std::stringstream ss; ss << "member operating on sets of different types:\n" << "child type: " << elementType << "\n" @@ -121,7 +114,7 @@ struct MemberTypeRule { } return nodeManager->booleanType(); } -};/* struct MemberTypeRule */ +}; /* struct MemberTypeRule */ struct SingletonTypeRule { diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2 index 56f7e8c5e..19b5850fa 100644 --- a/test/regress/regress0/sets/int-real-univ-unsat.smt2 +++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2 @@ -1,13 +1,13 @@ ; COMMAND-LINE: --sets-ext -; EXPECT: unsat +; EXPECT: sat (set-logic ALL) -(set-info :status unsat) +(set-info :status sat) (declare-fun a () (Set Real)) (declare-fun x () Real) -(assert (= (as univset (Set Real)) (as univset (Set Int)))) +(assert (= (as univset (Set Real)) (as univset (Set Real)))) (assert (member x a)) diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2 index afe20b92f..e7d79bbf6 100644 --- a/test/regress/regress0/sets/int-real-univ.smt2 +++ b/test/regress/regress0/sets/int-real-univ.smt2 @@ -7,7 +7,7 @@ (declare-fun x () Real) -(assert (= (as univset (Set Real)) (as univset (Set Int)))) +(assert (= (as univset (Set Real)) (as univset (Set Real)))) (assert (member x a)) diff --git a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 index 86a1d93b4..e8c98e09c 100644 --- a/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 +++ b/test/regress/regress0/sets/sets-of-sets-subtypes.smt2 @@ -1,10 +1,10 @@ (set-logic QF_LIRAFS) -(set-info :status unsat) +(set-info :status sat) (declare-fun s () (Set (Set Real))) -(declare-fun t () (Set (Set Int))) +(declare-fun t () (Set (Set Real))) -(declare-fun x () (Set Int)) +(declare-fun x () (Set Real)) (declare-fun y () (Set Real)) (assert (member 0.5 y)) diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2 index a0e883ace..58ff563bc 100644 --- a/test/regress/regress0/sets/sets-poly-nonint.smt2 +++ b/test/regress/regress0/sets/sets-poly-nonint.smt2 @@ -1,6 +1,6 @@ (set-logic QF_UFLIRAFS) -(set-info :status unsat) -(declare-fun s () (Set Int)) +(set-info :status sat) +(declare-fun s () (Set Real)) (declare-fun t () (Set Real)) (declare-fun r () (Set Real)) (declare-fun u () (Set Real)) diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 12fec6c91..cff92ca8d 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -347,6 +347,9 @@ def testSortSubtyping(): setSortI = solver.mkSetSort(intSort) setSortR = solver.mkSetSort(realSort) - # we support subtyping for sets - assert setSortI.isSubsortOf(setSortR) - assert setSortR.isComparableTo(setSortI) + # we don't support subtyping for sets + assert not setSortI.isComparableTo(setSortR) + assert not setSortI.isSubsortOf(setSortR) + assert not setSortR.isComparableTo(setSortI) + assert not setSortR.isSubsortOf(setSortI) + diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 32108bf84..53563f833 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -372,7 +372,9 @@ void SortBlack::testSortSubtyping() Sort setSortI = d_solver.mkSetSort(intSort); Sort setSortR = d_solver.mkSetSort(realSort); - // we support subtyping for sets - TS_ASSERT(setSortI.isSubsortOf(setSortR)); - TS_ASSERT(setSortR.isComparableTo(setSortI)); + // we don't support subtyping for sets + TS_ASSERT(!setSortI.isComparableTo(setSortR)); + TS_ASSERT(!setSortI.isSubsortOf(setSortR)); + TS_ASSERT(!setSortR.isComparableTo(setSortI)); + TS_ASSERT(!setSortR.isSubsortOf(setSortI)); } diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index 06f5608c8..c098ca9b8 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -41,6 +41,16 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite d_em.reset(); } + void testIsisComparableTo() + { + TypeNode setRealType = d_nm->mkSetType(d_nm->realType()); + TypeNode setIntType = d_nm->mkSetType(d_nm->integerType()); + TS_ASSERT(!setIntType.isComparableTo(setRealType)); + TS_ASSERT(!setIntType.isSubtypeOf(setRealType)); + TS_ASSERT(!setRealType.isComparableTo(setIntType)); + TS_ASSERT(!setRealType.isComparableTo(setIntType)); + } + void testSingletonTerm() { Sort realSort = d_slv->getRealSort();