Some new Datatype public functionality, as per Chris Conway's suggestions on the dev mailing list.

2 files changed, 12 insertions, 0 deletions

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 0edc7579b..77cf97bb1 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -567,6 +567,10 @@ bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }
 
+Expr DatatypeType::getConstructor(std::string name) const {
+  return getDatatype().getConstructor(name);
+}
+
 bool DatatypeType::isInstantiated() const {
   return d_typeNode->isInstantiatedDatatype();
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index f470f0874..b5aa18262 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -535,6 +535,7 @@ public:
 
   /** Instantiate a sort using this sort constructor */
   SortType instantiate(const std::vector<Type>& params) const;
+
 };/* class SortConstructorType */
 
 /**
@@ -563,6 +564,7 @@ public:
    * @return the width of the bit-vector type (> 0)
    */
   unsigned getSize() const;
+
 };/* class BitVectorType */
 
 
@@ -583,6 +585,12 @@ public:
   bool isParametric() const;
 
   /**
+   * Get the constructor operator associated to the given constructor
+   * name in this datatype.
+   */
+  Expr getConstructor(std::string name) const;
+
+  /**
    * Has this datatype been fully instantiated ?
    *
    * @return true if this datatype is not parametric or, if it is, it