From 3a7aafccadbfa1543c435b7dfe4f53116224a11f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 7 Oct 2011 14:57:38 +0000 Subject: [PATCH] Some new Datatype public functionality, as per Chris Conway's suggestions on the dev mailing list. --- src/expr/type.cpp | 4 ++++ src/expr/type.h | 8 +++++++ src/util/datatype.cpp | 26 ++++++++++++++++++++++ src/util/datatype.h | 39 +++++++++++++++++++++++++++++++++ test/unit/util/datatype_black.h | 11 ++++++++++ 5 files changed, 88 insertions(+) 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& params) const; + };/* class SortConstructorType */ /** @@ -563,6 +564,7 @@ public: * @return the width of the bit-vector type (> 0) */ unsigned getSize() const; + };/* class BitVectorType */ @@ -582,6 +584,12 @@ public: /** Is this datatype parametric? */ 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 ? * diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 93651f1a9..7d7c654bf 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -364,6 +364,19 @@ const Datatype::Constructor& Datatype::operator[](size_t index) const { return d_constructors[index]; } +const Datatype::Constructor& Datatype::operator[](std::string name) const { + for(const_iterator i = begin(); i != end(); ++i) { + if((*i).getName() == name) { + return *i; + } + } + CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str()); +} + +Expr Datatype::getConstructor(std::string name) const { + return (*this)[name].getConstructor(); +} + void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, const std::map& resolutions, const std::vector& placeholders, @@ -674,6 +687,19 @@ const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index return d_args[index]; } +const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string name) const { + for(const_iterator i = begin(); i != end(); ++i) { + if((*i).getName() == name) { + return *i; + } + } + CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str()); +} + +Expr Datatype::Constructor::getSelector(std::string name) const { + return (*this)[name].getSelector(); +} + Datatype::Constructor::Arg::Arg(std::string name, Expr selector) : d_name(name), d_selector(selector), diff --git a/src/util/datatype.h b/src/util/datatype.h index b536cdf2b..24a625bd1 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -221,6 +221,14 @@ public: const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements); public: + /** + * Create a new Datatype constructor with the given name for the + * constructor and the same name (prefixed with "is_") for the + * tester. The actual constructor and tester aren't created until + * resolution time. + */ + explicit Constructor(std::string name); + /** * Create a new Datatype constructor with the given name for the * constructor and the given name for the tester. The actual @@ -257,16 +265,19 @@ public: /** Get the name of this Datatype constructor. */ std::string getName() const throw(); + /** * Get the constructor operator of this Datatype constructor. The * Datatype must be resolved. */ Expr getConstructor() const; + /** * Get the tester operator of this Datatype constructor. The * Datatype must be resolved. */ Expr getTester() const; + /** * Get the number of arguments (so far) of this Datatype constructor. */ @@ -323,6 +334,21 @@ public: /** Get the ith Constructor arg. */ const Arg& operator[](size_t index) const; + /** + * Get the Constructor arg named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the first is returned. + */ + const Arg& operator[](std::string name) const; + + /** + * Get the selector named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the selector for the first + * is returned. + */ + Expr getSelector(std::string name) const; + };/* class Datatype::Constructor */ /** The type for iterators over constructors. */ @@ -459,6 +485,19 @@ public: /** Get the ith Constructor. */ const Constructor& operator[](size_t index) const; + /** + * Get the Constructor named. This is a linear search + * through the constructors, so in the case of multiple, + * similarly-named constructors, the first is returned. + */ + const Constructor& operator[](std::string name) const; + + /** + * Get the constructor operator for the named constructor. + * This Datatype must be resolved. + */ + Expr getConstructor(std::string name) const; + };/* class Datatype */ diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index ea8d8a900..6d5584924 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -64,6 +64,12 @@ public: Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); Debug("datatypes") << apply << std::endl; + const Datatype& colorsDT = colorsType.getDatatype(); + TS_ASSERT(colorsDT.getConstructor("blue") == ctor); + TS_ASSERT(colorsDT["blue"].getConstructor() == ctor); + TS_ASSERT_THROWS(colorsDT["blue"].getSelector("foo"), IllegalArgumentException); + TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException); + TS_ASSERT(colorsType.getDatatype().isFinite()); TS_ASSERT(colorsType.getDatatype().getCardinality() == 4); TS_ASSERT(ctor.getType().getCardinality() == 1); @@ -137,6 +143,11 @@ public: DatatypeType treeType = d_em->mkDatatypeType(tree); Debug("datatypes") << treeType << std::endl; + Expr ctor = treeType.getDatatype()[1].getConstructor(); + TS_ASSERT(treeType.getConstructor("leaf") == ctor); + TS_ASSERT(treeType.getConstructor("leaf") == ctor); + TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException); + TS_ASSERT(! treeType.getDatatype().isFinite()); TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); TS_ASSERT(treeType.getDatatype().isWellFounded()); -- 2.30.2