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).

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");