From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 28 Apr 2010 19:51:34 +0000 (+0000)
Subject: adding integer and real types to the public interface
X-Git-Tag: cvc5-1.0.0~9102
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2482b19ea90183d5040390b87877b7593021032c;p=cvc5.git

adding integer and real types to the public interface
---

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