Throw exception for getting value of non-well-founded datatype (#7806)

Fixes cvc5/cvc5-projects#383

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1e5738ed8fcb969a5df7ce2d444b9b93dd68a607..4202a7fabe2886621dafe4134b4b620e5d38e529 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7312,6 +7312,9 @@ Term Solver::getValue(const Term& term) const
   CVC5_API_SOLVER_CHECK_TERM(term);
   CVC5_API_RECOVERABLE_CHECK(term.getSort().isFirstClass())
       << "Cannot get value of a term that is not first class.";
+  CVC5_API_RECOVERABLE_CHECK(!term.getSort().isDatatype()
+                             || term.getSort().getDatatype().isWellFounded())
+      << "Cannot get value of a term of non-well-founded datatype sort.";
   //////// all checks before this line
   return getValueHelper(term);
   ////////
@@ -7330,6 +7333,9 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   {
     CVC5_API_RECOVERABLE_CHECK(t.getSort().isFirstClass())
         << "Cannot get value of a term that is not first class.";
+    CVC5_API_RECOVERABLE_CHECK(!t.getSort().isDatatype()
+                               || t.getSort().getDatatype().isWellFounded())
+        << "Cannot get value of a term of non-well-founded datatype sort.";
   }
   CVC5_API_SOLVER_CHECK_TERMS(terms);
   //////// all checks before this line

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 54b6dc81f8dad5ab5dbb218cc7cfca879c6118e6..b170546374dc7bea012f7ea18af29366335f99d8 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2777,5 +2777,30 @@ TEST_F(TestApiBlackSolver, proj_issue381)
   ASSERT_NO_THROW(d_solver.simplify(t187));
 }
 
+TEST_F(TestApiBlackSolver, proj_issue383)
+{
+  d_solver.setOption("produce-models", "true");
+
+  Sort s1 = d_solver.getBooleanSort();
+
+  DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("_x5");
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0");
+  dtdecl.addConstructor(ctordecl);
+  Sort s2 = d_solver.mkDatatypeSort(dtdecl);
+
+  ctordecl = d_solver.mkDatatypeConstructorDecl("_x23");
+  ctordecl.addSelectorSelf("_x21");
+  dtdecl = d_solver.mkDatatypeDecl("_x12");
+  dtdecl.addConstructor(ctordecl);
+  Sort s4 = d_solver.mkDatatypeSort(dtdecl);
+  ASSERT_FALSE(s4.getDatatype().isWellFounded());
+
+  Term t3 = d_solver.mkConst(s4, "_x25");
+  Term t13 = d_solver.mkConst(s1, "_x34");
+
+  d_solver.checkEntailed(t13);
+  ASSERT_THROW(d_solver.getValue(t3), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5