Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

11 files changed, 536 insertions, 163 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8d089901b..3dac28e11 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -494,10 +494,14 @@ Expr DefineFunctionCommand::getFormula() const throw() {
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   //Dump("declarations") << *this << endl; -- done by SmtEngine
-  if(!d_func.isNull()) {
-    smtEngine->defineFunction(d_func, d_formals, d_formula);
+  try {
+    if(!d_func.isNull()) {
+      smtEngine->defineFunction(d_func, d_formals, d_formula);
+    }
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
-  d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 46a7bb82c..533a4dd7f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -97,24 +97,33 @@ ExprManager::ExprManager(const Options& options) :
 #endif
 }
 
-ExprManager::~ExprManager() {
-#ifdef CVC4_STATISTICS_ON
+ExprManager::~ExprManager() throw() {
   NodeManagerScope nms(d_nodeManager);
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    if (d_exprStatistics[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
-      delete d_exprStatistics[i];
+
+  try {
+
+#ifdef CVC4_STATISTICS_ON
+    for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+      if (d_exprStatistics[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
+        delete d_exprStatistics[i];
+      }
     }
-  }
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-    if (d_exprStatisticsVars[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
-      delete d_exprStatisticsVars[i];
+    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+      if (d_exprStatisticsVars[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+        delete d_exprStatisticsVars[i];
+      }
     }
-  }
 #endif
-  delete d_nodeManager;
-  delete d_ctxt;
+
+    delete d_nodeManager;
+    delete d_ctxt;
+
+  } catch(Exception& e) {
+    Warning() << "CVC4 threw an exception during cleanup." << std::endl
+              << e << std::endl;
+  }
 }
 
 const Options* ExprManager::getOptions() const {
@@ -697,6 +706,39 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
+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);
+  }
+}
+
+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.
  *
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 2abd05821..bf9bfbb38 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -26,6 +26,7 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "expr/expr.h"
+#include "util/subrange_bound.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -119,7 +120,7 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager();
+  ~ExprManager() throw();
 
   /** Get this node manager's options */
   const Options* getOptions() const;
@@ -403,9 +404,34 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression.  A TypeCheckingException 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.
+   */
+  Type mkPredicateSubtype(Expr lambda)
+    throw(TypeCheckingException);
+
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression and whose non-emptiness is witnessed by the given
+   * witness.  A TypeCheckingException can be thrown if lambda is not
+   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
+   * ill-typed.
+   */
+  Type mkPredicateSubtype(Expr lambda, Expr witness)
+    throw(TypeCheckingException);
+
+  /**
+   * Make an integer subrange type as defined by the argument.
+   */
+  Type mkSubrangeType(const SubrangeBounds& bounds)
+    throw(TypeCheckingException);
+
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
-    throw (TypeCheckingException);
+    throw(TypeCheckingException);
 
   // variables are special, because duplicates are permitted
   Expr mkVar(const std::string& name, Type type);
@@ -421,6 +447,7 @@ public:
 
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
+
 };/* class ExprManager */
 
 ${mkConst_instantiations}
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c510ce381..d0f5fde9e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -76,7 +76,8 @@ TypeCheckingException::~TypeCheckingException() throw() {
 }
 
 void TypeCheckingException::toStream(std::ostream& os) const throw() {
-  os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr;
+  os << "Error during type checking: " << d_msg << endl
+     << "The ill-typed expression: " << *d_expr;
 }
 
 Expr TypeCheckingException::getExpression() const throw() {
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 695e572ab..e303a9e58 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -36,7 +36,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
 }
 
 void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() {
-  os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
+  os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node;
 }
 
 NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c647e128c..a2fddadfc 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -29,6 +29,7 @@
 
 #include <algorithm>
 #include <stack>
+#include <utility>
 #include <ext/hash_set>
 
 using namespace std;
@@ -235,14 +236,15 @@ void NodeManager::reclaimZombies() {
 }/* NodeManager::reclaimZombies() */
 
 TypeNode NodeManager::getType(TNode n, bool check)
-  throw (TypeCheckingExceptionPrivate, AssertionException) {
-  // Many theories' type checkers call Node::getType() directly.
-  // This is incorrect, since "this" might not be the caller's
-  // curent node manager.  Rather than force the individual typecheckers
-  // not to do this (by policy, which would be imperfect and lead
-  // to hard-to-find bugs, which it has in the past), we just
-  // set this node manager to be current for the duration of this
-  // check.
+  throw(TypeCheckingExceptionPrivate, AssertionException) {
+
+  // Many theories' type checkers call Node::getType() directly.  This
+  // is incorrect, since "this" might not be the caller's curent node
+  // manager.  Rather than force the individual typecheckers not to do
+  // this (by policy, which would be imperfect and lead to
+  // hard-to-find bugs, which it has in the past), we just set this
+  // node manager to be current for the duration of this check.
+  //
   NodeManagerScope nms(this);
 
   TypeNode typeNode;
@@ -321,4 +323,51 @@ 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) {
+    std::stringstream ss;
+    ss << Expr::setlanguage(Options::current()->outputLanguage)
+       << "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) {
+    std::stringstream ss;
+    ss << Expr::setlanguage(Options::current()->outputLanguage)
+       << "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));
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 704e930b5..da999cc82 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -38,6 +38,7 @@
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 #include "context/context.h"
+#include "util/subrange_bound.h"
 #include "util/configuration_private.h"
 #include "util/tls.h"
 #include "util/options.h"
@@ -662,6 +663,31 @@ public:
   inline 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
@@ -687,7 +713,7 @@ public:
    * (default: false)
    */
   TypeNode getType(TNode n, bool check = false)
-    throw (TypeCheckingExceptionPrivate, AssertionException);
+    throw(TypeCheckingExceptionPrivate, AssertionException);
 
   /**
    * Convert a node to an expression.  Uses the ExprManager
@@ -944,10 +970,15 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
 
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
-  CheckArgument(!indexType.isFunctionLike(), domain,
+  CheckArgument(!indexType.isNull(), indexType,
+                "unexpected NULL index type");
+  CheckArgument(!constituentType.isNull(), constituentType,
+                "unexpected NULL constituent type");
+  CheckArgument(!indexType.isFunctionLike(), indexType,
                 "cannot index arrays by a function-like type");
-  CheckArgument(!constituentType.isFunctionLike(), domain,
+  CheckArgument(!constituentType.isFunctionLike(), constituentType,
                 "cannot store function-like types in arrays");
+Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index a901af73a..eaf10ba20 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -103,26 +103,32 @@ Type& Type::operator=(const Type& t) {
 }
 
 bool Type::operator==(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode == *t.d_typeNode;
 }
 
 bool Type::operator!=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode != *t.d_typeNode;
 }
 
 bool Type::operator<(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode < *t.d_typeNode;
 }
 
 bool Type::operator<=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode <= *t.d_typeNode;
 }
 
 bool Type::operator>(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode > *t.d_typeNode;
 }
 
 bool Type::operator>=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode >= *t.d_typeNode;
 }
 
@@ -375,13 +381,39 @@ bool Type::isSortConstructor() const {
   return d_typeNode->isSortConstructor();
 }
 
-/** Cast to a sort type */
+/** Cast to a sort constructor type */
 Type::operator SortConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isNull() || isSortConstructor());
   return SortConstructorType(*this);
 }
 
+/** Is this a predicate subtype */
+bool Type::isPredicateSubtype() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isPredicateSubtype();
+}
+
+/** Cast to a predicate subtype */
+Type::operator PredicateSubtype() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isPredicateSubtype());
+  return PredicateSubtype(*this);
+}
+
+/** Is this an integer subrange */
+bool Type::isSubrange() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSubrange();
+}
+
+/** Cast to a predicate subtype */
+Type::operator SubrangeType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isSubrange());
+  return SubrangeType(*this);
+}
+
 /** Is this a kind type (i.e., the type of a type)? */
 bool Type::isKind() const {
   NodeManagerScope nms(d_nodeManager);
@@ -543,6 +575,18 @@ SortConstructorType::SortConstructorType(const Type& t)
   Assert(isNull() || isSortConstructor());
 }
 
