adding integer and real types to the public interface

2 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5d50dd100..3480cc0e6 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -56,6 +56,16 @@ KindType ExprManager::kindType() const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()));
 }
 
+RealType ExprManager::realType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->realType()));
+}
+
+IntegerType ExprManager::integerType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()));
+}
+
 Expr ExprManager::mkExpr(Kind kind) {
   const unsigned n = 0;
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index df5190af6..5ef6ef984 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -90,6 +90,12 @@ public:
   /** Get the type for sorts. */
   KindType kindType() const;
 
+  /** Get the type for reals. */
+  RealType realType() const;
+
+  /** Get the type for integers */
+  IntegerType integerType() const;
+
   /**
    * Make a unary expression of a given kind (TRUE, FALSE,...).
    * @param kind the kind of expression