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

29 files changed, 59 insertions, 771 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index be24dacdd..2757e3dbe 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -27,7 +27,6 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
-#include "expr/predicate.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -1257,6 +1256,7 @@ Type ValidityChecker::intType() {
 }
 
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
+/*
   bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF";
   bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF";
   CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
@@ -1264,10 +1264,12 @@ Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
   CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
   CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator());
   return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
+  */
+  Unimplemented("Subrange types not supported by CVC4 (sorry!)");
 }
 
 Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
-  Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)");
+  Unimplemented("Predicate subtyping not supported by CVC4 (sorry!)");
   /*
   if(witness.isNull()) {
     return d_em->mkPredicateSubtype(pred);
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index e45c765c0..859d5a312 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -61,8 +61,6 @@ libexpr_la_SOURCES = \
 	variable_type_map.h \
 	datatype.h \
 	datatype.cpp \
-	predicate.h \
-	predicate.cpp \
 	record.cpp \
 	record.h \
 	uninterpreted_constant.cpp \
@@ -103,7 +101,6 @@ EXTRA_DIST = \
 	kind.i \
 	expr.i \
 	record.i \
-	predicate.i \
 	variable_type_map.i \
 	uninterpreted_constant.i
 
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];
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 07dc88fd3..8719d8ef4 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -461,8 +461,8 @@ public:
   /**
    * Make an integer subrange type as defined by the argument.
    */
