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, 0 insertions, 39 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 735d531e1..d6249d6fd 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -842,43 +842,6 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return PredicateSubtype(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-*/
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return PredicateSubtype(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-*/
-
-Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return SubrangeType(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
 /**
  * Get the type for the given Expr and optionally do type checking.
  *
@@ -1062,8 +1025,6 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
     return to->mkTypeConst(n.getConst<TypeConstant>());
   } else if(n.getKind() == kind::BITVECTOR_TYPE) {
     return to->mkBitVectorType(n.getConst<BitVectorSize>());
-  } else if(n.getKind() == kind::SUBRANGE_TYPE) {
-    return to->mkSubrangeType(n.getSubrangeBounds());
   }
   Type from_t = from->toType(n);
   Type& to_t = vmap.d_typeMap[from_t];