From 9dcbbeb865a1efd1575811cab5da8dba08560b2f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 3 Dec 2021 11:57:11 -0600
Subject: [PATCH] Proper error for using constructor in multiple datatypes
 (#7738)

Now gives error cannot use a constructor for multiple datatypes.

Fixes cvc5/cvc5-projects#372.
---
 src/api/cpp/cvc5.cpp               | 10 ++++++++++
 src/api/cpp/cvc5.h                 |  6 ++++++
 test/unit/api/cpp/solver_black.cpp | 10 ++++++++++
 3 files changed, 26 insertions(+)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9e398b518..39410a4e6 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3558,6 +3558,11 @@ std::ostream& operator<<(std::ostream& out,
 
 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor == nullptr; }
 
+bool DatatypeConstructorDecl::isResolved() const
+{
+  return d_ctor == nullptr || d_ctor->isResolved();
+}
+
 /* DatatypeDecl ------------------------------------------------------------- */
 
 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
@@ -6737,6 +6742,11 @@ Sort Solver::declareDatatype(
   CVC5_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
       << "a datatype declaration with at least one constructor";
   CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors);
+  for (size_t i = 0, size = ctors.size(); i < size; i++)
+  {
+    CVC5_API_CHECK(!ctors[i].isResolved())
+        << "cannot use a constructor for multiple datatypes";
+  }
   //////// all checks before this line
   DatatypeDecl dtdecl(this, symbol);
   for (size_t i = 0, size = ctors.size(); i < size; i++)
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index cd448123a..61c7bb284 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1725,6 +1725,12 @@ class CVC5_EXPORT DatatypeConstructorDecl
    */
   bool isNullHelper() const;
 
+  /**
+   * Is the underlying constructor resolved (i.e. has it been used to declare
+   * a datatype already)?
+   */
+  bool isResolved() const;
+
   /**
    * The associated solver object.
    */
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 6e5c14257..66a35a1af 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2642,5 +2642,15 @@ TEST_F(TestApiBlackSolver, issue5893)
   ASSERT_NO_FATAL_FAILURE(distinct.getOp());
 }
 
+TEST_F(TestApiBlackSolver, doubleUseCons)
+{
+  DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
+  DatatypeConstructorDecl ctor2 = d_solver.mkDatatypeConstructorDecl("_x31");
+  Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
+
+  ASSERT_THROW(d_solver.declareDatatype(std::string("_x86"), {ctor1, ctor2}),
+               CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5
-- 
2.30.2