-  Type mkSubrangeType(const SubrangeBounds& bounds)
-    throw(TypeCheckingException);
+  //Type mkSubrangeType(const SubrangeBounds& bounds)
+  //  throw(TypeCheckingException);
 
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index b746e0de9..f7a1d98d6 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -506,51 +506,6 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }
 
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
-  throw(TypeCheckingExceptionPrivate) {
-
-  Node lambdan = Node::fromExpr(lambda);
-
-  if(lambda.isNull()) {
-    throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
-  }
-
-  TypeNode tn = lambdan.getType();
-  if(! tn.isPredicateLike() ||
-     tn.getArgTypes().size() != 1) {
-    stringstream ss;
-    ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
-    throw TypeCheckingExceptionPrivate(lambdan, ss.str());
-  }
-
-  return TypeNode(mkTypeConst(Predicate(lambda)));
-}
-
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
-  throw(TypeCheckingExceptionPrivate) {
-
-  Node lambdan = Node::fromExpr(lambda);
-
-  if(lambda.isNull()) {
-    throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
-  }
-
-  TypeNode tn = lambdan.getType();
-  if(! tn.isPredicateLike() ||
-     tn.getArgTypes().size() != 1) {
-    stringstream ss;
-    ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
-    throw TypeCheckingExceptionPrivate(lambdan, ss.str());
-  }
-
-  return TypeNode(mkTypeConst(Predicate(lambda, witness)));
-}
-
-TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
-  throw(TypeCheckingExceptionPrivate) {
-  return TypeNode(mkTypeConst(bounds));
-}
-
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
   if( index==types.size() ){
     if( d_data.isNull() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1d1150842..44c116558 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -875,31 +875,6 @@ public:
   TypeNode mkSortConstructor(const std::string& name, size_t arity);
 
   /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingExceptionPrivate can be thrown if
-   * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
-   * proving that the resulting predicate subtype is inhabited.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingExceptionPrivate can be thrown if lambda
-   * is not a LAMBDA, or is ill-typed, or if the witness is not a
-   * witness or ill-typed.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make an integer subrange type as defined by the argument.
-   */
-  TypeNode mkSubrangeType(const SubrangeBounds& bounds)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
    * Get the type for the given node and optionally do type checking.
    *
    * Initial type computation will be near-constant time if
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
deleted file mode 100644
index eaf587110..000000000
--- a/src/expr/predicate.cpp
+++ /dev/null
@@ -1,99 +0,0 @@
-/*********************                                                        */
-/*! \file predicate.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-#include "expr/predicate.h"
-
-#include "base/cvc4_assert.h"
-#include "expr/expr.h"
-
-
-using namespace std;
-
-namespace CVC4 {
-
-Predicate::Predicate(const Predicate& p)
-    : d_predicate(new Expr(p.getExpression()))
-    , d_witness(new Expr(p.getWitness()))
-{}
-
-Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
-    : d_predicate(new Expr(e))
-    , d_witness(new Expr())
-{
-  PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
-  PrettyCheckArgument(e.getType().isPredicate(), e,
-                      "Expression given is not predicate");
-  PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
-                      "Expression given is not predicate of a single argument");
-}
-
-Predicate::Predicate(const Expr& e, const Expr& w)
-    throw(IllegalArgumentException)
-    : d_predicate(new Expr(e))
-    , d_witness(new Expr(w))
-{
-  PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
-  PrettyCheckArgument(e.getType().isPredicate(), e,
-                      "Expression given is not predicate");
-  PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
-                      "Expression given is not predicate of a single argument");
-}
-
-Predicate::~Predicate() {
-  delete d_predicate;
-  delete d_witness;
-}
-
-Predicate& Predicate::operator=(const Predicate& p){
-  (*d_predicate) = p.getExpression();
-  (*d_witness) = p.getWitness();
-  return *this;
-}
-
-
-// Predicate::operator Expr() const {
-//   return d_predicate;
-// }
-
-const Expr& Predicate::getExpression() const {
-  return *d_predicate;
-}
-
-const Expr& Predicate::getWitness() const {
-  return *d_witness;
-}
-
-bool Predicate::operator==(const Predicate& p) const {
-  return getExpression() == p.getExpression() &&
-      getWitness() == p.getWitness();
-}
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) {
-  out << p.getExpression();
-  const Expr& witness = p.getWitness();
-  if(! witness.isNull()) {
-    out << " : " << witness;
-  }
-  return out;
-}
-
-size_t PredicateHashFunction::operator()(const Predicate& p) const {
-  ExprHashFunction h;
-  return h(p.getWitness()) * 5039 + h(p.getExpression());
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/predicate.h b/src/expr/predicate.h
deleted file mode 100644
index 99e589fcd..000000000
--- a/src/expr/predicate.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/*********************                                                        */
-/*! \file predicate.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PREDICATE_H
-#define __CVC4__PREDICATE_H
-
-#include "base/exception.h"
-
-namespace CVC4 {
-
-class Predicate;
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
-
-struct CVC4_PUBLIC PredicateHashFunction {
-  size_t operator()(const Predicate& p) const;
-};/* class PredicateHashFunction */
-
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Expr;
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Predicate {
-public:
-
-  Predicate(const Expr& e) throw(IllegalArgumentException);
-  Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException);
-
-  Predicate(const Predicate& p);
-  ~Predicate();
-  Predicate& operator=(const Predicate& p);
-
-  //operator Expr() const;
-
-  const Expr& getExpression() const;
-  const Expr& getWitness() const;
-
-  bool operator==(const Predicate& p) const;
-
-  friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
-  friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
-
-private:
-  Expr* d_predicate;
-  Expr* d_witness;
-};/* class Predicate */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PREDICATE_H */
diff --git a/src/expr/predicate.i b/src/expr/predicate.i
deleted file mode 100644
index aa80a98b5..000000000
--- a/src/expr/predicate.i
+++ /dev/null
@@ -1,12 +0,0 @@
-%{
-#include "expr/predicate.h"
-%}
-
-%rename(equals) CVC4::Predicate::operator==(const Predicate&) const;
-%rename(toExpr) CVC4::Predicate::operator Expr() const;
-
-%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const Predicate&);
-
-%include "expr/predicate.h"
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index bb3ce0f58..8bcb0f8d5 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -329,20 +329,6 @@ bool Type::isSortConstructor() const {
   return d_typeNode->isSortConstructor();
 }
 
-/** Is this a predicate subtype */
-/* - not in release 1.0
-bool Type::isPredicateSubtype() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isPredicateSubtype();
-}
-*/
-
-/** Is this an integer subrange */
-bool Type::isSubrange() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSubrange();
-}
-
 size_t FunctionType::getArity() const {
   return d_typeNode->getNumChildren() - 1;
 }
@@ -505,20 +491,6 @@ SortConstructorType::SortConstructorType(const Type& t)
   PrettyCheckArgument(isNull() || isSortConstructor(), this);
 }
 
