From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 13 Jul 2018 08:57:24 +0000 (-0700)
Subject: New C++ API: Implementation of datatype classes. (#2142)
X-Git-Tag: cvc5-1.0.0~4900
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99465e5ed6ee1415c060dc89cc666b562045cf20;p=cvc5.git

New C++ API: Implementation of datatype classes. (#2142)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ceed73d5b..958438751 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -769,7 +769,6 @@ bool Sort::isSortConstructor() const
   return d_type->isSortConstructor();
 }
 
-#if 0
 Datatype Sort::getDatatype() const
 {
   // CHECK: is this a datatype sort?
@@ -791,7 +790,6 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   Assert (d_type->isSortConstructor());
   return static_cast<SortConstructorType*>(d_type.get())->instantiate(tparams);
 }
-#endif
 
 std::string Sort::toString() const
 {
@@ -1209,6 +1207,255 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+/* DatatypeSelector --------------------------------------------------------- */
+
+DatatypeSelector::DatatypeSelector()
+{
+  d_stor = nullptr;
+}
+
+DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
+    : d_stor(new CVC4::DatatypeConstructorArg(stor))
+{
+}
+
+DatatypeSelector::~DatatypeSelector()
+{
+}
+
+std::string DatatypeSelector::toString() const
+{
+  std::stringstream ss;
+  ss << *d_stor;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
+{
+  out << stor.toString();
+  return out;
+}
+
+/* DatatypeConstructor ------------------------------------------------------ */
+
+DatatypeConstructor::DatatypeConstructor()
+{
+  d_ctor = nullptr;
+}
+
+DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
+: d_ctor(new CVC4::DatatypeConstructor(ctor))
+{
+}
+
+DatatypeConstructor::~DatatypeConstructor()
+{
+}
+
+DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
+{
+  // CHECK: selector with name exists?
+  // CHECK: is resolved?
+  return (*d_ctor)[name];
+}
+
+DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_ctor)[name];
+}
+
+Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return d_ctor->getSelector(name);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
+{
+  return DatatypeConstructor::const_iterator(*d_ctor, true);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::end() const
+{
+  return DatatypeConstructor::const_iterator(*d_ctor, false);
+}
+
+DatatypeConstructor::const_iterator::const_iterator(
+    const CVC4::DatatypeConstructor& ctor, bool begin)
+{
+  d_int_stors = ctor.getArgs();
+  const std::vector<CVC4::DatatypeConstructorArg>* sels =
+      static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
+          d_int_stors);
+  for (const auto& s : *sels)
+  {
+    /* Can not use emplace_back here since constructor is private. */
+    d_stors.push_back(DatatypeSelector(s));
+  }
+  d_idx = begin ? 0 : sels->size();
+}
+
+DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
+operator=(const DatatypeConstructor::const_iterator& it)
+{
+  d_int_stors = it.d_int_stors;
+  d_stors = it.d_stors;
+  d_idx = it.d_idx;
+  return *this;
+}
+
+const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const
+{
+  return d_stors[d_idx];
+}
+
+const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const
+{
+  return &d_stors[d_idx];
+}
+
+DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
+operator++()
+{
+  ++d_idx;
+  return *this;
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::const_iterator::
+operator++(int)
+{
+  DatatypeConstructor::const_iterator it(*this);
+  ++d_idx;
+  return it;
+}
+
+bool DatatypeConstructor::const_iterator::operator==(
+    const DatatypeConstructor::const_iterator& other) const
+{
+  return d_int_stors == other.d_int_stors && d_idx == other.d_idx;
+}
+
+bool DatatypeConstructor::const_iterator::operator!=(
+    const DatatypeConstructor::const_iterator& other) const
+{
+  return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
+}
+
+std::string DatatypeConstructor::toString() const
+{
+  std::stringstream ss;
+  ss << *d_ctor;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
+{
+  out << ctor.toString();
+  return out;
+}
+
+/* Datatype ----------------------------------------------------------------- */
+
+Datatype::Datatype(const CVC4::Datatype& dtype)
+: d_dtype(new CVC4::Datatype(dtype))
+{
+}
+
+Datatype::~Datatype()
+{
+}
+
+DatatypeConstructor Datatype::operator[](const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_dtype)[name];
+}
+
+DatatypeConstructor Datatype::getConstructor(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_dtype)[name];
+}
+
+Term Datatype::getConstructorTerm(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return d_dtype->getConstructor(name);
+}
+
+Datatype::const_iterator Datatype::begin() const
+{
+  return Datatype::const_iterator(*d_dtype, true);
+}
+
+Datatype::const_iterator Datatype::end() const
+{
+  return Datatype::const_iterator(*d_dtype, false);
+}
+
+Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin)
+{
+  d_int_ctors = dtype.getConstructors();
+  const std::vector<CVC4::DatatypeConstructor>* cons =
+    static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
+  for (const auto& c : *cons)
+  {
+    /* Can not use emplace_back here since constructor is private. */
+    d_ctors.push_back(DatatypeConstructor(c));
+  }
+  d_idx = begin ? 0 : cons->size();
+}
+
+Datatype::const_iterator& Datatype::const_iterator::operator=(
+    const Datatype::const_iterator& it)
+{
+  d_int_ctors = it.d_int_ctors;
+  d_ctors = it.d_ctors;
+  d_idx = it.d_idx;
+  return *this;
+}
+
+const DatatypeConstructor& Datatype::const_iterator::operator*() const
+{
+  return d_ctors[d_idx];
+}
+
+const DatatypeConstructor* Datatype::const_iterator::operator->() const
+{
+  return &d_ctors[d_idx];
+}
+
+Datatype::const_iterator& Datatype::const_iterator::operator++()
+{
+  ++d_idx;
+  return *this;
+}
+
+Datatype::const_iterator Datatype::const_iterator::operator++(int)
+{
+  Datatype::const_iterator it(*this);
+  ++d_idx;
+  return it;
+}
+
+bool Datatype::const_iterator::operator==(
+    const Datatype::const_iterator& other) const
+{
+  return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx;
+}
+
+bool Datatype::const_iterator::operator!=(
+    const Datatype::const_iterator& other) const
+{
+  return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
+}
+
 /* -------------------------------------------------------------------------- */
 /* Rounding Mode for Floating Points                                          */
 /* -------------------------------------------------------------------------- */
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 9b33b314c..8747c530e 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -695,6 +695,11 @@ bool Datatype::involvesUninterpretedType() const{
   return d_involvesUt;
 }
 
+const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
+{
+  return &d_constructors;
+}
+
 void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::map<std::string, DatatypeType>& resolutions,
                                   const std::vector<Type>& placeholders,
@@ -834,6 +839,12 @@ void DatatypeConstructor::setSygus(Expr op,
   d_sygus_pc = spc;
 }
 
+const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
+    const
+{
+  return &d_args;
+}
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a56a4f993..c2cf80158 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -450,6 +450,11 @@ class CVC4_PUBLIC DatatypeConstructor {
    */
   void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
 
+  /**
+   * Get the list of arguments to this constructor.
+   */
+  const std::vector<DatatypeConstructorArg>* getArgs() const;
+
  private:
   /** the name of the constructor */
   std::string d_name;
@@ -938,6 +943,11 @@ public:
    */
   bool involvesUninterpretedType() const;
 
+  /**
+   * Get the list of constructors.
+   */
+  const std::vector<DatatypeConstructor>* getConstructors() const;
+
  private:
   /** name of this datatype */
   std::string d_name;