Proper error for using constructor in multiple datatypes (#7738)

Now gives error cannot use a constructor for multiple datatypes.

Fixes cvc5/cvc5-projects#372.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 9e398b518d417f66c12232134917811447ccb974..39410a4e67d15da912bf5e0aec02528a4b7b5e4d 100644 (file)
--- 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 cd448123a8f7a0549239b7bbbe0c6b8e43d67e45..61c7bb284252ab58e8f3c8c4ff43b7bd3fb8d5f3 100644 (file)
--- 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 6e5c142571a81eda5819beb1f09bb72637048bce..66a35a1afe1ae4a2fccb153c7f8dcc34b5d0d5cd 100644 (file)
--- 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