-/* - not in release 1.0
-PredicateSubtype::PredicateSubtype(const Type& t)
-  throw(IllegalArgumentException) :
-  Type(t) {
-  PrettyCheckArgument(isNull() || isPredicateSubtype(), this);
-}
-*/
-
-SubrangeType::SubrangeType(const Type& t)
-  throw(IllegalArgumentException) :
-  Type(t) {
-  PrettyCheckArgument(isNull() || isSubrange(), this);
-}
-
 unsigned BitVectorType::getSize() const {
   return d_typeNode->getBitVectorSize();
 }
@@ -666,11 +638,6 @@ Type PredicateSubtype::getParentType() const {
 }
 */
 
-SubrangeBounds SubrangeType::getSubrangeBounds() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getSubrangeBounds();
-}
-
 size_t TypeHashFunction::operator()(const Type& t) const {
   return TypeNodeHashFunction()(NodeManager::fromType(t));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 04b2907ff..25f0c5436 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -372,7 +372,7 @@ public:
    * Is this an integer subrange type?
    * @return true if this is an integer subrange type
    */
-  bool isSubrange() const;
+  //bool isSubrange() const;
 
   /**
    * Outputs a string representation of this type to the stream.
@@ -584,7 +584,6 @@ public:
   Type getParentType() const;
 
 };/* class PredicateSubtype */
-#endif /* 0 */
 
 /**
  * Class encapsulating an integer subrange type.
@@ -600,6 +599,7 @@ public:
   SubrangeBounds getSubrangeBounds() const;
 
 };/* class SubrangeType */
+#endif /* 0 */
 
 /**
  * Class encapsulating the bit-vector type.
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 6e16ee9fa..383a31dd0 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -106,15 +106,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
       return false;
     }
   }
-  if(isSubrange()) {
-    if(t.isSubrange()) {
-      return t.getSubrangeBounds() <= getSubrangeBounds();
-    } else {
-      return t.getKind() == kind::TYPE_CONSTANT &&
-        ( t.getConst<TypeConstant>() == INTEGER_TYPE ||
-          t.getConst<TypeConstant>() == REAL_TYPE );
-    }
-  }
   if(isTuple() && t.isTuple()) {
     const Datatype& dt1 = getDatatype();
     const Datatype& dt2 = t.getDatatype();
@@ -151,9 +142,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     }
     return true;
   }
-  if(isPredicateSubtype()) {
-    return getSubtypeParentType().isSubtypeOf(t);
-  }
   if(isSet() && t.isSet()) {
     return getSetElementType().isSubtypeOf(t.getSetElementType());
   }
@@ -205,28 +193,13 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isArray() && t.isArray()) {
     return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
   }
-  //if(isPredicateSubtype()) {
-  //  return t.isComparableTo(getSubtypeParentType());
-  //}
   return false;
 }
 
-Node TypeNode::getSubtypePredicate() const {
-  Assert(isPredicateSubtype());
-  return Node::fromExpr(getConst<Predicate>().getExpression());
-}
-
-TypeNode TypeNode::getSubtypeParentType() const {
-  Assert(isPredicateSubtype());
-  return getSubtypePredicate().getType().getArgTypes()[0];
-}
-
 TypeNode TypeNode::getBaseType() const {
   TypeNode realt = NodeManager::currentNM()->realType();
   if (isSubtypeOf(realt)) {
     return realt;
-  } else if (isPredicateSubtype()) {
-    return getSubtypeParentType().getBaseType();
   } else if (isParametricDatatype()) {
     vector<Type> v;
     for(size_t i = 1; i < getNumChildren(); ++i) {
@@ -264,14 +237,12 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
 
 /** Is this a tuple type? */
 bool TypeNode::isTuple() const {
-  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() );
 }
 
 /** Is this a record type? */
 bool TypeNode::isRecord() const {
-  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() )  ||
-    ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+  return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() );
 }
 
 size_t TypeNode::getTupleLength() const {
@@ -375,11 +346,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
         return TypeNode(); // null type
       }
     default:
