diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:35:03 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-12 08:50:58 -0500 |
commit | 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 (patch) | |
tree | 9e1fb4d128a62ca3e9152530dbfadb448ed49a45 /src/theory/arrays | |
parent | d6d34604fa6d4c260edfc10a5b7f543540be75f4 (diff) |
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 4d3112129..2dbc5affd 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -36,8 +36,7 @@ struct ArraySelectTypeRule { throw TypeCheckingExceptionPrivate(n, "array select operating on non-array"); } TypeNode indexType = n[1].getType(check); - if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ - //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing + if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); } } @@ -56,12 +55,10 @@ struct ArrayStoreTypeRule { } TypeNode indexType = n[1].getType(check); TypeNode valueType = n[2].getType(check); - if(!indexType.isComparableTo(arrayType.getArrayIndexType())){ - //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing + if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); } - if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){ - //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ //FIXME:typing + if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; Debug("array-types") << "value types: " << valueType << std::endl; throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); |