From f214c70cab9c0d5a7c0ca83e232e762745ffaa3f Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Tue, 5 May 2026 08:02:00 -0700 Subject: [PATCH 1/5] Fix issue #615: crash in mcsat_value_construct_from_value during interpolation 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 (uninterpreted, function, tuple, or finite-field types), Yices crashed with mcsat/value.c:478: mcsat_value_construct_from_value: Assertion `false' failed. (or a SIGSEGV in release builds), inside the call stack: mcsat_decide_assumption -> mcsat_value_construct_from_value() Root cause: * mcsat_value_construct_from_value handles only BOOLEAN, RATIONAL, ALGEBRAIC, FINITEFIELD, and BITVECTOR value kinds; it asserts(false) on every other kind. * Independently, the uf_plugin (decision-maker for UNINTERPRETED_TYPE and FUNCTION_TYPE) and ff_plugin (decision-maker for FF_TYPE) have decide_assignment == NULL, so even if value construction succeeded the next step in mcsat_decide_assumption would dereference NULL. * The API entry points only verified that the assumption term was uninterpreted, not that its type was one MCSAT could actually decide on, so unsupported types reached the solver and tripped the assertion / crashed. Fix: validate the type kind of every assumption term at the API boundary and reject anything that is not BOOL_TYPE, INT_TYPE, REAL_TYPE, SCALAR_TYPE, or BITVECTOR_TYPE (the type kinds whose plugins provide a non-NULL decide_assignment). A new error code MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED distinguishes "wrong type" (this fix) from the existing MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED ("not an uninterpreted term"). Both yices_check_context_with_model and yices_check_context_with_model_and_hint now report the new code, and yices_check_context_with_interpolation propagates it through its internal yices_check_context_with_model call instead of crashing. Files: * src/api/yices_api.c -- new check_mcsat_assumption_types helper plus _o_good_assumption_terms_for_mcsat; wired into the two check_with_model entry points. * src/include/yices_types.h -- new MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. * src/include/yices.h -- documented the new error code on the affected functions. * src/api/yices_error.c -- yices_print_error / yices_error_string. * src/frontend/smt2/smt2_commands.c -- SMT2 frontend error printer. * tests/api/test_issue_615_assumption_type.c -- regression test covering uninterpreted-sort, function-type, supported-type, and non-uninterpreted-term cases. Verified: * New regression test passes in debug and release. * make MODE=release check 1705 pass / 0 fail. * make MODE=release check-api 31/31 pass. --- src/api/yices_api.c | 74 ++++++++- src/api/yices_error.c | 8 + src/frontend/smt2/smt2_commands.c | 4 + src/include/yices.h | 8 + src/include/yices_types.h | 1 + tests/api/test_issue_615_assumption_type.c | 173 +++++++++++++++++++++ 6 files changed, 260 insertions(+), 8 deletions(-) create mode 100644 tests/api/test_issue_615_assumption_type.c diff --git a/src/api/yices_api.c b/src/api/yices_api.c index b7da07b20..4688cd866 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -2534,6 +2534,45 @@ static bool check_good_vars_or_uninterpreted(term_manager_t *mngr, uint32_t n, c return true; } +// Check that the type of every term in v is one that the MCSAT solver can +// decide on as an assumption value (i.e. a type whose plugin provides a +// non-NULL decide_assignment callback). The supported assumption types are: +// BOOL_TYPE, INT_TYPE, REAL_TYPE, SCALAR_TYPE, BITVECTOR_TYPE. +// Other type kinds (UNINTERPRETED_TYPE, FUNCTION_TYPE, TUPLE_TYPE, FF_TYPE, +// ...) 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 = term_type(tbl, v[i]); + 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 +9610,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, where assumption terms of type + * UNINTERPRETED_TYPE, FUNCTION_TYPE, TUPLE_TYPE, FF_TYPE, etc. trigger an + * assertion failure deep in the MCSAT solver. + */ +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 +9639,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 +9726,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; } 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..88d5b2046 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3370,6 +3370,10 @@ __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, or BitVector) + * code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED + * * If the context does not have the MCSAT solver enabled * code = CTX_OPERATION_NOT_SUPPORTED * @@ -3418,6 +3422,10 @@ __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, or BitVector) + * code = MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED + * * If the context does not have the MCSAT solver enabled * code = CTX_OPERATION_NOT_SUPPORTED * 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/tests/api/test_issue_615_assumption_type.c b/tests/api/test_issue_615_assumption_type.c new file mode 100644 index 000000000..39d055844 --- /dev/null +++ b/tests/api/test_issue_615_assumption_type.c @@ -0,0 +1,173 @@ +/* + * 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, tuple, or finite-field types). + * + * The fix turns these crashes into a clean YICES_STATUS_ERROR with error code + * MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. + */ + +#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; +} + +/* + * 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); + + 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); + + 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); + /* Must not error and must not crash. */ + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + + 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); + 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_term_shape_check_preserved(); + + yices_exit(); + printf("test_issue_615_assumption_type: PASS\n"); + return 0; +} From b217b9a1e598b50b66d617138864266e48cdbb8a Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Tue, 5 May 2026 08:58:51 -0700 Subject: [PATCH 2/5] test_issue_615: replace assert() with CHECK() macro CI builds the api tests with -DNDEBUG -Werror=unused-variable, which turned every assert() into a no-op and produced 'unused variable s' errors on the smt_status_t locals. Replace assert() with a small CHECK() macro that is always live and calls exit(1) on failure, so the test fails as intended in both debug and release builds. Drop the now-unused include. --- tests/api/test_issue_615_assumption_type.c | 41 ++++++++++++++-------- 1 file changed, 27 insertions(+), 14 deletions(-) diff --git a/tests/api/test_issue_615_assumption_type.c b/tests/api/test_issue_615_assumption_type.c index 39d055844..68ea54305 100644 --- a/tests/api/test_issue_615_assumption_type.c +++ b/tests/api/test_issue_615_assumption_type.c @@ -12,13 +12,26 @@ * MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. */ -#include #include #include #include #include +/* + * CHECK(cond) is used instead of assert() so the test still fails when the + * code is compiled with -DNDEBUG (release builds). Otherwise the smt_status_t + * variables we check would also become "unused" under -Werror=unused-variable. + */ +#define CHECK(cond) \ + do { \ + if (!(cond)) { \ + fprintf(stderr, "%s:%d: CHECK failed: %s\n", \ + __FILE__, __LINE__, #cond); \ + exit(1); \ + } \ + } while (0) + 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; @@ -41,7 +54,7 @@ static context_t *make_mcsat_context(bool model_interpolation) { */ static void check_uninterpreted_sort_assumption_rejected(void) { context_t *ctx = make_mcsat_context(false); - assert(ctx != NULL); + CHECK(ctx != NULL); type_t T = yices_new_uninterpreted_type(); term_t x = yices_new_uninterpreted_term(T); @@ -58,14 +71,14 @@ static void check_uninterpreted_sort_assumption_rejected(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 2, assumptions); - assert(s == YICES_STATUS_ERROR); - assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + CHECK(s == YICES_STATUS_ERROR); + CHECK(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); + CHECK(s == YICES_STATUS_ERROR); + CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); @@ -78,7 +91,7 @@ static void check_uninterpreted_sort_assumption_rejected(void) { */ static void check_function_type_assumption_rejected(void) { context_t *ctx = make_mcsat_context(false); - assert(ctx != NULL); + CHECK(ctx != NULL); type_t int_t = yices_int_type(); type_t dom[1] = { int_t }; @@ -95,8 +108,8 @@ static void check_function_type_assumption_rejected(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); - assert(s == YICES_STATUS_ERROR); - assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + CHECK(s == YICES_STATUS_ERROR); + CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); @@ -110,7 +123,7 @@ static void check_function_type_assumption_rejected(void) { */ static void check_supported_types_still_work(void) { context_t *ctx = make_mcsat_context(false); - assert(ctx != NULL); + CHECK(ctx != NULL); /* x : Real; assert x > 0; assumption x with model x = 1 -> SAT */ term_t x = yices_new_uninterpreted_term(yices_real_type()); @@ -124,7 +137,7 @@ static void check_supported_types_still_work(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); /* Must not error and must not crash. */ - assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + CHECK(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); yices_free_model(mdl); yices_free_context(ctx); @@ -137,7 +150,7 @@ static void check_supported_types_still_work(void) { */ static void check_term_shape_check_preserved(void) { context_t *ctx = make_mcsat_context(false); - assert(ctx != NULL); + CHECK(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 */ @@ -147,8 +160,8 @@ static void check_term_shape_check_preserved(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); - assert(s == YICES_STATUS_ERROR); - assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + CHECK(s == YICES_STATUS_ERROR); + CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); From 020f3585640aad0bb358ee23afc313b109afcef3 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Tue, 5 May 2026 09:10:45 -0700 Subject: [PATCH 3/5] test_issue_615: drop CHECK macro, use plain assert + (void)s Match the codebase style: tests use assert() and rely on debug-mode CI to catch regressions. Silence the release-mode unused-variable warning on the smt_status_t locals with (void) s;. --- tests/api/test_issue_615_assumption_type.c | 45 +++++++++------------- 1 file changed, 18 insertions(+), 27 deletions(-) diff --git a/tests/api/test_issue_615_assumption_type.c b/tests/api/test_issue_615_assumption_type.c index 68ea54305..3dd52444a 100644 --- a/tests/api/test_issue_615_assumption_type.c +++ b/tests/api/test_issue_615_assumption_type.c @@ -12,26 +12,13 @@ * MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. */ +#include #include #include #include #include -/* - * CHECK(cond) is used instead of assert() so the test still fails when the - * code is compiled with -DNDEBUG (release builds). Otherwise the smt_status_t - * variables we check would also become "unused" under -Werror=unused-variable. - */ -#define CHECK(cond) \ - do { \ - if (!(cond)) { \ - fprintf(stderr, "%s:%d: CHECK failed: %s\n", \ - __FILE__, __LINE__, #cond); \ - exit(1); \ - } \ - } while (0) - 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; @@ -54,7 +41,7 @@ static context_t *make_mcsat_context(bool model_interpolation) { */ static void check_uninterpreted_sort_assumption_rejected(void) { context_t *ctx = make_mcsat_context(false); - CHECK(ctx != NULL); + assert(ctx != NULL); type_t T = yices_new_uninterpreted_type(); term_t x = yices_new_uninterpreted_term(T); @@ -70,15 +57,16 @@ static void check_uninterpreted_sort_assumption_rejected(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 2, assumptions); + (void) s; - CHECK(s == YICES_STATUS_ERROR); - CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + 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); - CHECK(s == YICES_STATUS_ERROR); - CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); @@ -91,7 +79,7 @@ static void check_uninterpreted_sort_assumption_rejected(void) { */ static void check_function_type_assumption_rejected(void) { context_t *ctx = make_mcsat_context(false); - CHECK(ctx != NULL); + assert(ctx != NULL); type_t int_t = yices_int_type(); type_t dom[1] = { int_t }; @@ -107,9 +95,10 @@ static void check_function_type_assumption_rejected(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); + (void) s; - CHECK(s == YICES_STATUS_ERROR); - CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); @@ -123,7 +112,7 @@ static void check_function_type_assumption_rejected(void) { */ static void check_supported_types_still_work(void) { context_t *ctx = make_mcsat_context(false); - CHECK(ctx != NULL); + 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()); @@ -136,8 +125,9 @@ static void check_supported_types_still_work(void) { 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. */ - CHECK(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); + assert(s == YICES_STATUS_SAT || s == YICES_STATUS_UNKNOWN); yices_free_model(mdl); yices_free_context(ctx); @@ -150,7 +140,7 @@ static void check_supported_types_still_work(void) { */ static void check_term_shape_check_preserved(void) { context_t *ctx = make_mcsat_context(false); - CHECK(ctx != NULL); + 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 */ @@ -160,8 +150,9 @@ static void check_term_shape_check_preserved(void) { smt_status_t s = yices_check_context_with_model(ctx, NULL, mdl, 1, assumptions); - CHECK(s == YICES_STATUS_ERROR); - CHECK(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); + (void) s; + assert(s == YICES_STATUS_ERROR); + assert(yices_error_code() == MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED); yices_clear_error(); yices_free_model(mdl); From b53a1406c381519bfe418130c020ca043adcc739 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 00:22:35 -0700 Subject: [PATCH 4/5] mcsat: support tuple-valued model assumptions Generalize issue #615 model-assumption validation so tuple-typed assumption variables are accepted when every recursively flattened leaf has an MCSAT-decidable scalar type: Bool, Int, Real, scalar, or BitVector. Unsupported leaves such as uninterpreted-sort, function, and finite-field values still fail at the API boundary with MCSAT_ERROR_ASSUMPTION_TYPE_NOT_SUPPORTED. Carry flattened tuple model values alongside the tuple-blasted leaf variables used for MCSAT assumptions and model hints. Tuple assumption leaves also follow the scalar assumption preprocessing path, reasserting leaf equalities when preprocessing substituted a leaf before registering the public leaf as an assumption decision. Tuple hints intentionally remain advisory cache entries and do not assert preprocessing equalities. Keep scalar assumptions sound by constructing scalar model values through the rational plugin using the scalar constant index, and document that embedding. Preserve interpolation cleanup by popping both pushed contexts while retaining the original model-refutation error report. Document the tuple-blast helper contract, share tuple leaf/value collection across assumptions and hints, and make the malformed-model failure path explicit. Add regression coverage for scalar assumptions, scalar tuple leaves, repeat tuple-assumption solves, tuple assumptions with preprocessor substitutions, nested tuple flattening, tuple hints/interpolation, and unsupported tuple leaves. --- src/api/yices_api.c | 84 ++++-- src/include/yices.h | 11 +- src/mcsat/preprocessor.c | 6 + src/mcsat/preprocessor.h | 8 + src/mcsat/solver.c | 212 ++++++++++++--- tests/api/test_issue_615_assumption_type.c | 290 ++++++++++++++++++++- 6 files changed, 550 insertions(+), 61 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 4688cd866..7fded0675 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -2534,12 +2534,38 @@ 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 (i.e. a type whose plugin provides a -// non-NULL decide_assignment callback). The supported assumption types are: -// BOOL_TYPE, INT_TYPE, REAL_TYPE, SCALAR_TYPE, BITVECTOR_TYPE. -// Other type kinds (UNINTERPRETED_TYPE, FUNCTION_TYPE, TUPLE_TYPE, FF_TYPE, -// ...) reach the MCSAT solver but trigger an assertion failure inside +// 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). // @@ -2552,22 +2578,14 @@ static bool check_mcsat_assumption_types(term_manager_t *mngr, uint32_t n, const 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 = term_type(tbl, v[i]); + error->type1 = tau; return false; } - } } return true; @@ -9613,9 +9631,9 @@ static bool good_terms_for_check_with_model(uint32_t n, const term_t 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, where assumption terms of type - * UNINTERPRETED_TYPE, FUNCTION_TYPE, TUPLE_TYPE, FF_TYPE, etc. trigger an - * assertion failure deep in the MCSAT solver. + * 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) @@ -9938,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/include/yices.h b/src/include/yices.h index 88d5b2046..80b955237 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3371,7 +3371,8 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte * 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, or BitVector) + * (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 @@ -3423,7 +3424,8 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t * * 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, or BitVector) + * (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 @@ -3514,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/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 001e680f1..f7e056e4b 100644 --- a/src/mcsat/preprocessor.c +++ b/src/mcsat/preprocessor.c @@ -2388,6 +2388,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 index 3dd52444a..8b1750f9b 100644 --- a/tests/api/test_issue_615_assumption_type.c +++ b/tests/api/test_issue_615_assumption_type.c @@ -6,17 +6,23 @@ * (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, tuple, or finite-field types). + * (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) { @@ -35,6 +41,49 @@ static context_t *make_mcsat_context(bool model_interpolation) { 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. @@ -131,6 +180,236 @@ static void check_supported_types_still_work(void) { 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_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_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); } /* @@ -169,6 +448,15 @@ int main(void) { 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_model_hint(); + check_tuple_interpolation_refutation(); + check_tuple_with_unsupported_leaf_rejected(); check_term_shape_check_preserved(); yices_exit(); From 2139806617878753a5d2dee8dc0c83a488c07744 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 08:52:17 -0700 Subject: [PATCH 5/5] tests: cover issue615 tuple model edge cases Add regression coverage for tuple-valued model assumptions with omitted model entries and for interpolation error preservation when internal model refutation rejects unsupported assumption types. --- tests/api/test_issue_615_assumption_type.c | 43 ++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/tests/api/test_issue_615_assumption_type.c b/tests/api/test_issue_615_assumption_type.c index 8b1750f9b..cd89d939a 100644 --- a/tests/api/test_issue_615_assumption_type.c +++ b/tests/api/test_issue_615_assumption_type.c @@ -336,6 +336,24 @@ static void check_tuple_repeat_solve_resets_assumptions(void) { 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); @@ -381,6 +399,29 @@ static void check_tuple_interpolation_refutation(void) { 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); @@ -454,8 +495,10 @@ int main(void) { 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();