-      //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-      //  return t0; // t0 is a constant type
-      //} else {
-        return TypeNode(); // null type
-      //}
+      return TypeNode(); // null type
     }
   } else if(t1.getKind() == kind::TYPE_CONSTANT) {
     return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
@@ -394,11 +361,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   case kind::CONSTRUCTOR_TYPE:
   case kind::SELECTOR_TYPE:
   case kind::TESTER_TYPE:
-    //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
-    //  return t0;
-    //} else {
-      return TypeNode();
-    //}
+    return TypeNode();
   case kind::FUNCTION_TYPE:
     return TypeNode(); // Not sure if this is right
   case kind::SET_TYPE: {
@@ -423,47 +386,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   case kind::SEXPR_TYPE:
     Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
     return TypeNode();
-  case kind::SUBTYPE_TYPE:
-    //if(t1.isPredicateSubtype()){
-    //  // This is the case where both t0 and t1 are predicate subtypes.
-    //  return leastCommonPredicateSubtype(t0, t1);
-    //}else{ // t0 is a predicate subtype and t1 is not
-    //  return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
-    //}
-    return TypeNode();
-  case kind::SUBRANGE_TYPE:
-    /*
-    if(t1.isSubrange()) {
-      const SubrangeBounds& t0SR = t0.getSubrangeBounds();
-      const SubrangeBounds& t1SR = t1.getSubrangeBounds();
-      if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) {
-        SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
-        return NodeManager::currentNM()->mkSubrangeType(j);
-      } else {
-        return NodeManager::currentNM()->integerType();
-      }
-    } else if(t1.isPredicateSubtype()) {
-      // t0 is a subrange
-      // t1 is not a subrange
-      // t1 is a predicate subtype
-      if(t1.isInteger()) {
-        return NodeManager::currentNM()->integerType();
-      } else if(t1.isReal()) {
-        return NodeManager::currentNM()->realType();
-      } else {
-        return TypeNode();
-      }
-    } else {
-      // t0 is a subrange
-      // t1 is not a subrange
-      // t1 is not a type constant && is not a predicate subtype
-      // t1 cannot be real subtype or integer.
-      Assert(t1.isReal());
-      Assert(t1.isInteger());
-      return TypeNode();
-    }
-*/
-    return TypeNode();
   case kind::DATATYPE_TYPE:
     if( t0.isTuple() && t1.isTuple() ){
       const Datatype& dt1 = t0.getDatatype();
@@ -490,9 +412,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
     if(!t1.isParametricDatatype()) {
       return TypeNode();
     }
-    while(t1.getKind() != kind::PARAMETRIC_DATATYPE) {
-      t1 = t1.getSubtypeParentType();
-    }
     if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) {
       return TypeNode();
     }
@@ -508,38 +427,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   }
 }
 
-TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
-  Assert(t0.isPredicateSubtype());
-  Assert(t1.isPredicateSubtype());
-
-  std::vector<TypeNode> t0stack;
-  t0stack.push_back(t0);
-  while(t0stack.back().isPredicateSubtype()){
-    t0stack.push_back(t0stack.back().getSubtypeParentType());
-  }
-  std::vector<TypeNode> t1stack;
-  t1stack.push_back(t1);
-  while(t1stack.back().isPredicateSubtype()){
-    t1stack.push_back(t1stack.back().getSubtypeParentType());
-  }
-
-  Assert(!t0stack.empty());
-  Assert(!t1stack.empty());
-
-  if(t0stack.back() == t1stack.back()){
-    TypeNode mostGeneral = t1stack.back();
-    t0stack.pop_back(); t1stack.pop_back();
-    while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){
-      mostGeneral = t0stack.back();
-      t0stack.pop_back(); t1stack.pop_back();
-    }
-    return mostGeneral;
-  }else{
-    return leastCommonTypeNode(t0stack.back(), t1stack.back());
-  }
-}
-
-
 Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
   TypeNode ntn = n.getType();
   Assert( ntn.isComparableTo( tn ) );
@@ -581,8 +468,7 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
 
 /** Is this a sort kind */
 bool TypeNode::isSort() const {
-  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isSort() );
+  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
 }
 
 /** Is this a sort constructor kind */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1a8bb14ed..8dd80bc37 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -620,27 +620,9 @@ public:
   /** Is this a sort constructor kind */
   bool isSortConstructor() const;
 
