From 2482b19ea90183d5040390b87877b7593021032c Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Wed, 28 Apr 2010 19:51:34 +0000
Subject: [PATCH] adding integer and real types to the public interface

---
 src/expr/expr_manager_template.cpp | 10 ++++++++++
 src/expr/expr_manager_template.h   |  6 ++++++
 2 files changed, 16 insertions(+)

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
-- 
2.30.2