1 files changed, 34 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 00fe6baa8..e763a1f10 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -362,6 +362,9 @@ public:
   /** Create a skolem constant with the given type. */
   Node mkSkolem(const TypeNode& type);
 
+  /** Create a instantiation constant with the given type. */
+  Node mkInstConstant(const TypeNode& type);
+
   /**
    * Create a constant of type T.  It will have the appropriate
    * CONST_* kind defined for T.
@@ -579,6 +582,15 @@ public:
   /** Get the (singleton) type for sorts. */
   inline TypeNode kindType();
 
+  /** Get the bound var list type. */
+  inline TypeNode boundVarListType();
+
+  /** Get the instantiation pattern type. */
+  inline TypeNode instPatternType();
+
+  /** Get the instantiation pattern type. */
+  inline TypeNode instPatternListType();
+
   /**
    * Get the (singleton) type for builtin operators (that is, the type
    * of the Node returned from Node::getOperator() when the operator
@@ -897,6 +909,21 @@ inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
 }
 
+/** Get the bound var list type. */
+inline TypeNode NodeManager::boundVarListType(){
+  return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternType(){
+  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternListType(){
+  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
+}
+
 /** Get the (singleton) type for builtin operators. */
 inline TypeNode NodeManager::builtinOperatorType() {
   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
@@ -1366,6 +1393,13 @@ inline Node NodeManager::mkSkolem(const TypeNode& type) {
   return n;
 }
 
+inline Node NodeManager::mkInstConstant(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   return mkConstInternal<Node, T>(val);