+PredicateSubtype::PredicateSubtype(const Type& t)
+  throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isPredicateSubtype());
+}
+
+SubrangeType::SubrangeType(const Type& t)
+  throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isSubrange());
+}
+
 unsigned BitVectorType::getSize() const {
   return d_typeNode->getBitVectorSize();
 }
@@ -648,6 +692,21 @@ BooleanType TesterType::getRangeType() const {
   return BooleanType(makeType(d_nodeManager->booleanType()));
 }
 
+Expr PredicateSubtype::getPredicate() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getSubtypePredicate().toExpr();
+}
+
+Type PredicateSubtype::getBaseType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getSubtypeBaseType().toType();
+}
+
+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 34cc925f6..76fccb37b 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -28,6 +28,7 @@
 
 #include "util/Assert.h"
 #include "util/cardinality.h"
+#include "util/subrange_bound.h"
 
 namespace CVC4 {
 
@@ -60,6 +61,8 @@ class TupleType;
 class KindType;
 class SortType;
 class SortConstructorType;
+class PredicateSubtype;
+class SubrangeType;
 class Type;
 
 /** Strategy for hashing Types */
@@ -405,6 +408,30 @@ public:
   operator SortConstructorType() const throw(AssertionException);
 
   /**
+   * Is this a predicate subtype?
+   * @return true if this is a predicate subtype
+   */
+  bool isPredicateSubtype() const;
+
+  /**
+   * Cast this type to a predicate subtype
+   * @return the predicate subtype
+   */
+  operator PredicateSubtype() const throw(AssertionException);
+
+  /**
+   * Is this an integer subrange type?
+   * @return true if this is an integer subrange type
+   */
+  bool isSubrange() const;
+
+  /**
+   * Cast this type to an integer subrange type
+   * @return the integer subrange type
+   */
+  operator SubrangeType() const throw(AssertionException);
+
+  /**
    * Is this a kind type (i.e., the type of a type)?
    * @return true if this is a kind type
    */
@@ -574,6 +601,39 @@ public:
 };/* class SortConstructorType */
 
 /**
+ * Class encapsulating a predicate subtype.
+ */
+class CVC4_PUBLIC PredicateSubtype : public Type {
+
+public:
+
+  /** Construct from the base type */
+  PredicateSubtype(const Type& type = Type()) throw(AssertionException);
+
+  /** Get the LAMBDA defining this predicate subtype */
+  Expr getPredicate() const;
+
+  /** Get the base type of this predicate subtype */
+  Type getBaseType() const;
+
+};/* class PredicateSubtype */
+
+/**
+ * Class encapsulating an integer subrange type.
+ */
+class CVC4_PUBLIC SubrangeType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SubrangeType(const Type& type = Type()) throw(AssertionException);
+
+  /** Get the bounds defining this integer subrange */
+  SubrangeBounds getSubrangeBounds() const;
+
+};/* class SubrangeType */
+
+/**
  * Class encapsulating the kind type (the type of types).
  */
 class CVC4_PUBLIC KindType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 77203bbb5..8cfb6387a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -71,68 +71,45 @@ Node TypeNode::mkGroundTerm() const {
   return kind::mkGroundTerm(*this);
 }
 