-  /** Is this a subtype predicate */
-  bool isPredicateSubtype() const;
-
-  /** Get the predicate defining this subtype */
-  Node getSubtypePredicate() const;
-
-  /**
-   * Get the parent type of this subtype; note that it could be
-   * another subtype.
-   */
-  TypeNode getSubtypeParentType() const;
-
   /** Get the most general base type of the type */
   TypeNode getBaseType() const;
 
-  /** Is this a subrange */
-  bool isSubrange() const;
-
-  /** Get the bounds defining this subrange */
-  const SubrangeBounds& getSubrangeBounds() const;
-
   /**
    * Returns the leastUpperBound in the extended type lattice of the two types.
    * If this is \top, i.e. there is no inhabited type that contains both,
@@ -657,13 +639,7 @@ public:
   static Node getEnsureTypeCondition( Node n, TypeNode tn );
 private:
   static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
-
-  /**
-   * Returns the leastUpperBound in the extended type lattice of two
-   * predicate subtypes.
-   */
-  static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1);
-
+  
   /**
    * Indents the given stream a given amount of spaces.
    *
@@ -852,22 +828,18 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
 
 inline bool TypeNode::isBoolean() const {
   return
-    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isBoolean() );
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE );
 }
 
 inline bool TypeNode::isInteger() const {
   return
-    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
-    isSubrange() ||
-    ( isPredicateSubtype() && getSubtypeParentType().isInteger() );
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE );
 }
 
 inline bool TypeNode::isReal() const {
   return
     ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
-    isInteger() ||
-    ( isPredicateSubtype() && getSubtypeParentType().isReal() );
+    isInteger();
 }
 
 inline bool TypeNode::isString() const {
@@ -944,43 +916,27 @@ inline TypeNode TypeNode::getRangeType() const {
 
 /** Is this a symbolic expression type? */
 inline bool TypeNode::isSExpr() const {
-  return getKind() == kind::SEXPR_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isSExpr() );
-}
-
-/** Is this a predicate subtype */
-inline bool TypeNode::isPredicateSubtype() const {
-  return getKind() == kind::SUBTYPE_TYPE;
-}
-
-/** Is this a subrange type */
-inline bool TypeNode::isSubrange() const {
-  return getKind() == kind::SUBRANGE_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isSubrange() );
+  return getKind() == kind::SEXPR_TYPE;
 }
 
 /** Is this a floating-point type */
 inline bool TypeNode::isFloatingPoint() const {
-  return getKind() == kind::FLOATINGPOINT_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() );
+  return getKind() == kind::FLOATINGPOINT_TYPE;
 }
 
 /** Is this a bit-vector type */
 inline bool TypeNode::isBitVector() const {
-  return getKind() == kind::BITVECTOR_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isBitVector() );
+  return getKind() == kind::BITVECTOR_TYPE;
 }
 
 /** Is this a datatype type */
 inline bool TypeNode::isDatatype() const {
-  return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
+  return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE;
 }
 
 /** Is this a parametric datatype type */
 inline bool TypeNode::isParametricDatatype() const {
-  return getKind() == kind::PARAMETRIC_DATATYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() );
+  return getKind() == kind::PARAMETRIC_DATATYPE;
 }
 
 /** Is this a codatatype type */
@@ -1013,15 +969,13 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
   return
     ( getKind() == kind::FLOATINGPOINT_TYPE &&
       getConst<FloatingPointSize>().exponent() == exp &&
-      getConst<FloatingPointSize>().significand() == sig ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
+      getConst<FloatingPointSize>().significand() == sig );
 }
 
 /** Is this a bit-vector type of size <code>size</code> */
 inline bool TypeNode::isBitVector(unsigned size) const {
   return
-    ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) );
+    ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
 }
 
 /** Get the datatype specification from a datatype type */
@@ -1054,16 +1008,6 @@ inline unsigned TypeNode::getBitVectorSize() const {
   return getConst<BitVectorSize>();
 }
 
-inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
-  Assert(isSubrange());
-  if(getKind() == kind::SUBRANGE_TYPE){
-    return getConst<SubrangeBounds>();
-  }else{
-    Assert(isPredicateSubtype());
-    return getSubtypeParentType().getSubrangeBounds();
-  }
-}
-
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index c865332e2..171c6cab0 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1293,7 +1293,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
            << "] inappropriate: range must be nonempty!";
         PARSER_STATE->parseError(ss.str());
       }
