1 files changed, 15 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 488590deb..938dc127d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2213,5 +2213,20 @@ std::vector<Expr> Solver::termVectorToExprs(
   return res;
 }
 
+/**
+ *  ( declare-datatype <symbol> <datatype_decl> )
+ */
+Sort Solver::declareDatatype(
+    const std::string& symbol,
+    const std::vector<DatatypeConstructorDecl>& ctors) const
+{
+  DatatypeDecl dtdecl(symbol);
+  for (const DatatypeConstructorDecl& ctor : ctors)
+  {
+    dtdecl.addConstructor(ctor);
+  }
+  return mkDatatypeSort(dtdecl);
+}
+
 }  // namespace api
 }  // namespace CVC4