From 994c86b5dc4cc6d3a54f9fc1cdda593fd9372012 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 26 Jun 2024 11:55:19 -0700 Subject: [PATCH] c api: Add support for model value related functions. (#10881) --- include/cvc5/c/cvc5.h | 26 +-- include/cvc5/cvc5.h | 13 +- src/api/c/cvc5.cpp | 96 +++++++++ test/unit/api/c/capi_solver_black.cpp | 264 +++++++++++++++++++++++++ test/unit/api/c/capi_term_black.cpp | 72 ++++--- test/unit/api/cpp/api_solver_black.cpp | 15 +- 6 files changed, 423 insertions(+), 63 deletions(-) diff --git a/include/cvc5/c/cvc5.h b/include/cvc5/c/cvc5.h index 8efe88d543e..5469cd68768 100644 --- a/include/cvc5/c/cvc5.h +++ b/include/cvc5/c/cvc5.h @@ -3875,14 +3875,16 @@ Cvc5Term cvc5_get_value(Cvc5* cvc5, Cvc5Term term); * (get-value ( * )) * \endverbatim * - * @param cvc5 The solver instance. - * @param size The number of terms for which the value is queried. + * @param cvc5 The solver instance. + * @param size The number of terms for which the value is queried. * @param terms The terms. + * @param rsize The resulting size of the timeout core. * @return The values of the given terms. */ const Cvc5Term* cvc5_get_values(Cvc5* cvc5, size_t size, - const Cvc5Term terms[]); + const Cvc5Term terms[], + size_t* rsize); /** * Get the domain elements of uninterpreted sort s in the current model. The @@ -3890,27 +3892,29 @@ const Cvc5Term* cvc5_get_values(Cvc5* cvc5, * given in the return value of this function. * * @param cvc5 The solver instance. - * @param s The uninterpreted sort in question. + * @param sort The uninterpreted sort in question. * @param size The size of the resulting domain elements array. * @return The domain elements of s in the current model. */ const Cvc5Term* cvc5_get_model_domain_elements(Cvc5* cvc5, - Cvc5Sort s, + Cvc5Sort sort, size_t* size); /** - * This returns false if the model value of free constant v was not essential - * for showing the satisfiability of the last call to checkSat using the - * current model. This function will only return false (for any `v`) if - * option + * Determine if the model value of the given free constant was essential for + * showing satisfiability of the last `cvc5_check_sat()` query based on the + * current model. + * + * For any free constant `v`, this will only return false if * \verbatim embed:rst:inline :ref:`model-cores - * `\endverbatim has been set. + * `\endverbatim + * has been set to true. * * @warning This function is experimental and may change in future versions. * * @param cvc5 The solver instance. * @param v The term in question. - * @return True if `v` is a model core symbol. + * @return True if `v` was essential and is thus a model core symbol. */ bool cvc5_is_model_core_symbol(Cvc5* cvc5, Cvc5Term v); diff --git a/include/cvc5/cvc5.h b/include/cvc5/cvc5.h index ca6e2b27889..7b2cfc17ac5 100644 --- a/include/cvc5/cvc5.h +++ b/include/cvc5/cvc5.h @@ -6113,13 +6113,14 @@ class CVC5_EXPORT Solver std::vector getModelDomainElements(const Sort& s) const; /** - * This returns false if the model value of free constant v was not essential - * for showing the satisfiability of the last call to checkSat using the - * current model. This function will only return false (for any `v`) if - * option - * \verbatim embed:rst:inline :ref:`model-cores - * `\endverbatim has been set. + * Determine if the model value of the given free constant was essential for + * showing satisfiability of the last `checkSat()` query based on the current + * model. * + * For any free constant `v`, this will only return false if + * \verbatim embed:rst:inline :ref:`model-cores + * `\endverbatim + * has been set to true. * @warning This function is experimental and may change in future versions. * * @param v The term in question. diff --git a/src/api/c/cvc5.cpp b/src/api/c/cvc5.cpp index 4d24763bb4c..fb5ae2d4daf 100644 --- a/src/api/c/cvc5.cpp +++ b/src/api/c/cvc5.cpp @@ -5109,6 +5109,102 @@ const Cvc5Term* cvc5_get_learned_literals(Cvc5* cvc5, return res.data(); } +Cvc5Term cvc5_get_value(Cvc5* cvc5, Cvc5Term term) +{ + Cvc5Term res = nullptr; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_TERM(term); + res = cvc5->d_tm->export_term(cvc5->d_solver.getValue(term->d_term)); + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +const Cvc5Term* cvc5_get_values(Cvc5* cvc5, + size_t size, + const Cvc5Term terms[], + size_t* rsize) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_NOT_NULL(terms); + CVC5_CAPI_CHECK_NOT_NULL(rsize); + res.clear(); + std::vector cterms; + for (size_t i = 0; i < size; ++i) + { + cterms.push_back(terms[i]->d_term); + } + auto values = cvc5->d_solver.getValue(cterms); + for (const auto& t : values) + { + res.push_back(cvc5->d_tm->export_term(t)); + } + *rsize = res.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + +const Cvc5Term* cvc5_get_model_domain_elements(Cvc5* cvc5, + Cvc5Sort sort, + size_t* size) +{ + static thread_local std::vector res; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_SORT(sort); + CVC5_CAPI_CHECK_NOT_NULL(size); + res.clear(); + auto elems = cvc5->d_solver.getModelDomainElements(sort->d_sort); + for (const auto& t : elems) + { + res.push_back(cvc5->d_tm->export_term(t)); + } + *size = res.size(); + CVC5_CAPI_TRY_CATCH_END; + return res.data(); +} + +bool cvc5_is_model_core_symbol(Cvc5* cvc5, Cvc5Term v) +{ + bool res = false; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + if (v) + { + res = cvc5->d_solver.isModelCoreSymbol(v->d_term); + } + CVC5_CAPI_TRY_CATCH_END; + return res; +} + +const char* cvc5_get_model(Cvc5* cvc5, + size_t nsorts, + const Cvc5Sort sorts[], + size_t nconsts, + const Cvc5Term consts[]) +{ + static thread_local std::string str; + CVC5_CAPI_TRY_CATCH_BEGIN; + CVC5_CAPI_CHECK_NOT_NULL(cvc5); + CVC5_CAPI_CHECK_NOT_NULL(sorts); + CVC5_CAPI_CHECK_NOT_NULL(consts); + std::vector csorts; + for (size_t i = 0; i < nsorts; ++i) + { + csorts.push_back(sorts[i]->d_sort); + } + std::vector cconsts; + for (size_t i = 0; i < nconsts; ++i) + { + cconsts.push_back(consts[i]->d_term); + } + str = cvc5->d_solver.getModel(csorts, cconsts); + CVC5_CAPI_TRY_CATCH_END; + return str.c_str(); +} + void cvc5_push(Cvc5* cvc5, uint32_t nscopes) { CVC5_CAPI_TRY_CATCH_BEGIN; diff --git a/test/unit/api/c/capi_solver_black.cpp b/test/unit/api/c/capi_solver_black.cpp index e964d407dae..ec382b85329 100644 --- a/test/unit/api/c/capi_solver_black.cpp +++ b/test/unit/api/c/capi_solver_black.cpp @@ -1704,6 +1704,270 @@ TEST_F(TestCApiBlackSolver, get_learned_literals2) (void)cvc5_get_learned_literals(d_solver, CVC5_LEARNED_LIT_TYPE_INPUT, &size); } +TEST_F(TestCApiBlackSolver, get_value1) +{ + cvc5_set_option(d_solver, "produce-models", "false"); + Cvc5Term t = cvc5_mk_true(d_tm); + cvc5_assert_formula(d_solver, t); + cvc5_check_sat(d_solver); + ASSERT_DEATH(cvc5_get_value(d_solver, t), "cannot get value"); +} + +TEST_F(TestCApiBlackSolver, get_value2) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + Cvc5Term t = cvc5_mk_false(d_tm); + cvc5_assert_formula(d_solver, t); + cvc5_check_sat(d_solver); + ASSERT_DEATH(cvc5_get_value(d_solver, t), "cannot get value"); +} + +TEST_F(TestCApiBlackSolver, get_value3) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + + std::vector domain = {d_uninterpreted}; + Cvc5Sort u_to_int = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int); + domain = {d_int}; + Cvc5Sort int_pred = + cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool); + + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z"); + Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f"); + Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1); + std::vector args = {f, x}; + Cvc5Term f_x = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f, y}; + Cvc5Term f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {f_x, f_y}; + Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data()); + args = {p, zero}; + Cvc5Term p_0 = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + args = {p, f_y}; + Cvc5Term p_f_y = + cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()); + + args = {zero, f_x}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data())); + args = {zero, f_y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data())); + args = {sum, one}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data())); + args = {p_0}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())); + cvc5_assert_formula(d_solver, p_f_y); + ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver))); + + (void)cvc5_get_value(d_solver, x); + (void)cvc5_get_value(d_solver, y); + (void)cvc5_get_value(d_solver, z); + (void)cvc5_get_value(d_solver, sum); + (void)cvc5_get_value(d_solver, p_f_y); + + ASSERT_DEATH(cvc5_get_value(nullptr, x), "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_value(d_solver, nullptr), "invalid term"); + + std::vector a = {cvc5_get_value(d_solver, x), + cvc5_get_value(d_solver, y), + cvc5_get_value(d_solver, z)}; + size_t size; + std::vector terms = {x, y, z}; + const Cvc5Term* b = + cvc5_get_values(d_solver, terms.size(), terms.data(), &size); + ASSERT_EQ(size, 3); + ASSERT_TRUE(cvc5_term_is_equal(a[0], b[0])); + ASSERT_TRUE(cvc5_term_is_equal(a[1], b[1])); + ASSERT_DEATH(cvc5_get_values(nullptr, terms.size(), terms.data(), &size), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_values(d_solver, terms.size(), nullptr, &size), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_values(d_solver, terms.size(), terms.data(), nullptr), + "unexpected NULL argument"); + + Cvc5* slv = cvc5_new(d_tm); + ASSERT_DEATH(cvc5_get_value(slv, x), "cannot get value"); + cvc5_delete(slv); + + slv = cvc5_new(d_tm); + cvc5_set_option(slv, "produce-models", "true"); + ASSERT_DEATH(cvc5_get_value(slv, x), "cannot get value"); + cvc5_delete(slv); + + slv = cvc5_new(d_tm); + cvc5_set_option(slv, "produce-models", "true"); + cvc5_check_sat(slv); + (void)cvc5_get_value(slv, x); + cvc5_delete(slv); + + Cvc5TermManager* tm = cvc5_term_manager_new(); + slv = cvc5_new(tm); + cvc5_set_option(slv, "produce-models", "true"); + cvc5_check_sat(slv); + // this will throw when NodeManager is not a singleton anymore + (void)cvc5_get_value(slv, x); + cvc5_delete(slv); + cvc5_term_manager_delete(tm); +} + +TEST_F(TestCApiBlackSolver, get_modelDomain_elements) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z"); + std::vector args = {x, y, z}; + Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()); + cvc5_assert_formula(d_solver, f); + cvc5_check_sat(d_solver); + size_t size; + (void)cvc5_get_model_domain_elements(d_solver, d_uninterpreted, &size); + ASSERT_TRUE(size >= 3); + ASSERT_DEATH(cvc5_get_model_domain_elements(nullptr, d_uninterpreted, &size), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_model_domain_elements(d_solver, nullptr, &size), + "invalid sort"); + ASSERT_DEATH( + cvc5_get_model_domain_elements(d_solver, d_uninterpreted, nullptr), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_model_domain_elements(d_solver, d_int, &size), + "expected an uninterpreted sort"); + + Cvc5TermManager* tm = cvc5_term_manager_new(); + Cvc5* slv = cvc5_new(tm); + cvc5_set_option(slv, "produce-models", "true"); + cvc5_check_sat(slv); + // this will throw when NodeManager is not a singleton anymore + (void)cvc5_get_model_domain_elements(slv, d_uninterpreted, &size); + cvc5_delete(slv); + cvc5_term_manager_delete(tm); +} + +TEST_F(TestCApiBlackSolver, getModel_domain_elements2) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + cvc5_set_option(d_solver, "finite-model-find", "true"); + Cvc5Term x = cvc5_mk_var(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_var(d_tm, d_uninterpreted, "y"); + std::vector args = {x, y}; + Cvc5Term eq = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()); + Cvc5Term bvl = + cvc5_mk_term(d_tm, CVC5_KIND_VARIABLE_LIST, args.size(), args.data()); + args = {bvl, eq}; + Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_FORALL, args.size(), args.data()); + cvc5_assert_formula(d_solver, f); + cvc5_check_sat(d_solver); + size_t size; + (void)cvc5_get_model_domain_elements(d_solver, d_uninterpreted, &size); + // a model for the above must interpret u as size 1 + ASSERT_EQ(size, 1); +} + +TEST_F(TestCApiBlackSolver, is_model_core_symbol) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + cvc5_set_option(d_solver, "model-cores", "simple"); + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z"); + Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0); + std::vector args = {x, y}; + args = {cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data())}; + Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()); + cvc5_assert_formula(d_solver, f); + cvc5_check_sat(d_solver); + ASSERT_TRUE(cvc5_is_model_core_symbol(d_solver, x)); + ASSERT_TRUE(cvc5_is_model_core_symbol(d_solver, y)); + ASSERT_FALSE(cvc5_is_model_core_symbol(d_solver, z)); + + ASSERT_DEATH(cvc5_is_model_core_symbol(nullptr, x), + "unexpected NULL argument"); + ASSERT_FALSE(cvc5_is_model_core_symbol(d_solver, nullptr)); + ASSERT_DEATH(cvc5_is_model_core_symbol(d_solver, zero), + "expected a free constant"); + + Cvc5TermManager* tm = cvc5_term_manager_new(); + Cvc5* slv = cvc5_new(tm); + cvc5_set_option(slv, "produce-models", "true"); + cvc5_check_sat(slv); + // this will throw when NodeManager is not a singleton anymore + (void)cvc5_is_model_core_symbol(slv, x); + cvc5_delete(slv); + cvc5_term_manager_delete(tm); +} + +TEST_F(TestCApiBlackSolver, get_model) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + std::vector args = {x, y}; + args = {cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data())}; + Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()); + cvc5_assert_formula(d_solver, f); + cvc5_check_sat(d_solver); + + std::vector sorts = {d_uninterpreted}; + std::vector terms = {x, y}; + (void)cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()); + + ASSERT_DEATH( + cvc5_get_model( + nullptr, sorts.size(), sorts.data(), terms.size(), terms.data()), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_model( + d_solver, sorts.size(), nullptr, terms.size(), terms.data()), + "unexpected NULL argument"); + ASSERT_DEATH(cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), nullptr), + "unexpected NULL argument"); + terms.push_back(nullptr); + ASSERT_DEATH( + cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()), + ""); +} + +TEST_F(TestCApiBlackSolver, get_model2) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + std::vector sorts; + std::vector terms; + ASSERT_DEATH( + cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()), + "unexpected NULL argument"); +} + +TEST_F(TestCApiBlackSolver, get_model3) +{ + cvc5_set_option(d_solver, "produce-models", "true"); + std::vector sorts; + std::vector terms; + cvc5_check_sat(d_solver); + ASSERT_DEATH( + cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()), + "unexpected NULL argument"); + sorts.push_back(d_int); + ASSERT_DEATH( + cvc5_get_model( + d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()), + "unexpected NULL argument"); +} + TEST_F(TestCApiBlackSolver, push1) { cvc5_set_option(d_solver, "incremental", "true"); diff --git a/test/unit/api/c/capi_term_black.cpp b/test/unit/api/c/capi_term_black.cpp index d0c63bb31d6..d0853f83db8 100644 --- a/test/unit/api/c/capi_term_black.cpp +++ b/test/unit/api/c/capi_term_black.cpp @@ -729,21 +729,20 @@ TEST_F(TestCApiBlackTerm, get_ff_value) TEST_F(TestCApiBlackTerm, get_uninterpreted_sort_value) { ASSERT_DEATH(cvc5_term_get_uninterpreted_sort_value(nullptr), "invalid term"); - // cvc5_set_option(d_solver, "produce-models", "true"); - // Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); - // Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); - // std::vector args = {x, y}; - // cvc5_assert_formula( - // d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), - // args.data())); - // Cvc5Result res = cvc5_check_sat(d_solver); - // ASSERT_TRUE(cvc5_result_is_sat(res)); - // Cvc5Term vx = cvc5_get_value(d_solver, x); - // Cvc5Term vy = cvc5_get_value(d_solver, y); - // ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vx)); - // ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vy)); - // ASSERT_TRUE(cvc5_term_is_equal(cvc5_term_get_uninterpreted_sort_value(vx), - // cvc5_term_get_uninterpreted_sort_value(vy))); + cvc5_set_option(d_solver, "produce-models", "true"); + Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x"); + Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y"); + std::vector args = {x, y}; + cvc5_assert_formula( + d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data())); + Cvc5Result res = cvc5_check_sat(d_solver); + ASSERT_TRUE(cvc5_result_is_sat(res)); + Cvc5Term vx = cvc5_get_value(d_solver, x); + Cvc5Term vy = cvc5_get_value(d_solver, y); + ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vx)); + ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vy)); + ASSERT_EQ(std::string(cvc5_term_get_uninterpreted_sort_value(vx)), + cvc5_term_get_uninterpreted_sort_value(vy)); } TEST_F(TestCApiBlackTerm, is_rm_value) @@ -1117,28 +1116,27 @@ TEST_F(TestCApiBlackTerm, get_real_algebraic_number) // Note that check-sat should only return "sat" if libpoly is enabled. // Otherwise, we do not test the following functionality. - // if (cvc5_result_is_sat(cvc5_check_sat(d_solver))) - //{ - // // We find a model for (x*x = 2), where x should be a real algebraic - // number. - // // We assert that its defining polynomial is non-null and its lower and - // // upper bounds are real. - // Cvc5Term vx = cvc5_get_value(d_solver, x); - // ASSERT_TRUE(cvc5_term_is_real_algebraic_number(vx)); - // Cvc5Term poly = - // cvc5_term_get_real_algebraic_number_defining_polynomial(vx, y); - // ASSERT_NE(poly, nullptr); - - // Cvc5Term lb = cvc5_term_get_real_algebraic_number_lower_bound(vx); - // Cvc5Term ub = cvc5_term_get_real_algebraic_number_upper_bound(vx); - // ASSERT_TRUE(cvc5_term_is_real_value(lb)); - // ASSERT_TRUE(cvc5_term_is_real_value(ub)); - // // cannot call with non-variable - // Cvc5Term yc = cvc5_mk_const(d_tm, d_real, "y"); - // ASSERT_DEATH( - // cvc5_term_get_real_algebraic_number_defining_polynomial(vx, yc), - // "asdf"); - //} + if (cvc5_result_is_sat(cvc5_check_sat(d_solver))) + { + // We find a model for (x*x = 2), where x should be a real algebraic number. + // We assert that its defining polynomial is non-null and its lower and + // upper bounds are real. + Cvc5Term vx = cvc5_get_value(d_solver, x); + ASSERT_TRUE(cvc5_term_is_real_algebraic_number(vx)); + Cvc5Term poly = + cvc5_term_get_real_algebraic_number_defining_polynomial(vx, y); + ASSERT_NE(poly, nullptr); + + Cvc5Term lb = cvc5_term_get_real_algebraic_number_lower_bound(vx); + Cvc5Term ub = cvc5_term_get_real_algebraic_number_upper_bound(vx); + ASSERT_TRUE(cvc5_term_is_real_value(lb)); + ASSERT_TRUE(cvc5_term_is_real_value(ub)); + // cannot call with non-variable + Cvc5Term yc = cvc5_mk_const(d_tm, d_real, "y"); + ASSERT_DEATH( + cvc5_term_get_real_algebraic_number_defining_polynomial(vx, yc), + "invalid argument"); + } } TEST_F(TestCApiBlackTerm, get_skolem) diff --git a/test/unit/api/cpp/api_solver_black.cpp b/test/unit/api/cpp/api_solver_black.cpp index 7f3cbbead4b..d29b0b12c20 100644 --- a/test/unit/api/cpp/api_solver_black.cpp +++ b/test/unit/api/cpp/api_solver_black.cpp @@ -1493,8 +1493,8 @@ TEST_F(TestApiBlackSolver, getModelDomainElements) Term f = d_tm.mkTerm(Kind::DISTINCT, {x, y, z}); d_solver->assertFormula(f); d_solver->checkSat(); - ASSERT_NO_THROW(d_solver->getModelDomainElements(uSort)); - ASSERT_TRUE(d_solver->getModelDomainElements(uSort).size() >= 3); + auto elems = d_solver->getModelDomainElements(uSort); + ASSERT_TRUE(elems.size() >= 3); ASSERT_THROW(d_solver->getModelDomainElements(intSort), CVC5ApiException); TermManager tm; @@ -1517,9 +1517,9 @@ TEST_F(TestApiBlackSolver, getModelDomainElements2) Term f = d_tm.mkTerm(Kind::FORALL, {bvl, eq}); d_solver->assertFormula(f); d_solver->checkSat(); - ASSERT_NO_THROW(d_solver->getModelDomainElements(uSort)); + auto elems = d_solver->getModelDomainElements(uSort); // a model for the above must interpret u as size 1 - ASSERT_TRUE(d_solver->getModelDomainElements(uSort).size() == 1); + ASSERT_TRUE(elems.size() == 1); } TEST_F(TestApiBlackSolver, isModelCoreSymbol) @@ -1557,11 +1557,8 @@ TEST_F(TestApiBlackSolver, getModel) Term f = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::EQUAL, {x, y})}); d_solver->assertFormula(f); d_solver->checkSat(); - std::vector sorts; - sorts.push_back(uSort); - std::vector terms; - terms.push_back(x); - terms.push_back(y); + std::vector sorts{uSort}; + std::vector terms{x, y}; ASSERT_NO_THROW(d_solver->getModel(sorts, terms)); Term null; terms.push_back(null);