-      t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
+      PARSER_STATE->unimplementedFeature("subrange typing not supported in this release");
+      //t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
     }
 
     /* tuple types / old-style function types */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 69ba63a47..936a7261e 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -145,12 +145,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
     }
-    case kind::SUBRANGE_TYPE:
-      out << '[' << n.getConst<SubrangeBounds>() << ']';
-      break;
-    case kind::SUBTYPE_TYPE:
-      out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
-      break;
     case kind::TYPE_CONSTANT:
       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
       case REAL_TYPE:
@@ -398,12 +392,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
           toStream(out, n[0], depth, types, true);
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
           int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          Assert( sindex>=0 );
           out << '.' << sindex;
         }else if( t.isRecord() ){
           toStream(out, n[0], depth, types, true);
           const Record& rec = t.getRecord();
           const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
           int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+          Assert( sindex>=0 );
           std::pair<std::string, Type> fld = rec[sindex];
           out << '.' << fld.first;
         }else{
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2ba593377..aa9c17e5a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,19 +281,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
-    case kind::SUBRANGE_TYPE: {
-      const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
-      // No way to represent subranges in SMT-LIBv2; this is inspired
-      // by yices format (but isn't identical to it).
-      out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
-      break;
-    }
-    case kind::SUBTYPE_TYPE:
-      // No way to represent predicate subtypes in SMT-LIBv2; this is
-      // inspired by yices format (but isn't identical to it).
-      out << "(subtype " << n.getConst<Predicate>() << ')';
-      break;
-
     case kind::DATATYPE_TYPE:
       {
         const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f6b17e4cb..327f978e4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -545,8 +545,6 @@ class SmtEnginePrivate : public NodeManagerListener {
 
   /** TODO: whether certain preprocess steps are necessary */
   //bool d_needsExpandDefs;
-  //bool d_needsRewriteBoolTerms;
-  //bool d_needsConstrainSubTypes;
 
 public:
   /**
@@ -625,14 +623,6 @@ private:
   void compressBeforeRealAssertions(size_t before);
 
   /**
-   * Any variable in an assertion that is declared as a subtype type
-   * (predicate subtype or integer subrange type) must be constrained
-   * to be in that type.
-   */
-  void constrainSubtypes(TNode n, AssertionPipeline& assertions)
-    throw();
-
-  /**
    * Trace nodes back to their assertions using CircuitPropagator's
    * BackEdgesMap.
    */
@@ -679,9 +669,7 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
-    //d_needsExpandDefs(true),
-    //d_needsRewriteBoolTerms(true),
-    //d_needsConstrainSubTypes(true), //TODO
+    //d_needsExpandDefs(true),  //TODO?
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
@@ -3270,64 +3258,6 @@ void SmtEnginePrivate::unconstrainedSimp() {
   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
 }
 
-
-void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
-  throw() {
-
-  Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
-
-  set<TNode> done;
-  stack<TNode> worklist;
-  worklist.push(top);
-  done.insert(top);
-
-  do {
-    TNode n = worklist.top();
-    worklist.pop();
-
-    TypeNode t = n.getType();
-    if(t.isPredicateSubtype()) {
-      WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
-      Node pred = t.getSubtypePredicate();
-      Kind k;
-      // pred can be a LAMBDA, a function constant, or a datatype tester
-      Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
-      if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) {
-        k = kind::APPLY;
-      } else if(pred.getType().isTester()) {
-        k = kind::APPLY_TESTER;
-      } else {
-        k = kind::APPLY_UF;
-      }
-      Node app = NodeManager::currentNM()->mkNode(k, pred, n);
-      Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
-      assertions.push_back(app);
-    } else if(t.isSubrange()) {
-      SubrangeBounds bounds = t.getSubrangeBounds();
-      Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
-      if(bounds.lower.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
-        Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
-        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
-        assertions.push_back(lb);
-      }
-      if(bounds.upper.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
-        Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
-        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
-        assertions.push_back(ub);
-      }
-    }
-
-    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-      if(done.find(*i) == done.end()) {
-        worklist.push(*i);
-        done.insert(*i);
-      }
-    }
-  } while(! worklist.empty());
-}
-
 void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
   for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
@@ -4080,22 +4010,6 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  dumpAssertions("pre-constrain-subtypes", d_assertions);
-  {
-    // Any variables of subtype types need to be constrained properly.
-    // Careful, here: constrainSubtypes() adds to the back of
-    // d_assertions, but we don't need to reprocess those.
-    // We also can't use an iterator, because the vector may be moved in
-    // memory during this loop.
-    Chat() << "constraining subtypes..." << endl;
-    for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
-      constrainSubtypes(d_assertions[i], d_assertions);
-    }
-  }
-  dumpAssertions("post-constrain-subtypes", d_assertions);
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
   bool noConflict = true;
 
   // Unconstrained simplification
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 0884083c0..34ae30f4c 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -51,19 +51,6 @@ sort INTEGER_TYPE \
         "expr/node_manager.h" \
     "integer type"
 
