1 files changed, 65 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e9f121047..7c847d8ce 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -105,6 +105,71 @@ NodeManager::NodeManager(ExprManager* exprManager)
   init();
 }
 
+TypeNode NodeManager::booleanType()
+{
+  return mkTypeConst<TypeConstant>(BOOLEAN_TYPE);
+}
+
+TypeNode NodeManager::integerType()
+{
+  return mkTypeConst<TypeConstant>(INTEGER_TYPE);
+}
+
+TypeNode NodeManager::realType()
+{
+  return mkTypeConst<TypeConstant>(REAL_TYPE);
+}
+
+TypeNode NodeManager::stringType()
+{
+  return mkTypeConst<TypeConstant>(STRING_TYPE);
+}
+
+TypeNode NodeManager::regExpType()
+{
+  return mkTypeConst<TypeConstant>(REGEXP_TYPE);
+}
+
+TypeNode NodeManager::roundingModeType()
+{
+  return mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE);
+}
+
+TypeNode NodeManager::boundVarListType()
+{
+  return mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE);
+}
+
+TypeNode NodeManager::instPatternType()
+{
+  return mkTypeConst<TypeConstant>(INST_PATTERN_TYPE);
+}
+
+TypeNode NodeManager::instPatternListType()
+{
+  return mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE);
+}
+
+TypeNode NodeManager::builtinOperatorType()
+{
+  return mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE);
+}
+
+TypeNode NodeManager::mkBitVectorType(unsigned size)
+{
+  return mkTypeConst<BitVectorSize>(BitVectorSize(size));
+}
+
+TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig)
+{
+  return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig));
+}
+
+TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs)
+{
+  return mkTypeConst<FloatingPointSize>(fs);
+}
+
 void NodeManager::init() {
   // `mkConst()` indirectly needs the correct NodeManager in scope because we
   // call `NodeValue::inc()` which uses `NodeManager::curentNM()`