From 3e9c44a361d287d30d4aa9771f77677a025a766e Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 4 Jul 2018 08:10:27 -0700
Subject: [PATCH] New C++ API: Implementation of datatype declaration classes.
 (#2136)

---
 src/api/cvc4cpp.cpp | 112 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 112 insertions(+)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 703c298d3..6d5a423e4 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1092,5 +1092,117 @@ size_t OpTermHashFunction::operator()(const OpTerm& t) const
   return ExprHashFunction()(*t.d_expr);
 }
 
+/* -------------------------------------------------------------------------- */
+/* Datatypes                                                                  */
+/* -------------------------------------------------------------------------- */
+
+/* DatatypeSelectorDecl ----------------------------------------------------- */
+
+DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort)
+    : d_name(name), d_sort(sort)
+{
+}
+
+DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name,
+                                           DatatypeDeclSelfSort sort)
+    : d_name(name), d_sort(Sort(CVC4::Type()))
+{
+}
+
+std::string DatatypeSelectorDecl::toString() const
+{
+  std::stringstream ss;
+  ss << d_name << ": " << d_sort;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
+{
+  out << dtdecl.toString();
+  return out;
+}
+
+/* DatatypeConstructorDecl -------------------------------------------------- */
+
+DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
+    : d_ctor(new CVC4::DatatypeConstructor(name))
+{
+}
+
+void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor)
+{
+  CVC4::Type t = *stor.d_sort.d_type;
+  if (t.isNull())
+  {
+    d_ctor->addArg(stor.d_name, DatatypeSelfType());
+  }
+  else
+  {
+    d_ctor->addArg(stor.d_name, t);
+  }
+}
+
+std::string DatatypeConstructorDecl::toString() const
+{
+  std::stringstream ss;
+  ss << *d_ctor;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out,
+                         const DatatypeConstructorDecl& ctordecl)
+{
+  out << ctordecl.toString();
+  return out;
+}
+
+/* DatatypeDecl ------------------------------------------------------------- */
+
+DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype)
+    : d_dtype(new CVC4::Datatype(name, isCoDatatype))
+{
+}
+
+DatatypeDecl::DatatypeDecl(const std::string& name,
+                           Sort param,
+                           bool isCoDatatype)
+    : d_dtype(new CVC4::Datatype(
+          name, std::vector<Type>{*param.d_type}, isCoDatatype))
+{
+}
+
+DatatypeDecl::DatatypeDecl(const std::string& name,
+                           const std::vector<Sort>& params,
+                           bool isCoDatatype)
+{
+  std::vector<Type> tparams;
+  for (const Sort& s : params) { tparams.push_back(*s.d_type); }
+  d_dtype = std::shared_ptr<CVC4::Datatype>(
+      new CVC4::Datatype(name, tparams, isCoDatatype));
+}
+
+DatatypeDecl::~DatatypeDecl()
+{
+}
+
+void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
+{
+  d_dtype->addConstructor(*ctor.d_ctor);
+}
+
+std::string DatatypeDecl::toString() const
+{
+  std::stringstream ss;
+  ss << *d_dtype;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out,
+                         const DatatypeSelectorDecl& stordecl)
+{
+  out << stordecl.toString();
+  return out;
+}
+
 }  // namespace api
 }  // namespace CVC4
-- 
2.30.2