-constant SUBRANGE_TYPE \
-    ::CVC4::SubrangeBounds \
-    ::CVC4::SubrangeBoundsHashFunction \
-    "util/subrange_bound.h" \
-    "the type of an integer subrange"
-cardinality SUBRANGE_TYPE \
-    "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
-    "theory/arith/theory_arith_type_rules.h"
-well-founded SUBRANGE_TYPE \
-    true \
-    "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
-    "theory/arith/theory_arith_type_rules.h"
-
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashFunction \
@@ -76,9 +63,6 @@ enumerator REAL_TYPE \
 enumerator INTEGER_TYPE \
     "::CVC4::theory::arith::IntegerEnumerator" \
     "theory/arith/type_enumerator.h"
-enumerator SUBRANGE_TYPE \
-    "::CVC4::theory::arith::SubrangeEnumerator" \
-    "theory/arith/type_enumerator.h"
 
 operator LT 2 "less than, x < y"
 operator LEQ 2 "less than or equal, x <= y"
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 59c2aaa8f..db3ae65f2 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -171,33 +171,6 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
-
-class SubrangeProperties {
-public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
-    if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
-      return Cardinality::INTEGERS;
-    }
-    return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
-    if(bounds.lower.hasBound()) {
-      return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
-    }
-    if(bounds.upper.hasBound()) {
-      return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
-    }
-    return NodeManager::currentNM()->mkConst(Rational(0));
-  }
-};/* class SubrangeProperties */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 5d6b936a7..4cb34ed4a 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -108,55 +108,6 @@ public:
 
 };/* class IntegerEnumerator */
 
-class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
-  Integer d_int;
-  SubrangeBounds d_bounds;
-  bool d_direction;// true == +, false == -
-
-public:
-
-  SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
-    TypeEnumeratorBase<SubrangeEnumerator>(type),
-    d_int(0),
-    d_bounds(type.getConst<SubrangeBounds>()),
-    d_direction(d_bounds.lower.hasBound()) {
-
-    d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
-
-    Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
-    // if we're counting down, there's no lower bound
-    Assert(d_direction || !d_bounds.lower.hasBound());
-  }
-
-  Node operator*() throw(NoMoreValuesException) {
-    if(isFinished()) {
-      throw NoMoreValuesException(getType());
-    }
-    return NodeManager::currentNM()->mkConst(Rational(d_int));
-  }
-
-  SubrangeEnumerator& operator++() throw() {
-    if(d_direction) {
-      if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
-        d_int += 1;
-      }
-    } else {
-      // if we're counting down, there's no lower bound
-      d_int -= 1;
-    }
-    return *this;
-  }
-
-  bool isFinished() throw() {
-    // if we're counting down, there's no lower bound
-    return d_direction &&
-      d_bounds.upper.hasBound() &&
-      d_int > d_bounds.upper.getBound();
-  }
-
-};/* class SubrangeEnumerator */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
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");
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 0ebebf1dd..12e897189 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -336,17 +336,4 @@ typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
-constant SUBTYPE_TYPE \
-    ::CVC4::Predicate \
-    ::CVC4::PredicateHashFunction \
-    "expr/predicate.h" \
-    "predicate subtype; payload is an instance of the CVC4::Predicate class"
-cardinality SUBTYPE_TYPE \
-    "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-well-founded SUBTYPE_TYPE \
-    "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-
 endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 7f86c7d0d..d8893d441 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -77,6 +77,9 @@ class EqualityTypeRule {
       TypeNode lhsType = n[0].getType(check);
       TypeNode rhsType = n[1].getType(check);
 
+      // TODO : we may want to limit cases where we have equalities between terms of different types 
+      //   equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets
+      //   one possibility is to only allow this for Int/Real
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
         ss << "Subexpressions must have a common base type:" << std::endl;
@@ -299,26 +302,6 @@ public:
   }
 };/* class SExprProperties */
 