-bool TypeNode::isBoolean() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isInteger() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == INTEGER_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isReal() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == REAL_TYPE ||
-      getConst<TypeConstant>() == INTEGER_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isPseudoboolean() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
-}
-
-bool TypeNode::isString() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == STRING_TYPE;
-}
-
-bool TypeNode::isArray() const {
-  return getKind() == kind::ARRAY_TYPE;
-}
-
-TypeNode TypeNode::getArrayIndexType() const {
-  Assert(isArray());
-  return (*this)[0];
-}
-
-TypeNode TypeNode::getArrayConstituentType() const {
-  Assert(isArray());
-  return (*this)[1];
-}
-
-TypeNode TypeNode::getConstructorRangeType() const {
-  Assert(isConstructor());
-  return (*this)[getNumChildren()-1];
-}
-
-bool TypeNode::isFunction() const {
-  return getKind() == kind::FUNCTION_TYPE;
+bool TypeNode::isSubtypeOf(TypeNode t) const {
+  if(*this == t) {
+    return true;
+  }
+  if(getKind() == kind::TYPE_CONSTANT) {
+    switch(getConst<TypeConstant>()) {
+    case PSEUDOBOOLEAN_TYPE:
+      return t.getKind() == kind::TYPE_CONSTANT &&
+        ( t.getConst<TypeConstant>() == BOOLEAN_TYPE ||
+          t.getConst<TypeConstant>() == INTEGER_TYPE );
+    case INTEGER_TYPE:
+      return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
+    default:
+      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(isPredicateSubtype()) {
+    return getSubtypeBaseType().isSubtypeOf(t);
+  }
+  return false;
 }
 
-bool TypeNode::isFunctionLike() const {
-  return
-    getKind() == kind::FUNCTION_TYPE ||
-    getKind() == kind::CONSTRUCTOR_TYPE ||
-    getKind() == kind::SELECTOR_TYPE ||
-    getKind() == kind::TESTER_TYPE;
+Node TypeNode::getSubtypePredicate() const {
+  Assert(isPredicateSubtype());
+  return Node::fromExpr(getConst<Predicate>());
 }
 
-bool TypeNode::isPredicate() const {
-  return isFunction() && getRangeType().isBoolean();
+TypeNode TypeNode::getSubtypeBaseType() const {
+  Assert(isPredicateSubtype());
+  return getSubtypePredicate().getType().getArgTypes()[0];
 }
 
 std::vector<TypeNode> TypeNode::getArgTypes() const {
@@ -158,19 +135,6 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
-TypeNode TypeNode::getRangeType() const {
-  if(isTester()) {
-    return NodeManager::currentNM()->booleanType();
-  }
-  Assert(isFunction() || isConstructor() || isSelector());
-  return (*this)[getNumChildren()-1];
-}
-
-/** Is this a tuple type? */
-bool TypeNode::isTuple() const {
-  return getKind() == kind::TUPLE_TYPE;
-}
-
 /** Is this a tuple type? */
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
@@ -181,37 +145,6 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   return types;
 }
 
-/** Is this a sort kind */
-bool TypeNode::isSort() const {
-  return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr());
-}
-
-/** Is this a sort constructor kind */
-bool TypeNode::isSortConstructor() const {
-  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
-}
-
-/** Is this a kind type (i.e., the type of a type)? */
-bool TypeNode::isKind() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == KIND_TYPE;
-}
-
-/** Is this a bit-vector type */
-bool TypeNode::isBitVector() const {
-  return getKind() == kind::BITVECTOR_TYPE;
-}
-
-/** Is this a datatype type */
-bool TypeNode::isDatatype() const {
-  return getKind() == kind::DATATYPE_TYPE;
-}
-
-/** Is this a parametric datatype type */
-bool TypeNode::isParametricDatatype() const {
-  return getKind() == kind::PARAMETRIC_DATATYPE;
-}
-
 /** Is this an instantiated datatype type */
 bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() == kind::DATATYPE_TYPE) {
@@ -239,31 +172,4 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 }
 
-/** Is this a constructor type */
-bool TypeNode::isConstructor() const {
-  return getKind() == kind::CONSTRUCTOR_TYPE;
-}
-
-/** Is this a selector type */
-bool TypeNode::isSelector() const {
-  return getKind() == kind::SELECTOR_TYPE;
-}
-
-/** Is this a tester type */
-bool TypeNode::isTester() const {
-  return getKind() == kind::TESTER_TYPE;
-}
-
-/** Is this a bit-vector type of size <code>size</code> */
-bool TypeNode::isBitVector(unsigned size) const {
-  return getKind() == kind::BITVECTOR_TYPE &&
-    getConst<BitVectorSize>() == size;
-}
-
-/** Get the size of this bit-vector type */
-unsigned TypeNode::getBitVectorSize() const {
-  Assert(isBitVector());
-  return getConst<BitVectorSize>();
-}
-
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c7da5ceb7..f59ce2dfe 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -447,6 +447,9 @@ public:
    */
   Node mkGroundTerm() const;
 
+  /** Is this type a subtype of the given type? */
+  bool isSubtypeOf(TypeNode t) const;
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 
@@ -519,6 +522,16 @@ public:
    */
   bool isPredicate() const;
 
+  /**
+   * Is this a predicate-LIKE type?  Predicate-like things
+   * (e.g. datatype testers) that aren't actually predicates ARE
+   * considered predicates, here.
+   *
+   * Arrays are explicitly *not* predicate-like for the purposes of
+   * this test.
+   */
+  bool isPredicateLike() const;
+
   /** Is this a tuple type? */
   bool isTuple() const;
 
@@ -561,6 +574,21 @@ 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 base type of this subtype */
+  TypeNode getSubtypeBaseType() const;
+
+  /** Is this a subrange */
+  bool isSubrange() const;
+
+  /** Get the bounds defining this subrange */
+  const SubrangeBounds& getSubrangeBounds() const;
+
   /** Is this a kind type (i.e., the type of a type)? */
   bool isKind() const;
 
@@ -755,6 +783,172 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
   d_nv->printAst(out, indent);
 }
 
+inline bool TypeNode::isBoolean() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
+      isPseudoboolean() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() );
+}
+
+inline bool TypeNode::isInteger() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
+    isSubrange() ||
+    isPseudoboolean() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isInteger() );
+}
+
+inline bool TypeNode::isReal() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
+    isInteger() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isReal() );
+}
+
+inline bool TypeNode::isPseudoboolean() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+}
+
+inline bool TypeNode::isString() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == STRING_TYPE;
+}
+
+inline bool TypeNode::isArray() const {
+  return getKind() == kind::ARRAY_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+}
+
+inline TypeNode TypeNode::getArrayIndexType() const {
+  Assert(isArray());
+  return (*this)[0];
+}
+
+inline TypeNode TypeNode::getArrayConstituentType() const {
+  Assert(isArray());
+  return (*this)[1];
+}
+
+inline TypeNode TypeNode::getConstructorRangeType() const {
+  Assert(isConstructor());
+  return (*this)[getNumChildren()-1];
+}
+
+inline bool TypeNode::isFunction() const {
+  return getKind() == kind::FUNCTION_TYPE;
+}
+
+inline bool TypeNode::isFunctionLike() const {
+  return
+    getKind() == kind::FUNCTION_TYPE ||
+    getKind() == kind::CONSTRUCTOR_TYPE ||
+    getKind() == kind::SELECTOR_TYPE ||
+    getKind() == kind::TESTER_TYPE;
+}
+
+inline bool TypeNode::isPredicate() const {
+  return isFunction() && getRangeType().isBoolean();
+}
+
+inline bool TypeNode::isPredicateLike() const {
+  return isFunctionLike() && getRangeType().isBoolean();
+}
+
+inline TypeNode TypeNode::getRangeType() const {
+  if(isTester()) {
+    return NodeManager::currentNM()->booleanType();
+  }
+  Assert(isFunction() || isConstructor() || isSelector());
+  return (*this)[getNumChildren() - 1];
+}
+
+/** Is this a tuple type? */
+inline bool TypeNode::isTuple() const {
+  return getKind() == kind::TUPLE_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isTuple() );
+}
+
+/** Is this a sort kind */
+inline bool TypeNode::isSort() const {
+  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isSort() );
+}
+
+/** Is this a sort constructor kind */
+inline bool TypeNode::isSortConstructor() const {
+  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
+}
+
+/** 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() && getSubtypeBaseType().isSubrange() );
+}
+
+/** Is this a kind type (i.e., the type of a type)? */
+inline bool TypeNode::isKind() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == KIND_TYPE;
+}
+
+/** Is this a bit-vector type */
+inline bool TypeNode::isBitVector() const {
+  return getKind() == kind::BITVECTOR_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isBitVector() );
+}
+
+/** Is this a datatype type */
+inline bool TypeNode::isDatatype() const {
+  return getKind() == kind::DATATYPE_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isDatatype() );
+}
+
+/** Is this a parametric datatype type */
+inline bool TypeNode::isParametricDatatype() const {
+  return getKind() == kind::PARAMETRIC_DATATYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isParametricDatatype() );
+}
+
+/** Is this a constructor type */
+inline bool TypeNode::isConstructor() const {
+  return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+/** Is this a selector type */
+inline bool TypeNode::isSelector() const {
+  return getKind() == kind::SELECTOR_TYPE;
+}
+
+/** Is this a tester type */
+inline bool TypeNode::isTester() const {
+  return getKind() == kind::TESTER_TYPE;
+}
+
+/** 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() && getSubtypeBaseType().isBitVector(size) );
+}
+
+/** Get the size of this bit-vector type */
+inline unsigned TypeNode::getBitVectorSize() const {
+  Assert(isBitVector());
+  return getConst<BitVectorSize>();
+}
+
+inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
+  Assert(isSubrange());
+  return getConst<SubrangeBounds>();
+}
+
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used