From 51785b09abffbacbfd9c599fc7648936291b055e Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 20:21:20 -0700 Subject: [PATCH 1/9] Draft: integrate supplementary MCSAT satellite in CDCL(T) --- src/Makefile | 1 + src/api/search_parameters.c | 47 +- src/api/search_parameters.h | 18 + src/api/yices_api.c | 1 + src/context/context.c | 528 ++++++++++ src/context/context_simplifier.c | 40 +- src/context/context_solver.c | 187 +++- src/context/context_types.h | 5 +- src/context/context_utils.h | 9 +- src/context/shared_terms.c | 21 +- src/frontend/common/parameters.c | 39 + src/frontend/common/parameters.h | 7 + src/frontend/smt2/smt2_commands.c | 59 +- src/frontend/smt2/smt2_commands.h | 7 + src/frontend/yices/yices_help.c | 14 +- src/frontend/yices/yices_reval.c | 13 +- src/frontend/yices_smt2.c | 20 +- src/mcsat/solver.c | 19 +- src/solvers/egraph/egraph.c | 68 ++ src/solvers/egraph/egraph.h | 16 + src/solvers/egraph/egraph_base_types.h | 15 +- src/solvers/egraph/egraph_printer.c | 5 +- src/solvers/egraph/egraph_types.h | 2 + src/solvers/mcsat_satellite.c | 1132 ++++++++++++++++++++++ src/solvers/mcsat_satellite.h | 85 ++ src/terms/term_explorer.c | 16 +- tests/regress/both/README.md | 16 + tests/regress/both/smoke_sat.smt2 | 4 + tests/regress/both/smoke_sat.smt2.gold | 1 + tests/regress/both/smoke_unsat.smt2 | 5 + tests/regress/both/smoke_unsat.smt2.gold | 1 + tests/regress/check.sh | 2 +- tests/regress/run_test.sh | 130 ++- 33 files changed, 2442 insertions(+), 91 deletions(-) create mode 100644 src/solvers/mcsat_satellite.c create mode 100644 src/solvers/mcsat_satellite.h create mode 100644 tests/regress/both/README.md create mode 100644 tests/regress/both/smoke_sat.smt2 create mode 100644 tests/regress/both/smoke_sat.smt2.gold create mode 100644 tests/regress/both/smoke_unsat.smt2 create mode 100644 tests/regress/both/smoke_unsat.smt2.gold diff --git a/src/Makefile b/src/Makefile index b3a79be6e..b646acc6f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -198,6 +198,7 @@ core_src_c := \ solvers/egraph/egraph_explanations.c \ solvers/egraph/egraph_utils.c \ solvers/egraph/theory_explanations.c \ + solvers/mcsat_satellite.c \ solvers/floyd_warshall/dl_vartable.c \ solvers/floyd_warshall/idl_floyd_warshall.c \ solvers/floyd_warshall/rdl_floyd_warshall.c \ diff --git a/src/api/search_parameters.c b/src/api/search_parameters.c index a798e352d..105c9e704 100644 --- a/src/api/search_parameters.c +++ b/src/api/search_parameters.c @@ -101,6 +101,7 @@ #define DEFAULT_USE_BOOL_DYN_ACK false #define DEFAULT_USE_OPTIMISTIC_FCHECK true #define DEFAULT_AUX_EQ_RATIO 0.3 +#define DEFAULT_MCSAT_SUPPLEMENT_CHECK MCSAT_SUPPLEMENT_CHECK_BOTH /* @@ -165,6 +166,7 @@ static const param_t default_settings = { DEFAULT_MAX_UPDATE_CONFLICTS, DEFAULT_MAX_EXTENSIONALITY, + DEFAULT_MCSAT_SUPPLEMENT_CHECK, }; @@ -221,9 +223,10 @@ typedef enum param_key { // array solver PARAM_MAX_UPDATE_CONFLICTS, PARAM_MAX_EXTENSIONALITY, + PARAM_MCSAT_SUPPLEMENT_CHECK, } param_key_t; -#define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+1) +#define NUM_PARAM_KEYS (PARAM_MCSAT_SUPPLEMENT_CHECK+1) // parameter names in lexicographic ordering static const char *const param_key_names[NUM_PARAM_KEYS] = { @@ -249,6 +252,7 @@ static const char *const param_key_names[NUM_PARAM_KEYS] = { "max-extensionality", "max-interface-eqs", "max-update-conflicts", + "mcsat-supplement-check", "optimistic-final-check", "prop-threshold", "r-factor", @@ -286,6 +290,7 @@ static const int32_t param_code[NUM_PARAM_KEYS] = { PARAM_MAX_EXTENSIONALITY, PARAM_MAX_INTERFACE_EQS, PARAM_MAX_UPDATE_CONFLICTS, + PARAM_MCSAT_SUPPLEMENT_CHECK, PARAM_OPTIMISTIC_FCHECK, PARAM_PROP_THRESHOLD, PARAM_R_FACTOR, @@ -322,6 +327,19 @@ static const int32_t branching_code[NUM_BRANCHING_MODES] = { BRANCHING_THEORY, }; +/* + * Supplementary MCSAT checking modes (in lexicographic order) + */ +static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + "both", + "final-only", +}; + +static const int32_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +}; + @@ -380,6 +398,29 @@ static int32_t set_branching_param(const char *value, branch_t *v) { return k; } +/* + * Parse value as supplementary MCSAT check mode. Store the result in *v. + * - return 0 if this works + * - return -2 otherwise + */ +static int32_t set_mcsat_supplement_check_param(const char *value, mcsat_supplement_check_t *v) { + int32_t k; + + k = parse_as_keyword(value, mcsat_supplement_check_modes, mcsat_supplement_check_code, + NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + assert(k >= 0 || k == -1); + + if (k >= 0) { + assert(MCSAT_SUPPLEMENT_CHECK_BOTH <= k && k <= MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY); + *v = (mcsat_supplement_check_t) k; + k = 0; + } else { + k = -2; + } + + return k; +} + /* * Parse val as a signed 32bit integer. Check whether @@ -685,6 +726,10 @@ int32_t params_set_field(param_t *parameters, const char *key, const char *value } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + r = set_mcsat_supplement_check_param(value, ¶meters->mcsat_supplement_check); + break; + default: assert(k == -1); r = -1; diff --git a/src/api/search_parameters.h b/src/api/search_parameters.h index ddcb4b158..57ff401b5 100644 --- a/src/api/search_parameters.h +++ b/src/api/search_parameters.h @@ -45,6 +45,17 @@ typedef enum { #define NUM_BRANCHING_MODES 6 +/* + * Supplementary MCSAT check mode (for CDCL(T) mode) + */ +typedef enum { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +} mcsat_supplement_check_t; + +// keep in sync with mcsat_supplement_check_modes in search_parameters.c +#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2 + struct param_s { /* @@ -170,6 +181,13 @@ struct param_s { uint32_t max_update_conflicts; uint32_t max_extensionality; + /* + * Supplementary MCSAT checks in CDCL(T) + * - BOTH: run in propagate and final_check + * - FINAL_ONLY: run in final_check only + */ + mcsat_supplement_check_t mcsat_supplement_check; + }; diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 6eedb9aba..1b28e2598 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8693,6 +8693,7 @@ static const error_code_t intern_code2error[NUM_INTERNALIZATION_ERRORS] = { CTX_BV_SOLVER_EXCEPTION, MCSAT_ERROR_UNSUPPORTED_THEORY, CTX_HIGH_ORDER_FUN_NOT_SUPPORTED, + MCSAT_ERROR_UNSUPPORTED_THEORY, }; static inline void convert_internalization_error(int32_t code) { diff --git a/src/context/context.c b/src/context/context.c index 27ee78d96..17339ea70 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -22,6 +22,7 @@ #include +#include "api/context_config.h" #include "context/context.h" #include "context/context_simplifier.h" #include "context/context_utils.h" @@ -31,10 +32,13 @@ #include "solvers/floyd_warshall/idl_floyd_warshall.h" #include "solvers/floyd_warshall/rdl_floyd_warshall.h" #include "solvers/funs/fun_solver.h" +#include "solvers/mcsat_satellite.h" #include "solvers/quant/quant_solver.h" #include "solvers/simplex/simplex.h" #include "terms/poly_buffer_terms.h" +#include "terms/term_explorer.h" #include "terms/term_utils.h" +#include "utils/int_hash_map.h" #include "utils/memalloc.h" #include "mcsat/solver.h" @@ -73,6 +77,424 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t); static thvar_t internalize_to_arith(context_t *ctx, term_t t); static thvar_t internalize_to_bv(context_t *ctx, term_t t); +static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx); +static bool context_atom_requires_mcsat(context_t *ctx, term_t atom); +static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom); +static int32_t context_enable_mcsat_supplement(context_t *ctx); +static void context_disable_mcsat_supplement(context_t *ctx); +static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a); +static int32_t context_seed_mcsat_satellite(context_t *ctx); + + +/* + * Supplementary MCSAT support (CDCL(T) mode) + */ +static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx) { + if (ctx->egraph == NULL) { + return NULL; + } + return (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; +} + +static inline bool divisor_requires_mcsat(term_table_t *terms, term_t t) { + t = unsigned_term(t); + if (term_kind(terms, t) != ARITH_CONSTANT) { + return true; + } + return q_is_zero(rational_term_desc(terms, t)); +} + +/* + * Detect whether t contains arithmetic or finite-field subterms. + * This is used to route all relevant arithmetic/FF atoms to the supplementary + * MCSAT context once supplementation is active. + */ +static bool term_contains_arith_or_ff(context_t *ctx, term_t t, int_hmap_t *cache) { + term_table_t *terms; + int_hmap_pair_t *p; + type_t tau; + type_kind_t tkind; + bool found; + uint32_t i, nchildren; + + if (t < 0) { + return false; + } + + t = unsigned_term(t); + p = int_hmap_find(cache, t); + if (p != NULL) { + return p->val != 0; + } + + terms = ctx->terms; + tau = term_type(terms, t); + tkind = type_kind(terms->types, tau); + + /* + * Variables of arithmetic/finite-field type may not satisfy + * is_arithmetic_term/is_finitefield_term, so include type-based detection. + */ + found = is_arithmetic_term(terms, t) || is_finitefield_term(terms, t) || + tkind == INT_TYPE || tkind == REAL_TYPE || is_ff_type(terms->types, tau); + + if (!found) { + if (term_is_projection(terms, t)) { + found = term_contains_arith_or_ff(ctx, proj_term_arg(terms, t), cache); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + term_t child; + mpq_t q; + mpq_init(q); + sum_term_component(terms, t, i, q, &child); + found = term_contains_arith_or_ff(ctx, child, cache); + mpq_clear(q); + } + + } else if (term_is_bvsum(terms, t)) { + int32_t *aux; + uint32_t nbits; + term_t child; + + nbits = term_bitsize(terms, t); + aux = (int32_t *) safe_malloc(nbits * sizeof(int32_t)); + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + bvsum_term_component(terms, t, i, aux, &child); + found = term_contains_arith_or_ff(ctx, child, cache); + } + safe_free(aux); + + } else if (term_is_product(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + term_t child; + uint32_t exp; + product_term_component(terms, t, i, &child, &exp); + found = term_contains_arith_or_ff(ctx, child, cache); + } + + } else if (term_is_composite(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + found = term_contains_arith_or_ff(ctx, term_child(terms, t, i), cache); + } + } + } + + p = int_hmap_get(cache, t); + p->val = found ? 1 : 0; + return found; +} + +static bool term_requires_mcsat_supplement(context_t *ctx, term_t t, int_hmap_t *cache) { + term_table_t *terms; + int_hmap_pair_t *p; + bool trigger; + uint32_t i, nchildren; + + if (t < 0) { + return false; + } + + t = unsigned_term(t); + p = int_hmap_find(cache, t); + if (p != NULL) { + return p->val != 0; + } + + terms = ctx->terms; + trigger = false; + + // finite-field usage + if (is_finitefield_term(terms, t)) { + trigger = true; + } + + if (!trigger) { + switch (term_kind(terms, t)) { + case ARITH_ROOT_ATOM: + case ARITH_FF_CONSTANT: + case ARITH_FF_POLY: + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + trigger = true; + break; + + case ARITH_RDIV: + trigger = divisor_requires_mcsat(terms, arith_rdiv_term_desc(terms, t)->arg[1]); + break; + + case ARITH_IDIV: + trigger = divisor_requires_mcsat(terms, arith_idiv_term_desc(terms, t)->arg[1]); + break; + + case ARITH_MOD: + trigger = divisor_requires_mcsat(terms, arith_mod_term_desc(terms, t)->arg[1]); + break; + + case ARITH_DIVIDES_ATOM: + trigger = divisor_requires_mcsat(terms, arith_divides_atom_desc(terms, t)->arg[0]); + break; + + default: + break; + } + } + + // arithmetic nonlinearity (including deep products in arithmetic predicates) + if (!trigger && is_arithmetic_term(terms, t) && term_degree(terms, t) > 1) { + trigger = true; + } + + if (!trigger) { + if (term_is_projection(terms, t)) { + trigger = term_requires_mcsat_supplement(ctx, proj_term_arg(terms, t), cache); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i=0; ival = trigger ? 1 : 0; + return trigger; +} + +static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a) { + int_hmap_t cache; + uint32_t i; + bool trigger; + + init_int_hmap(&cache, 0); + trigger = false; + for (i=0; imcsat_supplement_active) { + return CTX_NO_ERROR; + } + if (ctx->arch == CTX_ARCH_MCSAT || ctx->egraph == NULL) { + return CONTEXT_UNSUPPORTED_THEORY; + } + + sat = new_mcsat_satellite(ctx); + egraph_attach_mcsat_solver(ctx->egraph, sat, + mcsat_satellite_ctrl_interface(sat), + mcsat_satellite_smt_interface(sat), + mcsat_satellite_egraph_interface(sat)); + ctx->mcsat_supplement_active = true; + + code = context_seed_mcsat_satellite(ctx); + if (code < 0) { + context_disable_mcsat_supplement(ctx); + return code; + } + + return CTX_NO_ERROR; +} + +static void context_disable_mcsat_supplement(context_t *ctx) { + mcsat_satellite_t *sat; + + if (!ctx->mcsat_supplement_active || ctx->egraph == NULL) { + return; + } + + sat = context_mcsat_satellite(ctx); + egraph_detach_mcsat_solver(ctx->egraph); + delete_mcsat_satellite(sat); + ctx->mcsat_supplement_active = false; +} + +/* + * Import already-internalized arithmetic/FF atoms when supplementary MCSAT + * is activated after earlier assertions. + */ +static int32_t context_seed_mcsat_satellite(context_t *ctx) { + mcsat_satellite_t *sat; + term_table_t *terms; + uint32_t i, n; + uint32_t seeded = 0; + bool trace_seed; + + sat = context_mcsat_satellite(ctx); + if (sat == NULL) { + return CTX_NO_ERROR; + } + + terms = ctx->terms; + trace_seed = tracing_tag(ctx->trace, "mcsat::supplement::seed"); + n = intern_tbl_num_terms(&ctx->intern); + for (i = 1; i < n; i++) { + term_t t; + int32_t code; + literal_t l; + + if (!good_term_idx(terms, i)) { + continue; + } + + t = pos_term(i); + if (!is_boolean_term(terms, t) || + !intern_tbl_is_root(&ctx->intern, t) || + !intern_tbl_root_is_mapped(&ctx->intern, t)) { + continue; + } + + if (!context_atom_requires_mcsat(ctx, t)) { + continue; + } + + code = intern_tbl_map_of_root(&ctx->intern, t); + if (code_is_var(code)) { + l = code2literal(code); + } else { + occ_t u = code2occ(code); + if (u == true_occ) { + l = true_literal; + } else if (u == false_occ) { + l = false_literal; + } else if (ctx->egraph != NULL) { + l = egraph_occ2literal(ctx->egraph, u); + } else { + continue; + } + } + + code = mcsat_satellite_register_atom(sat, t, l, NULL); + if (code < 0) { + return code; + } + seeded ++; + if (trace_seed) { + trace_printf(ctx->trace, 1, "mcsat supplement seed: lit=%"PRId32" atom=", l); + trace_pp_term(ctx->trace, 1, terms, t); + } + } + + if (trace_seed) { + trace_printf(ctx->trace, 1, "mcsat supplement seeded %"PRIu32" atoms\n", seeded); + } + + return CTX_NO_ERROR; +} + +static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { + switch (term_kind(terms, atom)) { + case EQ_TERM: + case DISTINCT_TERM: + case ARITH_ROOT_ATOM: + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + case ARITH_IS_INT_ATOM: + case ARITH_EQ_ATOM: + case ARITH_GE_ATOM: + case ARITH_BINEQ_ATOM: + case ARITH_DIVIDES_ATOM: + return true; + + default: + return false; + } +} + +static bool context_atom_requires_mcsat(context_t *ctx, term_t atom) { + int_hmap_t cache; + bool trigger, all_arith_mode; + + atom = unsigned_term(atom); + if (!ctx->mcsat_supplement_active || !is_boolean_term(ctx->terms, atom)) { + return false; + } + if (!mcsat_satellite_candidate_atom(ctx->terms, atom)) { + return false; + } + + init_int_hmap(&cache, 0); + /* + * In supplementary mode, route every arithmetic/FF atom to MCSAT so that + * MCSAT sees the complete arithmetic conjunction (not just unsupported atoms). + */ + all_arith_mode = true; + if (all_arith_mode) { + trigger = term_contains_arith_or_ff(ctx, atom, &cache); + } else { + trigger = term_requires_mcsat_supplement(ctx, atom, &cache); + } + delete_int_hmap(&cache); + + return trigger; +} + +static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { + mcsat_satellite_t *sat; + literal_t l; + void *obj; + int32_t code; + + sat = context_mcsat_satellite(ctx); + assert(sat != NULL); + + l = pos_lit(create_boolean_variable(ctx->core)); + obj = NULL; + code = mcsat_satellite_register_atom(sat, atom, l, &obj); + if (code < 0) { + longjmp(ctx->env, code); + } + + attach_atom_to_bvar(ctx->core, var_of(l), tagged_mcsat_atom(obj)); + return l; +} + /**************************************** @@ -1848,6 +2270,13 @@ static thvar_t map_bvpoly_buffer_to_bv(context_t *ctx, bvpoly_buffer_t *b) { free_bvpoly(q); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_register_arith_term(sat, x, r); + } + } + return x; } @@ -2930,6 +3359,14 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat; + sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_register_arith_term(sat, x, unsigned_term(r)); + } + } + return x; abort: @@ -3185,6 +3622,12 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t) { /* * Recursively compute r's internalization */ + if (context_atom_requires_mcsat(ctx, r)) { + l = map_mcsat_atom_to_literal(ctx, r); + intern_tbl_map_root(&ctx->intern, r, literal2code(l)); + goto done; + } + terms = ctx->terms; switch (term_kind(terms, r)) { case CONSTANT_TERM: @@ -3237,6 +3680,15 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t) { l = map_arith_divides_to_literal(ctx, arith_divides_atom_desc(terms, r)); break; + case ARITH_ROOT_ATOM: + longjmp(ctx->env, FORMULA_NOT_LINEAR); + break; + + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + longjmp(ctx->env, CONTEXT_UNSUPPORTED_THEORY); + break; + case APP_TERM: l = map_apply_to_literal(ctx, app_term_desc(terms, r)); break; @@ -4688,6 +5140,7 @@ static void assert_toplevel_bvsge(context_t *ctx, composite_term_t *sge, bool tt static void assert_toplevel_formula(context_t *ctx, term_t t) { term_table_t *terms; int32_t code; + literal_t l; bool tt; assert(is_boolean_term(ctx->terms, t) && @@ -4704,6 +5157,14 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { * tt false: assert (not t) */ terms = ctx->terms; + if (context_atom_requires_mcsat(ctx, t)) { + l = map_mcsat_atom_to_literal(ctx, t); + code = literal2code(l); + intern_tbl_remap_root(&ctx->intern, t, code); + assert_internalization_code(ctx, code, tt); + return; + } + switch (term_kind(terms, t)) { case CONSTANT_TERM: case UNINTERPRETED_TERM: @@ -4808,6 +5269,7 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { static void assert_term(context_t *ctx, term_t t, bool tt) { term_table_t *terms; int32_t code; + literal_t l; assert(is_boolean_term(ctx->terms, t)); @@ -4829,6 +5291,14 @@ static void assert_term(context_t *ctx, term_t t, bool tt) { assert_internalization_code(ctx, code, tt); } else { + if (context_atom_requires_mcsat(ctx, t)) { + l = map_mcsat_atom_to_literal(ctx, t); + code = literal2code(l); + intern_tbl_map_root(&ctx->intern, t, code); + assert_internalization_code(ctx, code, tt); + return; + } + // store the mapping t --> tt intern_tbl_map_root(&ctx->intern, t, bool2code(tt)); @@ -5499,6 +5969,7 @@ static void init_solvers(context_t *ctx) { ctx->bv_solver = NULL; ctx->fun_solver = NULL; ctx->quant_solver = NULL; + ctx->mcsat_supplement_active = false; // Create egraph first, then satellite solvers if (solvers & EGRPH) { @@ -5745,6 +6216,10 @@ void delete_context(context_t *ctx) { ctx->mcsat = NULL; } + if (ctx->mcsat_supplement_active) { + context_disable_mcsat_supplement(ctx); + } + if (ctx->egraph != NULL) { delete_egraph(ctx->egraph); safe_free(ctx->egraph); @@ -5835,6 +6310,10 @@ void reset_context(context_t *ctx) { reset_smt_core(ctx->core); // this propagates reset to all solvers + if (ctx->mcsat_supplement_active) { + context_disable_mcsat_supplement(ctx); + } + if (ctx->mcsat != NULL) { mcsat_reset(ctx->mcsat); } @@ -5892,6 +6371,12 @@ void context_set_trace(context_t *ctx, tracer_t *trace) { if (ctx->mcsat != NULL) { mcsat_set_tracer(ctx->mcsat, trace); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_set_trace(sat, trace); + } + } } @@ -5997,6 +6482,25 @@ static int32_t context_process_assertions(context_t *ctx, uint32_t n, const term ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { + if (context_assertions_need_mcsat_supplement(ctx, n, a)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + code = mcsat_satellite_assert_formulas(sat, n, a); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { @@ -6336,6 +6840,15 @@ int32_t context_internalize(context_t *ctx, term_t t) { ivector_reset(&ctx->subst_eqs); ivector_reset(&ctx->aux_eqs); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx) && !ctx->mcsat_supplement_active) { + if (context_assertions_need_mcsat_supplement(ctx, 1, &t)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { // we must call internalization start first @@ -6416,6 +6929,15 @@ int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f) { ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { + if (context_assertions_need_mcsat_supplement(ctx, n, f)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { // flatten @@ -6717,4 +7239,10 @@ void context_gc_mark(context_t *ctx) { if (ctx->mcsat != NULL) { mcsat_gc_mark(ctx->mcsat); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_gc_mark(sat); + } + } } diff --git a/src/context/context_simplifier.c b/src/context/context_simplifier.c index 836587e8b..824ca8706 100644 --- a/src/context/context_simplifier.c +++ b/src/context/context_simplifier.c @@ -1161,6 +1161,15 @@ static void try_substitution(context_t *ctx, term_t t1, term_t t2, term_t e) { assert(is_pos_term(t1) && is_pos_term(t2) && term_is_true(ctx, e)); + /* + * In supplementary-MCSAT mode, keep equalities explicit so they can be + * routed to the MCSAT satellite as tracked atoms/constraints. + */ + if (ctx->mcsat_supplement_active) { + ivector_push(&ctx->top_eqs, e); + return; + } + if (context_var_elim_enabled(ctx)) { intern = &ctx->intern; @@ -1200,6 +1209,14 @@ static void try_bool_substitution(context_t *ctx, term_t t1, term_t t2, term_t e assert(term_is_true(ctx, e)); + /* + * In supplementary-MCSAT mode, keep boolean equalities explicit. + */ + if (ctx->mcsat_supplement_active) { + ivector_push(&ctx->top_formulas, e); + return; + } + if (context_var_elim_enabled(ctx)) { intern = &ctx->intern; @@ -2245,8 +2262,14 @@ void flatten_assertion(context_t *ctx, term_t f) { break; case ARITH_ROOT_ATOM: - exception = FORMULA_NOT_LINEAR; - goto abort; + if (context_mcsat_supplement_active(ctx)) { + intern_tbl_map_root(intern, r, bool2code(tt)); + ivector_push(&ctx->top_atoms, signed_term(r, tt)); + } else { + exception = FORMULA_NOT_LINEAR; + goto abort; + } + break; case ARITH_IS_INT_ATOM: intern_tbl_map_root(intern, r, bool2code(tt)); @@ -2324,10 +2347,19 @@ void flatten_assertion(context_t *ctx, term_t f) { flatten_bit_select(ctx, r, tt); break; - case ARITH_FF_POLY: - case ARITH_FF_CONSTANT: case ARITH_FF_EQ_ATOM: case ARITH_FF_BINEQ_ATOM: + if (context_mcsat_supplement_active(ctx)) { + intern_tbl_map_root(intern, r, bool2code(tt)); + ivector_push(&ctx->top_atoms, signed_term(r, tt)); + } else { + exception = CONTEXT_UNSUPPORTED_THEORY; + goto abort; + } + break; + + case ARITH_FF_POLY: + case ARITH_FF_CONSTANT: exception = CONTEXT_UNSUPPORTED_THEORY; goto abort; } diff --git a/src/context/context_solver.c b/src/context/context_solver.c index beb420ff3..78d49ed69 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -35,6 +35,7 @@ #include "mcsat/solver.h" #include "solvers/bv/dimacs_printer.h" #include "solvers/cdcl/delegate.h" +#include "solvers/mcsat_satellite.h" #include "solvers/funs/fun_solver.h" #include "solvers/simplex/simplex.h" #include "terms/term_explorer.h" @@ -525,6 +526,10 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params) egraph_set_max_interface_eqs(egraph, params->max_interface_eqs); } + if (ctx->mcsat_supplement_active && egraph != NULL && egraph->th[ETYPE_MCSAT] != NULL) { + mcsat_satellite_set_search_parameters((mcsat_satellite_t *) egraph->th[ETYPE_MCSAT], params); + } + /* * Set simplex parameters */ @@ -555,8 +560,22 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params) } static smt_status_t _o_call_mcsat_solver(context_t *ctx, const param_t *params) { + smt_status_t stat; + mcsat_solve(ctx->mcsat, params, NULL, 0, NULL); - return mcsat_status(ctx->mcsat); + stat = mcsat_status(ctx->mcsat); + + /* + * For plain UNSAT results (without explicit model assumptions), keep the + * interpolant API usable by providing the canonical false interpolant. + */ + if (stat == YICES_STATUS_UNSAT && + context_supports_model_interpolation(ctx) && + mcsat_get_unsat_model_interpolant(ctx->mcsat) == NULL_TERM) { + mcsat_set_unsat_result(ctx->mcsat, false_term); + } + + return stat; } static smt_status_t call_mcsat_solver(context_t *ctx, const param_t *params) { @@ -571,6 +590,7 @@ static smt_status_t call_mcsat_solver(context_t *ctx, const param_t *params) { smt_status_t check_context(context_t *ctx, const param_t *params) { smt_core_t *core; smt_status_t stat; + mcsat_satellite_t *sat; if (params == NULL) { params = get_default_params(); @@ -589,6 +609,19 @@ smt_status_t check_context(context_t *ctx, const param_t *params) { stat = smt_status(core); } + sat = NULL; + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + if (stat == YICES_STATUS_UNSAT && + sat != NULL && + context_supports_model_interpolation(ctx) && + mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) { + mcsat_satellite_set_unsat_model_interpolant(sat, false_term); + } + return stat; } @@ -600,6 +633,7 @@ smt_status_t check_context(context_t *ctx, const param_t *params) { smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const literal_t *a) { smt_core_t *core; smt_status_t stat; + mcsat_satellite_t *sat; assert(ctx->mcsat == NULL); @@ -615,6 +649,19 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param stat = smt_status(core); } + sat = NULL; + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + if (stat == YICES_STATUS_UNSAT && + sat != NULL && + context_supports_model_interpolation(ctx) && + mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) { + mcsat_satellite_set_unsat_model_interpolant(sat, false_term); + } + return stat; } @@ -813,6 +860,75 @@ static smt_status_t check_context_with_term_assumptions_mcsat(context_t *ctx, co MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_mcsat(ctx, params, n, a, error)); } +/* + * Supplemental-MCSAT variant for term assumptions in CDCL(T) mode. + * We encode assumptions via fresh labels b_i with implications (b_i => a_i), + * then solve under assumptions b_i = true. + * + * Labels are kept in the context (no push/pop) so the regular context status + * and multicheck protocol remain unchanged. + */ +static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { + smt_status_t stat; + ivector_t assumptions; + term_t interpolant; + uint32_t i; + literal_t l; + mcsat_satellite_t *sat; + + init_ivector(&assumptions, n); + + stat = YICES_STATUS_IDLE; + interpolant = NULL_TERM; + sat = NULL; + + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + + for (i=0; imcsat == NULL) { - smt_status_t stat; - ivector_t assumptions; - uint32_t i; - literal_t l; - - init_ivector(&assumptions, n); - for (i=0; imcsat_supplement_active) { + return check_context_with_term_assumptions_supplement(ctx, params, n, a, error); + } else { + smt_status_t stat; + ivector_t assumptions; + uint32_t i; + literal_t l; + + init_ivector(&assumptions, n); + for (i=0; icore) == YICES_STATUS_SAT || smt_status(ctx->core) == YICES_STATUS_UNKNOWN || mcsat_status(ctx->mcsat) == YICES_STATUS_SAT); + assert(smt_status(ctx->core) == YICES_STATUS_SAT || + smt_status(ctx->core) == YICES_STATUS_UNKNOWN || + (context_has_mcsat(ctx) && mcsat_status(ctx->mcsat) == YICES_STATUS_SAT)); /* * First build assignments in the satellite solvers @@ -1352,6 +1474,14 @@ void build_model(model_t *model, context_t *ctx) { } } } + + /* + * Supplemental MCSAT values are an overlay: apply them after the regular + * CDCL(T) model is fully built so nonlinear/FF values are not overwritten. + */ + if (ctx->mcsat_supplement_active && context_has_egraph(ctx) && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + mcsat_satellite_build_model((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT], model); + } } @@ -1482,6 +1612,19 @@ void context_build_unsat_core(context_t *ctx, ivector_t *v) { * MODEL INTERPOLANT */ term_t context_get_unsat_model_interpolant(context_t *ctx) { - assert(ctx->mcsat != NULL); - return mcsat_get_unsat_model_interpolant(ctx->mcsat); + if (ctx->mcsat != NULL) { + return mcsat_get_unsat_model_interpolant(ctx->mcsat); + } + + if (ctx->mcsat_supplement_active && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + return mcsat_satellite_get_unsat_model_interpolant((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]); + } + + if (context_supports_model_interpolation(ctx) && + ctx->core != NULL && + smt_status(ctx->core) == YICES_STATUS_UNSAT) { + return false_term; + } + + return NULL_TERM; } diff --git a/src/context/context_types.h b/src/context/context_types.h index 9a7b39911..f7298ff94 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -736,6 +736,9 @@ struct context_s { // flag for enabling adding quant instances bool en_quant; + + // true when supplementary mcsat satellite is active in cdcl(t) mode + bool mcsat_supplement_active; }; @@ -796,7 +799,7 @@ enum { /* * NUM_INTERNALIZATION_ERRORS: must be (1 + number of negative codes) */ -#define NUM_INTERNALIZATION_ERRORS 24 +#define NUM_INTERNALIZATION_ERRORS 25 diff --git a/src/context/context_utils.h b/src/context/context_utils.h index 488a22fc7..e72bd9e2a 100644 --- a/src/context/context_utils.h +++ b/src/context/context_utils.h @@ -657,7 +657,11 @@ static inline bool context_has_quant_solver(context_t *ctx) { } static inline bool context_has_mcsat(context_t *ctx) { - return ctx->mcsat != NULL; + return ctx->arch == CTX_ARCH_MCSAT; +} + +static inline bool context_mcsat_supplement_active(context_t *ctx) { + return ctx->mcsat_supplement_active; } @@ -686,7 +690,7 @@ static inline bool context_supports_cleaninterrupt(context_t *ctx) { } static inline bool context_supports_model_interpolation(context_t* ctx) { - return (ctx->mcsat != NULL && ctx->mcsat_options.model_interpolation); + return (context_has_mcsat(ctx) && ctx->mcsat_options.model_interpolation); } /* @@ -706,4 +710,3 @@ static inline bool context_quant_enabled(context_t *ctx) { #endif /* __CONTEXT_UTILS_H */ - diff --git a/src/context/shared_terms.c b/src/context/shared_terms.c index b69b35545..069999ecf 100644 --- a/src/context/shared_terms.c +++ b/src/context/shared_terms.c @@ -135,6 +135,12 @@ static void sharing_map_visit_poly(sharing_map_t *map, polynomial_t *c, int32_t } } +static void sharing_map_visit_root_atom(sharing_map_t *map, root_atom_t *c, int32_t p) { + assert(c == root_atom_for_idx(map->terms, p)); + sharing_map_process_occurrence(map, index_of(c->x), p); + sharing_map_process_occurrence(map, index_of(c->p), p); +} + static void sharing_map_visit_bvpoly64(sharing_map_t *map, bvpoly64_t *c, int32_t p) { uint32_t i, n; @@ -176,6 +182,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { switch (kind_for_idx(map->terms, i)) { case CONSTANT_TERM: case ARITH_CONSTANT: + case ARITH_FF_CONSTANT: case BV64_CONSTANT: case BV_CONSTANT: case VARIABLE: @@ -189,10 +196,11 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { case ARITH_FLOOR: case ARITH_CEIL: case ARITH_ABS: + case ARITH_FF_EQ_ATOM: sharing_map_process_occurrence(map, index_of(integer_value_for_idx(map->terms, i)), i); break; case ARITH_ROOT_ATOM: - assert(false); + sharing_map_visit_root_atom(map, root_atom_for_idx(map->terms, i), i); break; case ITE_TERM: @@ -211,6 +219,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { case ARITH_IDIV: case ARITH_MOD: case ARITH_DIVIDES_ATOM: + case ARITH_FF_BINEQ_ATOM: case BV_ARRAY: case BV_DIV: case BV_REM: @@ -236,6 +245,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { break; case ARITH_POLY: + case ARITH_FF_POLY: sharing_map_visit_poly(map, polynomial_for_idx(map->terms, i), i); break; @@ -247,14 +257,6 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { sharing_map_visit_bvpoly(map, bvpoly_for_idx(map->terms, i), i); break; - case ARITH_FF_CONSTANT: - case ARITH_FF_POLY: - case ARITH_FF_EQ_ATOM: - case ARITH_FF_BINEQ_ATOM: - // FF arithmetic is not supported in the non-mcsat solver yet - assert(false); - break; - case UNUSED_TERM: case RESERVED_TERM: assert(false); @@ -350,4 +352,3 @@ term_t unique_parent(sharing_map_t *map, term_t t) { return parent; } - diff --git a/src/frontend/common/parameters.c b/src/frontend/common/parameters.c index 318d0398e..b72774aa4 100644 --- a/src/frontend/common/parameters.c +++ b/src/frontend/common/parameters.c @@ -91,6 +91,7 @@ static const char * const param_names[NUM_PARAMETERS] = { "mcsat-partial-restart", "mcsat-rand-dec-freq", "mcsat-rand-dec-seed", + "mcsat-supplement-check", "mcsat-var-order", "optimistic-fcheck", "prop-threshold", @@ -167,6 +168,7 @@ static const yices_param_t param_code[NUM_PARAMETERS] = { PARAM_MCSAT_PARTIAL_RESTART, PARAM_MCSAT_RAND_DEC_FREQ, PARAM_MCSAT_RAND_DEC_SEED, + PARAM_MCSAT_SUPPLEMENT_CHECK, PARAM_MCSAT_VAR_ORDER, PARAM_OPTIMISTIC_FCHECK, PARAM_PROP_THRESHOLD, @@ -207,6 +209,21 @@ static const branch_t branching_code[NUM_BRANCHING_MODES] = { BRANCHING_THEORY, }; +/* + * Supplementary MCSAT check modes + */ +#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2 + +static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + "both", + "final-only", +}; + +static const mcsat_supplement_check_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +}; + /* @@ -454,6 +471,28 @@ bool param_val_to_branching(const char *name, const param_val_t *v, branch_t *va return false; } +/* + * Supplementary MCSAT check mode + * - allowed modes are "both" and "final-only" + */ +bool param_val_to_mcsat_supplement_check(const char *name, const param_val_t *v, + mcsat_supplement_check_t *value, char **reason) { + int32_t i; + + if (v->tag == PARAM_VAL_SYMBOL) { + i = binary_search_string(v->val.symbol, mcsat_supplement_check_modes, + NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + if (i >= 0) { + assert(i < NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + *value = mcsat_supplement_check_code[i]; + return true; + } + } + *reason = "must be one of 'both' 'final-only'"; + + return false; +} + /* diff --git a/src/frontend/common/parameters.h b/src/frontend/common/parameters.h index 97a11d19a..7e68c4936 100644 --- a/src/frontend/common/parameters.h +++ b/src/frontend/common/parameters.h @@ -125,6 +125,7 @@ typedef enum yices_param { PARAM_MCSAT_BV_VAR_SIZE, PARAM_MCSAT_VAR_ORDER, PARAM_MCSAT_PARTIAL_RESTART, + PARAM_MCSAT_SUPPLEMENT_CHECK, // error PARAM_UNKNOWN } yices_param_t; @@ -209,6 +210,12 @@ extern bool param_val_to_terms(const char *name, const param_val_t *v, ivector_t */ extern bool param_val_to_branching(const char *name, const param_val_t *v, branch_t *value, char **reason); +/* + * Supplementary MCSAT check mode + * - allowed modes are "both" and "final-only" + */ +extern bool param_val_to_mcsat_supplement_check(const char *name, const param_val_t *v, mcsat_supplement_check_t *value, char **reason); + /* * EF generalization mode * - allowed modes are 'none' 'substitution' 'projection' 'auto' diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index d8472510a..b07ceb8c6 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -634,6 +634,8 @@ static smt_status_t check_with_model(context_t *ctx, const param_t *params, uint model_t mdl; evaluator_t mdl_evaluator; + assert(ctx->mcsat != NULL); + // Init model and evaluation init_model(&mdl, ctx->terms, true); init_evaluator(&mdl_evaluator, &mdl); @@ -2250,6 +2252,23 @@ static void set_verbosity(smt2_globals_t *g, const char *name, aval_t value) { q_clear(&aux); } +/* + * Effective architecture for SMT2 logic: + * - defaults to arch_for_logic(logic) + * - if force_dpllt is enabled, replace MCSAT architecture with CDCL(T). + */ +static inline context_arch_t smt2_arch_for_logic(const smt2_globals_t *g, smt_logic_t logic) { + context_arch_t arch; + + assert(logic != SMT_UNKNOWN); + arch = (context_arch_t) arch_for_logic(logic); + if (g->force_dpllt && arch == CTX_ARCH_MCSAT) { + arch = CTX_ARCH_EGFUNSPLXBV; + } + + return arch; +} + /* * Options: produce-unsat-cores and produce-unsat-assumptions. @@ -2265,7 +2284,7 @@ static void set_unsat_core_option(smt2_globals_t *g, const char *name, aval_t va } else { g->produce_unsat_cores = flag; // Set model_interpolation if context is MCSAT or will use MCSAT architecture - if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) { + if (g->mcsat || (g->logic_code != SMT_UNKNOWN && smt2_arch_for_logic(g, g->logic_code) == CTX_ARCH_MCSAT)) { g->mcsat_options.model_interpolation = true; } report_success(); @@ -2284,7 +2303,7 @@ static void set_unsat_assumption_option(smt2_globals_t *g, const char *name, ava } else { g->produce_unsat_assumptions = flag; // Set model_interpolation if context is MCSAT or will use MCSAT architecture - if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) { + if (g->mcsat || (g->logic_code != SMT_UNKNOWN && smt2_arch_for_logic(g, g->logic_code) == CTX_ARCH_MCSAT)) { g->mcsat_options.model_interpolation = true; } report_success(); @@ -2581,7 +2600,7 @@ static void init_smt2_context(smt2_globals_t *g) { if (g->timeout > 0) { mode = CTX_MODE_INTERACTIVE; } - arch = arch_for_logic(logic); + arch = smt2_arch_for_logic(g, logic); iflag = iflag_for_logic(logic); qflag = qflag_for_logic(logic); @@ -4645,6 +4664,7 @@ static void init_smt2_globals(smt2_globals_t *g) { g->pushes_after_unsat = 0; g->logic_name = NULL; g->mcsat = false; + g->force_dpllt = false; init_ivector(&g->var_order, 0); init_mcsat_options(&g->mcsat_options); g->efmode = false; @@ -5042,7 +5062,8 @@ void smt2_get_unsat_assumptions(void) { /* Check whether MCSAT solver is going to be used. */ static bool mcsat_enabled(smt2_globals_t *g) { - return g->mcsat || arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT; + return !g->force_dpllt && + (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)); } /* @@ -5443,6 +5464,11 @@ static bool yices_get_option(smt2_globals_t *g, yices_param_t p) { print_int32_value(g->parameters.random_seed); break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + print_string_value(g->parameters.mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH ? + "both" : "final-only"); + break; + case PARAM_MCSAT_VAR_ORDER: print_terms_value(g, &g->var_order); break; @@ -6241,6 +6267,12 @@ static void yices_set_option(smt2_globals_t *g, const char *param, const param_v } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + if (param_val_to_mcsat_supplement_check(param, val, &g->parameters.mcsat_supplement_check, &reason)) { + // parameter is consumed during check-sat + } + break; + case PARAM_MCSAT_VAR_ORDER: if (param_val_to_terms(param, val, &terms, &reason)) { context = g->ctx; @@ -6462,7 +6494,7 @@ void smt2_set_logic(const char *name) { arch = ef_arch_for_logic(code); } else if (logic_is_supported(code)) { __smt2_globals.efmode = false; - arch = arch_for_logic(code); + arch = smt2_arch_for_logic(&__smt2_globals, code); } else { print_error("logic %s is not supported", name); return; @@ -6479,7 +6511,7 @@ void smt2_set_logic(const char *name) { } // if mcsat was requested, check whether the logic is supported by the MCSAT solver - if (__smt2_globals.mcsat && !logic_is_supported_by_mcsat(code)) { + if (__smt2_globals.mcsat && !__smt2_globals.force_dpllt && !logic_is_supported_by_mcsat(code)) { print_error("logic %s is not supported by the mcsat solver", name); return; } @@ -6492,7 +6524,7 @@ void smt2_set_logic(const char *name) { // in efmode : can't use the mcsat solver and must not be incremental if (__smt2_globals.efmode) { - if (__smt2_globals.mcsat) { + if (__smt2_globals.mcsat && !__smt2_globals.force_dpllt) { print_error("the mcsat solver does not support quantifiers"); return; } @@ -6507,8 +6539,8 @@ void smt2_set_logic(const char *name) { } // Set model_interpolation if unsat cores are enabled and architecture is MCSAT - if ((__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) && - (arch == CTX_ARCH_MCSAT || __smt2_globals.mcsat)) { + if ((__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) && + (arch == CTX_ARCH_MCSAT || (__smt2_globals.mcsat && !__smt2_globals.force_dpllt))) { __smt2_globals.mcsat_options.model_interpolation = true; } @@ -7272,5 +7304,14 @@ void smt2_add_pattern(int32_t op, term_t t, term_t *p, uint32_t n) { * Enables the mcsat solver. */ void smt2_enable_mcsat(void) { + assert(!__smt2_globals.force_dpllt); __smt2_globals.mcsat = true; } + +/* + * Force CDCL(T) architecture in SMT2 mode. + */ +void smt2_force_dpllt(void) { + assert(!__smt2_globals.mcsat); + __smt2_globals.force_dpllt = true; +} diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h index 9fea4ee96..29fbe07d7 100644 --- a/src/frontend/smt2/smt2_commands.h +++ b/src/frontend/smt2/smt2_commands.h @@ -354,6 +354,7 @@ typedef struct smt2_globals_s { // mcsat bool mcsat; // set to true to use the mcsat solver + bool force_dpllt; // force cdcl(t) architecture mcsat_options_t mcsat_options; // options for the mcsat solver ivector_t var_order; // order in which mcsat needs to assign variables @@ -490,6 +491,12 @@ extern void init_mt2(bool benchmark, uint32_t timeout, uint32_t nthreads, bool p */ extern void smt2_enable_mcsat(void); +/* + * Force CDCL(T) architecture in SMT2 frontend + * - must not be called before init_smt2 + */ +extern void smt2_force_dpllt(void); + /* * Force verbosity level to k * - this has the same effect as (set-option :verbosity k) diff --git a/src/frontend/yices/yices_help.c b/src/frontend/yices/yices_help.c index 51bc606f8..305ac155a 100644 --- a/src/frontend/yices/yices_help.c +++ b/src/frontend/yices/yices_help.c @@ -1622,11 +1622,20 @@ static const help_record_t help_data[] = { "whose values matter for satisfying the assertions.\n", NULL, }, - // END MARKER: index 162 + // mcsat-supplement-check: index 163 + { HPARAM, + "(set-param mcsat-supplement-check [mode])", + "Control supplementary MCSAT checks in CDCL(T) mode", + "Allowed modes are:\n" + " both --> check in propagate and final-check\n" + " final-only --> check only in final-check.\n", + NULL, }, + + // END MARKER: index 164 { HMISC, NULL, NULL, NULL, NULL }, }; -#define END_HELP_DATA 163 +#define END_HELP_DATA 164 @@ -2087,6 +2096,7 @@ static const help_index_t help_index[] = { { "max-extensionality", NULL, 139, help_basic }, { "max-interface-eqs", NULL, 130, help_basic }, { "max-update-conflicts", NULL, 138, help_basic }, + { "mcsat-supplement-check", NULL, 163, help_basic }, { "mk-bv", NULL, 58, help_basic }, { "mk-tuple", NULL, 36, help_basic }, { "mod", NULL, 156, help_basic }, diff --git a/src/frontend/yices/yices_reval.c b/src/frontend/yices/yices_reval.c index 4212ad262..cb94a6378 100644 --- a/src/frontend/yices/yices_reval.c +++ b/src/frontend/yices/yices_reval.c @@ -1396,6 +1396,12 @@ static void show_param(yices_param_t p, uint32_t n) { show_pos32_param(param2string[p], parameters.max_extensionality, n); break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + show_string_param(param2string[p], + parameters.mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH ? + "both" : "final-only", n); + break; + case PARAM_EF_FLATTEN_IFF: show_bool_param(param2string[p], ef_client_globals.ef_parameters.flatten_iff, n); break; @@ -1887,6 +1893,12 @@ static void yices_setparam_cmd(const char *param, const param_val_t *val) { } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + if (param_val_to_mcsat_supplement_check(param, val, ¶meters.mcsat_supplement_check, &reason)) { + print_ok(); + } + break; + case PARAM_EF_FLATTEN_IFF: if (param_val_to_bool(param, val, &tt, &reason)) { ef_client_globals.ef_parameters.flatten_iff = tt; @@ -4114,4 +4126,3 @@ int yices_main(int argc, char *argv[]) { return exit_code; } - diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c index ff964361b..681646bfe 100644 --- a/src/frontend/yices_smt2.c +++ b/src/frontend/yices_smt2.c @@ -108,6 +108,7 @@ static char *dimacsfile; // mcsat options static bool mcsat; +static bool force_dpllt; static double mcsat_rand_dec_freq; static int32_t mcsat_rand_dec_seed; static bool mcsat_na_mgcd; @@ -165,6 +166,7 @@ typedef enum optid { delegate_opt, // use an external sat solver dimacs_opt, // bitblast then export to DIMACS mcsat_opt, // enable mcsat + dpllt_opt, // force CDCL(T) mcsat_rand_dec_freq_opt, // random decision frequency when making a decision in mcsat mcsat_rand_dec_seed_opt, // seed for random decisions mcsat_na_mgcd_opt, // use the mgcd instead psc in projection @@ -217,6 +219,7 @@ static option_desc_t options[NUM_OPTIONS] = { { "delegate", '\0', MANDATORY_STRING, delegate_opt }, { "dimacs", '\0', MANDATORY_STRING, dimacs_opt }, { "mcsat", '\0', FLAG_OPTION, mcsat_opt }, + { "dpllt", '\0', FLAG_OPTION, dpllt_opt }, { "mcsat-rand-dec-freq", '\0', MANDATORY_FLOAT, mcsat_rand_dec_freq_opt }, { "mcsat-rand-dec-seed", '\0', MANDATORY_INT, mcsat_rand_dec_seed_opt }, { "mcsat-na-mgcd", '\0', FLAG_OPTION, mcsat_na_mgcd_opt }, @@ -284,7 +287,9 @@ static void print_help(const char *progname) { " --bvconst-in-decimal Display bit-vector constants as decimal numbers (default = false)\n" " --delegate= Use an external SAT solver (can be cadical, cryptominisat, kissat, or y2sat)\n" " --dimacs= Bitblast and export to a file (in DIMACS format)\n" - " --mcsat Use the MCSat solver\n" + " --mcsat Force MCSAT as top-level architecture\n" + " --dpllt Force CDCL(T) as top-level architecture\n" + " (mutually exclusive with --mcsat)\n" " --mcsat-help Show the MCSat options\n" " --ef-help Show the EF options\n" " --nthreads= Specify the number of threads (default = 0 = main thread only)\n" @@ -400,6 +405,7 @@ static void parse_command_line(int argc, char *argv[]) { dimacsfile = NULL; mcsat = false; + force_dpllt = false; mcsat_rand_dec_freq = -1; mcsat_rand_dec_seed = -1; mcsat_na_mgcd = false; @@ -560,6 +566,10 @@ static void parse_command_line(int argc, char *argv[]) { mcsat = true; break; + case dpllt_opt: + force_dpllt = true; + break; + case mcsat_rand_dec_freq_opt: if (! yices_has_mcsat()) goto no_mcsat; if (! validate_double_option(&parser, &elem, 0.0, false, 1.0, false)) goto bad_usage; @@ -724,6 +734,12 @@ static void parse_command_line(int argc, char *argv[]) { } done: + if (force_dpllt && mcsat) { + fprintf(stderr, "%s: options --dpllt and --mcsat are mutually exclusive\n", parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + } + if (incremental && delegate != NULL) { fprintf(stderr, "%s: delegate %s does not support incremental mode\n", parser.command_name, delegate); code = YICES_EXIT_USAGE; @@ -1153,6 +1169,7 @@ int main(int argc, char *argv[]) { yices_init(); init_mt2(!incremental, timeout, nthreads, interactive); + if (force_dpllt) smt2_force_dpllt(); if (smt2_model_format) smt2_force_smt2_model_format(); if (bvdecimal) smt2_force_bvdecimal_format(); if (dimacsfile != NULL && delegate == NULL) smt2_export_to_dimacs(dimacsfile); @@ -1220,4 +1237,3 @@ int main(int argc, char *argv[]) { return YICES_EXIT_SUCCESS; } - diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index df614679e..6e54a3b6b 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -3086,10 +3086,21 @@ void mcsat_build_model(mcsat_solver_t* mcsat, model_t* model) { mcsat_trace_printf(mcsat->ctx->trace, "\n"); } - // Add to model - model_map_term(model, x_term, x_value); - } - } + // Add to model + { + int_hmap_pair_t *entry = int_hmap_get(&model->map, x_term); + if (entry->val < 0) { + model_map_term(model, x_term, x_value); + } else { + /* + * Supplemental use may overlay values onto a model that already + * contains assignments from other CDCL(T) satellites. + */ + entry->val = x_value; + } + } + } + } // Let the plugins run add to the model (e.g. UF, division, ...) for (i = 0; i < mcsat->plugins_count; ++ i) { diff --git a/src/solvers/egraph/egraph.c b/src/solvers/egraph/egraph.c index e8b6a1b6c..c7be4ca5d 100644 --- a/src/solvers/egraph/egraph.c +++ b/src/solvers/egraph/egraph.c @@ -6107,6 +6107,18 @@ static fcheck_code_t baseline_final_check(egraph_t *egraph) { } } + if (egraph->ctrl[ETYPE_MCSAT] != NULL) { + // supplementary mcsat solver + c = egraph->ctrl[ETYPE_MCSAT]->final_check(egraph->th[ETYPE_MCSAT]); + if (c != FCHECK_SAT) { +#if TRACE_FCHECK + printf("---> exit at supplementary mcsat final check\n"); + fflush(stdout); +#endif + return c; + } + } + // i = number of interface equalities generated // max_eq = bound on number of interface equalities @@ -6218,6 +6230,17 @@ static fcheck_code_t experimental_final_check(egraph_t *egraph) { } } + if (egraph->ctrl[ETYPE_MCSAT] != NULL) { + c = egraph->ctrl[ETYPE_MCSAT]->final_check(egraph->th[ETYPE_MCSAT]); + if (c != FCHECK_SAT) { +#if TRACE_FCHECK + printf("---> exit at supplementary mcsat final check\n"); + fflush(stdout); +#endif + return c; + } + } + /* * Try egraph reconciliation @@ -6449,6 +6472,11 @@ bool egraph_assert_atom(egraph_t *egraph, void *atom, literal_t l) { case BV_ATM_TAG: resu = egraph->bv_smt->assert_atom(egraph->th[ETYPE_BV], untag_atom(atom), l); break; + + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + resu = egraph->mcsat_smt->assert_atom(egraph->th[ETYPE_MCSAT], untag_atom(atom), l); + break; } return resu; @@ -6711,6 +6739,11 @@ void egraph_expand_explanation(egraph_t *egraph, literal_t l, void *expl, ivecto case BV_ATM_TAG: egraph->bv_smt->expand_explanation(egraph->th[ETYPE_BV], l, expl, v); break; + + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + egraph->mcsat_smt->expand_explanation(egraph->th[ETYPE_MCSAT], l, expl, v); + break; } } @@ -6770,6 +6803,10 @@ static literal_t egraph_select_polarity(egraph_t *egraph, void *atom, literal_t case BV_ATM_TAG: return egraph->bv_smt->select_polarity(egraph->th[ETYPE_BV], untag_atom(atom), l); + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + return egraph->mcsat_smt->select_polarity(egraph->th[ETYPE_MCSAT], untag_atom(atom), l); + case EGRAPH_ATM_TAG: default: // FOR EQUALITY ATOMS: defer to the satellite solver if any @@ -6907,6 +6944,7 @@ void init_egraph(egraph_t *egraph, type_table_t *ttbl) { } egraph->arith_smt = NULL; egraph->bv_smt = NULL; + egraph->mcsat_smt = NULL; egraph->arith_eg = NULL; egraph->bv_eg = NULL; egraph->fun_eg = NULL; @@ -6958,6 +6996,36 @@ void egraph_attach_bvsolver(egraph_t *egraph, void *solver, th_ctrl_interface_t } +/* + * Attach supplementary mcsat solver + */ +void egraph_attach_mcsat_solver(egraph_t *egraph, void *solver, th_ctrl_interface_t *ctrl, + th_smt_interface_t *smt, th_egraph_interface_t *eg) { + etype_t id; + + assert(egraph->ctrl[ETYPE_MCSAT] == NULL && egraph->mcsat_smt == NULL); + + id = ETYPE_MCSAT; + egraph->th[id] = solver; + egraph->ctrl[id] = ctrl; + egraph->eg[id] = eg; + egraph->mcsat_smt = smt; +} + +/* + * Detach supplementary mcsat solver + */ +void egraph_detach_mcsat_solver(egraph_t *egraph) { + etype_t id; + + id = ETYPE_MCSAT; + egraph->th[id] = NULL; + egraph->ctrl[id] = NULL; + egraph->eg[id] = NULL; + egraph->mcsat_smt = NULL; +} + + /* * Attach a function subsolver * - solver = pointer to the subsolver object diff --git a/src/solvers/egraph/egraph.h b/src/solvers/egraph/egraph.h index 44566d963..ff14b9946 100644 --- a/src/solvers/egraph/egraph.h +++ b/src/solvers/egraph/egraph.h @@ -71,6 +71,22 @@ extern void egraph_attach_bvsolver(egraph_t *egraph, th_egraph_interface_t *eg, bv_egraph_interface_t *bv_eg); +/* + * Attach a supplementary MCSAT satellite + * - solver = pointer to the satellite object + * - ctrl, smt, eg = interface descriptors + */ +extern void egraph_attach_mcsat_solver(egraph_t *egraph, + void *solver, + th_ctrl_interface_t *ctrl, + th_smt_interface_t *smt, + th_egraph_interface_t *eg); + +/* + * Detach the supplementary MCSAT satellite + */ +extern void egraph_detach_mcsat_solver(egraph_t *egraph); + /* * Attach a function/array subsolver * - solver = pointer to the subsolver object diff --git a/src/solvers/egraph/egraph_base_types.h b/src/solvers/egraph/egraph_base_types.h index 4fb4b58c9..fec5b5470 100644 --- a/src/solvers/egraph/egraph_base_types.h +++ b/src/solvers/egraph/egraph_base_types.h @@ -422,16 +422,17 @@ typedef enum etype_s { ETYPE_BV, // 2 ETYPE_QUANT, // 3 ETYPE_FUNCTION, // 4 + ETYPE_MCSAT, // 5 // etypes internal to the egraph - ETYPE_BOOL, // 5 - ETYPE_TUPLE, // 6 - ETYPE_NONE, // 7 + ETYPE_BOOL, // 6 + ETYPE_TUPLE, // 7 + ETYPE_NONE, // 8 } etype_t; #define NUM_ETYPES (ETYPE_NONE + 1) -#define NUM_SATELLITES (ETYPE_FUNCTION + 1) +#define NUM_SATELLITES (ETYPE_MCSAT + 1) /* * tau is an arithmetic type if tau == 0 or 1 @@ -466,6 +467,7 @@ typedef enum atm_tag { EGRAPH_ATM_TAG = 0, ARITH_ATM_TAG = 1, BV_ATM_TAG = 2, + MCSAT_ATM_TAG = 3, } atm_tag_t; #define ATM_TAG_MASK ((size_t) 0x3) @@ -502,6 +504,11 @@ static inline void *tagged_bv_atom(void *atm) { return (void *)(((size_t) atm) | BV_ATM_TAG); } +static inline void *tagged_mcsat_atom(void *atm) { + assert((((size_t) atm) & ATM_TAG_MASK) == 0); + return (void *)(((size_t) atm) | MCSAT_ATM_TAG); +} + diff --git a/src/solvers/egraph/egraph_printer.c b/src/solvers/egraph/egraph_printer.c index a9ad7b531..e74fae8f1 100644 --- a/src/solvers/egraph/egraph_printer.c +++ b/src/solvers/egraph/egraph_printer.c @@ -48,11 +48,11 @@ static char **name = NULL; static const char * const etype2string[] = { - "int ", "real", "bv ", "quant ", "fun ", "bool", "tupl", "none", "", + "int ", "real", "bv ", "quant ", "fun ", "mcsat", "bool", "tupl", "none", "", }; static const char * const etype2theory[] = { - "arith", "arith", "bv", "quant", "fun", "bool", "tuple", "none", "", + "arith", "arith", "bv", "quant", "fun", "mcsat", "bool", "tuple", "none", "", }; static const char * const cmpkind2string[] = { @@ -904,4 +904,3 @@ void print_egraph_congruence_roots(FILE *f, egraph_t *egraph) { delete_pvector(&v); } - diff --git a/src/solvers/egraph/egraph_types.h b/src/solvers/egraph/egraph_types.h index 31b754c7a..4015b65a0 100644 --- a/src/solvers/egraph/egraph_types.h +++ b/src/solvers/egraph/egraph_types.h @@ -1466,6 +1466,7 @@ struct egraph_s { * Theory specific descriptors * - arith_smt: core interface for arith solver * - bv_smt: core interface for bitvector solver + * - mcsat_smt: core interface for supplementary mcsat solver * - arith_eg: egraph interface for arith solver * - bv_eg: egraph interface for the bitvector solver * - fun_eg: egraph interface for the array/function solver @@ -1477,6 +1478,7 @@ struct egraph_s { th_smt_interface_t *arith_smt; th_smt_interface_t *bv_smt; + th_smt_interface_t *mcsat_smt; arith_egraph_interface_t *arith_eg; bv_egraph_interface_t *bv_eg; diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c new file mode 100644 index 000000000..fae2a6af0 --- /dev/null +++ b/src/solvers/mcsat_satellite.c @@ -0,0 +1,1132 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2017 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#include +#include "context/context.h" +#include "model/models.h" +#include "solvers/egraph/composites.h" +#include "solvers/egraph/egraph.h" +#include "solvers/mcsat_satellite.h" +#include "terms/term_explorer.h" +#include "terms/term_manager.h" +#include "terms/term_substitution.h" +#include "utils/int_hash_sets.h" +#include "utils/memalloc.h" +#include "utils/pair_hash_map2.h" + + +typedef struct mcsat_atom_object_s { + uint32_t id; +} mcsat_atom_object_t; + +typedef struct mcsat_atom_entry_s { + term_t atom; + literal_t lit; + term_t pos_label; + term_t neg_label; + mcsat_atom_object_t *obj; + bool active; +} mcsat_atom_entry_t; + +typedef struct mcsat_eq_entry_s { + term_t label; + literal_t source_lit; +} mcsat_eq_entry_t; + +struct mcsat_satellite_s { + context_t *ctx; + smt_core_t *core; + egraph_t *egraph; + + context_t mctx; + term_manager_t tm; + + param_t params; + bool check_in_propagate; + + int32_t internal_error; + + bool cache_valid; + uint64_t cache_signature; + + mcsat_atom_entry_t *atoms; + uint32_t num_atoms; + uint32_t atom_size; + uint32_t push_depth; + ivector_t atom_push_mark; + + int_hmap_t arith_var_to_term; + + mcsat_eq_entry_t *eq; + uint32_t num_eq; + uint32_t eq_size; + uint32_t dlevel; + pmap2_t eq_active; + ivector_t eq_level_mark; + + ivector_t assumptions; + ivector_t assumption_lits; + int_hmap_t label_to_lit; + ivector_t conflict; +}; + + +/* + * Atom/generic vector growth. + */ +static void mcsat_satellite_extend_atoms(mcsat_satellite_t *sat) { + uint32_t n; + assert(sat->num_atoms == sat->atom_size); + n = sat->atom_size + 1; + n += n >> 1; + sat->atoms = (mcsat_atom_entry_t *) safe_realloc(sat->atoms, n * sizeof(mcsat_atom_entry_t)); + sat->atom_size = n; +} + +static void mcsat_satellite_extend_eq(mcsat_satellite_t *sat) { + uint32_t n; + assert(sat->num_eq == sat->eq_size); + n = sat->eq_size + 1; + n += n >> 1; + sat->eq = (mcsat_eq_entry_t *) safe_realloc(sat->eq, n * sizeof(mcsat_eq_entry_t)); + sat->eq_size = n; +} + +/* + * Hash helper for assignment signatures. + */ +static inline uint64_t sig_mix(uint64_t h, uint32_t x) { + h ^= x; + h *= UINT64_C(1099511628211); + return h; +} + +static uint64_t mcsat_satellite_signature(const mcsat_satellite_t *sat) { + uint64_t h; + uint32_t i, n; + + h = UINT64_C(1469598103934665603); + n = sat->assumptions.size; + for (i = 0; i < n; i++) { + h = sig_mix(h, (uint32_t) sat->assumptions.data[i]); + } + return sig_mix(h, n); +} + +/* + * Ensure mctx is ready for assertion. + */ +static void mcsat_satellite_prepare_assertion_state(mcsat_satellite_t *sat) { + smt_status_t status; + status = mcsat_status(sat->mctx.mcsat); + if (status != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } +} + +/* + * Assert a formula in the internal MCSAT context. + */ +static int32_t mcsat_satellite_assert_formula(mcsat_satellite_t *sat, term_t f) { + int32_t code; + + mcsat_satellite_prepare_assertion_state(sat); + code = mcsat_assert_formulas(sat->mctx.mcsat, 1, &f); + if (code < 0) { + sat->internal_error = code; + } + return code; +} + +/* + * Track one assumption. + */ +static inline void mcsat_satellite_add_assumption(mcsat_satellite_t *sat, term_t label, literal_t lit) { + int_hmap_pair_t *p; + + ivector_push(&sat->assumptions, label); + ivector_push(&sat->assumption_lits, lit); + if (lit != null_literal) { + p = int_hmap_get(&sat->label_to_lit, label); + p->val = lit; + } +} + +/* + * Build assumption lists from current assignment + active eq/diseq labels. + */ +static void mcsat_satellite_build_assumptions(mcsat_satellite_t *sat, bool complete_with_phase) { + bval_t v; + uint32_t i; + + ivector_reset(&sat->assumptions); + ivector_reset(&sat->assumption_lits); + int_hmap_reset(&sat->label_to_lit); + + for (i = 0; i < sat->num_atoms; i++) { + if (!sat->atoms[i].active) { + continue; + } + + v = literal_value(sat->core, sat->atoms[i].lit); + if (v == VAL_TRUE || (complete_with_phase && v == VAL_UNDEF_TRUE)) { + mcsat_satellite_add_assumption(sat, sat->atoms[i].pos_label, sat->atoms[i].lit); + } else if (v == VAL_FALSE || (complete_with_phase && v == VAL_UNDEF_FALSE)) { + mcsat_satellite_add_assumption(sat, sat->atoms[i].neg_label, not(sat->atoms[i].lit)); + } + } + + for (i = 0; i < sat->num_eq; i++) { + mcsat_satellite_add_assumption(sat, sat->eq[i].label, sat->eq[i].source_lit); + } + +} + +/* + * Explore a term and collect all Boolean atoms in atoms. + */ +static void collect_boolean_atoms(mcsat_satellite_t *sat, term_t t, int_hset_t *atoms, int_hset_t *visited) { + term_table_t *terms; + uint32_t i, nchildren; + + if (t < 0) { + t = not(t); + } + if (int_hset_member(visited, t)) { + return; + } + int_hset_add(visited, t); + + terms = sat->mctx.terms; + if (term_type(terms, t) == bool_type(terms->types)) { + int_hset_add(atoms, t); + } + + if (term_is_projection(terms, t)) { + collect_boolean_atoms(sat, proj_term_arg(terms, t), atoms, visited); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i=0; iconflict); + init_int_hset(&labels, 0); + init_int_hset(&visited, 0); + init_int_hset(&seen_lits, 0); + + interpolant = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + if (interpolant != NULL_TERM) { + collect_boolean_atoms(sat, interpolant, &labels, &visited); + p = int_hmap_first_record(&sat->label_to_lit); + while (p != NULL) { + if (int_hset_member(&labels, p->key) && p->val != null_literal && + !int_hset_member(&seen_lits, p->val)) { + int_hset_add(&seen_lits, p->val); + ivector_push(&sat->conflict, not(p->val)); + } + p = int_hmap_next_record(&sat->label_to_lit, p); + } + } + + if (sat->conflict.size == 0) { + for (i = 0; i < sat->assumption_lits.size; i++) { + l = sat->assumption_lits.data[i]; + if (l != null_literal && !int_hset_member(&seen_lits, l)) { + int_hset_add(&seen_lits, l); + ivector_push(&sat->conflict, not(l)); + } + } + } + + ivector_push(&sat->conflict, null_literal); + record_theory_conflict(sat->core, sat->conflict.data); + + delete_int_hset(&seen_lits); + delete_int_hset(&visited); + delete_int_hset(&labels); +} + +/* + * Run one consistency check in the internal MCSAT context. + */ +static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bool emit_conflict) { + model_t mdl; + smt_status_t status; + uint64_t sig; + uint32_t i; + value_t vtrue; + + if (sat->internal_error < 0) { + if (emit_conflict) { + literal_t c[1]; + c[0] = null_literal; + record_theory_conflict(sat->core, c); + } + return YICES_STATUS_UNSAT; + } + + mcsat_satellite_build_assumptions(sat, false); + sig = mcsat_satellite_signature(sat); + if (!force && sat->cache_valid && sat->cache_signature == sig) { + return YICES_STATUS_SAT; + } + + init_model(&mdl, sat->mctx.terms, true); + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + for (i=0; iassumptions.size; i++) { + if (model_find_term_value(&mdl, sat->assumptions.data[i]) == null_value) { + model_map_term(&mdl, sat->assumptions.data[i], vtrue); + } + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + delete_model(&mdl); + + sat->cache_valid = false; + if (status == YICES_STATUS_SAT) { + sat->cache_valid = true; + sat->cache_signature = sig; + } else if (status == YICES_STATUS_UNSAT && emit_conflict) { + mcsat_satellite_record_conflict(sat); + } + + return status; +} + +/* + * Open one decision level in the eq/diseq activation map. + */ +static void mcsat_satellite_open_level(mcsat_satellite_t *sat) { + pmap2_push(&sat->eq_active); + sat->dlevel ++; + if (sat->eq_level_mark.size <= sat->dlevel) { + ivector_push(&sat->eq_level_mark, sat->num_eq); + } else { + sat->eq_level_mark.data[sat->dlevel] = sat->num_eq; + } + sat->cache_valid = false; +} + +/* + * Backtrack eq/diseq activation to target. + */ +static void mcsat_satellite_backtrack_to(mcsat_satellite_t *sat, uint32_t target) { + while (sat->dlevel > target) { + sat->num_eq = sat->eq_level_mark.data[sat->dlevel]; + pmap2_pop(&sat->eq_active); + sat->dlevel --; + } + sat->cache_valid = false; +} + +/* + * Align the internal MCSAT scope stack with the outer context base level. + * This is needed when the satellite is attached after one or more pushes. + */ +static void mcsat_satellite_sync_base_level(mcsat_satellite_t *sat, uint32_t base_level) { + uint32_t i; + + for (i = 0; i < base_level; i++) { + context_push(&sat->mctx); + ivector_push(&sat->atom_push_mark, sat->num_atoms); + sat->push_depth ++; + mcsat_satellite_open_level(sat); + } +} + +/* + * Derive a source literal from a disequality hint if possible. + */ +static literal_t source_lit_from_hint(mcsat_satellite_t *sat, composite_t *hint) { + literal_t l; + + if (hint == NULL || sat->egraph == NULL) { + return null_literal; + } + + l = egraph_occ2literal(sat->egraph, pos_occ(hint->id)); + if (l == null_literal || l == false_literal) { + return null_literal; + } + + if (composite_kind(hint) == COMPOSITE_EQ) { + return not(l); + } + + return l; +} + +/* + * Add one eq/diseq notification as a labeled internal assumption. + */ +static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t1, term_t t2, bool eq, literal_t src) { + int32_t k0, k1; + pmap2_rec_t *r; + term_t atom; + term_t label; + term_t implication; + + if (t1 > t2) { + term_t aux = t1; + t1 = t2; + t2 = aux; + } + + k0 = eq ? (int32_t) t1 : -((int32_t) t1) - 1; + k1 = (int32_t) t2; + + r = pmap2_get(&sat->eq_active, k0, k1); + if (r->val >= 0) { + return; + } + + if (sat->num_eq == sat->eq_size) { + mcsat_satellite_extend_eq(sat); + } + + label = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + atom = eq ? mk_eq(&sat->tm, t1, t2) : mk_neq(&sat->tm, t1, t2); + implication = mk_implies(&sat->tm, label, atom); + if (mcsat_satellite_assert_formula(sat, implication) < 0) { + return; + } + + sat->eq[sat->num_eq].label = label; + sat->eq[sat->num_eq].source_lit = src; + sat->num_eq ++; + + r->val = 1; + sat->cache_valid = false; +} + +/* + * Control-interface callbacks. + */ +static void mcsat_satellite_start_internalization(void *solver) { + mcsat_satellite_t *sat = solver; + sat->cache_valid = false; +} + +static void mcsat_satellite_start_search(void *solver) { + mcsat_satellite_t *sat = solver; + sat->cache_valid = false; + if (mcsat_status(sat->mctx.mcsat) != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } +} + +static bool mcsat_satellite_propagate(void *solver) { + mcsat_satellite_t *sat = solver; + smt_status_t status; + + if (!sat->check_in_propagate) { + return true; + } + + status = mcsat_satellite_check(sat, false, true); + return status != YICES_STATUS_UNSAT; +} + +static fcheck_code_t mcsat_satellite_final_check(void *solver) { + mcsat_satellite_t *sat = solver; + smt_status_t status; + + status = mcsat_satellite_check(sat, false, true); + switch (status) { + case YICES_STATUS_UNSAT: + return FCHECK_CONTINUE; + case YICES_STATUS_UNKNOWN: + return FCHECK_UNKNOWN; + default: + return FCHECK_SAT; + } +} + +static void mcsat_satellite_increase_decision_level(void *solver) { + mcsat_satellite_open_level(solver); +} + +static void mcsat_satellite_backtrack(void *solver, uint32_t back_level) { + mcsat_satellite_backtrack_to(solver, back_level); +} + +static void mcsat_satellite_push(void *solver) { + mcsat_satellite_t *sat = solver; + context_push(&sat->mctx); + ivector_push(&sat->atom_push_mark, sat->num_atoms); + sat->push_depth ++; + mcsat_satellite_open_level(sat); +} + +static void mcsat_satellite_pop(void *solver) { + mcsat_satellite_t *sat = solver; + uint32_t i; + int32_t mark; + + assert(sat->push_depth > 0); + assert(sat->atom_push_mark.size > 0); + + context_pop(&sat->mctx); + assert(sat->dlevel > 0); + + mark = ivector_pop2(&sat->atom_push_mark); + for (i=mark; inum_atoms; i++) { + sat->atoms[i].active = false; + } + sat->push_depth --; + mcsat_satellite_backtrack_to(sat, sat->dlevel - 1); +} + +static void mcsat_satellite_reset(void *solver) { + mcsat_satellite_t *sat = solver; + uint32_t i; + + reset_context(&sat->mctx); + + for (i=0; inum_atoms; i++) { + if (sat->atoms[i].obj != NULL) { + safe_free(sat->atoms[i].obj); + sat->atoms[i].obj = NULL; + } + } + + sat->num_atoms = 0; + sat->num_eq = 0; + sat->push_depth = 0; + sat->dlevel = 0; + sat->cache_valid = false; + sat->internal_error = 0; + + ivector_reset(&sat->atom_push_mark); + reset_pmap2(&sat->eq_active); + ivector_reset(&sat->eq_level_mark); + ivector_push(&sat->eq_level_mark, 0); + + int_hmap_reset(&sat->arith_var_to_term); + int_hmap_reset(&sat->label_to_lit); + ivector_reset(&sat->assumptions); + ivector_reset(&sat->assumption_lits); + ivector_reset(&sat->conflict); +} + +static void mcsat_satellite_clear(void *solver) { + mcsat_satellite_t *sat = solver; + context_clear(&sat->mctx); + sat->cache_valid = false; +} + +/* + * SMT interface callbacks. + */ +static bool mcsat_satellite_assert_atom(void *solver, void *atom, literal_t l) { + (void) solver; + (void) atom; + (void) l; + return true; +} + +static void mcsat_satellite_expand_explanation(void *solver, literal_t l, void *expl, ivector_t *v) { + (void) solver; + (void) l; + (void) expl; + (void) v; +} + +static literal_t mcsat_satellite_select_polarity(void *solver, void *atom, literal_t l) { + (void) solver; + (void) atom; + return l; +} + +/* + * Egraph interface callbacks. + */ +static void mcsat_satellite_assert_equality(void *solver, thvar_t x1, thvar_t x2, int32_t id) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + (void) id; + + p1 = int_hmap_find(&sat->arith_var_to_term, x1); + p2 = int_hmap_find(&sat->arith_var_to_term, x2); + if (p1 != NULL && p2 != NULL) { + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, true, null_literal); + } +} + +static void mcsat_satellite_assert_disequality(void *solver, thvar_t x1, thvar_t x2, composite_t *hint) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + literal_t src; + + p1 = int_hmap_find(&sat->arith_var_to_term, x1); + p2 = int_hmap_find(&sat->arith_var_to_term, x2); + if (p1 != NULL && p2 != NULL) { + src = source_lit_from_hint(sat, hint); + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + } +} + +static bool mcsat_satellite_assert_distinct(void *solver, uint32_t n, thvar_t *a, composite_t *hint) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + literal_t src; + uint32_t i, j; + + src = source_lit_from_hint(sat, hint); + for (i=0; iarith_var_to_term, a[i]); + if (p1 == NULL) continue; + for (j=i+1; jarith_var_to_term, a[j]); + if (p2 != NULL) { + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + } + } + } + return true; +} + +static bool mcsat_satellite_check_diseq(void *solver, thvar_t x1, thvar_t x2) { + (void) solver; + (void) x1; + (void) x2; + return false; +} + +static bool mcsat_satellite_is_constant(void *solver, thvar_t x) { + (void) solver; + (void) x; + return false; +} + +static void mcsat_satellite_expand_th_expl(void *solver, thvar_t x1, thvar_t x2, void *expl, th_explanation_t *result) { + (void) solver; + (void) x1; + (void) x2; + (void) expl; + (void) result; +} + +static uint32_t mcsat_satellite_reconcile_model(void *solver, uint32_t max_eq) { + (void) solver; + (void) max_eq; + return 0; +} + +static void mcsat_satellite_prepare_model(void *solver) { + (void) solver; +} + +static bool mcsat_satellite_equal_in_model(void *solver, thvar_t x1, thvar_t x2) { + (void) solver; + (void) x1; + (void) x2; + return false; +} + +static void mcsat_satellite_gen_interface_lemma(void *solver, literal_t l, thvar_t x1, thvar_t x2, bool equiv) { + (void) solver; + (void) l; + (void) x1; + (void) x2; + (void) equiv; +} + +static void mcsat_satellite_release_model(void *solver) { + (void) solver; +} + +static ipart_t *mcsat_satellite_build_partition(void *solver) { + (void) solver; + return NULL; +} + +static void mcsat_satellite_release_partition(void *solver, ipart_t *partition) { + (void) solver; + (void) partition; +} + +static void mcsat_satellite_attach_eterm(void *solver, thvar_t x, eterm_t t) { + (void) solver; + (void) x; + (void) t; +} + +static eterm_t mcsat_satellite_eterm_of_var(void *solver, thvar_t x) { + (void) solver; + (void) x; + return null_eterm; +} + +static literal_t mcsat_satellite_select_eq_polarity(void *solver, thvar_t x, thvar_t y, literal_t l) { + (void) solver; + (void) x; + (void) y; + return l; +} + +/* + * Static interface records. + */ +static th_ctrl_interface_t mcsat_satellite_ctrl = { + (start_intern_fun_t) mcsat_satellite_start_internalization, + (start_fun_t) mcsat_satellite_start_search, + (propagate_fun_t) mcsat_satellite_propagate, + (final_check_fun_t) mcsat_satellite_final_check, + (increase_level_fun_t) mcsat_satellite_increase_decision_level, + (backtrack_fun_t) mcsat_satellite_backtrack, + (push_fun_t) mcsat_satellite_push, + (pop_fun_t) mcsat_satellite_pop, + (reset_fun_t) mcsat_satellite_reset, + (clear_fun_t) mcsat_satellite_clear, +}; + +static th_smt_interface_t mcsat_satellite_smt = { + (assert_fun_t) mcsat_satellite_assert_atom, + (expand_expl_fun_t) mcsat_satellite_expand_explanation, + (select_pol_fun_t) mcsat_satellite_select_polarity, + NULL, + NULL, +}; + +static th_egraph_interface_t mcsat_satellite_eg = { + (assert_eq_fun_t) mcsat_satellite_assert_equality, + (assert_diseq_fun_t) mcsat_satellite_assert_disequality, + (assert_distinct_fun_t) mcsat_satellite_assert_distinct, + (check_diseq_fun_t) mcsat_satellite_check_diseq, + (is_constant_fun_t) mcsat_satellite_is_constant, + (expand_eq_exp_fun_t) mcsat_satellite_expand_th_expl, + (reconcile_model_fun_t) mcsat_satellite_reconcile_model, + (prepare_model_fun_t) mcsat_satellite_prepare_model, + (equal_in_model_fun_t) mcsat_satellite_equal_in_model, + (gen_inter_lemma_fun_t) mcsat_satellite_gen_interface_lemma, + (release_model_fun_t) mcsat_satellite_release_model, + (build_partition_fun_t) mcsat_satellite_build_partition, + (free_partition_fun_t) mcsat_satellite_release_partition, + (attach_to_var_fun_t) mcsat_satellite_attach_eterm, + (get_eterm_fun_t) mcsat_satellite_eterm_of_var, + (select_eq_polarity_fun_t) mcsat_satellite_select_eq_polarity, +}; + + +/* + * Constructor/destructor. + */ +mcsat_satellite_t *new_mcsat_satellite(context_t *ctx) { + mcsat_satellite_t *sat; + + sat = (mcsat_satellite_t *) safe_malloc(sizeof(mcsat_satellite_t)); + + sat->ctx = ctx; + sat->core = ctx->core; + sat->egraph = ctx->egraph; + + init_context(&sat->mctx, ctx->terms, ctx->logic, CTX_MODE_PUSHPOP, CTX_ARCH_MCSAT, false); + sat->mctx.mcsat_options = ctx->mcsat_options; + sat->mctx.mcsat_options.model_interpolation = true; + ivector_copy(&sat->mctx.mcsat_var_order, ctx->mcsat_var_order.data, ctx->mcsat_var_order.size); + ivector_copy(&sat->mctx.mcsat_initial_var_order, ctx->mcsat_initial_var_order.data, ctx->mcsat_initial_var_order.size); + + init_term_manager(&sat->tm, sat->mctx.terms); + + init_params_to_defaults(&sat->params); + sat->check_in_propagate = true; + + sat->internal_error = 0; + + sat->cache_valid = false; + sat->cache_signature = 0; + + sat->atoms = NULL; + sat->num_atoms = 0; + sat->atom_size = 0; + sat->push_depth = 0; + init_ivector(&sat->atom_push_mark, 0); + + init_int_hmap(&sat->arith_var_to_term, 0); + + sat->eq = NULL; + sat->num_eq = 0; + sat->eq_size = 0; + sat->dlevel = 0; + init_pmap2(&sat->eq_active); + init_ivector(&sat->eq_level_mark, 8); + ivector_push(&sat->eq_level_mark, 0); + + init_ivector(&sat->assumptions, 0); + init_ivector(&sat->assumption_lits, 0); + init_int_hmap(&sat->label_to_lit, 0); + init_ivector(&sat->conflict, 0); + + if (ctx->trace != NULL) { + mcsat_satellite_set_trace(sat, ctx->trace); + } + + mcsat_satellite_sync_base_level(sat, ctx->base_level); + + return sat; +} + +void delete_mcsat_satellite(mcsat_satellite_t *sat) { + uint32_t i; + + if (sat == NULL) { + return; + } + + for (i = 0; i < sat->num_atoms; i++) { + if (sat->atoms[i].obj != NULL) { + safe_free(sat->atoms[i].obj); + sat->atoms[i].obj = NULL; + } + } + safe_free(sat->atoms); + sat->atoms = NULL; + + safe_free(sat->eq); + sat->eq = NULL; + + delete_ivector(&sat->conflict); + delete_int_hmap(&sat->label_to_lit); + delete_ivector(&sat->assumption_lits); + delete_ivector(&sat->assumptions); + + delete_ivector(&sat->eq_level_mark); + delete_pmap2(&sat->eq_active); + + delete_int_hmap(&sat->arith_var_to_term); + delete_ivector(&sat->atom_push_mark); + + delete_term_manager(&sat->tm); + delete_context(&sat->mctx); + safe_free(sat); +} + + +/* + * Public interface getters. + */ +th_ctrl_interface_t *mcsat_satellite_ctrl_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_ctrl; +} + +th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_smt; +} + +th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_eg; +} + +int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a) { + uint32_t i; + int32_t code; + + for (i = 0; i < n; i++) { + code = mcsat_satellite_assert_formula(sat, a[i]); + if (code < 0) { + return code; + } + } + + return CTX_NO_ERROR; +} + +/* + * Register one tracked unsupported atom. + */ +int32_t mcsat_satellite_register_atom(mcsat_satellite_t *sat, term_t atom, literal_t l, void **obj) { + mcsat_atom_entry_t *entry; + term_t plabel, nlabel; + term_t implication; + int32_t code; + mcsat_atom_object_t *atom_obj; + uint32_t i; + + assert(l >= 0); + + // Already tracked: keep the existing object/literal association. + for (i = 0; i < sat->num_atoms; i++) { + entry = sat->atoms + i; + if (entry->atom == atom && entry->lit == l) { + if (obj != NULL) { + *obj = entry->obj; + } + return CTX_NO_ERROR; + } + } + + if (sat->num_atoms == sat->atom_size) { + mcsat_satellite_extend_atoms(sat); + } + + plabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + nlabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + + implication = mk_implies(&sat->tm, plabel, atom); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + return code; + } + + implication = mk_implies(&sat->tm, nlabel, not(atom)); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + return code; + } + + atom_obj = NULL; + if (obj != NULL) { + atom_obj = safe_malloc(sizeof(mcsat_atom_object_t)); + atom_obj->id = sat->num_atoms; + *obj = atom_obj; + } + + entry = sat->atoms + sat->num_atoms; + entry->atom = atom; + entry->lit = l; + entry->pos_label = plabel; + entry->neg_label = nlabel; + entry->obj = atom_obj; + entry->active = true; + sat->num_atoms ++; + + sat->cache_valid = false; + return CTX_NO_ERROR; +} + +/* + * Register thvar -> term for arithmetic terms. + */ +void mcsat_satellite_register_arith_term(mcsat_satellite_t *sat, thvar_t x, term_t t) { + int_hmap_pair_t *p; + p = int_hmap_get(&sat->arith_var_to_term, x); + p->val = t; +} + +/* + * Parameters/tracing/model/GC support. + */ +void mcsat_satellite_set_search_parameters(mcsat_satellite_t *sat, const param_t *params) { + sat->params = *params; + sat->check_in_propagate = (params->mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH); + sat->cache_valid = false; +} + +void mcsat_satellite_set_trace(mcsat_satellite_t *sat, tracer_t *trace) { + mcsat_set_tracer(sat->mctx.mcsat, trace); +} + +term_t mcsat_satellite_get_unsat_model_interpolant(mcsat_satellite_t *sat) { + return mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); +} + +void mcsat_satellite_set_unsat_model_interpolant(mcsat_satellite_t *sat, term_t t) { + mcsat_set_unsat_result(sat->mctx.mcsat, t); +} + +term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, const param_t *params, uint32_t n, const term_t *a) { + ivector_t labels; + ivector_t assumptions; + term_manager_t tm; + model_t mdl; + value_t vtrue; + term_t result; + smt_status_t status; + uint32_t i; + bool pushed; + + if (sat->internal_error < 0) { + return NULL_TERM; + } + + init_ivector(&labels, n); + init_ivector(&assumptions, n); + init_term_manager(&tm, sat->mctx.terms); + init_model(&mdl, sat->mctx.terms, true); + + pushed = false; + result = NULL_TERM; + + if (context_supports_pushpop(&sat->mctx)) { + context_push(&sat->mctx); + pushed = true; + } + + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + + for (i = 0; i < n; i++) { + term_t b, implication; + int32_t code; + + b = new_uninterpreted_term(sat->mctx.terms, bool_id); + implication = mk_implies(&tm, b, a[i]); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + goto done; + } + + ivector_push(&labels, b); + ivector_push(&assumptions, b); + model_map_term(&mdl, b, vtrue); + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, params != NULL ? params : &sat->params, &mdl, + assumptions.size, (const term_t *) assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + if (status == YICES_STATUS_UNSAT) { + term_t raw = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + if (raw == NULL_TERM) { + raw = false_term; + } + if (labels.size > 0) { + term_subst_t subst; + init_term_subst(&subst, &tm, labels.size, labels.data, a); + result = apply_term_subst(&subst, raw); + delete_term_subst(&subst); + } else { + result = raw; + } + } + +done: + delete_model(&mdl); + delete_term_manager(&tm); + delete_ivector(&assumptions); + delete_ivector(&labels); + + if (pushed) { + mcsat_cleanup_assumptions(sat->mctx.mcsat); + context_pop(&sat->mctx); + } + + if (result != NULL_TERM) { + mcsat_set_unsat_result(sat->mctx.mcsat, result); + } + + return result; +} + +void mcsat_satellite_build_model(mcsat_satellite_t *sat, model_t *model) { + model_t mdl; + smt_status_t status; + uint32_t i; + value_t vtrue; + + if (sat->internal_error < 0) { + return; + } + + /* + * For model construction, complete unassigned tracked literals with their + * current polarity hint so MCSAT can compute a concrete witness model. + */ + mcsat_satellite_build_assumptions(sat, true); + + init_model(&mdl, sat->mctx.terms, true); + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + for (i = 0; i < sat->assumptions.size; i++) { + if (model_find_term_value(&mdl, sat->assumptions.data[i]) == null_value) { + model_map_term(&mdl, sat->assumptions.data[i], vtrue); + } + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + delete_model(&mdl); + + if (status == YICES_STATUS_SAT) { + mcsat_build_model(sat->mctx.mcsat, model); + } +} + +void mcsat_satellite_gc_mark(mcsat_satellite_t *sat) { + uint32_t i; + + for (i=0; inum_atoms; i++) { + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].atom)); + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].pos_label)); + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].neg_label)); + } + + for (i=0; inum_eq; i++) { + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->eq[i].label)); + } + + mcsat_gc_mark(sat->mctx.mcsat); +} diff --git a/src/solvers/mcsat_satellite.h b/src/solvers/mcsat_satellite.h new file mode 100644 index 000000000..172f1d3cd --- /dev/null +++ b/src/solvers/mcsat_satellite.h @@ -0,0 +1,85 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2017 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#ifndef __MCSAT_SATELLITE_H +#define __MCSAT_SATELLITE_H + +#include +#include + +#include "context/context_types.h" +#include "solvers/egraph/egraph_types.h" + +typedef struct mcsat_satellite_s mcsat_satellite_t; + +extern mcsat_satellite_t *new_mcsat_satellite(context_t *ctx); +extern void delete_mcsat_satellite(mcsat_satellite_t *sat); + +extern th_ctrl_interface_t *mcsat_satellite_ctrl_interface(mcsat_satellite_t *sat); +extern th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat); +extern th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat); + +extern int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a); + +/* + * Register a Boolean atom term tracked by the supplementary MCSAT satellite. + * - atom must be a Boolean term. + * - l must be a positive core literal. + * - *obj is set to a satellite-owned atom object for egraph tagging/dispatch. + * Return code: + * - CTX_NO_ERROR on success + * - a negative internalization code on error. + */ +/* + * Register one tracked atom/literal pair. + * - if obj is non-NULL, create an opaque atom object for egraph tagging. + * - if obj is NULL, register as observation-only (no egraph atom tag). + */ +extern int32_t mcsat_satellite_register_atom(mcsat_satellite_t *sat, term_t atom, literal_t l, void **obj); + +/* + * Record a mapping from an arithmetic theory variable to the source term. + * This is used to materialize eq/diseq notifications into MCSAT assumptions. + */ +extern void mcsat_satellite_register_arith_term(mcsat_satellite_t *sat, thvar_t x, term_t t); + +/* + * Copy search parameters relevant to supplementary checking. + */ +extern void mcsat_satellite_set_search_parameters(mcsat_satellite_t *sat, const param_t *params); + +/* + * Return the most recent UNSAT model interpolant from the satellite solver. + * Returns NULL_TERM if unavailable. + */ +extern term_t mcsat_satellite_get_unsat_model_interpolant(mcsat_satellite_t *sat); +extern void mcsat_satellite_set_unsat_model_interpolant(mcsat_satellite_t *sat, term_t t); +extern term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, const param_t *params, uint32_t n, const term_t *a); + +/* + * Overlay model values from the supplementary MCSAT context. + */ +extern void mcsat_satellite_build_model(mcsat_satellite_t *sat, model_t *model); + +/* + * Trace + GC support. + */ +extern void mcsat_satellite_set_trace(mcsat_satellite_t *sat, tracer_t *trace); +extern void mcsat_satellite_gc_mark(mcsat_satellite_t *sat); + +#endif /* __MCSAT_SATELLITE_H */ diff --git a/src/terms/term_explorer.c b/src/terms/term_explorer.c index b2d93487c..63f3191d1 100644 --- a/src/terms/term_explorer.c +++ b/src/terms/term_explorer.c @@ -449,6 +449,15 @@ term_t term_child(term_table_t *table, term_t t, uint32_t i) { } break; + case ARITH_FF_EQ_ATOM: + assert(i < 2); + if (i == 0) { + result = arith_ff_eq_arg(table, t); + } else { + result = ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t))); + } + break; + case ARITH_IS_INT_ATOM: case ARITH_FLOOR: case ARITH_CEIL: @@ -500,6 +509,12 @@ void get_term_children(term_table_t *table, term_t t, ivector_t *v) { ivector_push(v, zero_term); break; + case ARITH_FF_EQ_ATOM: + // t == 0 over finite fields: expose both sides uniformly + ivector_push(v, arith_ff_eq_arg(table, t)); + ivector_push(v, ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t)))); + break; + case ARITH_IS_INT_ATOM: case ARITH_FLOOR: case ARITH_CEIL: @@ -684,4 +699,3 @@ int32_t generic_const_value(term_table_t *table, term_t t) { assert(is_pos_term(t) && t != true_term); return constant_term_index(table, t); } - diff --git a/tests/regress/both/README.md b/tests/regress/both/README.md new file mode 100644 index 000000000..bd3f87b36 --- /dev/null +++ b/tests/regress/both/README.md @@ -0,0 +1,16 @@ +# Shared Regression Tests (`regress/both`) + +Tests in this directory are expected to pass in both solver modes: + +- `--mcsat` +- `--dpllt` + +The regression harness runs each SMT2 test in this directory twice, once per +mode. Do not put `--mcsat` or `--dpllt` in `.options` files here; the harness +injects these flags automatically. + +Keep MCSAT-only tests (for example, `check-sat-assuming-model` and +`get-unsat-model-interpolant`) in `tests/regress/mcsat`. + +Keep core-shape-sensitive tests where outputs differ across solvers outside this +directory. diff --git a/tests/regress/both/smoke_sat.smt2 b/tests/regress/both/smoke_sat.smt2 new file mode 100644 index 000000000..85d6f47e7 --- /dev/null +++ b/tests/regress/both/smoke_sat.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_LIA) +(declare-const x Int) +(assert (> x 0)) +(check-sat) diff --git a/tests/regress/both/smoke_sat.smt2.gold b/tests/regress/both/smoke_sat.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/both/smoke_sat.smt2.gold @@ -0,0 +1 @@ +sat diff --git a/tests/regress/both/smoke_unsat.smt2 b/tests/regress/both/smoke_unsat.smt2 new file mode 100644 index 000000000..725d76139 --- /dev/null +++ b/tests/regress/both/smoke_unsat.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(declare-const x Int) +(assert (> x 0)) +(assert (< x 0)) +(check-sat) diff --git a/tests/regress/both/smoke_unsat.smt2.gold b/tests/regress/both/smoke_unsat.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/both/smoke_unsat.smt2.gold @@ -0,0 +1 @@ +unsat diff --git a/tests/regress/check.sh b/tests/regress/check.sh index b5d9e471a..67d93edfd 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -117,7 +117,7 @@ fi ./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null if [ $? -ne 0 ] then - MCSAT_FILTER="-v mcsat" + MCSAT_FILTER="-v -E /(mcsat|both)/" else MCSAT_FILTER="." fi diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index 2ddbcefc7..655430188 100755 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -110,6 +110,8 @@ fi # outfile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } timefile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } +outfile2= +timefile2= if [[ -z "$TIME_LIMIT" ]]; then @@ -160,38 +162,120 @@ if [ -d "$out_dir" ] ; then log_file="$out_dir/_$(echo "${test_file//_/__}" | tr '/' '_')" fi -# Run the binary -( - ulimit -S -t $TIME_LIMIT &> /dev/null - ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null - (time "./$bin_dir/$binary" $options "./$test_file" >& "$outfile" ) >& "$timefile" -) -status=$? -runtime=$(cat "$timefile") +run_solver_once() { + local run_options=$1 + local run_outfile=$2 + local run_timefile=$3 -# Do the diff -DIFF=$(diff -w "$outfile" "$gold") + ( + ulimit -S -t $TIME_LIMIT &> /dev/null + ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null + (time "./$bin_dir/$binary" $run_options "./$test_file" >& "$run_outfile") >& "$run_timefile" + ) +} -if [ $? -eq 0 ] && [ $status -eq 0 ] -then - echo -e "$green PASS [${runtime} s] $black $test_string" +strip_solver_mode_flags() { + local input=$1 + local output= + local tok + + for tok in $input; do + case "$tok" in + --mcsat|--dpllt) + ;; + *) + output="$output $tok" + ;; + esac + done + + echo "$output" +} + +if [ "$binary" = yices_smt2 ] && [[ "$test_file" == *"/both/"* ]]; then + options=$(strip_solver_mode_flags "$options") + test_string="$test_file [ $options --mcsat ] [ $options --dpllt ]" + + outfile2=$($mktemp_cmd) || { echo "Can't create temp file" ; rm -f "$timefile" "$outfile" ; exit 3 ; } + timefile2=$($mktemp_cmd) || { echo "Can't create temp file" ; rm -f "$timefile" "$outfile" "$outfile2" ; exit 3 ; } + + run_solver_once "$options --mcsat" "$outfile" "$timefile" + status_mcsat=$? + runtime_mcsat=$(cat "$timefile") + diff_mcsat=$(diff -w "$outfile" "$gold") + diff_status_mcsat=$? + + run_solver_once "$options --dpllt" "$outfile2" "$timefile2" + status_dpllt=$? + runtime_dpllt=$(cat "$timefile2") + diff_dpllt=$(diff -w "$outfile2" "$gold") + diff_status_dpllt=$? + + if [ $status_mcsat -eq 0 ] && [ $diff_status_mcsat -eq 0 ] && [ $status_dpllt -eq 0 ] && [ $diff_status_dpllt -eq 0 ]; then + echo -e "$green PASS [mcsat ${runtime_mcsat} s, dpllt ${runtime_dpllt} s] $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.pass" - echo "$test_string" > "$log_file" - echo "$runtime" >> "$log_file" + log_file="$log_file.pass" + echo "$test_string" > "$log_file" + echo "mcsat: $runtime_mcsat" >> "$log_file" + echo "dpllt: $runtime_dpllt" >> "$log_file" fi code=0 -else + else + DIFF= + if [ $status_mcsat -ne 0 ] || [ $diff_status_mcsat -ne 0 ]; then + DIFF+="--- mcsat (--mcsat) ---"$'\n' + if [ $status_mcsat -ne 0 ]; then + DIFF+="exit status: $status_mcsat"$'\n' + fi + DIFF+="$diff_mcsat"$'\n' + fi + if [ $status_dpllt -ne 0 ] || [ $diff_status_dpllt -ne 0 ]; then + DIFF+="--- dpllt (--dpllt) ---"$'\n' + if [ $status_dpllt -ne 0 ]; then + DIFF+="exit status: $status_dpllt"$'\n' + fi + DIFF+="$diff_dpllt"$'\n' + fi + echo -e "$red FAIL $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.error" - echo "$test_string" > "$log_file" - echo "$runtime" >> "$log_file" - echo "$DIFF" >> "$log_file" + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "mcsat: $runtime_mcsat" >> "$log_file" + echo "dpllt: $runtime_dpllt" >> "$log_file" + echo "$DIFF" >> "$log_file" fi code=1 + fi +else + # Run the binary once + run_solver_once "$options" "$outfile" "$timefile" + status=$? + runtime=$(cat "$timefile") + + # Do the diff + DIFF=$(diff -w "$outfile" "$gold") + + if [ $? -eq 0 ] && [ $status -eq 0 ] + then + echo -e "$green PASS [${runtime} s] $black $test_string" + if [ -n "$log_file" ] ; then + log_file="$log_file.pass" + echo "$test_string" > "$log_file" + echo "$runtime" >> "$log_file" + fi + code=0 + else + echo -e "$red FAIL $black $test_string" + if [ -n "$log_file" ] ; then + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "$runtime" >> "$log_file" + echo "$DIFF" >> "$log_file" + fi + code=1 + fi fi -rm "$timefile" -rm "$outfile" +rm -f "$timefile" "$outfile" "$timefile2" "$outfile2" exit $code From b268ef575dc84511755a1d61b274fc0a90c7e7a8 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 21:24:21 -0700 Subject: [PATCH 2/9] Fix supplemental trigger to preserve div-by-zero errors --- src/context/context.c | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 17339ea70..b626d50f5 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -98,10 +98,7 @@ static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx) { static inline bool divisor_requires_mcsat(term_table_t *terms, term_t t) { t = unsigned_term(t); - if (term_kind(terms, t) != ARITH_CONSTANT) { - return true; - } - return q_is_zero(rational_term_desc(terms, t)); + return term_kind(terms, t) != ARITH_CONSTANT; } /* From ccde68223bf6e8c968e12493e6c7bb1000e174ad Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 22:41:53 -0700 Subject: [PATCH 3/9] Add broad CDCL(T)+supplementary-MCSAT API coverage --- src/solvers/mcsat_satellite.c | 8 + tests/api/test_cdclt_mcsat_supplement.c | 383 ++++++++++++++++++++++++ 2 files changed, 391 insertions(+) create mode 100644 tests/api/test_cdclt_mcsat_supplement.c diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index fae2a6af0..84a478502 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -1019,6 +1019,14 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c pushed = false; result = NULL_TERM; + /* + * Internal push requires an idle MCSAT state in debug builds. + * This path may be called after a previous UNSAT check. + */ + if (mcsat_status(sat->mctx.mcsat) != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } + if (context_supports_pushpop(&sat->mctx)) { context_push(&sat->mctx); pushed = true; diff --git a/tests/api/test_cdclt_mcsat_supplement.c b/tests/api/test_cdclt_mcsat_supplement.c new file mode 100644 index 000000000..22f1f49b4 --- /dev/null +++ b/tests/api/test_cdclt_mcsat_supplement.c @@ -0,0 +1,383 @@ +/* + * API coverage for CDCL(T) with supplementary MCSAT. + * + * This test intentionally forces top-level solver-type=dpllt and exercises: + * - nonlinear arithmetic handled via supplementary MCSAT + * - finite-field constraints handled via supplementary MCSAT + * - assumptions + unsat-core extraction on unsupported atoms + * - push/pop lifecycle on supplemental formulas + * - supplementary check-mode parameter (both/final-only) + * - division-by-zero behavior remains a front-end error path + */ + +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include +#include +#include +#include +#include +#include + +#include + +static void fail(const char *msg) { + fprintf(stderr, "FAIL: %s\n", msg); + yices_print_error(stderr); + exit(2); +} + +static void check(bool cond, const char *msg) { + if (!cond) { + fail(msg); + } +} + +static void check_code(int32_t code, const char *msg) { + if (code < 0) { + fail(msg); + } +} + +static void check_status(smt_status_t actual, smt_status_t expected, const char *msg) { + if (actual != expected) { + fail(msg); + } +} + +static bool has_term(const term_vector_t *v, term_t t) { + uint32_t i; + + for (i = 0; i < v->size; i++) { + if (v->data[i] == t) { + return true; + } + } + return false; +} + +static context_t *make_cdclt_context(const char *logic_name) { + ctx_config_t *cfg; + context_t *ctx; + int32_t code; + + cfg = yices_new_config(); + if (cfg == NULL) { + fail("yices_new_config failed"); + } + + if (logic_name != NULL) { + code = yices_default_config_for_logic(cfg, logic_name); + if (code < 0) { + yices_free_config(cfg); + fail("yices_default_config_for_logic failed"); + } + } + + code = yices_set_config(cfg, "solver-type", "dpllt"); + if (code < 0) { + yices_free_config(cfg); + fail("setting solver-type=dpllt failed"); + } + + code = yices_set_config(cfg, "mode", "push-pop"); + if (code < 0) { + yices_free_config(cfg); + fail("setting mode=push-pop failed"); + } + + ctx = yices_new_context(cfg); + yices_free_config(cfg); + if (ctx == NULL) { + fail("yices_new_context failed"); + } + + return ctx; +} + +static term_t ff_const_si(long val, long mod) { + mpz_t zval, zmod; + term_t t; + + mpz_init_set_si(zval, val); + mpz_init_set_si(zmod, mod); + t = yices_ff_const(zval, zmod); + mpz_clear(zmod); + mpz_clear(zval); + return t; +} + +static void test_nla_sat_unsat_and_model(void) { + context_t *ctx; + term_t x, xx, eq4, eq2, eq3; + smt_status_t stat; + model_t *mdl; + int64_t v; + + ctx = make_cdclt_context("QF_UFLIA"); + + x = yices_new_uninterpreted_term(yices_int_type()); + xx = yices_mul(x, x); + eq4 = yices_arith_eq_atom(xx, yices_int32(4)); + check(eq4 != NULL_TERM, "building nonlinear equation failed"); + + check_code(yices_assert_formula(ctx, eq4), "assert x*x=4 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x*x=4"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "yices_get_model failed on SAT nonlinear context"); + check(yices_formula_true_in_model(mdl, eq4) == 1, "model must satisfy x*x=4"); + check_code(yices_get_int64_value(mdl, xx, &v), "reading value of x*x failed"); + check(v == 4, "expected model value x*x = 4"); + yices_free_model(mdl); + + yices_reset_context(ctx); + eq2 = yices_arith_eq_atom(xx, yices_int32(2)); + eq3 = yices_arith_eq_atom(xx, yices_int32(3)); + check_code(yices_assert_formula(ctx, eq2), "assert x*x=2 failed"); + check_code(yices_assert_formula(ctx, eq3), "assert x*x=3 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for x*x=2 and x*x=3"); + + yices_free_context(ctx); +} + +static void test_nla_hidden_product_and_push_pop(void) { + context_t *ctx; + term_t x, y, xy, ge5, xle1, yle1, xge0, yge0, eq2, eq1, xeq1; + smt_status_t stat; + + ctx = make_cdclt_context("QF_UFLIA"); + x = yices_new_uninterpreted_term(yices_int_type()); + y = yices_new_uninterpreted_term(yices_int_type()); + xy = yices_mul(x, y); + + ge5 = yices_arith_geq_atom(xy, yices_int32(5)); + xle1 = yices_arith_leq_atom(x, yices_int32(1)); + yle1 = yices_arith_leq_atom(y, yices_int32(1)); + xge0 = yices_arith_geq_atom(x, yices_int32(0)); + yge0 = yices_arith_geq_atom(y, yices_int32(0)); + + check_code(yices_assert_formula(ctx, ge5), "assert x*y>=5 failed"); + check_code(yices_assert_formula(ctx, xle1), "assert x<=1 failed"); + check_code(yices_assert_formula(ctx, yle1), "assert y<=1 failed"); + check_code(yices_assert_formula(ctx, xge0), "assert x>=0 failed"); + check_code(yices_assert_formula(ctx, yge0), "assert y>=0 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for hidden-product constraints"); + + yices_reset_context(ctx); + + check_code(yices_push(ctx), "push failed"); + eq2 = yices_arith_eq_atom(yices_mul(x, x), yices_int32(2)); + check_code(yices_assert_formula(ctx, eq2), "assert x*x=2 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for integer x*x=2"); + check_code(yices_pop(ctx), "pop failed"); + + check_code(yices_push(ctx), "second push failed"); + eq1 = yices_arith_eq_atom(yices_mul(x, x), yices_int32(1)); + xeq1 = yices_arith_eq_atom(x, yices_int32(1)); + check_code(yices_assert_formula(ctx, eq1), "assert x*x=1 failed"); + check_code(yices_assert_formula(ctx, xeq1), "assert x=1 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x*x=1 and x=1"); + check_code(yices_pop(ctx), "second pop failed"); + + yices_free_context(ctx); +} + +static void test_nonconstant_divisor_and_param_modes(void) { + context_t *ctx; + param_t *params; + term_t x, y; + term_t yeq2, xeq6, div_eq3, div_eq4; + smt_status_t stat; + model_t *mdl; + + ctx = make_cdclt_context("QF_UFLRA"); + x = yices_new_uninterpreted_term(yices_real_type()); + y = yices_new_uninterpreted_term(yices_real_type()); + + yeq2 = yices_arith_eq_atom(y, yices_rational32(2, 1)); + xeq6 = yices_arith_eq_atom(x, yices_rational32(6, 1)); + div_eq3 = yices_arith_eq_atom(yices_division(x, y), yices_rational32(3, 1)); + div_eq4 = yices_arith_eq_atom(yices_division(x, y), yices_rational32(4, 1)); + + params = yices_new_param_record(); + check(params != NULL, "yices_new_param_record failed"); + yices_default_params_for_context(ctx, params); + + check_code(yices_set_param(params, "mcsat-supplement-check", "final-only"), + "set_param(final-only) failed"); + check_code(yices_assert_formula(ctx, yeq2), "assert y=2 failed"); + check_code(yices_assert_formula(ctx, xeq6), "assert x=6 failed"); + check_code(yices_assert_formula(ctx, div_eq3), "assert x/y=3 failed"); + stat = yices_check_context(ctx, params); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x=6,y=2,x/y=3"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed for nonconstant-divisor SAT"); + check(yices_formula_true_in_model(mdl, div_eq3) == 1, "model must satisfy x/y=3"); + yices_free_model(mdl); + + yices_reset_context(ctx); + + check_code(yices_set_param(params, "mcsat-supplement-check", "both"), + "set_param(both) failed"); + check_code(yices_assert_formula(ctx, yeq2), "reassert y=2 failed"); + check_code(yices_assert_formula(ctx, xeq6), "reassert x=6 failed"); + check_code(yices_assert_formula(ctx, div_eq4), "assert x/y=4 failed"); + stat = yices_check_context(ctx, params); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for x=6,y=2,x/y=4"); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void test_ff_sat_unsat_model_and_assumption_core(void) { + context_t *ctx; + mpz_t p, val, mod, tmp; + type_t tau; + term_t a, c1, c3, sat_eq, ff_eq, ff_neq; + term_t pa, qa, imp1, imp2; + term_t assumptions[2]; + term_vector_t core; + smt_status_t stat; + model_t *mdl; + + mpz_init_set_si(p, 7); + mpz_init(val); + mpz_init(mod); + mpz_init(tmp); + + ctx = make_cdclt_context(NULL); + tau = yices_ff_type(p); + check(tau != NULL_TYPE, "creating FF type failed"); + a = yices_new_uninterpreted_term(tau); + check(a != NULL_TERM, "creating FF variable failed"); + + c1 = ff_const_si(1, 7); + c3 = ff_const_si(3, 7); + sat_eq = yices_ff_eq_atom(yices_ff_add(a, c1), c3); + check(sat_eq != NULL_TERM, "building FF SAT constraint failed"); + + check_code(yices_assert_formula(ctx, sat_eq), "assert FF SAT constraint failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for a+1=3 in F7"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed for FF SAT"); + check_code(yices_get_ff_value(mdl, a, val, mod), "get_ff_value failed"); + check(mpz_cmp_si(mod, 7) == 0, "expected FF modulus 7"); + mpz_mod(tmp, val, mod); + check(mpz_cmp_si(tmp, 2) == 0, "expected a = 2 mod 7"); + check(yices_formula_true_in_model(mdl, sat_eq) == 1, "model must satisfy a+1=3"); + yices_free_model(mdl); + + yices_reset_context(ctx); + + ff_eq = yices_ff_eq_atom(a, c1); + ff_neq = yices_ff_neq_atom(a, c1); + check_code(yices_assert_formula(ctx, ff_eq), "assert a=1 failed"); + check_code(yices_assert_formula(ctx, ff_neq), "assert a!=1 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for a=1 and a!=1"); + + yices_reset_context(ctx); + + pa = yices_new_uninterpreted_term(yices_bool_type()); + qa = yices_new_uninterpreted_term(yices_bool_type()); + imp1 = yices_implies(pa, yices_ff_eq_atom(a, c1)); + imp2 = yices_implies(qa, yices_ff_neq_atom(a, c1)); + check_code(yices_assert_formula(ctx, imp1), "assert implication pa=>a=1 failed"); + check_code(yices_assert_formula(ctx, imp2), "assert implication qa=>a!=1 failed"); + + assumptions[0] = pa; + assumptions[1] = qa; + stat = yices_check_context_with_assumptions(ctx, NULL, 2, assumptions); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT with FF assumptions pa,qa"); + + yices_init_term_vector(&core); + check_code(yices_get_unsat_core(ctx, &core), "yices_get_unsat_core failed for FF assumptions"); + check(core.size == 2, "expected two assumptions in FF unsat core"); + check(has_term(&core, pa) && has_term(&core, qa), "FF unsat core missing assumptions"); + yices_delete_term_vector(&core); + + yices_free_context(ctx); + mpz_clear(tmp); + mpz_clear(mod); + mpz_clear(val); + mpz_clear(p); +} + +static void test_nla_assumption_core(void) { + context_t *ctx; + term_t x, p, q; + term_t imp1, imp2; + term_t assumptions[2]; + term_vector_t core; + smt_status_t stat; + + ctx = make_cdclt_context("QF_UFLRA"); + x = yices_new_uninterpreted_term(yices_real_type()); + p = yices_new_uninterpreted_term(yices_bool_type()); + q = yices_new_uninterpreted_term(yices_bool_type()); + + imp1 = yices_implies(p, yices_arith_eq_atom(yices_mul(x, x), yices_rational32(2, 1))); + imp2 = yices_implies(q, yices_arith_eq_atom(yices_mul(x, x), yices_rational32(3, 1))); + check_code(yices_assert_formula(ctx, imp1), "assert p=>x*x=2 failed"); + check_code(yices_assert_formula(ctx, imp2), "assert q=>x*x=3 failed"); + + assumptions[0] = p; + assumptions[1] = q; + stat = yices_check_context_with_assumptions(ctx, NULL, 2, assumptions); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT with NLA assumptions p,q"); + + yices_init_term_vector(&core); + check_code(yices_get_unsat_core(ctx, &core), "yices_get_unsat_core failed for NLA assumptions"); + check(core.size == 2, "expected two assumptions in NLA unsat core"); + check(has_term(&core, p) && has_term(&core, q), "NLA unsat core missing assumptions"); + yices_delete_term_vector(&core); + + yices_free_context(ctx); +} + +static void test_division_by_zero_remains_error(void) { + context_t *ctx; + term_t r, z, div, f; + int32_t code; + + ctx = make_cdclt_context("QF_ALIRA"); + r = yices_new_uninterpreted_term(yices_real_type()); + z = yices_rational32(0, 1); + div = yices_division(r, z); + f = yices_arith_eq_atom(div, z); + + code = yices_assert_formula(ctx, f); + check(code < 0, "asserting division-by-zero formula should fail"); + check(yices_error_code() == DIVISION_BY_ZERO, "expected DIVISION_BY_ZERO"); + + yices_free_context(ctx); +} + +int main(void) { + if (!yices_has_mcsat()) { + return 1; // skipped + } + + yices_init(); + + test_nla_sat_unsat_and_model(); + test_nla_hidden_product_and_push_pop(); + test_nonconstant_divisor_and_param_modes(); + test_ff_sat_unsat_model_and_assumption_core(); + test_nla_assumption_core(); + test_division_by_zero_remains_error(); + + yices_exit(); + return 0; +} From 8e210b2e14c0416ce1183fff5f38a5b9c6c94394 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Wed, 20 May 2026 23:21:39 -0700 Subject: [PATCH 4/9] Implement cube-only MCSAT satellite for CDCLT Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- src/api/context_config.c | 94 ++++- src/api/context_config.h | 7 +- src/api/yices_api.c | 10 +- src/context/context.c | 224 ++++-------- src/context/context.h | 7 + src/context/context_simplifier.c | 8 +- src/context/context_solver.c | 21 +- src/context/context_types.h | 4 +- src/context/context_utils.h | 4 +- src/frontend/smt2/smt2_commands.c | 21 +- src/solvers/egraph/egraph.c | 120 +++++++ src/solvers/egraph/egraph.h | 15 +- src/solvers/egraph/egraph_types.h | 26 ++ src/solvers/mcsat_satellite.c | 322 ++++++++++-------- src/solvers/mcsat_satellite.h | 4 +- tests/api/test_cdclt_mcsat_supplement.c | 28 ++ .../mcsat_supplement_qf_nia_unsat.smt2 | 6 + .../mcsat_supplement_qf_nia_unsat.smt2.gold | 1 + ...mcsat_supplement_qf_nia_unsat.smt2.options | 1 + 19 files changed, 585 insertions(+), 338 deletions(-) create mode 100644 tests/regress/mcsat_supplement_qf_nia_unsat.smt2 create mode 100644 tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold create mode 100644 tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options diff --git a/src/api/context_config.c b/src/api/context_config.c index 8257e9a51..2156491c6 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -90,6 +90,7 @@ typedef enum ctx_config_key { CTX_CONFIG_KEY_ARRAY_SOLVER, CTX_CONFIG_KEY_BV_SOLVER, CTX_CONFIG_KEY_ARITH_SOLVER, + CTX_CONFIG_KEY_MCSAT_SUPPLEMENT, CTX_CONFIG_KEY_MODEL_INTERPOLATION, CTX_CONFIG_KEY_SAT_DELEGATE, CTX_CONFIG_KEY_SAT_DELEGATE_INCREMENTAL_MODE, @@ -103,6 +104,7 @@ static const char *const config_key_names[NUM_CONFIG_KEYS] = { "arith-solver", "array-solver", "bv-solver", + "mcsat-supplement", "mode", "model-interpolation", "sat-delegate", @@ -117,6 +119,7 @@ static const int32_t config_key[NUM_CONFIG_KEYS] = { CTX_CONFIG_KEY_ARITH_SOLVER, CTX_CONFIG_KEY_ARRAY_SOLVER, CTX_CONFIG_KEY_BV_SOLVER, + CTX_CONFIG_KEY_MCSAT_SUPPLEMENT, CTX_CONFIG_KEY_MODE, CTX_CONFIG_KEY_MODEL_INTERPOLATION, CTX_CONFIG_KEY_SAT_DELEGATE, @@ -258,17 +261,20 @@ static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = { static const ctx_config_t default_config = { CTX_MODE_PUSHPOP, // mode CTX_SOLVER_TYPE_DPLLT, // DPLLT solver + false, // solver type set by user SMT_UNKNOWN, // logic CTX_CONFIG_DEFAULT, // uf CTX_CONFIG_DEFAULT, // array CTX_CONFIG_DEFAULT, // bv CTX_CONFIG_DEFAULT, // arith ARITH_LIRA, // fragment + false, // mcsat supplement false, // model interpolation SAT_DELEGATE_NONE, // sat delegate SAT_DELEGATE_MODE_REBUILD, // sat delegate incremental mode (unused unless explicitly set) false, // sat delegate incremental mode set by user NULL, // trace tags + false, // mcsat supplement set by user }; @@ -385,6 +391,7 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu r = -2; } else { config->solver_type = v; + config->solver_type_set = true; } break; @@ -422,6 +429,14 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu config->arith_config = v; } break; + case CTX_CONFIG_KEY_MCSAT_SUPPLEMENT: + v = parse_as_boolean(value, &config->mcsat_supplement); + if (v < 0) { + r = -2; + } else { + config->mcsat_supplement_set = true; + } + break; case CTX_CONFIG_KEY_MODEL_INTERPOLATION: v = parse_as_boolean(value, &config->model_interpolation); if (v < 0) { @@ -604,6 +619,46 @@ static bool arch_is_supported(context_arch_t a) { #endif } +/* + * Check whether architecture a has an E-graph coordinator. + */ +static bool arch_has_egraph(context_arch_t a) { + switch (a) { + case CTX_ARCH_EG: + case CTX_ARCH_EGFUN: + case CTX_ARCH_EGSPLX: + case CTX_ARCH_EGBV: + case CTX_ARCH_EGFUNSPLX: + case CTX_ARCH_EGFUNBV: + case CTX_ARCH_EGSPLXBV: + case CTX_ARCH_EGFUNSPLXBV: + return true; + default: + return false; + } +} + +/* + * CDCL(T) architecture to use when a logic's default backend is MCSAT + * but the configuration requests a DPLL(T) top-level solver. + */ +static inline context_arch_t mcsat_supplement_arch_for_logic(smt_logic_t logic) { + (void) logic; + return CTX_ARCH_EGFUNSPLXBV; +} + +static bool mcsat_supplement_is_supported(void) { +#if HAVE_MCSAT + return true; +#else + return false; +#endif +} + +static bool logic_supported_by_mcsat_config(smt_logic_t code) { + return code == SMT_ALL || !logic_has_quantifiers(code); +} + /* * Check whether config is valid (and supported by this version of Yices) @@ -619,11 +674,12 @@ static bool arch_is_supported(context_arch_t a) { * -2 if the config is valid but not currently supported * -3 if the solver combination is valid but does not support the specified mode */ -int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, context_mode_t *mode, bool *iflag, bool *qflag) { +int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, context_mode_t *mode, bool *iflag, bool *qflag, bool *mcsat_supplement) { smt_logic_t logic_code; int32_t a, r; r = 0; // default return code + *mcsat_supplement = false; logic_code = config->logic; if (logic_code != SMT_UNKNOWN) { @@ -655,7 +711,26 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar } } - a = logic2arch[logic_code]; + if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_MCSAT) { + if (!arch_is_supported(CTX_ARCH_MCSAT) || !logic_supported_by_mcsat_config(logic_code)) { + r = -2; + goto done; + } + a = CTX_ARCH_MCSAT; + } else { + a = logic2arch[logic_code]; + } + + if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_DPLLT && a == CTX_ARCH_MCSAT) { + if (config->mcsat_supplement_set && !config->mcsat_supplement) { + r = -1; + goto done; + } + a = mcsat_supplement_arch_for_logic(logic_code); + *mcsat_supplement = true; + } else if (config->mcsat_supplement) { + *mcsat_supplement = true; + } if (a < 0 || !arch_is_supported(a)) { // not supported r = -2; @@ -668,7 +743,11 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar *mode = config->mode; } - } else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) { + } else if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_MCSAT) { + if (config->mcsat_supplement) { + r = -1; + goto done; + } if (arch_is_supported(CTX_ARCH_MCSAT)) { /* * MCSAT solver/no logic specified @@ -699,6 +778,7 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar a = arch_add_bv(a); } a = arch_add_arith(a, config->arith_config); + *mcsat_supplement = config->mcsat_supplement; // a is either -1 or an architecture code if (a < 0) { @@ -716,6 +796,14 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar } } + if (r == 0 && *mcsat_supplement) { + if (!mcsat_supplement_is_supported()) { + r = -2; + } else if (*arch == CTX_ARCH_MCSAT || !arch_has_egraph(*arch)) { + r = -1; + } + } + done: return r; } diff --git a/src/api/context_config.h b/src/api/context_config.h index b05b477bb..f12616060 100644 --- a/src/api/context_config.h +++ b/src/api/context_config.h @@ -99,17 +99,20 @@ typedef enum solver_code { struct ctx_config_s { context_mode_t mode; context_solver_type_t solver_type; + bool solver_type_set; smt_logic_t logic; solver_code_t uf_config; solver_code_t array_config; solver_code_t bv_config; solver_code_t arith_config; arith_fragment_t arith_fragment; + bool mcsat_supplement; bool model_interpolation; sat_delegate_t sat_delegate; sat_delegate_incremental_mode_t sat_delegate_incremental_mode; bool sat_delegate_incremental_mode_set; char* trace_tags; + bool mcsat_supplement_set; }; @@ -149,7 +152,7 @@ extern int32_t config_set_logic(ctx_config_t *config, const char *logic); * * This can't be used to set config->logic: key must be one of "mode", * "arith-fragment", "uf-solver", "array-solver", "bv-solver", - * "arith-solver" or "trace". + * "arith-solver", "mcsat-supplement", or "trace". * * Return code: * -1 if the key is not recognized @@ -188,7 +191,7 @@ extern int32_t config_set_field(ctx_config_t *config, const char *key, const cha * 0 if the config is valid and supported */ extern int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, - context_mode_t *mode, bool *iflag, bool *qflag); + context_mode_t *mode, bool *iflag, bool *qflag, bool *mcsat_supplement); diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 331235eaa..8931fda6c 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8870,6 +8870,7 @@ context_t *_o_yices_new_context(const ctx_config_t *config) { context_mode_t mode; bool iflag; bool qflag; + bool mcsat_supplement; int32_t k; if (config == NULL) { @@ -8879,9 +8880,10 @@ context_t *_o_yices_new_context(const ctx_config_t *config) { mode = CTX_MODE_PUSHPOP; iflag = true; qflag = false; + mcsat_supplement = false; } else { // read the config - k = decode_config(config, &logic, &arch, &mode, &iflag, &qflag); + k = decode_config(config, &logic, &arch, &mode, &iflag, &qflag, &mcsat_supplement); if (k < 0) { // invalid configuration set_error_code(CTX_INVALID_CONFIG); @@ -8900,6 +8902,12 @@ context_t *_o_yices_new_context(const ctx_config_t *config) { } context_t* ctx = _o_yices_create_context(logic, arch, mode, iflag, qflag); + if (mcsat_supplement && context_attach_mcsat_supplement(ctx) < 0) { + delete_context(ctx); + safe_free(ctx); + set_error_code(CTX_INVALID_CONFIG); + return NULL; + } // Additional setup for MCSAT options in the config if (config != NULL) { diff --git a/src/context/context.c b/src/context/context.c index 75ce7f9f3..e90fd1c06 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -80,11 +80,9 @@ static thvar_t internalize_to_bv(context_t *ctx, term_t t); static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx); static bool context_atom_requires_mcsat(context_t *ctx, term_t atom); +static void context_observe_mcsat_atom(context_t *ctx, term_t atom, literal_t l); static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom); -static int32_t context_enable_mcsat_supplement(context_t *ctx); static void context_disable_mcsat_supplement(context_t *ctx); -static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a); -static int32_t context_seed_mcsat_satellite(context_t *ctx); /* @@ -190,6 +188,7 @@ static bool term_contains_arith_or_ff(context_t *ctx, term_t t, int_hmap_t *cach static bool term_requires_mcsat_supplement(context_t *ctx, term_t t, int_hmap_t *cache) { term_table_t *terms; int_hmap_pair_t *p; + type_t tau; bool trigger; uint32_t i, nchildren; @@ -204,10 +203,11 @@ static bool term_requires_mcsat_supplement(context_t *ctx, term_t t, int_hmap_t } terms = ctx->terms; + tau = term_type(terms, t); trigger = false; // finite-field usage - if (is_finitefield_term(terms, t)) { + if (is_finitefield_term(terms, t) || is_ff_type(terms->types, tau)) { trigger = true; } @@ -298,26 +298,10 @@ static bool term_requires_mcsat_supplement(context_t *ctx, term_t t, int_hmap_t return trigger; } -static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a) { - int_hmap_t cache; - uint32_t i; - bool trigger; - - init_int_hmap(&cache, 0); - trigger = false; - for (i=0; imcsat_supplement_active) { + if (ctx->mcsat_supplement) { return CTX_NO_ERROR; } if (ctx->arch == CTX_ARCH_MCSAT || ctx->egraph == NULL) { @@ -328,14 +312,9 @@ static int32_t context_enable_mcsat_supplement(context_t *ctx) { egraph_attach_mcsat_solver(ctx->egraph, sat, mcsat_satellite_ctrl_interface(sat), mcsat_satellite_smt_interface(sat), - mcsat_satellite_egraph_interface(sat)); - ctx->mcsat_supplement_active = true; - - code = context_seed_mcsat_satellite(ctx); - if (code < 0) { - context_disable_mcsat_supplement(ctx); - return code; - } + NULL); + egraph_attach_arith_observer(ctx->egraph, sat, mcsat_satellite_arith_observer_interface(sat)); + ctx->mcsat_supplement = true; return CTX_NO_ERROR; } @@ -343,93 +322,19 @@ static int32_t context_enable_mcsat_supplement(context_t *ctx) { static void context_disable_mcsat_supplement(context_t *ctx) { mcsat_satellite_t *sat; - if (!ctx->mcsat_supplement_active || ctx->egraph == NULL) { + if (!ctx->mcsat_supplement || ctx->egraph == NULL) { return; } sat = context_mcsat_satellite(ctx); + egraph_detach_arith_observer(ctx->egraph, sat); egraph_detach_mcsat_solver(ctx->egraph); delete_mcsat_satellite(sat); - ctx->mcsat_supplement_active = false; -} - -/* - * Import already-internalized arithmetic/FF atoms when supplementary MCSAT - * is activated after earlier assertions. - */ -static int32_t context_seed_mcsat_satellite(context_t *ctx) { - mcsat_satellite_t *sat; - term_table_t *terms; - uint32_t i, n; - uint32_t seeded = 0; - bool trace_seed; - - sat = context_mcsat_satellite(ctx); - if (sat == NULL) { - return CTX_NO_ERROR; - } - - terms = ctx->terms; - trace_seed = tracing_tag(ctx->trace, "mcsat::supplement::seed"); - n = intern_tbl_num_terms(&ctx->intern); - for (i = 1; i < n; i++) { - term_t t; - int32_t code; - literal_t l; - - if (!good_term_idx(terms, i)) { - continue; - } - - t = pos_term(i); - if (!is_boolean_term(terms, t) || - !intern_tbl_is_root(&ctx->intern, t) || - !intern_tbl_root_is_mapped(&ctx->intern, t)) { - continue; - } - - if (!context_atom_requires_mcsat(ctx, t)) { - continue; - } - - code = intern_tbl_map_of_root(&ctx->intern, t); - if (code_is_var(code)) { - l = code2literal(code); - } else { - occ_t u = code2occ(code); - if (u == true_occ) { - l = true_literal; - } else if (u == false_occ) { - l = false_literal; - } else if (ctx->egraph != NULL) { - l = egraph_occ2literal(ctx->egraph, u); - } else { - continue; - } - } - - code = mcsat_satellite_register_atom(sat, t, l, NULL); - if (code < 0) { - return code; - } - seeded ++; - if (trace_seed) { - trace_printf(ctx->trace, 1, "mcsat supplement seed: lit=%"PRId32" atom=", l); - trace_pp_term(ctx->trace, 1, terms, t); - } - } - - if (trace_seed) { - trace_printf(ctx->trace, 1, "mcsat supplement seeded %"PRIu32" atoms\n", seeded); - } - - return CTX_NO_ERROR; + ctx->mcsat_supplement = false; } static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { switch (term_kind(terms, atom)) { - case EQ_TERM: - case DISTINCT_TERM: case ARITH_ROOT_ATOM: case ARITH_FF_EQ_ATOM: case ARITH_FF_BINEQ_ATOM: @@ -447,10 +352,10 @@ static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { static bool context_atom_requires_mcsat(context_t *ctx, term_t atom) { int_hmap_t cache; - bool trigger, all_arith_mode; + bool trigger; atom = unsigned_term(atom); - if (!ctx->mcsat_supplement_active || !is_boolean_term(ctx->terms, atom)) { + if (!ctx->mcsat_supplement || !is_boolean_term(ctx->terms, atom)) { return false; } if (!mcsat_satellite_candidate_atom(ctx->terms, atom)) { @@ -458,13 +363,12 @@ static bool context_atom_requires_mcsat(context_t *ctx, term_t atom) { } init_int_hmap(&cache, 0); - /* - * In supplementary mode, route every arithmetic/FF atom to MCSAT so that - * MCSAT sees the complete arithmetic conjunction (not just unsupported atoms). - */ - all_arith_mode = true; - if (all_arith_mode) { + if (!context_has_arith_solver(ctx)) { trigger = term_contains_arith_or_ff(ctx, atom, &cache); + if (!trigger) { + int_hmap_reset(&cache); + trigger = term_requires_mcsat_supplement(ctx, atom, &cache); + } } else { trigger = term_requires_mcsat_supplement(ctx, atom, &cache); } @@ -473,6 +377,27 @@ static bool context_atom_requires_mcsat(context_t *ctx, term_t atom) { return trigger; } +static void context_observe_mcsat_atom(context_t *ctx, term_t atom, literal_t l) { + int_hmap_t cache; + bool observe; + + if (!ctx->mcsat_supplement || !is_boolean_term(ctx->terms, atom) || + !mcsat_satellite_candidate_atom(ctx->terms, atom)) { + return; + } + + init_int_hmap(&cache, 0); + observe = term_contains_arith_or_ff(ctx, atom, &cache); + delete_int_hmap(&cache); + + if (observe) { + int32_t code = egraph_arith_observer_register_atom(ctx->egraph, atom, l); + if (code < 0) { + longjmp(ctx->env, code); + } + } +} + static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { mcsat_satellite_t *sat; literal_t l; @@ -2268,7 +2193,7 @@ static thvar_t map_bvpoly_buffer_to_bv(context_t *ctx, bvpoly_buffer_t *b) { free_bvpoly(q); } - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { mcsat_satellite_t *sat = context_mcsat_satellite(ctx); if (sat != NULL) { mcsat_satellite_register_arith_term(sat, x, r); @@ -3394,12 +3319,8 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { } - if (ctx->mcsat_supplement_active) { - mcsat_satellite_t *sat; - sat = context_mcsat_satellite(ctx); - if (sat != NULL) { - mcsat_satellite_register_arith_term(sat, x, unsigned_term(r)); - } + if (ctx->mcsat_supplement && ctx->egraph != NULL) { + egraph_arith_observer_register_arith_term(ctx->egraph, x, unsigned_term(r)); } return x; @@ -3769,6 +3690,10 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t) { break; } + if (ctx->mcsat_supplement) { + context_observe_mcsat_atom(ctx, r, l); + } + // map r to l in the internalization table intern_tbl_map_root(&ctx->intern, r, literal2code(l)); } @@ -5199,6 +5124,9 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { assert_internalization_code(ctx, code, tt); return; } + if (ctx->mcsat_supplement) { + context_observe_mcsat_atom(ctx, t, tt ? true_literal : false_literal); + } switch (term_kind(terms, t)) { case CONSTANT_TERM: @@ -5333,6 +5261,9 @@ static void assert_term(context_t *ctx, term_t t, bool tt) { assert_internalization_code(ctx, code, tt); return; } + if (ctx->mcsat_supplement) { + context_observe_mcsat_atom(ctx, t, tt ? true_literal : false_literal); + } // store the mapping t --> tt intern_tbl_map_root(&ctx->intern, t, bool2code(tt)); @@ -6004,7 +5935,7 @@ static void init_solvers(context_t *ctx) { ctx->bv_solver = NULL; ctx->fun_solver = NULL; ctx->quant_solver = NULL; - ctx->mcsat_supplement_active = false; + ctx->mcsat_supplement = false; // Create egraph first, then satellite solvers if (solvers & EGRPH) { @@ -6258,7 +6189,7 @@ void delete_context(context_t *ctx) { ctx->mcsat = NULL; } - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { context_disable_mcsat_supplement(ctx); } @@ -6354,10 +6285,6 @@ void reset_context(context_t *ctx) { reset_smt_core(ctx->core); // this propagates reset to all solvers - if (ctx->mcsat_supplement_active) { - context_disable_mcsat_supplement(ctx); - } - if (ctx->mcsat != NULL) { mcsat_reset(ctx->mcsat); } @@ -6415,7 +6342,7 @@ void context_set_trace(context_t *ctx, tracer_t *trace) { if (ctx->mcsat != NULL) { mcsat_set_tracer(ctx->mcsat, trace); } - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { mcsat_satellite_t *sat = context_mcsat_satellite(ctx); if (sat != NULL) { mcsat_satellite_set_trace(sat, trace); @@ -6528,25 +6455,6 @@ static int32_t context_process_assertions(context_t *ctx, uint32_t n, const term ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); - if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { - if (context_assertions_need_mcsat_supplement(ctx, n, a)) { - code = context_enable_mcsat_supplement(ctx); - if (code < 0) { - return code; - } - } - } - - if (ctx->mcsat_supplement_active) { - mcsat_satellite_t *sat = context_mcsat_satellite(ctx); - if (sat != NULL) { - code = mcsat_satellite_assert_formulas(sat, n, a); - if (code < 0) { - return code; - } - } - } - code = setjmp(ctx->env); if (code == 0) { @@ -6886,15 +6794,6 @@ int32_t context_internalize(context_t *ctx, term_t t) { ivector_reset(&ctx->subst_eqs); ivector_reset(&ctx->aux_eqs); - if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx) && !ctx->mcsat_supplement_active) { - if (context_assertions_need_mcsat_supplement(ctx, 1, &t)) { - code = context_enable_mcsat_supplement(ctx); - if (code < 0) { - return code; - } - } - } - code = setjmp(ctx->env); if (code == 0) { // we must call internalization start first @@ -6975,15 +6874,6 @@ int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f) { ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); - if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { - if (context_assertions_need_mcsat_supplement(ctx, n, f)) { - code = context_enable_mcsat_supplement(ctx); - if (code < 0) { - return code; - } - } - } - code = setjmp(ctx->env); if (code == 0) { // flatten @@ -7285,7 +7175,7 @@ void context_gc_mark(context_t *ctx) { if (ctx->mcsat != NULL) { mcsat_gc_mark(ctx->mcsat); } - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { mcsat_satellite_t *sat = context_mcsat_satellite(ctx); if (sat != NULL) { mcsat_satellite_gc_mark(sat); diff --git a/src/context/context.h b/src/context/context.h index 6a2d827f2..ccecae4d5 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -58,6 +58,13 @@ extern bool context_arch_has_mcsat(context_arch_t arch); extern void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, context_mode_t mode, context_arch_t arch, bool qflag); +/* + * Attach the supplemental MCSAT E-graph satellite. + * This must be called before assertions/search; it is a construction-time + * configuration step, not an assertion-time activation path. + */ +extern int32_t context_attach_mcsat_supplement(context_t *ctx); + /* * Deletion diff --git a/src/context/context_simplifier.c b/src/context/context_simplifier.c index 824ca8706..e155bd79d 100644 --- a/src/context/context_simplifier.c +++ b/src/context/context_simplifier.c @@ -1165,7 +1165,7 @@ static void try_substitution(context_t *ctx, term_t t1, term_t t2, term_t e) { * In supplementary-MCSAT mode, keep equalities explicit so they can be * routed to the MCSAT satellite as tracked atoms/constraints. */ - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { ivector_push(&ctx->top_eqs, e); return; } @@ -1212,7 +1212,7 @@ static void try_bool_substitution(context_t *ctx, term_t t1, term_t t2, term_t e /* * In supplementary-MCSAT mode, keep boolean equalities explicit. */ - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { ivector_push(&ctx->top_formulas, e); return; } @@ -2262,7 +2262,7 @@ void flatten_assertion(context_t *ctx, term_t f) { break; case ARITH_ROOT_ATOM: - if (context_mcsat_supplement_active(ctx)) { + if (context_mcsat_supplement(ctx)) { intern_tbl_map_root(intern, r, bool2code(tt)); ivector_push(&ctx->top_atoms, signed_term(r, tt)); } else { @@ -2349,7 +2349,7 @@ void flatten_assertion(context_t *ctx, term_t f) { case ARITH_FF_EQ_ATOM: case ARITH_FF_BINEQ_ATOM: - if (context_mcsat_supplement_active(ctx)) { + if (context_mcsat_supplement(ctx)) { intern_tbl_map_root(intern, r, bool2code(tt)); ivector_push(&ctx->top_atoms, signed_term(r, tt)); } else { diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 9d0ac9444..71cd75be8 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -528,7 +528,7 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params) egraph_set_max_interface_eqs(egraph, params->max_interface_eqs); } - if (ctx->mcsat_supplement_active && egraph != NULL && egraph->th[ETYPE_MCSAT] != NULL) { + if (ctx->mcsat_supplement && egraph != NULL && egraph->th[ETYPE_MCSAT] != NULL) { mcsat_satellite_set_search_parameters((mcsat_satellite_t *) egraph->th[ETYPE_MCSAT], params); } @@ -612,7 +612,7 @@ smt_status_t check_context(context_t *ctx, const param_t *params) { } sat = NULL; - if (ctx->mcsat_supplement_active && + if (ctx->mcsat_supplement && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; @@ -652,7 +652,7 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param } sat = NULL; - if (ctx->mcsat_supplement_active && + if (ctx->mcsat_supplement && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; @@ -1403,7 +1403,7 @@ static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t interpolant = NULL_TERM; sat = NULL; - if (ctx->mcsat_supplement_active && + if (ctx->mcsat_supplement && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; @@ -1470,7 +1470,7 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * context_invalidate_unsat_core_cache(ctx); if (ctx->mcsat == NULL) { - if (ctx->mcsat_supplement_active) { + if (ctx->mcsat_supplement) { return check_context_with_term_assumptions_supplement(ctx, params, n, a, error); } smt_status_t stat; @@ -1574,6 +1574,13 @@ smt_status_t check_context_with_model(context_t *ctx, const param_t *params, mod // } } + if (stat == YICES_STATUS_UNSAT && n == 0 && + context_supports_model_interpolation(ctx) && + mcsat_get_unsat_model_interpolant(ctx->mcsat) == NULL_TERM) { + // With no model assumptions, false is the canonical interpolant. + mcsat_set_unsat_result_from_labeled_interpolant(ctx->mcsat, false_term, 0, NULL, NULL); + } + return stat; } @@ -2104,7 +2111,7 @@ void build_model(model_t *model, context_t *ctx) { * Supplemental MCSAT values are an overlay: apply them after the regular * CDCL(T) model is fully built so nonlinear/FF values are not overwritten. */ - if (ctx->mcsat_supplement_active && context_has_egraph(ctx) && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + if (ctx->mcsat_supplement && context_has_egraph(ctx) && ctx->egraph->th[ETYPE_MCSAT] != NULL) { mcsat_satellite_build_model((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT], model); } } @@ -2241,7 +2248,7 @@ term_t context_get_unsat_model_interpolant(context_t *ctx) { return mcsat_get_unsat_model_interpolant(ctx->mcsat); } - if (ctx->mcsat_supplement_active && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + if (ctx->mcsat_supplement && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { return mcsat_satellite_get_unsat_model_interpolant((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]); } diff --git a/src/context/context_types.h b/src/context/context_types.h index 40b776457..f6cc838de 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -752,8 +752,8 @@ struct context_s { // flag for enabling adding quant instances bool en_quant; - // true when supplementary mcsat satellite is active in cdcl(t) mode - bool mcsat_supplement_active; + // true when the supplemental MCSAT satellite is configured in CDCL(T) mode + bool mcsat_supplement; }; diff --git a/src/context/context_utils.h b/src/context/context_utils.h index e72bd9e2a..21adc5140 100644 --- a/src/context/context_utils.h +++ b/src/context/context_utils.h @@ -660,8 +660,8 @@ static inline bool context_has_mcsat(context_t *ctx) { return ctx->arch == CTX_ARCH_MCSAT; } -static inline bool context_mcsat_supplement_active(context_t *ctx) { - return ctx->mcsat_supplement_active; +static inline bool context_mcsat_supplement(context_t *ctx) { + return ctx->mcsat_supplement; } diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index 528568a91..4746d9df1 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -2273,6 +2273,10 @@ static inline context_arch_t smt2_arch_for_logic(const smt2_globals_t *g, smt_lo return arch; } +static inline bool smt2_logic_uses_mcsat_supplement(const smt2_globals_t *g, smt_logic_t logic) { + return g->force_dpllt && arch_for_logic(logic) == CTX_ARCH_MCSAT; +} + /* * Options: produce-unsat-cores and produce-unsat-assumptions. @@ -2592,6 +2596,7 @@ static void init_smt2_context(smt2_globals_t *g) { smt_logic_t logic; context_arch_t arch; context_mode_t mode; + int32_t code; bool iflag; bool qflag; @@ -2635,14 +2640,24 @@ static void init_smt2_context(smt2_globals_t *g) { g->ctx = yices_create_context(logic, arch, mode, iflag, qflag); assert(g->ctx != NULL); - if (g->verbosity > 0 || g->tracer != NULL) { - context_set_trace(g->ctx, get_tracer(g)); - } // Set the mcsat options g->ctx->mcsat_options = g->mcsat_options; ivector_copy(&g->ctx->mcsat_var_order, g->var_order.data, g->var_order.size); + if (!g->mcsat && smt2_logic_uses_mcsat_supplement(g, logic)) { + code = context_attach_mcsat_supplement(g->ctx); + assert(code == CTX_NO_ERROR); + if (code < 0) { + print_error("failed to attach the mcsat supplement"); + done = true; + return; + } + } + if (g->verbosity > 0 || g->tracer != NULL) { + context_set_trace(g->ctx, get_tracer(g)); + } + /* * TODO: override the default context options based on * ctx_parameters. I don't want to do it now (2015/07/22). If we diff --git a/src/solvers/egraph/egraph.c b/src/solvers/egraph/egraph.c index c7be4ca5d..b82bbd679 100644 --- a/src/solvers/egraph/egraph.c +++ b/src/solvers/egraph/egraph.c @@ -3630,10 +3630,23 @@ static void create_ackermann_lemma(egraph_t *egraph, composite_t *c1, composite_ * visible in the egraph). */ static void propagate_satellite_equality(egraph_t *egraph, etype_t i, thvar_t v1, thvar_t v2, int32_t id) { + arith_observer_t *obs; + uint32_t j, n; + assert(i < NUM_SATELLITES && egraph->eg[i] != NULL); // call the merge function for theory i egraph->eg[i]->assert_equality(egraph->th[i], v1, v2, id); + + if (i == ETYPE_INT || i == ETYPE_REAL) { + n = egraph->num_arith_observers; + for (j=0; jarith_observer + j; + if (obs->interface->assert_equality != NULL) { + obs->interface->assert_equality(obs->solver, v1, v2, id); + } + } + } } @@ -3641,8 +3654,21 @@ static void propagate_satellite_equality(egraph_t *egraph, etype_t i, thvar_t v1 * Propagate disequality between v1 and v2 in theory i */ static void propagate_satellite_disequality(egraph_t *egraph, etype_t i, thvar_t v1, thvar_t v2, composite_t *hint) { + arith_observer_t *obs; + uint32_t j, n; + assert(i < NUM_SATELLITES && egraph->eg[i] != NULL); egraph->eg[i]->assert_disequality(egraph->th[i], v1, v2, hint); + + if (i == ETYPE_INT || i == ETYPE_REAL) { + n = egraph->num_arith_observers; + for (j=0; jarith_observer + j; + if (obs->interface->assert_disequality != NULL) { + obs->interface->assert_disequality(obs->solver, v1, v2, hint); + } + } + } } @@ -3654,8 +3680,23 @@ static void propagate_satellite_disequality(egraph_t *egraph, etype_t i, thvar_t * and each a[i] is a theory variable attached to the class of some term t_j */ static void propagate_satellite_distinct(egraph_t *egraph, etype_t i, uint32_t n, thvar_t *a, composite_t *hint) { + arith_observer_t *obs; + uint32_t j, m; + assert(i < NUM_SATELLITES && egraph->eg[i] != NULL); egraph->eg[i]->assert_distinct(egraph->th[i], n, a, hint); + + if (i == ETYPE_INT || i == ETYPE_REAL) { + m = egraph->num_arith_observers; + for (j=0; jarith_observer + j; + if (obs->interface->assert_distinct != NULL) { + // Arithmetic observers are notification-only: conflicts must be + // reported by their propagate/final_check callbacks, not here. + (void) obs->interface->assert_distinct(obs->solver, n, a, hint); + } + } + } } @@ -6949,6 +6990,9 @@ void init_egraph(egraph_t *egraph, type_table_t *ttbl) { egraph->bv_eg = NULL; egraph->fun_eg = NULL; egraph->quant_eg = NULL; + egraph->arith_observer = NULL; + egraph->num_arith_observers = 0; + egraph->arith_observer_size = 0; // model-construction object init_egraph_model(&egraph->mdl); @@ -7025,6 +7069,77 @@ void egraph_detach_mcsat_solver(egraph_t *egraph) { egraph->mcsat_smt = NULL; } +static void egraph_extend_arith_observers(egraph_t *egraph) { + uint32_t n; + + assert(egraph->num_arith_observers == egraph->arith_observer_size); + n = egraph->arith_observer_size + 1; + n += n >> 1; + egraph->arith_observer = (arith_observer_t *) safe_realloc(egraph->arith_observer, n * sizeof(arith_observer_t)); + egraph->arith_observer_size = n; +} + +void egraph_attach_arith_observer(egraph_t *egraph, void *solver, + arith_observer_interface_t *interface) { + arith_observer_t *obs; + + assert(interface != NULL); + if (egraph->num_arith_observers == egraph->arith_observer_size) { + egraph_extend_arith_observers(egraph); + } + + obs = egraph->arith_observer + egraph->num_arith_observers; + obs->solver = solver; + obs->interface = interface; + egraph->num_arith_observers ++; +} + +void egraph_detach_arith_observer(egraph_t *egraph, void *solver) { + uint32_t i, n; + + n = egraph->num_arith_observers; + for (i=0; iarith_observer[i].solver == solver) { + n --; + egraph->arith_observer[i] = egraph->arith_observer[n]; + egraph->num_arith_observers = n; + return; + } + } +} + +int32_t egraph_arith_observer_register_atom(egraph_t *egraph, term_t atom, literal_t l) { + arith_observer_t *obs; + int32_t code; + uint32_t i, n; + + n = egraph->num_arith_observers; + for (i=0; iarith_observer + i; + if (obs->interface->register_atom != NULL) { + code = obs->interface->register_atom(obs->solver, atom, l); + if (code < 0) { + return code; + } + } + } + + return 0; +} + +void egraph_arith_observer_register_arith_term(egraph_t *egraph, thvar_t x, term_t t) { + arith_observer_t *obs; + uint32_t i, n; + + n = egraph->num_arith_observers; + for (i=0; iarith_observer + i; + if (obs->interface->register_arith_term != NULL) { + obs->interface->register_arith_term(obs->solver, x, t); + } + } +} + /* * Attach a function subsolver @@ -7092,6 +7207,11 @@ void egraph_attach_core(egraph_t *egraph, smt_core_t *core) { * Delete everything */ void delete_egraph(egraph_t *egraph) { + safe_free(egraph->arith_observer); + egraph->arith_observer = NULL; + egraph->num_arith_observers = 0; + egraph->arith_observer_size = 0; + delete_egraph_model(&egraph->mdl); if (egraph->app_partition != NULL) { delete_ptr_partition(egraph->app_partition); diff --git a/src/solvers/egraph/egraph.h b/src/solvers/egraph/egraph.h index ff14b9946..cf4d752ff 100644 --- a/src/solvers/egraph/egraph.h +++ b/src/solvers/egraph/egraph.h @@ -74,7 +74,8 @@ extern void egraph_attach_bvsolver(egraph_t *egraph, /* * Attach a supplementary MCSAT satellite * - solver = pointer to the satellite object - * - ctrl, smt, eg = interface descriptors + * - ctrl, smt = interface descriptors + * - eg is optional; supplemental observers should normally pass NULL */ extern void egraph_attach_mcsat_solver(egraph_t *egraph, void *solver, @@ -87,6 +88,18 @@ extern void egraph_attach_mcsat_solver(egraph_t *egraph, */ extern void egraph_detach_mcsat_solver(egraph_t *egraph); +/* + * Attach/detach an arithmetic observer. + */ +extern void egraph_attach_arith_observer(egraph_t *egraph, + void *solver, + arith_observer_interface_t *interface); + +extern void egraph_detach_arith_observer(egraph_t *egraph, void *solver); + +extern int32_t egraph_arith_observer_register_atom(egraph_t *egraph, term_t atom, literal_t l); +extern void egraph_arith_observer_register_arith_term(egraph_t *egraph, thvar_t x, term_t t); + /* * Attach a function/array subsolver * - solver = pointer to the subsolver object diff --git a/src/solvers/egraph/egraph_types.h b/src/solvers/egraph/egraph_types.h index 4015b65a0..e742d4cbc 100644 --- a/src/solvers/egraph/egraph_types.h +++ b/src/solvers/egraph/egraph_types.h @@ -1146,6 +1146,28 @@ typedef struct arith_egraph_interface_s { arith_val_fun_t value_in_model; } arith_egraph_interface_t; +/* + * ARITHMETIC OBSERVER INTERFACE + * + * Supplemental arithmetic-capable solvers can observe arithmetic atoms and + * arrangement facts without owning the primary arithmetic solver slot. + */ +typedef int32_t (*arith_observer_atom_fun_t)(void *solver, term_t atom, literal_t l); +typedef void (*arith_observer_term_fun_t)(void *solver, thvar_t x, term_t t); + +typedef struct arith_observer_interface_s { + arith_observer_atom_fun_t register_atom; + arith_observer_term_fun_t register_arith_term; + assert_eq_fun_t assert_equality; + assert_diseq_fun_t assert_disequality; + assert_distinct_fun_t assert_distinct; +} arith_observer_interface_t; + +typedef struct arith_observer_s { + void *solver; + arith_observer_interface_t *interface; +} arith_observer_t; + /* @@ -1485,6 +1507,10 @@ struct egraph_s { fun_egraph_interface_t *fun_eg; quant_egraph_interface_t *quant_eg; + arith_observer_t *arith_observer; + uint32_t num_arith_observers; + uint32_t arith_observer_size; + /* * Model structure diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index 9fd6b111d..5330bc651 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -45,7 +45,13 @@ typedef struct mcsat_atom_entry_s { typedef struct mcsat_eq_entry_s { term_t label; + term_t t1; + term_t t2; + eterm_t e1; + eterm_t e2; literal_t source_lit; + int32_t edge_id; + bool is_eq; } mcsat_eq_entry_t; struct mcsat_satellite_s { @@ -213,7 +219,8 @@ static void collect_boolean_atoms(mcsat_satellite_t *sat, term_t t, int_hset_t * int_hset_add(visited, t); terms = sat->mctx.terms; - if (term_type(terms, t) == bool_type(terms->types)) { + if (term_type(terms, t) == bool_type(terms->types) && + term_kind(terms, t) == UNINTERPRETED_TERM) { int_hset_add(atoms, t); } @@ -261,54 +268,138 @@ static void collect_boolean_atoms(mcsat_satellite_t *sat, term_t t, int_hset_t * } } +static void mcsat_satellite_push_negated_literal(mcsat_satellite_t *sat, int_hset_t *seen_lits, literal_t l) { + if (l != null_literal && !int_hset_member(seen_lits, l)) { + int_hset_add(seen_lits, l); + ivector_push(&sat->conflict, not(l)); + } +} + +static mcsat_eq_entry_t *mcsat_satellite_find_eq_label(mcsat_satellite_t *sat, term_t label) { + uint32_t i; + + for (i=0; inum_eq; i++) { + if (sat->eq[i].label == label) { + return sat->eq + i; + } + } + + return NULL; +} + +static bool mcsat_satellite_expand_label(mcsat_satellite_t *sat, term_t label, int_hset_t *seen_lits); + +static bool mcsat_satellite_expand_eq_label(mcsat_satellite_t *sat, mcsat_eq_entry_t *eq, int_hset_t *seen_lits) { + ivector_t v; + uint32_t i; + + if (eq->source_lit != null_literal) { + mcsat_satellite_push_negated_literal(sat, seen_lits, eq->source_lit); + return true; + } + + if (eq->is_eq && sat->egraph != NULL && eq->e1 != null_eterm && eq->e2 != null_eterm && eq->edge_id >= 0) { + init_ivector(&v, 0); + egraph_explain_equality(sat->egraph, pos_occ(eq->e1), pos_occ(eq->e2), eq->edge_id, &v); + for (i=0; ilabel_to_lit, label); + if (p != NULL) { + mcsat_satellite_push_negated_literal(sat, seen_lits, p->val); + return true; + } + + eq = mcsat_satellite_find_eq_label(sat, label); + return eq != NULL && mcsat_satellite_expand_eq_label(sat, eq, seen_lits); +} + +static bool mcsat_satellite_expand_all_assumptions(mcsat_satellite_t *sat, int_hset_t *seen_lits) { + uint32_t i; + + for (i=0; iassumptions.size; i++) { + if (!mcsat_satellite_expand_label(sat, sat->assumptions.data[i], seen_lits)) { + return false; + } + } + + return true; +} + /* * Build a conflict clause from mcsat interpolant labels. - * Fallback: use all current tracked assumptions. */ -static void mcsat_satellite_record_conflict(mcsat_satellite_t *sat) { +static bool mcsat_satellite_record_conflict(mcsat_satellite_t *sat) { term_t interpolant; int_hset_t labels; int_hset_t visited; int_hset_t seen_lits; - int_hmap_pair_t *p; - literal_t l; + term_t label; + bool ok; uint32_t i; ivector_reset(&sat->conflict); init_int_hset(&labels, 0); init_int_hset(&visited, 0); init_int_hset(&seen_lits, 0); + ok = true; interpolant = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); if (interpolant != NULL_TERM) { collect_boolean_atoms(sat, interpolant, &labels, &visited); - p = int_hmap_first_record(&sat->label_to_lit); - while (p != NULL) { - if (int_hset_member(&labels, p->key) && p->val != null_literal && - !int_hset_member(&seen_lits, p->val)) { - int_hset_add(&seen_lits, p->val); - ivector_push(&sat->conflict, not(p->val)); + if (labels.z_flag) { + ok = mcsat_satellite_expand_label(sat, 0, &seen_lits); + } + for (i=0; ok && ilabel_to_lit, p); } + if (!ok) { + /* + * Some MCSAT interpolants can contain internal Boolean structure rather + * than just our public labels. The coarse active-cube clause is still + * sound, provided every active label has a CDCL/E-graph explanation. + */ + ivector_reset(&sat->conflict); + int_hset_reset(&seen_lits); + ok = mcsat_satellite_expand_all_assumptions(sat, &seen_lits); + } + } else { + /* + * MCSAT does not produce a label interpolant for every assumption conflict. + * In that case, learn the clause over the whole active cube, but only if + * every active label can be expanded to a CDCL/E-graph explanation. + */ + ok = mcsat_satellite_expand_all_assumptions(sat, &seen_lits); } - if (sat->conflict.size == 0) { - for (i = 0; i < sat->assumption_lits.size; i++) { - l = sat->assumption_lits.data[i]; - if (l != null_literal && !int_hset_member(&seen_lits, l)) { - int_hset_add(&seen_lits, l); - ivector_push(&sat->conflict, not(l)); - } - } + if (!ok) { + assert(false && "MCSAT conflict label has no expandable CDCL explanation"); } - ivector_push(&sat->conflict, null_literal); - record_theory_conflict(sat->core, sat->conflict.data); + if (ok) { + ivector_push(&sat->conflict, null_literal); + record_theory_conflict(sat->core, sat->conflict.data); + } delete_int_hset(&seen_lits); delete_int_hset(&visited); delete_int_hset(&labels); + + return ok; } /* @@ -355,7 +446,9 @@ static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bo sat->cache_valid = true; sat->cache_signature = sig; } else if (status == YICES_STATUS_UNSAT && emit_conflict) { - mcsat_satellite_record_conflict(sat); + if (!mcsat_satellite_record_conflict(sat)) { + status = YICES_STATUS_UNKNOWN; + } } return status; @@ -389,13 +482,15 @@ static void mcsat_satellite_backtrack_to(mcsat_satellite_t *sat, uint32_t target /* * Align the internal MCSAT scope stack with the outer context base level. - * This is needed when the satellite is attached after one or more pushes. + * This keeps the MCSAT engine scoped like the outer context even if an + * internal caller attaches the satellite after one or more pushes. */ static void mcsat_satellite_sync_base_level(mcsat_satellite_t *sat, uint32_t base_level) { uint32_t i; for (i = 0; i < base_level; i++) { - context_push(&sat->mctx); + mcsat_satellite_prepare_assertion_state(sat); + mcsat_push(sat->mctx.mcsat); ivector_push(&sat->atom_push_mark, sat->num_atoms); sat->push_depth ++; mcsat_satellite_open_level(sat); @@ -427,7 +522,20 @@ static literal_t source_lit_from_hint(mcsat_satellite_t *sat, composite_t *hint) /* * Add one eq/diseq notification as a labeled internal assumption. */ -static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t1, term_t t2, bool eq, literal_t src) { +static eterm_t mcsat_satellite_arith_eterm(mcsat_satellite_t *sat, thvar_t x) { + context_t *ctx; + + ctx = sat->ctx; + if (ctx->arith_solver != NULL && ctx->arith.eterm_of_var != NULL) { + return ctx->arith.eterm_of_var(ctx->arith_solver, x); + } + + return null_eterm; +} + +static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t1, term_t t2, + eterm_t e1, eterm_t e2, bool eq, + literal_t src, int32_t edge_id) { int32_t k0, k1; pmap2_rec_t *r; term_t atom; @@ -436,8 +544,11 @@ static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t if (t1 > t2) { term_t aux = t1; + eterm_t eaux = e1; t1 = t2; t2 = aux; + e1 = e2; + e2 = eaux; } k0 = eq ? (int32_t) t1 : -((int32_t) t1) - 1; @@ -460,7 +571,13 @@ static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t } sat->eq[sat->num_eq].label = label; + sat->eq[sat->num_eq].t1 = t1; + sat->eq[sat->num_eq].t2 = t2; + sat->eq[sat->num_eq].e1 = e1; + sat->eq[sat->num_eq].e2 = e2; sat->eq[sat->num_eq].source_lit = src; + sat->eq[sat->num_eq].edge_id = edge_id; + sat->eq[sat->num_eq].is_eq = eq; sat->num_eq ++; r->val = 1; @@ -520,7 +637,14 @@ static void mcsat_satellite_backtrack(void *solver, uint32_t back_level) { static void mcsat_satellite_push(void *solver) { mcsat_satellite_t *sat = solver; - context_push(&sat->mctx); + + /* + * sat->mctx is a thin host for the MCSAT engine. The satellite asserts + * only label-guarded facts into that engine, so bypass the wrapping + * context_t push/pop machinery and scope the MCSAT engine directly. + */ + mcsat_satellite_prepare_assertion_state(sat); + mcsat_push(sat->mctx.mcsat); ivector_push(&sat->atom_push_mark, sat->num_atoms); sat->push_depth ++; mcsat_satellite_open_level(sat); @@ -534,7 +658,7 @@ static void mcsat_satellite_pop(void *solver) { assert(sat->push_depth > 0); assert(sat->atom_push_mark.size > 0); - context_pop(&sat->mctx); + mcsat_pop(sat->mctx.mcsat); assert(sat->dlevel > 0); mark = ivector_pop2(&sat->atom_push_mark); @@ -606,18 +730,28 @@ static literal_t mcsat_satellite_select_polarity(void *solver, void *atom, liter return l; } +static int32_t mcsat_satellite_observe_atom(void *solver, term_t atom, literal_t l) { + return mcsat_satellite_register_atom((mcsat_satellite_t *) solver, atom, l, NULL); +} + +static void mcsat_satellite_observe_arith_term(void *solver, thvar_t x, term_t t) { + mcsat_satellite_register_arith_term((mcsat_satellite_t *) solver, x, t); +} + /* * Egraph interface callbacks. */ static void mcsat_satellite_assert_equality(void *solver, thvar_t x1, thvar_t x2, int32_t id) { mcsat_satellite_t *sat = solver; int_hmap_pair_t *p1, *p2; - (void) id; p1 = int_hmap_find(&sat->arith_var_to_term, x1); p2 = int_hmap_find(&sat->arith_var_to_term, x2); if (p1 != NULL && p2 != NULL) { - mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, true, null_literal); + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, + mcsat_satellite_arith_eterm(sat, x1), + mcsat_satellite_arith_eterm(sat, x2), + true, null_literal, id); } } @@ -630,7 +764,10 @@ static void mcsat_satellite_assert_disequality(void *solver, thvar_t x1, thvar_t p2 = int_hmap_find(&sat->arith_var_to_term, x2); if (p1 != NULL && p2 != NULL) { src = source_lit_from_hint(sat, hint); - mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, + mcsat_satellite_arith_eterm(sat, x1), + mcsat_satellite_arith_eterm(sat, x2), + false, src, -1); } } @@ -647,92 +784,16 @@ static bool mcsat_satellite_assert_distinct(void *solver, uint32_t n, thvar_t *a for (j=i+1; jarith_var_to_term, a[j]); if (p2 != NULL) { - mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, + mcsat_satellite_arith_eterm(sat, a[i]), + mcsat_satellite_arith_eterm(sat, a[j]), + false, src, -1); } } } return true; } -static bool mcsat_satellite_check_diseq(void *solver, thvar_t x1, thvar_t x2) { - (void) solver; - (void) x1; - (void) x2; - return false; -} - -static bool mcsat_satellite_is_constant(void *solver, thvar_t x) { - (void) solver; - (void) x; - return false; -} - -static void mcsat_satellite_expand_th_expl(void *solver, thvar_t x1, thvar_t x2, void *expl, th_explanation_t *result) { - (void) solver; - (void) x1; - (void) x2; - (void) expl; - (void) result; -} - -static uint32_t mcsat_satellite_reconcile_model(void *solver, uint32_t max_eq) { - (void) solver; - (void) max_eq; - return 0; -} - -static void mcsat_satellite_prepare_model(void *solver) { - (void) solver; -} - -static bool mcsat_satellite_equal_in_model(void *solver, thvar_t x1, thvar_t x2) { - (void) solver; - (void) x1; - (void) x2; - return false; -} - -static void mcsat_satellite_gen_interface_lemma(void *solver, literal_t l, thvar_t x1, thvar_t x2, bool equiv) { - (void) solver; - (void) l; - (void) x1; - (void) x2; - (void) equiv; -} - -static void mcsat_satellite_release_model(void *solver) { - (void) solver; -} - -static ipart_t *mcsat_satellite_build_partition(void *solver) { - (void) solver; - return NULL; -} - -static void mcsat_satellite_release_partition(void *solver, ipart_t *partition) { - (void) solver; - (void) partition; -} - -static void mcsat_satellite_attach_eterm(void *solver, thvar_t x, eterm_t t) { - (void) solver; - (void) x; - (void) t; -} - -static eterm_t mcsat_satellite_eterm_of_var(void *solver, thvar_t x) { - (void) solver; - (void) x; - return null_eterm; -} - -static literal_t mcsat_satellite_select_eq_polarity(void *solver, thvar_t x, thvar_t y, literal_t l) { - (void) solver; - (void) x; - (void) y; - return l; -} - /* * Static interface records. */ @@ -757,23 +818,12 @@ static th_smt_interface_t mcsat_satellite_smt = { NULL, }; -static th_egraph_interface_t mcsat_satellite_eg = { +static arith_observer_interface_t mcsat_satellite_arith_observer = { + (arith_observer_atom_fun_t) mcsat_satellite_observe_atom, + (arith_observer_term_fun_t) mcsat_satellite_observe_arith_term, (assert_eq_fun_t) mcsat_satellite_assert_equality, (assert_diseq_fun_t) mcsat_satellite_assert_disequality, (assert_distinct_fun_t) mcsat_satellite_assert_distinct, - (check_diseq_fun_t) mcsat_satellite_check_diseq, - (is_constant_fun_t) mcsat_satellite_is_constant, - (expand_eq_exp_fun_t) mcsat_satellite_expand_th_expl, - (reconcile_model_fun_t) mcsat_satellite_reconcile_model, - (prepare_model_fun_t) mcsat_satellite_prepare_model, - (equal_in_model_fun_t) mcsat_satellite_equal_in_model, - (gen_inter_lemma_fun_t) mcsat_satellite_gen_interface_lemma, - (release_model_fun_t) mcsat_satellite_release_model, - (build_partition_fun_t) mcsat_satellite_build_partition, - (free_partition_fun_t) mcsat_satellite_release_partition, - (attach_to_var_fun_t) mcsat_satellite_attach_eterm, - (get_eterm_fun_t) mcsat_satellite_eterm_of_var, - (select_eq_polarity_fun_t) mcsat_satellite_select_eq_polarity, }; @@ -884,23 +934,9 @@ th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat) { return &mcsat_satellite_smt; } -th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat) { +arith_observer_interface_t *mcsat_satellite_arith_observer_interface(mcsat_satellite_t *sat) { (void) sat; - return &mcsat_satellite_eg; -} - -int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a) { - uint32_t i; - int32_t code; - - for (i = 0; i < n; i++) { - code = mcsat_satellite_assert_formula(sat, a[i]); - if (code < 0) { - return code; - } - } - - return CTX_NO_ERROR; + return &mcsat_satellite_arith_observer; } /* @@ -1028,7 +1064,7 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c } if (context_supports_pushpop(&sat->mctx)) { - context_push(&sat->mctx); + mcsat_push(sat->mctx.mcsat); pushed = true; } @@ -1078,7 +1114,7 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c if (pushed) { mcsat_cleanup_assumptions(sat->mctx.mcsat); - context_pop(&sat->mctx); + mcsat_pop(sat->mctx.mcsat); } if (result != NULL_TERM) { diff --git a/src/solvers/mcsat_satellite.h b/src/solvers/mcsat_satellite.h index 172f1d3cd..b689b1bde 100644 --- a/src/solvers/mcsat_satellite.h +++ b/src/solvers/mcsat_satellite.h @@ -32,9 +32,7 @@ extern void delete_mcsat_satellite(mcsat_satellite_t *sat); extern th_ctrl_interface_t *mcsat_satellite_ctrl_interface(mcsat_satellite_t *sat); extern th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat); -extern th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat); - -extern int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a); +extern arith_observer_interface_t *mcsat_satellite_arith_observer_interface(mcsat_satellite_t *sat); /* * Register a Boolean atom term tracked by the supplementary MCSAT satellite. diff --git a/tests/api/test_cdclt_mcsat_supplement.c b/tests/api/test_cdclt_mcsat_supplement.c index 22f1f49b4..da6d8d200 100644 --- a/tests/api/test_cdclt_mcsat_supplement.c +++ b/tests/api/test_cdclt_mcsat_supplement.c @@ -82,6 +82,12 @@ static context_t *make_cdclt_context(const char *logic_name) { fail("setting solver-type=dpllt failed"); } + code = yices_set_config(cfg, "mcsat-supplement", "true"); + if (code < 0) { + yices_free_config(cfg); + fail("setting mcsat-supplement=true failed"); + } + code = yices_set_config(cfg, "mode", "push-pop"); if (code < 0) { yices_free_config(cfg); @@ -364,6 +370,27 @@ static void test_division_by_zero_remains_error(void) { yices_free_context(ctx); } +static void test_disabling_required_supplement_is_invalid(void) { + ctx_config_t *cfg; + context_t *ctx; + + cfg = yices_new_config(); + check(cfg != NULL, "yices_new_config failed"); + + check_code(yices_default_config_for_logic(cfg, "QF_NIA"), + "default_config_for_logic(QF_NIA) failed"); + check_code(yices_set_config(cfg, "solver-type", "dpllt"), + "setting solver-type=dpllt failed"); + check_code(yices_set_config(cfg, "mcsat-supplement", "false"), + "setting mcsat-supplement=false failed"); + + ctx = yices_new_context(cfg); + check(ctx == NULL, "expected invalid config when DPLL(T) QF_NIA disables MCSAT supplement"); + check(yices_error_code() == CTX_INVALID_CONFIG, "expected CTX_INVALID_CONFIG"); + + yices_free_config(cfg); +} + int main(void) { if (!yices_has_mcsat()) { return 1; // skipped @@ -377,6 +404,7 @@ int main(void) { test_ff_sat_unsat_model_and_assumption_core(); test_nla_assumption_core(); test_division_by_zero_remains_error(); + test_disabling_required_supplement_is_invalid(); yices_exit(); return 0; diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2 b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2 new file mode 100644 index 000000000..ec19038e2 --- /dev/null +++ b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +(assert (= x 0)) +(assert (= (* x y) 1)) +(check-sat) diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold @@ -0,0 +1 @@ +unsat diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options new file mode 100644 index 000000000..49d45d417 --- /dev/null +++ b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options @@ -0,0 +1 @@ +--dpllt From 85ce0c73655793c22384166af65e90519f5eedc9 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Wed, 20 May 2026 23:42:54 -0700 Subject: [PATCH 5/9] Move MCSAT supplement regression under both Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- tests/regress/{ => both}/mcsat_supplement_qf_nia_unsat.smt2 | 0 tests/regress/{ => both}/mcsat_supplement_qf_nia_unsat.smt2.gold | 0 tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options | 1 - 3 files changed, 1 deletion(-) rename tests/regress/{ => both}/mcsat_supplement_qf_nia_unsat.smt2 (100%) rename tests/regress/{ => both}/mcsat_supplement_qf_nia_unsat.smt2.gold (100%) delete mode 100644 tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2 b/tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2 similarity index 100% rename from tests/regress/mcsat_supplement_qf_nia_unsat.smt2 rename to tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2 diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold b/tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2.gold similarity index 100% rename from tests/regress/mcsat_supplement_qf_nia_unsat.smt2.gold rename to tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2.gold diff --git a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options b/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options deleted file mode 100644 index 49d45d417..000000000 --- a/tests/regress/mcsat_supplement_qf_nia_unsat.smt2.options +++ /dev/null @@ -1 +0,0 @@ ---dpllt From 29722f7fc69a85556da391e2e714d6f6f1925a2d Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Wed, 20 May 2026 23:55:16 -0700 Subject: [PATCH 6/9] Fix MCSAT supplement context cleanup Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- src/api/yices_api.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 8931fda6c..045ea1624 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8904,7 +8904,7 @@ context_t *_o_yices_new_context(const ctx_config_t *config) { context_t* ctx = _o_yices_create_context(logic, arch, mode, iflag, qflag); if (mcsat_supplement && context_attach_mcsat_supplement(ctx) < 0) { delete_context(ctx); - safe_free(ctx); + free_context(ctx); set_error_code(CTX_INVALID_CONFIG); return NULL; } From 596923db3a6699c58cb31bb0965cfaba0a806098 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Thu, 21 May 2026 00:08:04 -0700 Subject: [PATCH 7/9] Add simplex relaxation for MCSAT supplement Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- src/context/context.c | 420 ++++++++++++++++++++++-- src/context/context_types.h | 7 + tests/api/test_cdclt_mcsat_supplement.c | 59 ++++ 3 files changed, 466 insertions(+), 20 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index e90fd1c06..14ab81a78 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -37,7 +37,9 @@ #include "solvers/cdcl/delegate.h" #include "solvers/simplex/simplex.h" #include "terms/poly_buffer_terms.h" +#include "terms/rba_buffer_terms.h" #include "terms/term_explorer.h" +#include "terms/term_manager.h" #include "terms/term_utils.h" #include "utils/int_hash_map.h" #include "utils/memalloc.h" @@ -78,10 +80,16 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t); static thvar_t internalize_to_arith(context_t *ctx, term_t t); static thvar_t internalize_to_bv(context_t *ctx, term_t t); +static literal_t map_arith_eq_to_literal(context_t *ctx, term_t t); +static literal_t map_arith_geq_to_literal(context_t *ctx, term_t t); +static literal_t map_arith_is_int_to_literal(context_t *ctx, term_t t); +static literal_t map_arith_divides_const_to_literal(context_t *ctx, term_t d, term_t t); + static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx); static bool context_atom_requires_mcsat(context_t *ctx, term_t atom); static void context_observe_mcsat_atom(context_t *ctx, term_t atom, literal_t l); static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom); +static void context_reset_mcsat_relaxation(context_t *ctx); static void context_disable_mcsat_supplement(context_t *ctx); @@ -333,6 +341,36 @@ static void context_disable_mcsat_supplement(context_t *ctx) { ctx->mcsat_supplement = false; } +static void context_reset_mcsat_relaxation(context_t *ctx) { + if (ctx->mcsat_relax_abstractions != NULL) { + int_hmap_reset(ctx->mcsat_relax_abstractions); + } + if (ctx->mcsat_relax_abstraction_terms != NULL) { + int_hset_reset(ctx->mcsat_relax_abstraction_terms); + } + if (ctx->mcsat_relax_manager != NULL) { + reset_term_manager(ctx->mcsat_relax_manager); + } +} + +static void context_delete_mcsat_relaxation(context_t *ctx) { + if (ctx->mcsat_relax_abstractions != NULL) { + delete_int_hmap(ctx->mcsat_relax_abstractions); + safe_free(ctx->mcsat_relax_abstractions); + ctx->mcsat_relax_abstractions = NULL; + } + if (ctx->mcsat_relax_abstraction_terms != NULL) { + delete_int_hset(ctx->mcsat_relax_abstraction_terms); + safe_free(ctx->mcsat_relax_abstraction_terms); + ctx->mcsat_relax_abstraction_terms = NULL; + } + if (ctx->mcsat_relax_manager != NULL) { + delete_term_manager(ctx->mcsat_relax_manager); + safe_free(ctx->mcsat_relax_manager); + ctx->mcsat_relax_manager = NULL; + } +} + static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { switch (term_kind(terms, atom)) { case ARITH_ROOT_ATOM: @@ -398,9 +436,329 @@ static void context_observe_mcsat_atom(context_t *ctx, term_t atom, literal_t l) } } +static inline bool context_mcsat_relaxation_enabled(context_t *ctx) { + return ctx->mcsat_supplement && context_has_simplex_solver(ctx); +} + +static term_manager_t *context_get_mcsat_relax_manager(context_t *ctx) { + term_manager_t *manager; + + manager = ctx->mcsat_relax_manager; + if (manager == NULL) { + manager = (term_manager_t *) safe_malloc(sizeof(term_manager_t)); + init_term_manager(manager, ctx->terms); + ctx->mcsat_relax_manager = manager; + } + return manager; +} + +static int_hmap_t *context_get_mcsat_relax_abstractions(context_t *ctx) { + int_hmap_t *map; + + map = ctx->mcsat_relax_abstractions; + if (map == NULL) { + map = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t)); + init_int_hmap(map, 0); + ctx->mcsat_relax_abstractions = map; + } + return map; +} + +static int_hset_t *context_get_mcsat_relax_abstraction_terms(context_t *ctx) { + int_hset_t *set; + + set = ctx->mcsat_relax_abstraction_terms; + if (set == NULL) { + set = (int_hset_t *) safe_malloc(sizeof(int_hset_t)); + init_int_hset(set, 0); + ctx->mcsat_relax_abstraction_terms = set; + } + return set; +} + +static bool context_is_mcsat_relax_abstraction(context_t *ctx, term_t t) { + t = unsigned_term(intern_tbl_get_root(&ctx->intern, t)); + return ctx->mcsat_relax_abstraction_terms != NULL && + int_hset_member(ctx->mcsat_relax_abstraction_terms, t); +} + +static bool term_requires_mcsat_supplement_uncached(context_t *ctx, term_t t) { + int_hmap_t cache; + bool trigger; + + init_int_hmap(&cache, 0); + trigger = term_requires_mcsat_supplement(ctx, t, &cache); + delete_int_hmap(&cache); + + return trigger; +} + +static bool arith_const_is_zero(context_t *ctx, term_t t) { + t = unsigned_term(intern_tbl_get_root(&ctx->intern, t)); + return term_kind(ctx->terms, t) == ARITH_CONSTANT && + q_is_zero(rational_term_desc(ctx->terms, t)); +} + +/* + * Fresh internal arithmetic term used as a simplex relaxation variable. + * The term is intentionally not registered as the original nonlinear term: + * it is a pure over-approximation variable for the simplex view. + * + * This cache maps original nonlinear terms to fresh term-table variables, + * rather than directly to simplex thvars. Internalizing the fresh term gives + * the canonical thvar and keeps the relaxation path in the normal arithmetic + * internalizer. The companion set identifies these fresh terms so observer + * notifications can ignore only relaxation abstractions, not user terms that + * happen to be internalized while building a relaxation. + */ +static term_t mcsat_relax_abstraction_for_term(context_t *ctx, term_t t) { + int_hmap_pair_t *p; + type_t tau; + + t = unsigned_term(intern_tbl_get_root(&ctx->intern, t)); + p = int_hmap_get(context_get_mcsat_relax_abstractions(ctx), t); + if (p->val < 0) { + tau = term_type(ctx->terms, t); + assert(is_arithmetic_type(tau)); + p->val = new_uninterpreted_term(ctx->terms, tau); + int_hset_add(context_get_mcsat_relax_abstraction_terms(ctx), p->val); + } + + return p->val; +} + +static term_t mcsat_relax_arith_term(context_t *ctx, term_manager_t *manager, term_t t); + +static term_t mcsat_relax_pprod(context_t *ctx, term_manager_t *manager, term_t t) { + pprod_t *p; + term_t *a; + term_t r; + uint32_t i, n; + + p = pprod_term_desc(ctx->terms, t); + if (pprod_degree(p) > 1) { + return mcsat_relax_abstraction_for_term(ctx, t); + } + + n = p->len; + a = alloc_istack_array(&ctx->istack, n); + for (i=0; iprod[i].var); + if (r == NULL_TERM) { + free_istack_array(&ctx->istack, a); + return NULL_TERM; + } + a[i] = r; + } + + r = mk_arith_pprod(manager, p, n, a); + free_istack_array(&ctx->istack, a); + + return r; +} + +static term_t mcsat_relax_poly(context_t *ctx, term_manager_t *manager, term_t t) { + polynomial_t *p; + term_t *a; + term_t r; + uint32_t i, n; + + p = poly_term_desc(ctx->terms, t); + n = p->nterms; + a = alloc_istack_array(&ctx->istack, n); + for (i=0; imono[i].var == const_idx) { + a[i] = const_idx; + } else { + r = mcsat_relax_arith_term(ctx, manager, p->mono[i].var); + if (r == NULL_TERM) { + free_istack_array(&ctx->istack, a); + return NULL_TERM; + } + a[i] = r; + } + } + + r = mk_arith_poly(manager, p, n, a); + free_istack_array(&ctx->istack, a); + + return r; +} + +static term_t mcsat_relax_const_division(context_t *ctx, term_manager_t *manager, term_kind_t kind, composite_term_t *d) { + term_t x, y; + + assert(d->arity == 2); + if (arith_const_is_zero(ctx, d->arg[1])) { + // The standard internalizer preserves Yices's literal-zero-divisor error. + // If relaxation reaches one as a side term, leave the atom MCSAT-only. + return NULL_TERM; + } + assert(!divisor_requires_mcsat(ctx->terms, d->arg[1])); + + x = mcsat_relax_arith_term(ctx, manager, d->arg[0]); + if (x == NULL_TERM) { + return NULL_TERM; + } + y = unsigned_term(intern_tbl_get_root(&ctx->intern, d->arg[1])); + + switch (kind) { + case ARITH_RDIV: + return mk_arith_rdiv(manager, x, y); + case ARITH_IDIV: + return mk_arith_idiv(manager, x, y); + case ARITH_MOD: + return mk_arith_mod(manager, x, y); + default: + assert(false); + return NULL_TERM; + } +} + +static term_t mcsat_relax_arith_term(context_t *ctx, term_manager_t *manager, term_t t) { + term_table_t *terms; + composite_term_t *c; + term_t x; + + t = unsigned_term(intern_tbl_get_root(&ctx->intern, t)); + terms = ctx->terms; + assert(is_arithmetic_term(terms, t)); + + switch (term_kind(terms, t)) { + case ARITH_CONSTANT: + case UNINTERPRETED_TERM: + return t; + + case POWER_PRODUCT: + return mcsat_relax_pprod(ctx, manager, t); + + case ARITH_POLY: + return mcsat_relax_poly(ctx, manager, t); + + case ARITH_FLOOR: + x = mcsat_relax_arith_term(ctx, manager, arith_floor_arg(terms, t)); + return x == NULL_TERM ? NULL_TERM : mk_arith_floor(manager, x); + + case ARITH_CEIL: + x = mcsat_relax_arith_term(ctx, manager, arith_ceil_arg(terms, t)); + return x == NULL_TERM ? NULL_TERM : mk_arith_ceil(manager, x); + + case ARITH_ABS: + x = mcsat_relax_arith_term(ctx, manager, arith_abs_arg(terms, t)); + return x == NULL_TERM ? NULL_TERM : mk_arith_abs(manager, x); + + case ARITH_RDIV: + c = arith_rdiv_term_desc(terms, t); + if (divisor_requires_mcsat(terms, c->arg[1])) { + return mcsat_relax_abstraction_for_term(ctx, t); + } + return mcsat_relax_const_division(ctx, manager, ARITH_RDIV, c); + + case ARITH_IDIV: + c = arith_idiv_term_desc(terms, t); + if (divisor_requires_mcsat(terms, c->arg[1])) { + return mcsat_relax_abstraction_for_term(ctx, t); + } + return mcsat_relax_const_division(ctx, manager, ARITH_IDIV, c); + + case ARITH_MOD: + c = arith_mod_term_desc(terms, t); + if (divisor_requires_mcsat(terms, c->arg[1])) { + return mcsat_relax_abstraction_for_term(ctx, t); + } + return mcsat_relax_const_division(ctx, manager, ARITH_MOD, c); + + default: + /* + * For arithmetic constructs supported by simplex, keep the term exact. + * If an unsupported construct occurs below an otherwise opaque term + * (for example under an arithmetic ITE), abstract the whole term. + */ + if (term_requires_mcsat_supplement_uncached(ctx, t)) { + return mcsat_relax_abstraction_for_term(ctx, t); + } + return t; + } +} + +static term_t mcsat_relax_arith_difference(context_t *ctx, term_manager_t *manager, term_t t1, term_t t2) { + rba_buffer_t *b; + + b = term_manager_get_arith_buffer(manager); + reset_rba_buffer(b); + rba_buffer_add_term(b, ctx->terms, t1); + rba_buffer_sub_term(b, ctx->terms, t2); + + return mk_arith_term(manager, b); +} + +static literal_t map_mcsat_relaxation_to_literal(context_t *ctx, term_t atom) { + term_table_t *terms; + term_manager_t *manager; + composite_term_t *eq; + literal_t l; + term_t t, u; + + if (!context_mcsat_relaxation_enabled(ctx)) { + return null_literal; + } + + terms = ctx->terms; + manager = context_get_mcsat_relax_manager(ctx); + l = null_literal; + + switch (term_kind(terms, atom)) { + case ARITH_IS_INT_ATOM: + t = mcsat_relax_arith_term(ctx, manager, arith_is_int_arg(terms, atom)); + if (t != NULL_TERM) { + l = map_arith_is_int_to_literal(ctx, t); + } + break; + + case ARITH_EQ_ATOM: + t = mcsat_relax_arith_term(ctx, manager, arith_eq_arg(terms, atom)); + if (t != NULL_TERM) { + l = map_arith_eq_to_literal(ctx, t); + } + break; + + case ARITH_GE_ATOM: + t = mcsat_relax_arith_term(ctx, manager, arith_ge_arg(terms, atom)); + if (t != NULL_TERM) { + l = map_arith_geq_to_literal(ctx, t); + } + break; + + case ARITH_BINEQ_ATOM: + eq = arith_bineq_atom_desc(terms, atom); + t = mcsat_relax_arith_term(ctx, manager, eq->arg[0]); + u = mcsat_relax_arith_term(ctx, manager, eq->arg[1]); + if (t != NULL_TERM && u != NULL_TERM) { + t = mcsat_relax_arith_difference(ctx, manager, t, u); + l = map_arith_eq_to_literal(ctx, t); + } + break; + + case ARITH_DIVIDES_ATOM: + eq = arith_divides_atom_desc(terms, atom); + if (!divisor_requires_mcsat(terms, eq->arg[0])) { + t = mcsat_relax_arith_term(ctx, manager, eq->arg[1]); + if (t != NULL_TERM) { + l = map_arith_divides_const_to_literal(ctx, eq->arg[0], t); + } + } + break; + + default: + break; + } + + return l; +} + static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { mcsat_satellite_t *sat; - literal_t l; + literal_t l, lr; void *obj; int32_t code; @@ -415,6 +773,15 @@ static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { } attach_atom_to_bvar(ctx->core, var_of(l), tagged_mcsat_atom(obj)); + + lr = map_mcsat_relaxation_to_literal(ctx, atom); + if (lr != null_literal) { + // Scope the equivalence with the two atoms: if a push-level atom is popped, + // its relaxation literal and these clauses disappear with it. + add_binary_clause(ctx->core, not(l), lr); + add_binary_clause(ctx->core, l, not(lr)); + } + return l; } @@ -2744,35 +3111,42 @@ static literal_t map_arith_is_int_to_literal(context_t *ctx, term_t t) { return l; } -// atom (divides k t) we assume k != 0 -static literal_t map_arith_divides_to_literal(context_t *ctx, composite_term_t *divides) { +// atom (divides k t) we assume k != 0 and constant +static literal_t map_arith_divides_const_to_literal(context_t *ctx, term_t d, term_t t) { rational_t k; polynomial_t *p; thvar_t map[2]; thvar_t x, y; - term_t d; literal_t l; - assert(divides->arity == 2); + assert(term_kind(ctx->terms, d) == ARITH_CONSTANT); - d = divides->arg[0]; - if (term_kind(ctx->terms, d) == ARITH_CONSTANT) { - // make a copy of divides->arg[0] in k - q_init(&k); - q_set(&k, rational_term_desc(ctx->terms, d)); - assert(q_is_nonzero(&k)); + // make a copy of the divider in k + q_init(&k); + q_set(&k, rational_term_desc(ctx->terms, d)); + assert(q_is_nonzero(&k)); - x = internalize_to_arith(ctx, divides->arg[1]); // this is t - y = get_div(ctx, x, &k); // y := (div x k) - p = context_get_aux_poly(ctx, 3); - context_store_divides_constraint(p, map, x, y, &k); // p is (- x + k * y) - // atom (x <= k * y) is (p >= 0) - l = ctx->arith.create_poly_ge_atom(ctx->arith_solver, p, map); + x = internalize_to_arith(ctx, t); // this is t + y = get_div(ctx, x, &k); // y := (div x k) + p = context_get_aux_poly(ctx, 3); + context_store_divides_constraint(p, map, x, y, &k); // p is (- x + k * y) + // atom (x <= k * y) is (p >= 0) + l = ctx->arith.create_poly_ge_atom(ctx->arith_solver, p, map); - q_clear(&k); + q_clear(&k); - return l; + return l; +} +// atom (divides k t) we assume k != 0 +static literal_t map_arith_divides_to_literal(context_t *ctx, composite_term_t *divides) { + term_t d; + + assert(divides->arity == 2); + + d = divides->arg[0]; + if (term_kind(ctx->terms, d) == ARITH_CONSTANT) { + return map_arith_divides_const_to_literal(ctx, d, divides->arg[1]); } else { // k is not a constant: not supported longjmp(ctx->env, FORMULA_NOT_LINEAR); @@ -3319,7 +3693,8 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { } - if (ctx->mcsat_supplement && ctx->egraph != NULL) { + if (ctx->mcsat_supplement && ctx->egraph != NULL && + !context_is_mcsat_relax_abstraction(ctx, unsigned_term(r))) { egraph_arith_observer_register_arith_term(ctx->egraph, x, unsigned_term(r)); } @@ -6159,6 +6534,9 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, init_mcsat_options(&ctx->mcsat_options); init_ivector(&ctx->mcsat_var_order, CTX_DEFAULT_VECTOR_SIZE); init_ivector(&ctx->mcsat_initial_var_order, CTX_DEFAULT_VECTOR_SIZE); + ctx->mcsat_relax_abstractions = NULL; + ctx->mcsat_relax_abstraction_terms = NULL; + ctx->mcsat_relax_manager = NULL; /* * Allocate and initialize the solvers and core * NOTE: no theory solver yet if arch is AUTO_IDL or AUTO_RDL @@ -6225,6 +6603,7 @@ void delete_context(context_t *ctx) { /* delete_mcsat_options(&ctx->mcsat_options); // if used then the same memory is freed twice */ delete_ivector(&ctx->mcsat_var_order); delete_ivector(&ctx->mcsat_initial_var_order); + context_delete_mcsat_relaxation(ctx); delete_intern_tbl(&ctx->intern); delete_ivector(&ctx->top_eqs); @@ -6293,6 +6672,7 @@ void reset_context(context_t *ctx) { ivector_reset(&ctx->mcsat_var_order); ivector_reset(&ctx->mcsat_initial_var_order); + context_reset_mcsat_relaxation(ctx); reset_intern_tbl(&ctx->intern); ivector_reset(&ctx->top_eqs); diff --git a/src/context/context_types.h b/src/context/context_types.h index f6cc838de..3d901f364 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -43,8 +43,10 @@ #include "terms/conditionals.h" #include "terms/int_rational_hash_maps.h" #include "terms/poly_buffer.h" +#include "terms/term_manager.h" #include "terms/terms.h" #include "utils/int_bv_sets.h" +#include "utils/int_hash_map.h" #include "utils/int_hash_sets.h" #include "utils/int_queues.h" #include "utils/int_stack.h" @@ -754,6 +756,11 @@ struct context_s { // true when the supplemental MCSAT satellite is configured in CDCL(T) mode bool mcsat_supplement; + + // Phase-2 simplex relaxation for MCSAT-owned arithmetic atoms + int_hmap_t *mcsat_relax_abstractions; // original arithmetic term -> fresh internal arithmetic term + int_hset_t *mcsat_relax_abstraction_terms; // fresh internal arithmetic terms above + term_manager_t *mcsat_relax_manager; // allocated lazily }; diff --git a/tests/api/test_cdclt_mcsat_supplement.c b/tests/api/test_cdclt_mcsat_supplement.c index da6d8d200..e68c974c6 100644 --- a/tests/api/test_cdclt_mcsat_supplement.c +++ b/tests/api/test_cdclt_mcsat_supplement.c @@ -352,6 +352,64 @@ static void test_nla_assumption_core(void) { yices_free_context(ctx); } +static void test_simplex_relaxation_phase2(void) { + context_t *ctx; + term_t x, y, xy, yx; + term_t ge1, le0, xeq0, gt0, xeq2, yeq2, eq4; + smt_status_t stat; + model_t *mdl; + int32_t v32; + + ctx = make_cdclt_context("QF_UFLIA"); + x = yices_new_uninterpreted_term(yices_int_type()); + y = yices_new_uninterpreted_term(yices_int_type()); + xy = yices_mul(x, y); + yx = yices_mul(y, x); + + /* + * The relaxation should canonicalize (* x y) and (* y x) to the same + * internal simplex variable; exact MCSAT remains the final authority. + */ + ge1 = yices_arith_geq_atom(xy, yices_int32(1)); + le0 = yices_arith_leq_atom(yx, yices_int32(0)); + check_code(yices_assert_formula(ctx, ge1), "assert x*y>=1 failed"); + check_code(yices_assert_formula(ctx, le0), "assert y*x<=0 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for canonicalized product relaxation"); + + yices_reset_context(ctx); + + /* + * The linear relaxation is satisfiable here (p_xy > 0 with x = 0), so + * the exact MCSAT satellite must still run after simplex. + */ + xeq0 = yices_arith_eq_atom(x, yices_int32(0)); + gt0 = yices_arith_gt_atom(xy, yices_int32(0)); + check_code(yices_assert_formula(ctx, xeq0), "assert x=0 failed"); + check_code(yices_assert_formula(ctx, gt0), "assert x*y>0 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected exact MCSAT UNSAT after satisfiable relaxation"); + + yices_reset_context(ctx); + + xeq2 = yices_arith_eq_atom(x, yices_int32(2)); + yeq2 = yices_arith_eq_atom(y, yices_int32(2)); + eq4 = yices_arith_eq_atom(xy, yices_int32(4)); + check_code(yices_assert_formula(ctx, xeq2), "assert x=2 failed"); + check_code(yices_assert_formula(ctx, yeq2), "assert y=2 failed"); + check_code(yices_assert_formula(ctx, eq4), "assert x*y=4 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for relaxed product with exact MCSAT model"); + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed for Phase-2 relaxation SAT case"); + check(yices_formula_true_in_model(mdl, eq4) == 1, "model must satisfy exact x*y=4"); + check_code(yices_get_int32_value(mdl, xy, &v32), "model must define exact x*y"); + check(v32 == 4, "model value for exact x*y must be 4"); + yices_free_model(mdl); + + yices_free_context(ctx); +} + static void test_division_by_zero_remains_error(void) { context_t *ctx; term_t r, z, div, f; @@ -403,6 +461,7 @@ int main(void) { test_nonconstant_divisor_and_param_modes(); test_ff_sat_unsat_model_and_assumption_core(); test_nla_assumption_core(); + test_simplex_relaxation_phase2(); test_division_by_zero_remains_error(); test_disabling_required_supplement_is_invalid(); From 8c84b9486a0d6d888af50e1d8d8c547cbd848f4d Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Thu, 21 May 2026 08:14:14 -0700 Subject: [PATCH 8/9] Serialize supplemental MCSAT satellite entry points Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- src/api/yices_api.c | 8 ++++- src/context/context_solver.c | 2 +- src/mt/yices_locks.h | 3 ++ src/mt/yices_locks_posix.c | 17 +++++++++ src/mt/yices_locks_win.c | 7 ++++ src/solvers/mcsat_satellite.c | 66 +++++++++++++++++++++++++++++++---- src/solvers/mcsat_satellite.h | 7 ++++ 7 files changed, 102 insertions(+), 8 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 045ea1624..b4f567158 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -1023,7 +1023,13 @@ static void init_globals(yices_globals_t *glob) { glob->fvars = NULL; #ifdef THREAD_SAFE - create_yices_lock(&(glob->lock)); + /* + * Recursive: the supplemental MCSAT satellite may re-acquire the + * global lock from internalization paths where the outer API call + * already holds it. The satellite also uses this lock to serialize + * embedded MCSAT operations reached from unlocked CDCL(T) search. + */ + create_yices_recursive_lock(&(glob->lock)); #endif } diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 71cd75be8..65ce5c722 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -1447,7 +1447,7 @@ static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t } static smt_status_t check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { - MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_supplement(ctx, params, n, a, error)); + return _o_check_context_with_term_assumptions_supplement(ctx, params, n, a, error); } /* diff --git a/src/mt/yices_locks.h b/src/mt/yices_locks.h index fccc0dbc7..fdb278d71 100644 --- a/src/mt/yices_locks.h +++ b/src/mt/yices_locks.h @@ -40,6 +40,9 @@ typedef pthread_mutex_t yices_lock_t; /* returns 0 on success; -1 on failure (and prints an error message) */ extern int32_t create_yices_lock(yices_lock_t* lock); +/* returns 0 on success; -1 on failure (and prints an error message) */ +extern int32_t create_yices_recursive_lock(yices_lock_t* lock); + /* returns 0 on success; 1 if the lock was already taken; -1 on failure (and prints an error message) */ extern int32_t try_yices_lock(yices_lock_t* lock); diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index 821b809df..c0d98d47c 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -60,6 +60,23 @@ int32_t create_yices_lock(yices_lock_t* lock){ return 0; } +int32_t create_yices_recursive_lock(yices_lock_t* lock){ + pthread_mutexattr_t mta; + + check_thread_api(pthread_mutexattr_init(&mta), + "create_yices_recursive_lock: pthread_mutexattr_init"); + check_thread_api(pthread_mutexattr_settype(&mta, + PTHREAD_MUTEX_RECURSIVE), + "create_yices_recursive_lock: pthread_mutextattr_settype"); + + check_thread_api(pthread_mutex_init(lock, &mta), + "create_yices_recursive_lock: pthread_mutex_init"); + check_thread_api(pthread_mutexattr_destroy(&mta), + "create_yices_recursive_lock: pthread_mutexattr_destroy"); + + return 0; +} + int32_t try_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_trylock(lock); if(retcode){ diff --git a/src/mt/yices_locks_win.c b/src/mt/yices_locks_win.c index ed6065b66..d831d6fd1 100644 --- a/src/mt/yices_locks_win.c +++ b/src/mt/yices_locks_win.c @@ -26,6 +26,13 @@ int32_t create_yices_lock(yices_lock_t* lock){ return 0; } +int32_t create_yices_recursive_lock(yices_lock_t* lock){ + /* + * Windows critical sections are recursive for the owning thread. + */ + return create_yices_lock(lock); +} + int32_t try_yices_lock(yices_lock_t* lock){ if (TryEnterCriticalSection(lock) != 0) { return 0; diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index 5330bc651..50b692637 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -17,6 +17,7 @@ */ #include +#include "api/yices_mutex.h" #include "context/context.h" #include "model/models.h" #include "solvers/egraph/composites.h" @@ -34,6 +35,14 @@ typedef struct mcsat_atom_object_s { uint32_t id; } mcsat_atom_object_t; +static inline void mcsat_satellite_obtain_mutex(void) { + (void) yices_obtain_mutex(); +} + +static inline void mcsat_satellite_release_mutex(void) { + (void) yices_release_mutex(); +} + typedef struct mcsat_atom_entry_s { term_t atom; literal_t lit; @@ -151,8 +160,10 @@ static void mcsat_satellite_prepare_assertion_state(mcsat_satellite_t *sat) { static int32_t mcsat_satellite_assert_formula(mcsat_satellite_t *sat, term_t f) { int32_t code; + mcsat_satellite_obtain_mutex(); mcsat_satellite_prepare_assertion_state(sat); code = mcsat_assert_formulas(sat->mctx.mcsat, 1, &f); + mcsat_satellite_release_mutex(); if (code < 0) { sat->internal_error = code; } @@ -435,12 +446,16 @@ static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bo } } + /* + * Pure MCSAT check-sat is serialized by the global Yices mutex. Do the + * same for the supplemental engine entry point without locking the whole + * CDCL(T) search. + */ + mcsat_satellite_obtain_mutex(); mcsat_clear(sat->mctx.mcsat); mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); status = mcsat_status(sat->mctx.mcsat); - delete_model(&mdl); - sat->cache_valid = false; if (status == YICES_STATUS_SAT) { sat->cache_valid = true; @@ -450,6 +465,9 @@ static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bo status = YICES_STATUS_UNKNOWN; } } + mcsat_satellite_release_mutex(); + + delete_model(&mdl); return status; } @@ -489,8 +507,10 @@ static void mcsat_satellite_sync_base_level(mcsat_satellite_t *sat, uint32_t bas uint32_t i; for (i = 0; i < base_level; i++) { + mcsat_satellite_obtain_mutex(); mcsat_satellite_prepare_assertion_state(sat); mcsat_push(sat->mctx.mcsat); + mcsat_satellite_release_mutex(); ivector_push(&sat->atom_push_mark, sat->num_atoms); sat->push_depth ++; mcsat_satellite_open_level(sat); @@ -563,12 +583,15 @@ static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t mcsat_satellite_extend_eq(sat); } + mcsat_satellite_obtain_mutex(); label = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); atom = eq ? mk_eq(&sat->tm, t1, t2) : mk_neq(&sat->tm, t1, t2); implication = mk_implies(&sat->tm, label, atom); if (mcsat_satellite_assert_formula(sat, implication) < 0) { + mcsat_satellite_release_mutex(); return; } + mcsat_satellite_release_mutex(); sat->eq[sat->num_eq].label = label; sat->eq[sat->num_eq].t1 = t1; @@ -595,9 +618,11 @@ static void mcsat_satellite_start_internalization(void *solver) { static void mcsat_satellite_start_search(void *solver) { mcsat_satellite_t *sat = solver; sat->cache_valid = false; + mcsat_satellite_obtain_mutex(); if (mcsat_status(sat->mctx.mcsat) != YICES_STATUS_IDLE) { mcsat_clear(sat->mctx.mcsat); } + mcsat_satellite_release_mutex(); } static bool mcsat_satellite_propagate(void *solver) { @@ -643,8 +668,10 @@ static void mcsat_satellite_push(void *solver) { * only label-guarded facts into that engine, so bypass the wrapping * context_t push/pop machinery and scope the MCSAT engine directly. */ + mcsat_satellite_obtain_mutex(); mcsat_satellite_prepare_assertion_state(sat); mcsat_push(sat->mctx.mcsat); + mcsat_satellite_release_mutex(); ivector_push(&sat->atom_push_mark, sat->num_atoms); sat->push_depth ++; mcsat_satellite_open_level(sat); @@ -658,7 +685,9 @@ static void mcsat_satellite_pop(void *solver) { assert(sat->push_depth > 0); assert(sat->atom_push_mark.size > 0); + mcsat_satellite_obtain_mutex(); mcsat_pop(sat->mctx.mcsat); + mcsat_satellite_release_mutex(); assert(sat->dlevel > 0); mark = ivector_pop2(&sat->atom_push_mark); @@ -673,7 +702,9 @@ static void mcsat_satellite_reset(void *solver) { mcsat_satellite_t *sat = solver; uint32_t i; + mcsat_satellite_obtain_mutex(); reset_context(&sat->mctx); + mcsat_satellite_release_mutex(); for (i=0; inum_atoms; i++) { if (sat->atoms[i].obj != NULL) { @@ -703,7 +734,9 @@ static void mcsat_satellite_reset(void *solver) { static void mcsat_satellite_clear(void *solver) { mcsat_satellite_t *sat = solver; + mcsat_satellite_obtain_mutex(); context_clear(&sat->mctx); + mcsat_satellite_release_mutex(); sat->cache_valid = false; } @@ -967,20 +1000,24 @@ int32_t mcsat_satellite_register_atom(mcsat_satellite_t *sat, term_t atom, liter mcsat_satellite_extend_atoms(sat); } + mcsat_satellite_obtain_mutex(); plabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); nlabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); implication = mk_implies(&sat->tm, plabel, atom); code = mcsat_satellite_assert_formula(sat, implication); if (code < 0) { + mcsat_satellite_release_mutex(); return code; } implication = mk_implies(&sat->tm, nlabel, not(atom)); code = mcsat_satellite_assert_formula(sat, implication); if (code < 0) { + mcsat_satellite_release_mutex(); return code; } + mcsat_satellite_release_mutex(); atom_obj = NULL; if (obj != NULL) { @@ -1021,15 +1058,25 @@ void mcsat_satellite_set_search_parameters(mcsat_satellite_t *sat, const param_t } void mcsat_satellite_set_trace(mcsat_satellite_t *sat, tracer_t *trace) { + mcsat_satellite_obtain_mutex(); mcsat_set_tracer(sat->mctx.mcsat, trace); + mcsat_satellite_release_mutex(); } term_t mcsat_satellite_get_unsat_model_interpolant(mcsat_satellite_t *sat) { - return mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + term_t t; + + mcsat_satellite_obtain_mutex(); + t = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + mcsat_satellite_release_mutex(); + + return t; } void mcsat_satellite_set_unsat_model_interpolant(mcsat_satellite_t *sat, term_t t) { + mcsat_satellite_obtain_mutex(); mcsat_set_unsat_result_from_labeled_interpolant(sat->mctx.mcsat, t, 0, NULL, NULL); + mcsat_satellite_release_mutex(); } term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, const param_t *params, uint32_t n, const term_t *a) { @@ -1055,6 +1102,8 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c pushed = false; result = NULL_TERM; + mcsat_satellite_obtain_mutex(); + /* * Internal push requires an idle MCSAT state in debug builds. * This path may be called after a previous UNSAT check. @@ -1121,6 +1170,8 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c mcsat_set_unsat_result_from_labeled_interpolant(sat->mctx.mcsat, result, 0, NULL, NULL); } + mcsat_satellite_release_mutex(); + return result; } @@ -1148,15 +1199,16 @@ void mcsat_satellite_build_model(mcsat_satellite_t *sat, model_t *model) { } } + mcsat_satellite_obtain_mutex(); mcsat_clear(sat->mctx.mcsat); mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); status = mcsat_status(sat->mctx.mcsat); - - delete_model(&mdl); - if (status == YICES_STATUS_SAT) { mcsat_build_model(sat->mctx.mcsat, model); } + mcsat_satellite_release_mutex(); + + delete_model(&mdl); } void mcsat_satellite_gc_mark(mcsat_satellite_t *sat) { @@ -1172,5 +1224,7 @@ void mcsat_satellite_gc_mark(mcsat_satellite_t *sat) { term_table_set_gc_mark(sat->mctx.terms, index_of(sat->eq[i].label)); } + mcsat_satellite_obtain_mutex(); mcsat_gc_mark(sat->mctx.mcsat); + mcsat_satellite_release_mutex(); } diff --git a/src/solvers/mcsat_satellite.h b/src/solvers/mcsat_satellite.h index b689b1bde..a19fc62da 100644 --- a/src/solvers/mcsat_satellite.h +++ b/src/solvers/mcsat_satellite.h @@ -27,6 +27,13 @@ typedef struct mcsat_satellite_s mcsat_satellite_t; +/* + * Thread-safety note: the satellite shares the global term table with the + * outer context. In THREAD_SAFE builds, calls into the embedded MCSAT engine + * and satellite-side term construction that can be reached from unlocked + * CDCL(T) search are serialized by the global Yices mutex. + */ + extern mcsat_satellite_t *new_mcsat_satellite(context_t *ctx); extern void delete_mcsat_satellite(mcsat_satellite_t *sat); From cbe97450363188488dc1b5d581b46c5d8d090da5 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Thu, 21 May 2026 12:15:35 -0700 Subject: [PATCH 9/9] Address MCSAT supplement review issues Supported by Codex/GPT5.5 and Windsurf/Opus4.7 --- src/context/context.c | 24 ++++++++++++++++-- src/context/context_solver.c | 4 +++ src/frontend/smt2/smt2_commands.c | 1 - src/mcsat/solver.c | 30 +++++++++++----------- src/solvers/mcsat_satellite.c | 27 ++++++++++++-------- tests/api/test_cdclt_mcsat_supplement.c | 33 +++++++++++++++++++++++++ 6 files changed, 91 insertions(+), 28 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 14ab81a78..756910a58 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -445,6 +445,10 @@ static term_manager_t *context_get_mcsat_relax_manager(context_t *ctx) { manager = ctx->mcsat_relax_manager; if (manager == NULL) { + /* + * Use a private manager over the shared term table so relaxation rewrites + * do not reuse in-flight arithmetic buffers from the main internalizer. + */ manager = (term_manager_t *) safe_malloc(sizeof(term_manager_t)); init_term_manager(manager, ctx->terms); ctx->mcsat_relax_manager = manager; @@ -615,6 +619,11 @@ static term_t mcsat_relax_const_division(context_t *ctx, term_manager_t *manager } } +/* + * Build a simplex over-approximation of t. NULL_TERM means that no sound + * linear relaxation could be built; callers must then leave the atom + * MCSAT-only. + */ static term_t mcsat_relax_arith_term(context_t *ctx, term_manager_t *manager, term_t t) { term_table_t *terms; composite_term_t *c; @@ -750,6 +759,10 @@ static literal_t map_mcsat_relaxation_to_literal(context_t *ctx, term_t atom) { break; default: + /* + * Finite-field and other non-simplex atoms stay MCSAT-only: simplex has + * no useful linear relaxation for them. + */ break; } @@ -776,8 +789,11 @@ static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { lr = map_mcsat_relaxation_to_literal(ctx, atom); if (lr != null_literal) { - // Scope the equivalence with the two atoms: if a push-level atom is popped, - // its relaxation literal and these clauses disappear with it. + /* + * Link the exact MCSAT atom to its simplex relaxation. The clauses are + * added with the atoms that introduce both literals; after pop, the + * literals are no longer reachable from active assertions. + */ add_binary_clause(ctx->core, not(l), lr); add_binary_clause(ctx->core, l, not(lr)); } @@ -5495,6 +5511,10 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { if (context_atom_requires_mcsat(ctx, t)) { l = map_mcsat_atom_to_literal(ctx, t); code = literal2code(l); + /* + * Top-level formulas may already have a placeholder mapping from + * preprocessing, so overwrite it. assert_term only maps unmapped roots. + */ intern_tbl_remap_root(&ctx->intern, t, code); assert_internalization_code(ctx, code, tt); return; diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 65ce5c722..b8deadea7 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -1447,6 +1447,10 @@ static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t } static smt_status_t check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { + /* + * Do not MT_PROTECT the whole CDCL(T) search here. The supplemental MCSAT + * satellite serializes only its embedded MCSAT/term-construction calls. + */ return _o_check_context_with_term_assumptions_supplement(ctx, params, n, a, error); } diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index 4746d9df1..5e04e4b8d 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -2647,7 +2647,6 @@ static void init_smt2_context(smt2_globals_t *g) { if (!g->mcsat && smt2_logic_uses_mcsat_supplement(g, logic)) { code = context_attach_mcsat_supplement(g->ctx); - assert(code == CTX_NO_ERROR); if (code < 0) { print_error("failed to attach the mcsat supplement"); done = true; diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index bf05bc849..3a3a0bb98 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -3264,21 +3264,21 @@ void mcsat_build_model(mcsat_solver_t* mcsat, model_t* model) { mcsat_trace_printf(mcsat->ctx->trace, "\n"); } - // Add to model - { - int_hmap_pair_t *entry = int_hmap_get(&model->map, x_term); - if (entry->val < 0) { - model_map_term(model, x_term, x_value); - } else { - /* - * Supplemental use may overlay values onto a model that already - * contains assignments from other CDCL(T) satellites. - */ - entry->val = x_value; - } - } - } - } + // Add to model + { + int_hmap_pair_t *entry = int_hmap_get(&model->map, x_term); + if (entry->val < 0) { + model_map_term(model, x_term, x_value); + } else { + /* + * Supplemental use may overlay values onto a model that already + * contains assignments from other CDCL(T) satellites. + */ + entry->val = x_value; + } + } + } + } // Let the plugins run add to the model (e.g. UF, division, ...) for (i = 0; i < mcsat->plugins_count; ++ i) { diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index 50b692637..346e8aa5b 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -36,6 +36,11 @@ typedef struct mcsat_atom_object_s { } mcsat_atom_object_t; static inline void mcsat_satellite_obtain_mutex(void) { + /* + * Recursive by construction: some satellite calls are reached from API + * paths that already hold the global lock, while CDCL(T) search reaches + * the same calls without holding it. + */ (void) yices_obtain_mutex(); } @@ -75,6 +80,7 @@ struct mcsat_satellite_s { bool check_in_propagate; int32_t internal_error; + uint32_t internal_error_push_depth; bool cache_valid; uint64_t cache_signature; @@ -166,6 +172,7 @@ static int32_t mcsat_satellite_assert_formula(mcsat_satellite_t *sat, term_t f) mcsat_satellite_release_mutex(); if (code < 0) { sat->internal_error = code; + sat->internal_error_push_depth = sat->push_depth; } return code; } @@ -397,10 +404,6 @@ static bool mcsat_satellite_record_conflict(mcsat_satellite_t *sat) { ok = mcsat_satellite_expand_all_assumptions(sat, &seen_lits); } - if (!ok) { - assert(false && "MCSAT conflict label has no expandable CDCL explanation"); - } - if (ok) { ivector_push(&sat->conflict, null_literal); record_theory_conflict(sat->core, sat->conflict.data); @@ -424,12 +427,7 @@ static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bo value_t vtrue; if (sat->internal_error < 0) { - if (emit_conflict) { - literal_t c[1]; - c[0] = null_literal; - record_theory_conflict(sat->core, c); - } - return YICES_STATUS_UNSAT; + return YICES_STATUS_UNKNOWN; } mcsat_satellite_build_assumptions(sat, false); @@ -686,6 +684,7 @@ static void mcsat_satellite_pop(void *solver) { assert(sat->atom_push_mark.size > 0); mcsat_satellite_obtain_mutex(); + mcsat_satellite_prepare_assertion_state(sat); mcsat_pop(sat->mctx.mcsat); mcsat_satellite_release_mutex(); assert(sat->dlevel > 0); @@ -695,6 +694,10 @@ static void mcsat_satellite_pop(void *solver) { sat->atoms[i].active = false; } sat->push_depth --; + if (sat->internal_error < 0 && sat->internal_error_push_depth > sat->push_depth) { + sat->internal_error = 0; + sat->internal_error_push_depth = 0; + } mcsat_satellite_backtrack_to(sat, sat->dlevel - 1); } @@ -719,6 +722,7 @@ static void mcsat_satellite_reset(void *solver) { sat->dlevel = 0; sat->cache_valid = false; sat->internal_error = 0; + sat->internal_error_push_depth = 0; ivector_reset(&sat->atom_push_mark); reset_pmap2(&sat->eq_active); @@ -738,6 +742,8 @@ static void mcsat_satellite_clear(void *solver) { context_clear(&sat->mctx); mcsat_satellite_release_mutex(); sat->cache_valid = false; + sat->internal_error = 0; + sat->internal_error_push_depth = 0; } /* @@ -884,6 +890,7 @@ mcsat_satellite_t *new_mcsat_satellite(context_t *ctx) { sat->check_in_propagate = true; sat->internal_error = 0; + sat->internal_error_push_depth = 0; sat->cache_valid = false; sat->cache_signature = 0; diff --git a/tests/api/test_cdclt_mcsat_supplement.c b/tests/api/test_cdclt_mcsat_supplement.c index e68c974c6..ca935110f 100644 --- a/tests/api/test_cdclt_mcsat_supplement.c +++ b/tests/api/test_cdclt_mcsat_supplement.c @@ -449,6 +449,38 @@ static void test_disabling_required_supplement_is_invalid(void) { yices_free_config(cfg); } +static void test_reset_reassert_supplement(void) { + context_t *ctx; + term_t x, xx, bad, xeq2, good; + smt_status_t stat; + model_t *mdl; + + ctx = make_cdclt_context("QF_UFLIA"); + x = yices_new_uninterpreted_term(yices_int_type()); + xx = yices_mul(x, x); + + bad = yices_arith_eq_atom(xx, yices_int32(2)); + check_code(yices_assert_formula(ctx, bad), "assert x*x=2 before reset failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for integer x*x=2 before reset"); + + yices_reset_context(ctx); + + xeq2 = yices_arith_eq_atom(x, yices_int32(2)); + good = yices_arith_eq_atom(xx, yices_int32(4)); + check_code(yices_assert_formula(ctx, xeq2), "assert x=2 after reset failed"); + check_code(yices_assert_formula(ctx, good), "assert x*x=4 after reset failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT after reset/reassert"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed after reset/reassert"); + check(yices_formula_true_in_model(mdl, good) == 1, "model must satisfy x*x=4 after reset"); + yices_free_model(mdl); + + yices_free_context(ctx); +} + int main(void) { if (!yices_has_mcsat()) { return 1; // skipped @@ -464,6 +496,7 @@ int main(void) { test_simplex_relaxation_phase2(); test_division_by_zero_remains_error(); test_disabling_required_supplement_is_invalid(); + test_reset_reassert_supplement(); yices_exit(); return 0;