-class SubtypeProperties {
-public:
-
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Computing the cardinality for predicate subtype not yet supported.");
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Computing the well-foundedness for predicate subtype not yet supported.");
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::SUBTYPE_TYPE);
-    Unimplemented("Constructing a ground term for predicate subtype not yet supported.");
-  }
-
-};/* class SubtypeProperties */
-
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 82d7274fa..e787ebc49 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -79,8 +79,7 @@ struct DatatypeConstructorTypeRule {
           Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
                                  << (*tchild_it) << std::endl;
           TypeNode argumentType = *tchild_it;
-          if (!childType.isComparableTo(argumentType)) {
-          //if (!childType.isSubtypeOf(argumentType)) {   //FIXME:typing
+          if (!childType.isSubtypeOf(argumentType)) { 
             std::stringstream ss;
             ss << "bad type for constructor argument:\n"
                << "child type:  " << childType << "\n"
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 1fd5f08be..23b185230 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -115,6 +115,21 @@ struct MemberTypeRule {
         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
         std::stringstream ss;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3ddb18754..82607a165 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -243,9 +243,6 @@ public:
   static inline TheoryId theoryOf(TypeNode typeNode) {
     Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
-    while (typeNode.isPredicateSubtype()) {
-      typeNode = typeNode.getSubtypeParentType();
-    }
     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
     } else {
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index a3c775a2a..c31de403c 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -45,8 +45,7 @@ class UfTypeRule {
            ++argument_it, ++argument_type_it) {
         TypeNode currentArgument = (*argument_it).getType();
         TypeNode currentArgumentType = *argument_type_it;
-        if (!currentArgument.isComparableTo(currentArgumentType)) {
-        //if (!currentArgument.isSubtypeOf(currentArgumentType)) {   //FIXME:typing
+        if (!currentArgument.isSubtypeOf(currentArgumentType)) { 
           std::stringstream ss;
           ss << "argument type is not a subtype of the function's argument "
              << "type:\n"
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9a16f68ca..17a2ea2ef 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -172,7 +172,6 @@ BUG_TESTS = \
 	bug576.smt2 \
 	bug576a.smt2 \
 	bug578.smt2 \
-	bug585.cvc \
 	bug586.cvc \
 	bug593.smt2 \
 	bug595.cvc \
@@ -189,8 +188,10 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 # bug512 -- taking too long, --time-per not working perhaps? in any case,
 # we have a minimized version still getting tested
 # bug639 -- still fails, reopened bug
+# bug585 -- contains subrange type (not supported)
 DISABLED_TESTS = \
-	bug512.smt2
+	bug512.smt2 \
+	bug585.cvc
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index b437f1878..572e2790d 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -27,11 +27,11 @@ TESTS =	\
 	rec1.cvc \
 	rec2.cvc \
 	rec4.cvc \
-	rec5.cvc \
 	datatype.cvc \
 	datatype0.cvc \
 	datatype1.cvc \
 	datatype2.cvc \
+	datatype3.cvc \
 	datatype4.cvc \
 	datatype13.cvc \
 	empty_tuprec.cvc \
@@ -83,10 +83,10 @@ TESTS =	\
 	tuple-no-clash.cvc \
 	jsat-2.6.smt2
 
+# rec5 -- no longer support subrange types
 FAILING_TESTS = \
-	datatype-dump.cvc
-
-# takes a long time to build model on debug : datatype3.cvc
+	datatype-dump.cvc \
+	rec5.cvc
 
 EXTRA_DIST = $(TESTS)