diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/type.cpp | 4 | ||||
-rw-r--r-- | src/expr/type.h | 8 |
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 |