1 files changed, 57 insertions, 8 deletions
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 */