From e029a6ace6456008ab774776d5f74919eefc9529 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Dec 2021 11:50:56 -0600 Subject: [PATCH] Throw exception for getting value of non-well-founded datatype (#7806) Fixes cvc5/cvc5-projects#383 --- src/api/cpp/cvc5.cpp | 6 ++++++ test/unit/api/cpp/solver_black.cpp | 25 +++++++++++++++++++++++++ 2 files changed, 31 insertions(+) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1e5738ed8..4202a7fab 100644 --- 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 Solver::getValue(const std::vector& 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 54b6dc81f..b17054637 100644 --- 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 -- 2.30.2