1 files changed, 21 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f4c3a1999..f52c7732f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -685,6 +685,9 @@ public:
   /** Get the (singleton) type for RegExp. */
   inline TypeNode regexpType();
 
+  /** Get the (singleton) type for rounding modes. */
+  inline TypeNode roundingModeType();
+
   /** Get the bound var list type. */
   inline TypeNode boundVarListType();
 
@@ -764,6 +767,11 @@ public:
    */
   inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
 
+  /** Make the type of floating-point with <code>exp</code> bit exponent and
+      <code>sig</code> bit significand */
+  inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);  
+  inline TypeNode mkFloatingPointType(FloatingPointSize fs);
+
   /** Make the type of bitvectors of size <code>size</code> */
   inline TypeNode mkBitVectorType(unsigned size);
 
@@ -980,6 +988,11 @@ inline TypeNode NodeManager::regexpType() {
   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 }
 
+/** Get the (singleton) type for rounding modes. */
+inline TypeNode NodeManager::roundingModeType() {
+  return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
+}
+
 /** Get the bound var list type. */
 inline TypeNode NodeManager::boundVarListType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
@@ -1066,6 +1079,14 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
 }
 
+inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
+  return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
+}
+
+inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
+  return TypeNode(mkTypeConst<FloatingPointSize>(fs));
+}
+
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,