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

12 files changed, 20 insertions, 518 deletions

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