From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 7 Oct 2011 14:57:38 +0000 (+0000)
Subject: Some new Datatype public functionality, as per Chris Conway's suggestions on the... 
X-Git-Tag: cvc5-1.0.0~8420
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a7aafccadbfa1543c435b7dfe4f53116224a11f;p=cvc5.git

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

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 */
 
 
@@ -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<std::string, DatatypeType>& resolutions,
                                     const std::vector<Type>& 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());