diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:02:51 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:03:20 -0500 |
commit | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (patch) | |
tree | ebe6334ca8a415a4d5a24a83ee40441419c93876 /src/theory/sets | |
parent | ae1d4e4f05fdc2db61d7de7efee5bd567363ceef (diff) |
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index a5a78e691..e2830b57e 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -116,7 +116,13 @@ struct MemberTypeRule { } TypeNode elementType = n[0].getType(check); if(!elementType.isComparableTo(setType.getSetElementType())) { - throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); + //if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing + std::stringstream ss; + ss << "member operating on sets of different types:\n" + << "child type: " << elementType << "\n" + << "not subtype: " << setType.getSetElementType() << "\n" + << "in term : " << n; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } return nodeManager->booleanType(); |