diff --git a/src/api/yices_api.c b/src/api/yices_api.c index b7da07b20..7fded0675 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -2534,6 +2534,63 @@ static bool check_good_vars_or_uninterpreted(term_manager_t *mngr, uint32_t n, c return true; } +static bool mcsat_assumption_type_supported(type_table_t *types, type_t tau) { + type_kind_t kind = type_kind(types, tau); + uint32_t i; + + switch (kind) { + case BOOL_TYPE: + case INT_TYPE: + case REAL_TYPE: + case SCALAR_TYPE: + case BITVECTOR_TYPE: + return true; + + case TUPLE_TYPE: { + tuple_type_t *tuple = tuple_type_desc(types, tau); + for (i = 0; i < tuple->nelem; i++) { + if (! mcsat_assumption_type_supported(types, tuple->elem[i])) { + return false; + } + } + return true; + } + + default: + return false; + } +} + +// Check that the type of every term in v is one that the MCSAT solver can +// decide on as an assumption value. Tuple types are supported if all their +// recursively flattened leaves are supported scalar decision types. Other +// type kinds (UNINTERPRETED_TYPE, FUNCTION_TYPE, FF_TYPE, etc.) reach the +// MCSAT solver but trigger an assertion failure inside +// mcsat_value_construct_from_value (or a NULL decide_assignment dispatch), +// so we reject them here with a clear error code (issue #615). +// +// All elements of v must already be good terms. +static bool check_mcsat_assumption_types(term_manager_t *mngr, uint32_t n, const term_t *v) { + term_table_t *tbl; + type_table_t *types; + uint32_t i; + + tbl = term_manager_get_terms(mngr); + types = tbl->types; + for (i=0; icode = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED; + error->term1 = v[i]; + error->type1 = tau; + return false; + } + } + + return true; +} + // Check whether arrays v and a define a valid substitution // both must be arrays of n elements static bool check_good_substitution(term_manager_t *mngr, uint32_t n, const term_t *v, const term_t *a) { @@ -9571,6 +9628,18 @@ static bool good_terms_for_check_with_model(uint32_t n, const term_t t[]) { MT_PROTECT(bool, __yices_globals.lock, _o_good_terms_for_check_with_model(n, t)); } +/* + * Same as _o_good_terms_for_check_with_model, but additionally checks that + * the type of each assumption term is one MCSAT can decide on. This guards + * against the crash reported in issue #615. Tuple assumptions are allowed + * only if every recursively flattened leaf type is supported by an MCSAT + * decision plugin. + */ +static bool _o_good_assumption_terms_for_mcsat(uint32_t n, const term_t t[]) { + return _o_good_terms_for_check_with_model(n, t) + && check_mcsat_assumption_types(__yices_globals.manager, n, t); +} + /* * Check context with model * - param = parameter for check sat (or NULL for default parameters) @@ -9588,10 +9657,16 @@ static smt_status_t _o_yices_check_context_with_model(context_t *ctx, const para return YICES_STATUS_ERROR; } - if (! _o_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); + if (! _o_good_assumption_terms_for_mcsat(n, t)) { + // Normalize the error code: VARIABLE_REQUIRED (set by the + // term-shape check) becomes MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED, + // matching the long-standing convention here. The new + // MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED (set by the type-kind + // check) is left as-is so callers can distinguish "wrong shape" from + // "wrong type". term1/type1 fields are preserved. + if (yices_error_code() == VARIABLE_REQUIRED) { + set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + } return YICES_STATUS_ERROR; } @@ -9669,10 +9744,11 @@ static smt_status_t _o_yices_check_context_with_model_and_hint(context_t *ctx, c return YICES_STATUS_ERROR; } - if (! _o_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); + if (! _o_good_assumption_terms_for_mcsat(n, t)) { + // See note in _o_yices_check_context_with_model. + if (yices_error_code() == VARIABLE_REQUIRED) { + set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + } return YICES_STATUS_ERROR; } @@ -9880,16 +9956,28 @@ EXPORTED smt_status_t yices_check_context_with_interpolation(interpolation_conte ctx->model = yices_get_model(ctx->ctx_A, true); } - // Pop both contexts - if (result != YICES_STATUS_ERROR) { + // Pop both contexts. Preserve the original error report if the loop above + // failed (for example, via model-refutation assumption validation). + { + bool preserve_error = result == YICES_STATUS_ERROR; + error_report_t saved_error; + if (preserve_error) { + saved_error = *get_yices_error(); + } + ret = yices_pop(ctx->ctx_B); - if (ret) { + if (ret && !preserve_error) { result = YICES_STATUS_ERROR; - } else { - ret = yices_pop(ctx->ctx_A); - if (ret) { - result = YICES_STATUS_ERROR; - } + } + // Pop A even if popping B failed: both contexts were pushed above and + // must be balanced independently. + ret = yices_pop(ctx->ctx_A); + if (ret && !preserve_error) { + result = YICES_STATUS_ERROR; + } + + if (preserve_error) { + *get_yices_error() = saved_error; } } diff --git a/src/api/yices_error.c b/src/api/yices_error.c index e69dc1232..47759d941 100644 --- a/src/api/yices_error.c +++ b/src/api/yices_error.c @@ -608,6 +608,10 @@ int32_t print_error(FILE *f) { code = fprintf(f, "mcsat: checking with assumptions only supports variables as assumptions\n"); break; + case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED: + code = fprintf(f, "mcsat: assumption variable has a type that mcsat cannot decide on\n"); + break; + case INTERNAL_EXCEPTION: default: code = fprintf(f, "internal error\n"); @@ -1137,6 +1141,10 @@ char *error_string(void) { nchar = snprintf(buffer, BUFFER_SIZE, "mcsat: checking with assumptions only supports variables as assumptions\n"); break; + case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED: + nchar = snprintf(buffer, BUFFER_SIZE, "mcsat: assumption variable has a type that mcsat cannot decide on\n"); + break; + case INTERNAL_EXCEPTION: default: nchar = snprintf(buffer, BUFFER_SIZE, "internal error"); diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index d8472510a..f76082e31 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -1102,6 +1102,10 @@ static void print_yices_error(bool full) { print_out("mcsat: checking with assumptions only supports variables as assumptions"); break; + case MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED: + print_out("mcsat: assumption variable has a type that mcsat cannot decide on"); + break; + case OUTPUT_ERROR: print_out(" IO error"); break; diff --git a/src/include/yices.h b/src/include/yices.h index 06309abcf..80b955237 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3370,6 +3370,11 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte * if one of the terms t[i] is not an uninterpreted term * code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED * + * if one of the terms t[i] has a type that MCSAT cannot decide on + * (i.e. not Bool, Int, Real, scalar, BitVector, or a tuple whose + * recursively flattened leaves all have one of these types) + * code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED + * * If the context does not have the MCSAT solver enabled * code = CTX_OPERATION_NOT_SUPPORTED * @@ -3418,6 +3423,11 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t * * if one of the terms t[i] is not an uninterpreted term * code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED * + * if one of the terms t[i] has a type that MCSAT cannot decide on + * (i.e. not Bool, Int, Real, scalar, BitVector, or a tuple whose + * recursively flattened leaves all have one of these types) + * code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED + * * If the context does not have the MCSAT solver enabled * code = CTX_OPERATION_NOT_SUPPORTED * @@ -3506,8 +3516,9 @@ __YICES_DLLSPEC__ extern smt_status_t yices_mcsat_set_initial_var_order(context_ * a model is returned in ctx->model. This model must be freed when no-longer needed by * calling yices_free_model. * - * If something is wrong, the function returns YICES_STATUS_ERROR and sets the yices error report - * (code = CTX_INVALID_OPERATION). + * If something is wrong, the function returns YICES_STATUS_ERROR and sets the yices error report. + * This includes CTX_INVALID_OPERATION and any error propagated from the internal + * yices_check_context_with_model call used for model refutation. * * Since 2.6.4. */ diff --git a/src/include/yices_types.h b/src/include/yices_types.h index e464d7d93..a04dbf85f 100644 --- a/src/include/yices_types.h +++ b/src/include/yices_types.h @@ -480,6 +480,7 @@ typedef enum error_code { */ MCSAT_ERROR_UNSUPPORTED_THEORY = 1000, MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED = 1001, + MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED = 1002, /* * Input/output and system errors diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 19c468d51..b95ee9ea9 100644 --- a/src/mcsat/preprocessor.c +++ b/src/mcsat/preprocessor.c @@ -2397,6 +2397,12 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is return t_pre; } +void preprocessor_tuple_blast(preprocessor_t* pre, term_t t, ivector_t* out) { + ivector_reset(out); + tuple_blast_term(pre, t); + tuple_blast_get(pre, t, out); +} + void preprocessor_set_exception_handler(preprocessor_t* pre, jmp_buf* handler) { pre->exception = handler; } diff --git a/src/mcsat/preprocessor.h b/src/mcsat/preprocessor.h index 26522c3f5..f1183af7d 100644 --- a/src/mcsat/preprocessor.h +++ b/src/mcsat/preprocessor.h @@ -111,6 +111,14 @@ void preprocessor_destruct(preprocessor_t* pre); /** Preprocess the term, add any additional assertions to output vector. */ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is_assertion); +/* + * Tuple-blast term t and copy its flattened leaves into out. + * - out is reset first. + * - leaf order matches type_collect_blasted_atom_types/type leaf order. + * - leaves are memoized and stable across later tuple-blast calls. + */ +void preprocessor_tuple_blast(preprocessor_t* pre, term_t t, ivector_t* out); + /** Set tracer */ void preprocessor_set_tracer(preprocessor_t* pre, tracer_t* tracer); diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 4247f4fa8..ab9512fde 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -256,6 +256,9 @@ struct mcsat_solver_s { /** Assumption variables */ ivector_t assumption_vars; + /** Model values for assumption variables, parallel to assumption_vars */ + ivector_t assumption_values; + /** Index of the assumption to process next */ uint32_t assumption_i; @@ -338,6 +341,13 @@ void mcsat_add_lemma(mcsat_solver_t* mcsat, ivector_t* lemma, term_t decision_bo static void mcsat_set_interpolant_from_internal(mcsat_solver_t* mcsat, term_t interpolant); +static +bool mcsat_flatten_model_value(mcsat_solver_t* mcsat, value_table_t* vtbl, type_t tau, value_t value, ivector_t* out); + +static +void mcsat_value_construct_from_typed_model_value(mcsat_value_t* mcsat_value, value_table_t* vtbl, + type_table_t* types, type_t tau, value_t value); + static void propagation_check(const ivector_t* reasons, term_t x, term_t subst); @@ -945,6 +955,7 @@ void mcsat_construct(mcsat_solver_t* mcsat, const context_t* ctx) { // Assumptions vector init_ivector(&mcsat->assumption_vars, 0); + init_ivector(&mcsat->assumption_values, 0); // Lemmas vector init_ivector(&mcsat->plugin_lemmas, 0); @@ -999,6 +1010,7 @@ void mcsat_destruct(mcsat_solver_t* mcsat) { statistics_destruct(&mcsat->stats); scope_holder_destruct(&mcsat->scope); delete_ivector(&mcsat->assumption_vars); + delete_ivector(&mcsat->assumption_values); delete_int_hset(&mcsat->internal_kinds); } @@ -1192,6 +1204,8 @@ void mcsat_clear(mcsat_solver_t* mcsat) { // Clear to be ready for more assertions: // - Pop internal to base level mcsat->assumption_i = 0; + ivector_reset(&mcsat->assumption_vars); + ivector_reset(&mcsat->assumption_values); mcsat->assumptions_decided_level = -1; mcsat_backtrack_to(mcsat, mcsat->trail->decision_level_base, true); mcsat->status = YICES_STATUS_IDLE; @@ -2110,6 +2124,56 @@ void mcsat_set_interpolant_from_internal(mcsat_solver_t* mcsat, term_t interpola mcsat->interpolant = preprocessor_unblast_term(&mcsat->preprocessor, interpolant); } +static +bool mcsat_flatten_model_value(mcsat_solver_t* mcsat, value_table_t* vtbl, type_t tau, value_t value, ivector_t* out) { + type_table_t* types = mcsat->types; + type_kind_t kind = type_kind(types, tau); + + if (value < 0) { + return false; + } + + if (kind == TUPLE_TYPE) { + tuple_type_t* tuple = tuple_type_desc(types, tau); + uint32_t i; + + if (!object_is_tuple(vtbl, value)) { + return false; + } + value_tuple_t* tuple_value = vtbl_tuple(vtbl, value); + if (tuple_value->nelems != tuple->nelem) { + return false; + } + for (i = 0; i < tuple->nelem; ++i) { + if (!mcsat_flatten_model_value(mcsat, vtbl, tuple->elem[i], tuple_value->elem[i], out)) { + return false; + } + } + return true; + } + + ivector_push(out, value); + return true; +} + +static +void mcsat_value_construct_from_typed_model_value(mcsat_value_t* mcsat_value, value_table_t* vtbl, + type_table_t* types, type_t tau, value_t value) { + if (type_kind(types, tau) == SCALAR_TYPE) { + value_unint_t* c = vtbl_unint(vtbl, value); + rational_t q; + + /* Scalar values are decided by the rational plugin; the scalar + * constant index is the corresponding integer value. */ + q_init(&q); + q_set32(&q, c->index); + mcsat_value_construct_rational(mcsat_value, &q); + q_clear(&q); + } else { + mcsat_value_construct_from_value(mcsat_value, vtbl, value); + } +} + static bool mcsat_conflict_with_assumptions(mcsat_solver_t* mcsat, uint32_t conflict_level) { // If we decided some assumptions, then backtracked under that level @@ -2394,11 +2458,13 @@ void mcsat_analyze_conflicts(mcsat_solver_t* mcsat, uint32_t* restart_resource) } static -bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_assumptions, const term_t assumptions[]) { +bool mcsat_decide_assumption(mcsat_solver_t* mcsat, value_table_t* vtbl) { assert(!mcsat->trail->inconsistent); + assert(mcsat->assumption_vars.size == mcsat->assumption_values.size); variable_t var; term_t var_term; + value_t value; mcsat_value_t var_mdl_value; uint32_t plugin_i; @@ -2407,7 +2473,7 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass plugin_trail_token_t decision_token; bool assumption_decided = false; - for (; !assumption_decided && mcsat->assumption_i < n_assumptions; mcsat->assumption_i ++) { + for (; !assumption_decided && mcsat->assumption_i < mcsat->assumption_vars.size; mcsat->assumption_i ++) { // Break if any conflicts if (mcsat->trail->inconsistent) { @@ -2417,16 +2483,16 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass break; } - // The variable (should exist already) - var_term = assumptions[mcsat->assumption_i]; - var = variable_db_get_variable_if_exists(mcsat->var_db, var_term); + var = mcsat->assumption_vars.data[mcsat->assumption_i]; + var_term = variable_db_get_term(mcsat->var_db, var); + value = mcsat->assumption_values.data[mcsat->assumption_i]; assert(var != variable_null); // Get the owner that will 'decide' the value of the variable plugin_i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, var)]; assert(plugin_i != MCSAT_MAX_PLUGINS); - // The given value the variable in the provided model - value_t value = model_get_term_value(mdl, var_term); - mcsat_value_construct_from_value(&var_mdl_value, &mdl->vtbl, value); + // The given value for the flattened assumption leaf + mcsat_value_construct_from_typed_model_value(&var_mdl_value, vtbl, mcsat->types, + term_type(mcsat->terms, var_term), value); if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide_assumption(): with %s\n", mcsat->plugins[plugin_i].plugin_name); @@ -2737,8 +2803,97 @@ 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); +static +void mcsat_add_assumption_leaf(mcsat_solver_t* mcsat, term_t x, value_t value) { + variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x)); + ivector_push(&mcsat->assumption_vars, x_var); + ivector_push(&mcsat->assumption_values, value); + mcsat_process_registration_queue(mcsat); +} + +static +bool mcsat_collect_tuple_leaves_and_values(mcsat_solver_t* mcsat, model_t* mdl, term_t x, + ivector_t* leaves, ivector_t* values) { + value_table_t* vtbl = model_get_vtbl(mdl); + + preprocessor_tuple_blast(&mcsat->preprocessor, x, leaves); + return mcsat_flatten_model_value(mcsat, vtbl, term_type(mcsat->terms, x), + model_get_term_value(mdl, x), values) && + leaves->size == values->size; +} + +static +void mcsat_add_tuple_assumption_leaves(mcsat_solver_t* mcsat, model_t* mdl, term_t x) { + ivector_t leaves, values; + uint32_t i; + + init_ivector(&leaves, 0); + init_ivector(&values, 0); + + if (!mcsat_collect_tuple_leaves_and_values(mcsat, mdl, x, &leaves, &values)) { + /* Defensive path for malformed user models: API validation has already + * rejected unsupported tuple leaf types before solver entry. */ + delete_ivector(&values); + delete_ivector(&leaves); + longjmp(*mcsat->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY); + } + + for (i = 0; i < leaves.size; ++i) { + term_t leaf = leaves.data[i]; + term_t leaf_pre = preprocessor_apply(&mcsat->preprocessor, leaf, NULL, true); + if (leaf != leaf_pre) { + /* As with scalar assumptions, keep the original public assumption leaf + * decidable while preserving substitutions learned during preprocessing. */ + term_t eq = mk_eq(&mcsat->tm, leaf, leaf_pre); + mcsat_assert_formulas_internal(mcsat, 1, &eq, false); + } + mcsat_add_assumption_leaf(mcsat, leaf, values.data[i]); + } + + delete_ivector(&values); + delete_ivector(&leaves); +} + +static +void mcsat_set_hint_leaf(mcsat_solver_t* mcsat, value_table_t* vtbl, term_t x, value_t x_value) { + variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x)); + mcsat_value_t value; + + mcsat_value_construct_from_typed_model_value(&value, vtbl, mcsat->types, term_type(mcsat->terms, x), x_value); + trail_set_cached_value(mcsat->trail, x_var, &value); + mcsat_value_destruct(&value); +} + +static +void mcsat_set_tuple_hint_leaves(mcsat_solver_t* mcsat, model_t* mdl, term_t x) { + value_table_t* vtbl = model_get_vtbl(mdl); + ivector_t leaves, values; + uint32_t i; + + init_ivector(&leaves, 0); + init_ivector(&values, 0); + + if (!mcsat_collect_tuple_leaves_and_values(mcsat, mdl, x, &leaves, &values)) { + /* Defensive path for malformed user models: API validation has already + * rejected unsupported tuple leaf types before solver entry. */ + delete_ivector(&values); + delete_ivector(&leaves); + longjmp(*mcsat->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY); + } + + /* Hints are advisory cache entries, not assumption decisions. No + * preprocessor_apply/equality assertion is needed here: if a leaf was + * substituted, search can ignore or overwrite the stale cached hint. */ + for (i = 0; i < leaves.size; ++i) { + mcsat_set_hint_leaf(mcsat, vtbl, leaves.data[i], values.data[i]); + } + + delete_ivector(&values); + delete_ivector(&leaves); +} + void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_filter, - const term_t mdl_filter[]) { + const term_t mdl_filter[]) { if (n_mdl_filter == 0) { return; } @@ -2746,8 +2901,6 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi assert(mdl != NULL); assert(mdl_filter != NULL); - value_table_t* vtbl = model_get_vtbl(mdl); - trail_clear_cache(mcsat->trail); trail_update_extra_cache(mcsat->trail); @@ -2756,14 +2909,11 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi 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)); - 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_set_cached_value(mcsat->trail, x_var, &value); + if (term_type_kind(mcsat->terms, x) == TUPLE_TYPE) { + mcsat_set_tuple_hint_leaves(mcsat, mdl, x); + } else { + mcsat_set_hint_leaf(mcsat, model_get_vtbl(mdl), x, model_get_term_value(mdl, x)); + } } mcsat_process_registration_queue(mcsat); @@ -2800,6 +2950,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin mcsat_trace_printf(mcsat->ctx->trace, "solving with assumptions\n"); } assert(mcsat->assumption_vars.size == 0); + assert(mcsat->assumption_values.size == 0); uint32_t i; for (i = 0; i < n_assumptions; ++ i) { // Apply the pre-processor. If the variable is substituted, we @@ -2807,16 +2958,18 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin term_t x = assumptions[i]; assert(term_kind(mcsat->terms, x) == UNINTERPRETED_TERM || term_kind(mcsat->terms, x) == VARIABLE); assert(is_pos_term(x)); - term_t x_pre = preprocessor_apply(&mcsat->preprocessor, x, NULL, true); - if (x != x_pre) { - // Assert x = t although we solved it already :( - term_t eq = mk_eq(&mcsat->tm, x, x_pre); - mcsat_assert_formulas_internal(mcsat, 1, &eq, false); + if (term_type_kind(mcsat->terms, x) == TUPLE_TYPE) { + mcsat_add_tuple_assumption_leaves(mcsat, mdl, x); + } else { + term_t x_pre = preprocessor_apply(&mcsat->preprocessor, x, NULL, true); + if (x != x_pre) { + // Assert x = t although we solved it already :( + term_t eq = mk_eq(&mcsat->tm, x, x_pre); + mcsat_assert_formulas_internal(mcsat, 1, &eq, false); + } + // Make sure the variable is registered (maybe it doesn't appear in assertions) + mcsat_add_assumption_leaf(mcsat, x, model_get_term_value(mdl, x)); } - // Make sure the variable is registered (maybe it doesn't appear in assertions) - variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x)); - ivector_push(&mcsat->assumption_vars, x_var); - mcsat_process_registration_queue(mcsat); } } @@ -2900,7 +3053,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin } // Should we decide on an assumption - bool assumption_decided = mcsat_decide_assumption(mcsat, mdl, n_assumptions, assumptions); + bool assumption_decided = mcsat_decide_assumption(mcsat, model_get_vtbl(mdl)); if (assumption_decided) { continue; } @@ -2972,6 +3125,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin solve_done: ivector_reset(&mcsat->assumption_vars); + ivector_reset(&mcsat->assumption_values); } void mcsat_cleanup_assumptions(mcsat_solver_t* mcsat) { diff --git a/tests/api/test_issue_615_assumption_type.c b/tests/api/test_issue_615_assumption_type.c new file mode 100644 index 000000000..cd89d939a --- /dev/null +++ b/tests/api/test_issue_615_assumption_type.c @@ -0,0 +1,508 @@ +/* + * Regression test for issue #615: + * + * Yices used to crash with + * mcsat/value.c:478: mcsat_value_construct_from_value: Assertion `false' failed. + * (or a SIGSEGV in release builds) when yices_check_context_with_model, + * yices_check_context_with_model_and_hint, or yices_check_context_with_interpolation + * was called with assumption variables whose type kind MCSAT cannot decide on + * (e.g. uninterpreted, function, or finite-field types). Tuple assumptions + * whose flattened leaves are decidable scalar types are supported. + * + * The fix turns these crashes into a clean YICES_STATUS_ERROR with error code + * MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. + */ + +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include +#include +#include +#include + +#include +#include + +static context_t *make_mcsat_context(bool model_interpolation) { + ctx_config_t *config = yices_new_config(); + if (yices_set_config(config, "solver-type", "mcsat") < 0) goto error; + if (model_interpolation && + yices_set_config(config, "model-interpolation", "true") < 0) goto error; + + context_t *ctx = yices_new_context(config); + yices_free_config(config); + return ctx; + + error: + yices_print_error(stderr); + yices_free_config(config); + return NULL; +} + +static void set_tuple_int_bool(model_t *mdl, term_t tuple, int32_t i, int32_t b) { + term_t ivar = yices_new_uninterpreted_term(yices_int_type()); + term_t bvar = yices_new_uninterpreted_term(yices_bool_type()); + yval_t elems[2]; + + assert(yices_model_set_int32(mdl, ivar, i) == 0); + assert(yices_model_set_bool(mdl, bvar, b) == 0); + assert(yices_get_value(mdl, ivar, &elems[0]) == 0); + assert(yices_get_value(mdl, bvar, &elems[1]) == 0); + assert(yices_model_set_tuple(mdl, tuple, 2, elems) == 0); +} + +static void set_tuple_int_scalar(model_t *mdl, term_t tuple, type_t scalar_t, + int32_t i, int32_t s) { + term_t ivar = yices_new_uninterpreted_term(yices_int_type()); + term_t svar = yices_new_uninterpreted_term(scalar_t); + yval_t elems[2]; + + assert(yices_model_set_int32(mdl, ivar, i) == 0); + assert(yices_model_set_scalar(mdl, svar, s) == 0); + assert(yices_get_value(mdl, ivar, &elems[0]) == 0); + assert(yices_get_value(mdl, svar, &elems[1]) == 0); + assert(yices_model_set_tuple(mdl, tuple, 2, elems) == 0); +} + +static void set_nested_tuple_int_bool_bv(model_t *mdl, term_t tuple, + int32_t i, int32_t b, uint32_t bv) { + term_t ivar = yices_new_uninterpreted_term(yices_int_type()); + term_t bvar = yices_new_uninterpreted_term(yices_bool_type()); + term_t bvvar = yices_new_uninterpreted_term(yices_bv_type(4)); + yval_t outer[2], inner[2], inner_tuple; + + assert(yices_model_set_int32(mdl, ivar, i) == 0); + assert(yices_model_set_bool(mdl, bvar, b) == 0); + assert(yices_model_set_bv_uint32(mdl, bvvar, bv) == 0); + assert(yices_get_value(mdl, ivar, &outer[0]) == 0); + assert(yices_get_value(mdl, bvar, &inner[0]) == 0); + assert(yices_get_value(mdl, bvvar, &inner[1]) == 0); + assert(yices_model_make_tuple(mdl, 2, inner, &inner_tuple) == 0); + outer[1] = inner_tuple; + assert(yices_model_set_tuple(mdl, tuple, 2, outer) == 0); +} + +/* + * Case 1: assumption variable of uninterpreted-sort type. + * Reproduces the original crash trace from issue #615. + */ +static void check_uninterpreted_sort_assumption_rejected(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t T = yices_new_uninterpreted_type(); + term_t x = yices_new_uninterpreted_term(T); + term_t y = yices_new_uninterpreted_term(T); + yices_set_term_name(x, "x_u"); + yices_set_term_name(y, "y_u"); + + /* Make ctx satisfiable so the call really exercises mcsat. */ + yices_assert_formula(ctx, yices_neq(x, y)); + + model_t *mdl = yices_new_model(); + term_t assumptions[2] = { x, y }; + + smt_status_t s = + yices_check_context_with_model(ctx, NULL, mdl, 2, assumptions); + (void) s; + + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + yices_clear_error(); + + s = yices_check_context_with_model_and_hint(ctx, NULL, mdl, 2, + assumptions, /*m=*/1); + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + yices_clear_error(); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +/* + * Case 2: assumption variable of function type. + * Same crash path; same fix applies. + */ +static void check_function_type_assumption_rejected(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t int_t = yices_int_type(); + type_t dom[1] = { int_t }; + type_t fty = yices_function_type(1, dom, int_t); + term_t f = yices_new_uninterpreted_term(fty); + yices_set_term_name(f, "f"); + + yices_assert_formula(ctx, yices_eq(yices_application1(f, yices_int32(0)), + yices_int32(0))); + + model_t *mdl = yices_new_model(); + term_t assumptions[1] = { f }; + + smt_status_t s = + yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + (void) s; + + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + yices_clear_error(); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +/* + * Case 3: supported types must keep working unchanged. + * Bool / Int / Real / BV / scalar assumptions go through the regular code path + * and do not trigger the new error. + */ +static void check_supported_types_still_work(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + /* x : Real; assert x > 0; assumption x with model x = 1 -> SAT */ + term_t x = yices_new_uninterpreted_term(yices_real_type()); + yices_set_term_name(x, "x_real"); + yices_assert_formula(ctx, yices_arith_gt0_atom(x)); + + model_t *mdl = yices_new_model(); + yices_model_set_int32(mdl, x, 1); + + term_t assumptions[1] = { x }; + smt_status_t s = + yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + (void) s; + /* Must not error and must not crash. */ + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); + + ctx = make_mcsat_context(false); + assert(ctx != NULL); + + /* s : scalar(3); assert s = c1; assumption s with model s = c1 -> SAT */ + type_t scalar_t = yices_new_scalar_type(3); + term_t s_var = yices_new_uninterpreted_term(scalar_t); + term_t s_val = yices_constant(scalar_t, 1); + yices_set_term_name(s_var, "x_scalar"); + assert(yices_assert_formula(ctx, yices_eq(s_var, s_val)) == 0); + + mdl = yices_new_model(); + assert(yices_model_set_scalar(mdl, s_var, 1) == 0); + + assumptions[0] = s_var; + s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_assumption_sat(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_arith_gt0_atom(yices_select(1, x))) == 0); + assert(yices_assert_formula(ctx, yices_eq(yices_select(2, x), yices_true())) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_bool(mdl, x, 3, 1); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_assumption_unsat(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_arith_gt0_atom(yices_select(1, x))) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_bool(mdl, x, -1, 1); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_UNSAT); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_assumption_respects_preprocessing(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t fixed = yices_tuple(2, (term_t[]){ yices_int32(2), yices_true() }); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_eq(x, fixed)) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_bool(mdl, x, 3, 1); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_UNSAT); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_nested_tuple_assumption_sat(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t bv4_t = yices_bv_type(4); + type_t inner_t = yices_tuple_type2(yices_bool_type(), bv4_t); + type_t outer_t = yices_tuple_type2(yices_int_type(), inner_t); + term_t x = yices_new_uninterpreted_term(outer_t); + term_t inner = yices_select(2, x); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_arith_eq_atom(yices_select(1, x), yices_int32(5))) == 0); + assert(yices_assert_formula(ctx, yices_eq(yices_select(1, inner), yices_false())) == 0); + assert(yices_assert_formula(ctx, yices_bveq_atom(yices_select(2, inner), + yices_bvconst_uint32(4, 0xa))) == 0); + + model_t *mdl = yices_new_model(); + set_nested_tuple_int_bool_bv(mdl, x, 5, 0, 0xa); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_with_scalar_leaf(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t scalar_t = yices_new_scalar_type(3); + type_t tuple_t = yices_tuple_type2(yices_int_type(), scalar_t); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_arith_eq_atom(yices_select(1, x), yices_int32(7))) == 0); + assert(yices_assert_formula(ctx, yices_eq(yices_select(2, x), + yices_constant(scalar_t, 2))) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_scalar(mdl, x, scalar_t, 7, 2); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_repeat_solve_resets_assumptions(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[1] = { x }; + + assert(yices_assert_formula(ctx, yices_arith_gt0_atom(yices_select(1, x))) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_bool(mdl, x, 4, 1); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_empty_model_uses_default_value(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[1] = { x }; + + model_t *mdl = yices_new_model(); + + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + assert(yices_error_code() == YICES_NO_ERROR); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_model_hint(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + term_t y = yices_new_uninterpreted_term(tuple_t); + term_t assumptions[2] = { x, y }; + + assert(yices_assert_formula(ctx, yices_arith_eq_atom(yices_select(1, x), yices_int32(4))) == 0); + + model_t *mdl = yices_new_model(); + set_tuple_int_bool(mdl, x, 4, 1); + set_tuple_int_bool(mdl, y, 9, 0); + + smt_status_t s = yices_check_context_with_model_and_hint(ctx, NULL, mdl, 2, assumptions, 1); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +static void check_tuple_interpolation_refutation(void) { + context_t *ctx_A = make_mcsat_context(true); + context_t *ctx_B = make_mcsat_context(false); + assert(ctx_A != NULL && ctx_B != NULL); + + type_t tuple_t = yices_tuple_type2(yices_int_type(), yices_bool_type()); + term_t x = yices_new_uninterpreted_term(tuple_t); + assert(yices_set_term_name(x, "issue615_tuple_interp_x") == 0); + term_t a_tuple = yices_tuple(2, (term_t[]){ yices_int32(1), yices_true() }); + term_t b_tuple = yices_tuple(2, (term_t[]){ yices_int32(2), yices_true() }); + + assert(yices_assert_formula(ctx_A, yices_eq(x, a_tuple)) == 0); + assert(yices_assert_formula(ctx_B, yices_eq(x, b_tuple)) == 0); + + interpolation_context_t ictx = { ctx_A, ctx_B, NULL_TERM, NULL }; + smt_status_t s = yices_check_context_with_interpolation(&ictx, NULL, 0); + assert(s == YICES_STATUS_UNSAT); + assert(ictx.interpolant != NULL_TERM); + + yices_free_context(ctx_B); + yices_free_context(ctx_A); +} + +static void check_interpolation_preserves_refutation_error(void) { + context_t *ctx_A = make_mcsat_context(true); + context_t *ctx_B = yices_new_context(NULL); + assert(ctx_A != NULL && ctx_B != NULL); + + type_t u_t = yices_new_uninterpreted_type(); + term_t x = yices_new_uninterpreted_term(u_t); + term_t y = yices_new_uninterpreted_term(u_t); + assert(yices_set_term_name(x, "issue615_interp_bad_x") == 0); + assert(yices_set_term_name(y, "issue615_interp_bad_y") == 0); + + assert(yices_assert_formula(ctx_B, yices_neq(x, y)) == 0); + + interpolation_context_t ictx = { ctx_A, ctx_B, NULL_TERM, NULL }; + smt_status_t s = yices_check_context_with_interpolation(&ictx, NULL, 0); + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + yices_clear_error(); + + yices_free_context(ctx_B); + yices_free_context(ctx_A); +} + +static void check_tuple_with_unsupported_leaf_rejected(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + type_t int_t = yices_int_type(); + type_t u_t = yices_new_uninterpreted_type(); + type_t fun_t = yices_function_type1(int_t, int_t); + mpz_t p; + mpz_init_set_ui(p, 7); + type_t ff_t = yices_ff_type(p); + mpz_clear(p); + + type_t bad_types[3] = { + yices_tuple_type2(int_t, u_t), + yices_tuple_type2(int_t, fun_t), + yices_tuple_type2(int_t, ff_t), + }; + + model_t *mdl = yices_new_model(); + for (uint32_t i = 0; i < 3; ++i) { + term_t x = yices_new_uninterpreted_term(bad_types[i]); + smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, &x); + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + yices_clear_error(); + } + + yices_free_model(mdl); + yices_free_context(ctx); +} + +/* + * Case 4: non-uninterpreted assumption term still reported with the original + * MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED code (regression guard for + * backward compatibility). + */ +static void check_term_shape_check_preserved(void) { + context_t *ctx = make_mcsat_context(false); + assert(ctx != NULL); + + term_t x = yices_new_uninterpreted_term(yices_int_type()); + term_t not_a_var = yices_add(x, yices_int32(1)); /* x + 1, not a variable */ + + model_t *mdl = yices_new_model(); + term_t assumptions[1] = { not_a_var }; + + smt_status_t s = + yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + (void) s; + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + yices_clear_error(); + + yices_free_model(mdl); + yices_free_context(ctx); +} + +int main(void) { + if (!yices_has_mcsat()) { + return 1; /* skipped */ + } + + yices_init(); + + check_uninterpreted_sort_assumption_rejected(); + check_function_type_assumption_rejected(); + check_supported_types_still_work(); + check_tuple_assumption_sat(); + check_tuple_assumption_unsat(); + check_tuple_assumption_respects_preprocessing(); + check_nested_tuple_assumption_sat(); + check_tuple_with_scalar_leaf(); + check_tuple_repeat_solve_resets_assumptions(); + check_tuple_empty_model_uses_default_value(); + check_tuple_model_hint(); + check_tuple_interpolation_refutation(); + check_interpolation_preserves_refutation_error(); + check_tuple_with_unsupported_leaf_rejected(); + check_term_shape_check_preserved(); + + yices_exit(); + printf("test_issue_615_assumption_type: PASS\n"); + return 0; +}