diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 11:50:56 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 17:50:56 +0000 |
| commit | e029a6ace6456008ab774776d5f74919eefc9529 (patch) | |
| tree | 97b3fcf28c2c6069b973fa314c73aa3f718cc644 | |
| parent | 2abdb475ad265c33f1b1658b965bc5b2387313ed (diff) | |
Throw exception for getting value of non-well-founded datatype (#7806)
Fixes cvc5/cvc5-projects#383
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 6 | ||||
| -rw-r--r-- | test/unit/api/cpp/solver_black.cpp | 25 |
2 files changed, 31 insertions, 0 deletions
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<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 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 |