From 8ae7340ebbca62f9291b35640dddc27a5089b61f Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Tue, 31 Oct 2023 23:09:12 -0700 Subject: [PATCH 1/5] adds the model-with-hint api method --- src/api/yices_api.c | 77 ++++++++++++++++++++++++++++++++++++ src/context/context.h | 18 +++++++++ src/context/context_solver.c | 10 +++++ src/include/yices.h | 54 ++++++++++++++++++++++++- src/mcsat/no_mcsat.c | 3 ++ src/mcsat/solver.c | 36 +++++++++++++++++ src/mcsat/solver.h | 8 ++++ src/mcsat/value.c | 18 +++++++-- 8 files changed, 220 insertions(+), 4 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 06b8b35f9..797420b26 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -9240,6 +9240,83 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param } +/* + * Check context with model and hint + * - param = parameter for check sat (or NULL for default parameters) + * - mdl = a model + * - t = array of n variables or uninterpred terms + * - m = number of terms that are asserted to be equal to their model values, + * the remaining are treated as hints + * + * This checks ctx /\ t[0] = val(mdl, t[0]) /\ .... /\ t[m-1] = val(mdl, t[m-1]) + */ +EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) { + + param_t default_params; + smt_status_t stat; + + if (! context_has_mcsat(ctx)) { + set_error_code(CTX_OPERATION_NOT_SUPPORTED); + return STATUS_ERROR; + } + + if (! good_terms_for_check_with_model(n, t)) { + // this sets the error code already (to VARIABLE_REQUIRED) + // but Dejan created another error code that means the same thing here. + set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + return STATUS_ERROR; + } + + // cleanup + switch (context_status(ctx)) { + case STATUS_UNKNOWN: + case STATUS_SAT: + if (! context_supports_multichecks(ctx)) { + set_error_code(CTX_OPERATION_NOT_SUPPORTED); + return STATUS_ERROR; + } + context_clear(ctx); + break; + + case STATUS_IDLE: + break; + + case STATUS_UNSAT: + context_clear_unsat(ctx); + if (context_status(ctx) == STATUS_UNSAT) { + return STATUS_UNSAT; + } + break; + + case STATUS_SEARCHING: + case YICES_STATUS_INTERRUPTED: + set_error_code(CTX_INVALID_OPERATION); + return STATUS_ERROR; + + case STATUS_ERROR: + default: + set_error_code(INTERNAL_EXCEPTION); + return STATUS_ERROR; + } + + assert(context_status(ctx) == STATUS_IDLE); + + // set parameters + if (params == NULL) { + yices_default_params_for_context(ctx, &default_params); + params = &default_params; + } + + // call check + stat = check_context_with_model_and_hint(ctx, params, mdl, n, t, m); + if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) { + context_cleanup(ctx); + } + + return stat; +} + + /* * CHECK SAT AND COMPUTE INTERPOLANT diff --git a/src/context/context.h b/src/context/context.h index d67f7a4d0..3b2cc12db 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -242,6 +242,24 @@ extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t extern smt_status_t check_context_with_model(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]); +/* + * Check satisfiability under model with hint: check whether the assertions stored in ctx + * conjoined with the assignment that the model gives to t is satisfiable. + * + * - params is an optional structure to store heuristic parameters + * - if params is NULL, default parameter settings are used. + * - model = model to assume + * - t = variables to use from the model (size = n) + * - m = number of terms in t to be used as assumption + * + * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN, + * YICES_STATUS_INTERRUPTED + * + * If status is STATUS_UNSAT then the context and model are inconsistent + */ +extern smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m); + + /* * Build a model: the context's status must be STATUS_SAT or STATUS_UNKNOWN * - model must be initialized (and empty) diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 1eb3b9c27..979042532 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -633,6 +633,16 @@ smt_status_t check_context_with_model(context_t *ctx, const param_t *params, mod return stat; } +/* + * Check with given model and hints + * - set the model hint and call check_context_with_model + */ +smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) { + mcsat_set_model_hint(ctx->mcsat, mdl, n, t); + + return check_context_with_model(ctx, params, mdl, m, t); +} + /* * Precheck: force generation of clauses and other stuff that's diff --git a/src/include/yices.h b/src/include/yices.h index 8fb3dd269..c8e0b9a6f 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3196,7 +3196,7 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte * This function checks statisfiability of the constraints in ctx conjoined with * a conjunction of equalities defined by t[i] and the model, namely, * - * t[0] == v_0 /\ .... /\ t[n-1] = v_{n-1} + * t[0] = v_0 /\ .... /\ t[n-1] = v_{n-1} * * where v_i is the value of t[i] in mdl. * @@ -3223,6 +3223,58 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *ctx, const param_t *params, model_t *mdl, uint32_t n, const term_t t[]); +/* + * Check satisfiability modulo a model and hints. + * + * Check whether the assertions stored in ctx conjoined with a model are satisfiable. + * - ctx must be a context initialized with support for MCSAT + * (see yices_new_context, yices_new_config, yices_set_config). + * - params is an optional structure to store heuristic parameters + * if params is NULL, default parameter settings are used. + * - mdl is a model + * - t is an array of n terms + * - the terms t[0] ... t[n-1] must all be uninterpreted terms + * + * This function checks statisfiability of the constraints in ctx + * conjoined with a conjunction of equalities defined by first m terms + * in t and their model values, namely, + * + * t[0] = v_0 /\ .... /\ t[m-1] = v_{m-1} + * + * and the remaining n-m terms in t are provided with hints from the + * model, i.e. + * + * t[m], ... , t[n-1] will be given v_{m}, ... , v_{n-1} values when deciding + * + * where v_i is the value of t[i] in mdl. + * + * NOTE: if t[i] does not have a value in mdl, then a default value is picked for v_i. + * + * If this function returns STATUS_UNSAT and the context supports + * model interpolation, then one can construct a model interpolant by + * calling function yices_get_model_interpolant. + * + * Error codes: + * + * if one of the terms t[i] is not an uninterpreted term + * code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED + * + * If the context does not have the MCSAT solver enabled + * code = CTX_OPERATION_NOT_SUPPORTED + * + * If the resulting status is STATUS_SAT and context does not support multichecks + * code = CTX_OPERATION_NOT_SUPPORTED + * + * + * Since 2.6.4. + */ +__YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, + const param_t *params, + model_t *mdl, + uint32_t n, + const term_t t[], + uint32_t m); + /* * Check satisfiability and compute interpolant. * diff --git a/src/mcsat/no_mcsat.c b/src/mcsat/no_mcsat.c index 8d374da25..6761a3983 100644 --- a/src/mcsat/no_mcsat.c +++ b/src/mcsat/no_mcsat.c @@ -54,6 +54,9 @@ int32_t mcsat_assert_formulas(mcsat_solver_t *mcsat, uint32_t n, const term_t *f return 0; } +void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_filter, const term_t mdl_filter[]) { +} + void mcsat_solve(mcsat_solver_t *mcsat, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]) { } diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 085cdeed7..eff0df933 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2522,6 +2522,42 @@ void mcsat_check_model(mcsat_solver_t* mcsat, bool assert) { static void mcsat_assert_formulas_internal(mcsat_solver_t* mcsat, uint32_t n, const term_t *f, bool preprocess); +void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_filter, + const term_t mdl_filter[]) { + if (n_mdl_filter == 0) { + return; + } + + assert(mdl != NULL); + assert(mdl_filter != NULL); + + value_table_t* vtbl = model_get_vtbl(mdl); + + mcsat_push(mcsat); + + uint32_t i; + for (i = 0; i < n_mdl_filter; ++i) { + term_t x = mdl_filter[i]; + assert(term_kind(mcsat->terms, x) == UNINTERPRETED_TERM || term_kind(mcsat->terms, x) == VARIABLE); + assert(is_pos_term(x)); + + variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x)); + if (trail_has_value(mcsat->trail, x_var)) { + continue; + } + + uint32_t plugin_i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, x_var)]; + value_t x_value = model_get_term_value(mdl, x); + mcsat_value_t value; + mcsat_value_construct_from_value(&value, vtbl, x_value); + assert(x_value >= 0); + trail_add_propagation(mcsat->trail, x_var, &value, plugin_i, mcsat->trail->decision_level); + mcsat_value_destruct(&value); + } + + mcsat_pop(mcsat); +} + void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uint32_t n_assumptions, const term_t assumptions[]) { uint32_t restart_resource; diff --git a/src/mcsat/solver.h b/src/mcsat/solver.h index efca59993..8930685b0 100644 --- a/src/mcsat/solver.h +++ b/src/mcsat/solver.h @@ -75,6 +75,14 @@ void mcsat_pop(mcsat_solver_t* mcsat); */ int32_t mcsat_assert_formulas(mcsat_solver_t *mcsat, uint32_t n, const term_t *f); +/* + * Set model hint. + * + * @param mdl the model to use. + * @param mdl_filter part of the model to use. + */ +void mcsat_set_model_hint(mcsat_solver_t *mcsat, model_t* mdl, uint32_t n, const term_t mdl_filter[]); + /* * Solve asserted constraints module given model. * diff --git a/src/mcsat/value.c b/src/mcsat/value.c index 2a0017ff1..03053fd1b 100644 --- a/src/mcsat/value.c +++ b/src/mcsat/value.c @@ -415,12 +415,24 @@ void mcsat_value_construct_from_value(mcsat_value_t* mcsat_value, value_table_t* case BOOLEAN_VALUE: mcsat_value_construct_bool(mcsat_value, is_true(vtbl, v)); break; - case RATIONAL_VALUE: - mcsat_value_construct_rational(mcsat_value, vtbl_rational(vtbl, v)); + case RATIONAL_VALUE: { + rational_t* value_q = vtbl_rational(vtbl, v); + mpq_t value_mpq; + mpq_init(value_mpq); + q_get_mpq(value_q, value_mpq); + lp_value_t value_lp; + lp_value_construct(&value_lp, LP_VALUE_RATIONAL, value_mpq); + mcsat_value_construct_lp_value(mcsat_value, &value_lp); + lp_value_destruct(&value_lp); + mpq_clear(value_mpq); break; + } case ALGEBRAIC_VALUE: { lp_algebraic_number_t* a = vtbl_algebraic_number(vtbl, v); - mcsat_value_construct_lp_value_direct(mcsat_value, LP_VALUE_ALGEBRAIC, a);; + lp_value_t value_lp; + lp_value_construct(&value_lp, LP_VALUE_ALGEBRAIC, a); + mcsat_value_construct_lp_value(mcsat_value, &value_lp); + lp_value_destruct(&value_lp); break; } case BITVECTOR_VALUE: { From f183843fa211b05dbe7af157c1418744079a208b Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Tue, 31 Oct 2023 23:09:30 -0700 Subject: [PATCH 2/5] api test --- tests/api/test_model_hint.c | 233 ++++++++++++++++++++++++++++++++++++ 1 file changed, 233 insertions(+) create mode 100644 tests/api/test_model_hint.c diff --git a/tests/api/test_model_hint.c b/tests/api/test_model_hint.c new file mode 100644 index 000000000..2a5da6273 --- /dev/null +++ b/tests/api/test_model_hint.c @@ -0,0 +1,233 @@ +/* + * Examples of check_with_model and model interpolants + */ + +#include +#include +#include + +#include "assert.h" + +#include + +/* + * Create an MCSAT context that supports model interpolants + */ +static context_t *make_mcsat_context(void) { + ctx_config_t *config; + context_t *context; + int32_t code; + + config = yices_new_config(); + code = yices_set_config(config, "solver-type", "mcsat"); + if (code < 0) goto error; + code = yices_set_config(config, "model-interpolation", "true"); + if (code < 0) goto error; + context = yices_new_context(config); + if (context == NULL) goto error; + yices_free_config(config); + return context; + + error: + yices_print_error(stderr); + yices_free_config(config); + return NULL; +} + +/* + * Create assertion x^2 + y^2 < 1 + * - return terms x and y in var: + * var[0] = x + * var[1] = y + */ +static term_t make_circle_constraint(term_t var[2]) { + type_t real; + term_t x, y, p; + + real = yices_real_type(); + x = yices_new_uninterpreted_term(real); + yices_set_term_name(x, "x"); + y = yices_new_uninterpreted_term(real); + yices_set_term_name(y, "y"); + + var[0] = x; + var[1] = y; + + p = yices_add(yices_square(x), yices_square(y)); // p is x^2 + y^2 + return yices_arith_lt_atom(p, yices_int32(1)); // p < 1 +} + +/* + * Create an unsat assertion: x^2 + y^2 < 1 AND x>2 + * - return variables x and y in var[0] and var[1], respectively. + */ +static term_t make_unsat_constraint(term_t var[2]) { + term_t p1, p2; + + p1 = make_circle_constraint(var); // x^2 + y^2 < 1 + p2 = yices_arith_gt_atom(var[0], yices_int32(2)); // x>2 + return yices_and2(p1, p2); +} + + +/* + * Check with model + */ +static smt_status_t check_with_model_and_hint(context_t *ctx, model_t *model, term_t assertion, uint32_t n, const term_t t[], uint32_t m) { + int32_t code = yices_assert_formula(ctx, assertion); + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + return yices_check_context_with_model_and_hint(ctx, NULL, model, n, t, m); +} + + +static void check_with_sat_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 0); // x == 0 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_SAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_SAT); + } + yices_free_model(model); + yices_free_context(ctx); +} + + +static void check_with_unsat_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 1); // x == 1 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_SAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_UNSAT); + } + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_sat_with_empty_model(void) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + + ctx = make_mcsat_context(); + assertion = make_circle_constraint(vars); // x^2 + y^2 < 1 + + model = yices_new_model(); + + smt_status_t status; + status = check_with_model_and_hint(ctx, model, assertion, 0, vars, 0); + assert(status == STATUS_SAT); + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_unsat_with_empty_model(void) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + + ctx = make_mcsat_context(); + assertion = make_unsat_constraint(vars); + + model = yices_new_model(); + + smt_status_t status; + status = check_with_model_and_hint(ctx, model, assertion, 0, vars, 0); + assert(status == STATUS_UNSAT); + + yices_free_model(model); + yices_free_context(ctx); +} + +static void check_unsat_with_model(bool use_hint) { + context_t *ctx; + model_t *model; + term_t vars[2]; + term_t assertion; + int32_t code; + + ctx = make_mcsat_context(); + assertion = make_unsat_constraint(vars); + + model = yices_new_model(); + code = yices_model_set_int32(model, vars[0], 0); // x == 0 + if (code < 0) { + yices_print_error(stderr); + exit(1); + } + + smt_status_t status; + if (use_hint) { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0); + assert(status == STATUS_UNSAT); + } else { + status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 1); + assert(status == STATUS_UNSAT); + } + + yices_free_model(model); + yices_free_context(ctx); +} + + +int main(void) { + yices_init(); + if (yices_has_mcsat()) { + printf("MCSAT supported\n"); + check_with_sat_model(false); + check_with_sat_model(true); + check_with_unsat_model(false); + check_with_unsat_model(true); + check_sat_with_empty_model(); + check_unsat_with_empty_model(); + check_unsat_with_model(false); + check_unsat_with_model(true); + } else { + printf("MCSAT not supported\n"); + } + yices_exit(); + + return 0; +} + From ad6eb079ab7d0477f0d8bd92d9c2b1cc801d45db Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 1 Nov 2023 10:38:21 -0700 Subject: [PATCH 3/5] minor --- tests/api/test_model_hint.c | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/api/test_model_hint.c b/tests/api/test_model_hint.c index 2a5da6273..2a148648e 100644 --- a/tests/api/test_model_hint.c +++ b/tests/api/test_model_hint.c @@ -1,5 +1,5 @@ /* - * Examples of check_with_model and model interpolants + * Test mcsat model hint api */ #include @@ -11,7 +11,7 @@ #include /* - * Create an MCSAT context that supports model interpolants + * Create an MCSAT context */ static context_t *make_mcsat_context(void) { ctx_config_t *config; @@ -21,8 +21,6 @@ static context_t *make_mcsat_context(void) { config = yices_new_config(); code = yices_set_config(config, "solver-type", "mcsat"); if (code < 0) goto error; - code = yices_set_config(config, "model-interpolation", "true"); - if (code < 0) goto error; context = yices_new_context(config); if (context == NULL) goto error; yices_free_config(config); @@ -71,7 +69,7 @@ static term_t make_unsat_constraint(term_t var[2]) { /* - * Check with model + * Check context with model and hint */ static smt_status_t check_with_model_and_hint(context_t *ctx, model_t *model, term_t assertion, uint32_t n, const term_t t[], uint32_t m) { int32_t code = yices_assert_formula(ctx, assertion); From eb52eef7bed7ba5f8411b6b7ceaa732ada83fcbe Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 1 Nov 2023 11:24:43 -0700 Subject: [PATCH 4/5] update doc --- doc/sphinx/source/context-operations.rst | 103 +++++++++++++++++++++-- 1 file changed, 98 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index c1eb7f583..04ca247e2 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -939,10 +939,11 @@ Check Modulo a Model and Model Interpolant When checking satisfiability, it is possible to provide a partial model such that the satisfiability is checked for the assertions in -conjunction with the provided model. To use this functionality, the -context must be a context initialized with support for MCSAT (see -yices_new_context, yices_new_config, yices_set_config). -Here is an example:: +conjunction with the provided model. Moreover, it is possible to +provide hints as initial model guesses when mcsat decides a +variable. To use this functionality, the context must be a context +initialized with support for MCSAT (see yices_new_context, +yices_new_config, yices_set_config). Here is an example:: ctx_config_t* config = yices_new_config(); yices_set_config(config, "solver-type", "mcsat"); @@ -958,6 +959,23 @@ uninterpreted terms ``a[0]``, ..., ``a[4]``. This amounts to checking the conjunction of ``f`` and the equalities between the unintpreted terms and their value in the ``model``. +Here is an example of checking context with model and hint:: + + ctx_config_t* config = yices_new_config(); + yices_set_config(config, "solver-type", "mcsat"); + context_t *ctx = yices_new_context(config); + yices_assert_formula(ctx, f); + status = yices_check_context_with_model_and_hint(ctx, NULL, model, 5, a, 3); + +In this fragment, similar to the earlier one, we assert a formula +``f``. In the call to check on the last line, we give an array of +five uninterpreted terms ``a[0]``, ..., ``a[4]``. However, this time +we would be checking the conjunction of ``f`` and the equalities +between the first three (the number is given as the last argument) +unintpreted terms and their value in the ``model``. The remaining two +terms and their values will be provided as hints to the internal mcsat +decide method. + The check modulo a model provides an additional functionality, namely, the construction of a model interpolant, if the yices context is unsatisfiable and supports model interpolation (see @@ -1013,6 +1031,79 @@ yices_set_config). This model interpolant is constructed by calling - If *ctx*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`. + This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is + configured for one-shot solving and *ctx*'s status is anything + other than :c:enum:`STATUS_IDLE`. + + **Error report** + + - If one of the terms *t[i]* is not an uninterpreted: + + -- error code: :c:enum:`MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED` + + - If the context does not have the MCSAT solver enabled: + + -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` + + - If the resulting status is :c:enum:`STATUS_SAT` and context does not support multichecks: + + -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` + + +.. c:function:: smt_status_t yices_check_context_with_model_and_hint(context_t* ctx, const param_t* params, model_t *mdl, uint32_t n, const term_t t[], uint32_t m) + + Checks whether *n* assumptions are satisfiable in a context *ctx*. + + **Parameters** + + - *ctx* is a context + + - *params* is an optional structure to a search-parameter structure. + + - *mdl* is a model + + - *n* is the number of terms in *t* + + - *t* is an array of *n* uninterpreted terms + + - *m* is the number of terms + + The *params* structure controls search heuristics. If *params* is NULL, default + settings are used. See :ref:`params` and :c:func:`yices_check_context`. + + This function checks statisfiability of the constraints in ctx + conjoined with a conjunction of equalities defined by *t[i]* and the + model, namely, + + *t[0] == v_0 /\ .... /\ t[n-1] = v_{m-1}*, + + and the remaining n-m terms in t are provided with hints from the model, i.e. + + *t[m], ... , t[n-1]* will be given *v_{m}, ... , v_{n-1}* values when deciding + + where *v_i* is the value of *t[i]* in *mdl*. + + NOTE: if *t[i]* does not have a value in *mdl*, then a default value is + picked for *v_i*. + + If this function returns STATUS_UNSAT and the context supports + model interpolation, then one can construct a model interpolant by + calling function :c:func:`yices_get_model_interpolant`. + + More precisely: + + - If *ctx*'s current status is :c:enum:`STATUS_UNSAT` then the function does nothing + and returns :c:enum:`STATUS_UNSAT`. + + - If *ctx*'s status is :c:enum:`STATUS_IDLE`, :c:enum:`STATUS_SAT`, + or :c:enum:`STATUS_UNKNOWN` then the function checks whether + *ctx* conjoined with the *n* equalities given by *mdl* and *t* is + satisfiable. This is done even if *n* is zero. The function will + then return a code as in :c:func:`yices_check_context`. + + - If *ctx*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`. + + This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is configured for one-shot solving and *ctx*'s status is anything other than :c:enum:`STATUS_IDLE`. @@ -1045,7 +1136,9 @@ yices_set_config). This model interpolant is constructed by calling Otherwise, it sets an error code and return NULL_TERM. This is intended to be used after a call to - :c:func:`yices_check_context_with_model` that returned + :c:func:`yices_check_context_with_model` or + :c:func:`yices_check_context_with_model_and_hint` + that returned :c:enum:`STATUS_UNSAT`. In this case, the function builds an model interpolant. The model interpolant is a clause implied by the current context that is false in the model provides to From bdd5e40d55221c3838ce99965f72a9a08a67d0a8 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 1 Nov 2023 11:27:28 -0700 Subject: [PATCH 5/5] asserts --- src/api/yices_api.c | 2 ++ src/context/context_solver.c | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 797420b26..13be62ee5 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -9267,6 +9267,8 @@ EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, co return STATUS_ERROR; } + assert(m <= n); + // cleanup switch (context_status(ctx)) { case STATUS_UNKNOWN: diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 979042532..f4ec1fb1a 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -638,6 +638,8 @@ smt_status_t check_context_with_model(context_t *ctx, const param_t *params, mod * - set the model hint and call check_context_with_model */ smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) { + assert(m <= n); + mcsat_set_model_hint(ctx->mcsat, mdl, n, t); return check_context_with_model(ctx, params, mdl, m, t);