From 78f7f298ec050bbd01793cd5241ee89238254106 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 2 Jul 2026 02:10:11 -0700 Subject: [PATCH 1/4] Add on-demand zero lemmas for MCSAT-supplement nonlinear relaxation Each nonlinear monomial abstracted for simplex (mcsat_relax_pprod) now also gets on-demand "zero lemma" clauses relating the abstraction variable to its factors (z=0 <-> some factor=0), checked against live simplex values from propagate/final_check and gated by the existing mcsat-supplement-check parameter. Atoms are pre-built once at abstraction time (base level), since simplex only supports creating new atoms there, not mid-search; the on-demand check only ever combines those cached literals into new clauses. --- src/context/context.c | 238 +++++++++++++++++++++++++++++++++- src/context/context.h | 8 ++ src/context/context_types.h | 16 +++ src/solvers/mcsat_satellite.c | 9 ++ src/solvers/simplex/simplex.c | 9 ++ src/solvers/simplex/simplex.h | 8 ++ 6 files changed, 283 insertions(+), 5 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 683ae1b93..9afcc5fb7 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -351,6 +351,12 @@ static void context_reset_mcsat_relaxation(context_t *ctx) { if (ctx->mcsat_relax_manager != NULL) { reset_term_manager(ctx->mcsat_relax_manager); } + if (ctx->mcsat_relax_zero_atoms != NULL) { + int_hmap_reset(ctx->mcsat_relax_zero_atoms); + } + if (ctx->mcsat_relax_zero_lemma_done != NULL) { + int_hmap_reset(ctx->mcsat_relax_zero_lemma_done); + } } static void context_delete_mcsat_relaxation(context_t *ctx) { @@ -369,6 +375,16 @@ static void context_delete_mcsat_relaxation(context_t *ctx) { safe_free(ctx->mcsat_relax_manager); ctx->mcsat_relax_manager = NULL; } + if (ctx->mcsat_relax_zero_atoms != NULL) { + delete_int_hmap(ctx->mcsat_relax_zero_atoms); + safe_free(ctx->mcsat_relax_zero_atoms); + ctx->mcsat_relax_zero_atoms = NULL; + } + if (ctx->mcsat_relax_zero_lemma_done != NULL) { + delete_int_hmap(ctx->mcsat_relax_zero_lemma_done); + safe_free(ctx->mcsat_relax_zero_lemma_done); + ctx->mcsat_relax_zero_lemma_done = NULL; + } } static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { @@ -468,6 +484,30 @@ static int_hmap_t *context_get_mcsat_relax_abstractions(context_t *ctx) { return map; } +static int_hmap_t *context_get_mcsat_relax_zero_lemma_done(context_t *ctx) { + int_hmap_t *map; + + map = ctx->mcsat_relax_zero_lemma_done; + if (map == NULL) { + map = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t)); + init_int_hmap(map, 0); + ctx->mcsat_relax_zero_lemma_done = map; + } + return map; +} + +static int_hmap_t *context_get_mcsat_relax_zero_atoms(context_t *ctx) { + int_hmap_t *map; + + map = ctx->mcsat_relax_zero_atoms; + if (map == NULL) { + map = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t)); + init_int_hmap(map, 0); + ctx->mcsat_relax_zero_atoms = map; + } + return map; +} + static int_hset_t *context_get_mcsat_relax_abstraction_terms(context_t *ctx) { int_hset_t *set; @@ -533,15 +573,57 @@ static term_t mcsat_relax_abstraction_for_term(context_t *ctx, term_t t) { static term_t mcsat_relax_arith_term(context_t *ctx, term_manager_t *manager, term_t t); +/* + * Build (if not already cached) and cache the literal for the atom "t = 0". + * This must only be called at the base decision level (e.g. from ordinary + * internalization, as mcsat_relax_pprod does below): building a new theory + * atom is unsafe once the search is past the base level, unlike combining + * already-existing literals into new clauses. Building this atom also + * internalizes t as a side effect, so its value becomes queryable via + * simplex without any separate internalization step. + */ +static literal_t mcsat_relax_cache_zero_atom(context_t *ctx, term_t t) { + int_hmap_pair_t *r; + + r = int_hmap_get(context_get_mcsat_relax_zero_atoms(ctx), t); + if (r->val < 0) { + r->val = map_arith_eq_to_literal(ctx, t); + } + return r->val; +} + +/* + * Pre-build the "z = 0" and "xi = 0" atoms for monomial p (abstracted as z) + * now, at base level (ordinary internalization time), for later on-demand + * zero-lemma checking (context_check_mcsat_relax_zero_lemmas), which runs + * mid-search and may only look up and combine these literals into new + * clauses, never create new atoms. A factor that itself requires MCSAT has + * no sound simplex atom to build here, so it is left untouched + * (context_check_mcsat_relax_zero_lemmas treats a missing cached atom as + * "skip this monomial"). + */ +static void mcsat_relax_setup_zero_lemma_atoms(context_t *ctx, pprod_t *p, term_t z) { + uint32_t i; + + (void) mcsat_relax_cache_zero_atom(ctx, z); + for (i=0; ilen; i++) { + if (!term_requires_mcsat_supplement_uncached(ctx, p->prod[i].var)) { + (void) mcsat_relax_cache_zero_atom(ctx, p->prod[i].var); + } + } +} + 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; + term_t r, z; uint32_t i, n; p = pprod_term_desc(ctx->terms, t); if (pprod_degree(p) > 1) { - return mcsat_relax_abstraction_for_term(ctx, t); + z = mcsat_relax_abstraction_for_term(ctx, t); + mcsat_relax_setup_zero_lemma_atoms(ctx, p, z); + return z; } n = p->len; @@ -3722,9 +3804,153 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { -/*************************************** - * CONVERSION TO BITVECTOR VARIABLES * - **************************************/ +/**************************************************** + * ON-DEMAND ZERO LEMMAS FOR THE MCSAT RELAXATION * + ***************************************************/ + +/* + * thvar_t for term t if t is already internalized to arithmetic, without + * forcing internalization as a side effect of this (read-only) check. + */ +static bool mcsat_relax_term_thvar(context_t *ctx, term_t t, thvar_t *x) { + term_t r; + + r = intern_tbl_get_root(&ctx->intern, t); + if (!intern_tbl_root_is_mapped(&ctx->intern, r)) { + return false; + } + *x = translate_code_to_arith(ctx, intern_tbl_map_of_root(&ctx->intern, r)); + return true; +} + +/* + * Look up (without building) the literal cached by mcsat_relax_cache_zero_atom + * for the atom "t = 0". Read-only: never creates a new atom, which is unsafe + * once the search is past the base level. + */ +static bool mcsat_relax_cached_zero_atom(context_t *ctx, term_t t, literal_t *l) { + int_hmap_pair_t *r; + + if (ctx->mcsat_relax_zero_atoms == NULL) { + return false; + } + r = int_hmap_find(ctx->mcsat_relax_zero_atoms, t); + if (r == NULL) { + return false; + } + *l = r->val; + return true; +} + +/* + * Check monomial (t, z) against the live simplex assignment and add at most + * one zero-lemma clause for it: + * - some factor xi = 0 while z != 0 ==> add not(xi=0) or (z=0) + * - z = 0 while every factor is nonzero ==> add not(z=0) or (x1=0) or ... or (xk=0) + * Returns true if a clause was added. + * + * Only ever combines the literals cached by mcsat_relax_cache_zero_atom + * (built eagerly at base level, see mcsat_relax_pprod) into new clauses; + * it never builds a new atom itself, since that's unsafe mid-search. + * + * Those literals are typically fresh and unassigned, so nothing forces the + * search to change the sampled assignment on its own: without the "done" + * bitmask below, the same violation would be redetected and the same + * clause re-added forever. At most one bit is ever set per call (bits + * 0..n-1 for the forward clauses, bit 30 for the reverse clause), matching + * the one-clause-per-monomial-per-call rule. Once every bit is set, this + * monomial has nothing left to ever contribute and is skipped up front. + */ +static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int_hmap_t *done_map) { + simplex_solver_t *simplex; + pprod_t *p; + thvar_t zx, fxi; + literal_t lz, *lf, *lits; + int_hmap_pair_t *done; + bool z_is_zero, added; + int32_t forward_i, full_mask; + uint32_t i, n; + + p = pprod_term_desc(ctx->terms, t); + n = p->len; + assert(n < 30); + full_mask = ((1 << n) - 1) | (1 << 30); + + done = int_hmap_get(done_map, t); + if (done->val < 0) { + done->val = 0; + } + if ((done->val & full_mask) == full_mask) { + return false; + } + + if (!mcsat_relax_term_thvar(ctx, z, &zx) || !mcsat_relax_cached_zero_atom(ctx, z, &lz)) { + return false; + } + simplex = ctx->arith_solver; + z_is_zero = simplex_var_is_zero_in_assignment(simplex, zx); + + lf = alloc_istack_array(&ctx->istack, n); + added = false; + forward_i = -1; + for (i=0; iprod[i].var, &fxi) || + !mcsat_relax_cached_zero_atom(ctx, p->prod[i].var, lf+i)) { + goto cleanup; + } + if (!z_is_zero && forward_i < 0 && (done->val & (1 << i)) == 0 && + simplex_var_is_zero_in_assignment(simplex, fxi)) { + forward_i = (int32_t) i; + } + } + + if (forward_i >= 0) { + add_binary_clause(ctx->core, not(lf[forward_i]), lz); + done->val |= (1 << forward_i); + added = true; + } else if (z_is_zero && (done->val & (1 << 30)) == 0) { + lits = alloc_istack_array(&ctx->istack, n+1); + lits[0] = not(lz); + for (i=0; icore, n+1, lits); + free_istack_array(&ctx->istack, lits); + done->val |= (1 << 30); + added = true; + } + + cleanup: + free_istack_array(&ctx->istack, lf); + return added; +} + +/* + * Scan every tracked monomial abstraction once and add at most one zero-lemma + * clause per monomial (batched across monomials, capped per monomial so the + * per-round cost stays bounded as more lemma families are layered on later). + * Returns true if at least one clause was added. + */ +bool context_check_mcsat_relax_zero_lemmas(context_t *ctx) { + int_hmap_t *done_map; + int_hmap_pair_t *r; + bool added; + + if (!context_mcsat_relaxation_enabled(ctx) || ctx->mcsat_relax_abstractions == NULL) { + return false; + } + + done_map = context_get_mcsat_relax_zero_lemma_done(ctx); + added = false; + for (r = int_hmap_first_record(ctx->mcsat_relax_abstractions); + r != NULL; + r = int_hmap_next_record(ctx->mcsat_relax_abstractions, r)) { + if (term_kind(ctx->terms, r->key) == POWER_PRODUCT) { + added |= mcsat_relax_check_zero_lemma(ctx, r->key, r->val, done_map); + } + } + return added; +} /* * Translate internalization code x to a bitvector variable @@ -6558,6 +6784,8 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, ctx->mcsat_relax_abstractions = NULL; ctx->mcsat_relax_abstraction_terms = NULL; ctx->mcsat_relax_manager = NULL; + ctx->mcsat_relax_zero_atoms = NULL; + ctx->mcsat_relax_zero_lemma_done = NULL; /* * Allocate and initialize the solvers and core * NOTE: no theory solver yet if arch is AUTO_IDL or AUTO_RDL diff --git a/src/context/context.h b/src/context/context.h index ccecae4d5..1987e119b 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -65,6 +65,14 @@ extern void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, */ extern int32_t context_attach_mcsat_supplement(context_t *ctx); +/* + * Scan the MCSAT-relaxation abstraction variables against the live simplex + * assignment and add on-demand zero lemmas for any violated monomial + * (see context.c). Meant to be called from the MCSAT satellite's + * propagate/final_check hooks. Returns true if at least one clause was added. + */ +extern bool context_check_mcsat_relax_zero_lemmas(context_t *ctx); + /* * Deletion diff --git a/src/context/context_types.h b/src/context/context_types.h index 9fce2be1e..8eb2b84e2 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -764,6 +764,22 @@ struct context_s { 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 + + // term (a monomial's abstraction variable, or one of its factors) -> the + // literal for the atom "term = 0". Built eagerly, at base level, when the + // monomial is abstracted (mcsat_relax_pprod) -- new theory atoms cannot be + // created later mid-search (simplex only allows atom creation at the base + // decision level), so on-demand zero-lemma checking may only look up and + // combine these pre-existing literals into new clauses, never create atoms. + int_hmap_t *mcsat_relax_zero_atoms; + + // monomial term -> bitmask of which on-demand zero-lemma clauses were + // already added for it (bit i: factor i's forward clause; top bit: the + // reverse clause). Needed because the literals these clauses are built + // from are typically fresh and unassigned, so nothing forces the search + // to move on: without this, the same violation would be redetected and + // the same clause re-added on every subsequent propagate/final_check call. + int_hmap_t *mcsat_relax_zero_lemma_done; }; diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index 6cf7ad6e3..7c50023bf 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -632,6 +632,11 @@ static bool mcsat_satellite_propagate(void *solver) { return true; } + if (context_check_mcsat_relax_zero_lemmas(sat->ctx)) { + // lemma(s) queued; let the core re-propagate before the (expensive) exact check + return true; + } + status = mcsat_satellite_check(sat, false, true); return status != YICES_STATUS_UNSAT; } @@ -640,6 +645,10 @@ static fcheck_code_t mcsat_satellite_final_check(void *solver) { mcsat_satellite_t *sat = solver; smt_status_t status; + if (context_check_mcsat_relax_zero_lemmas(sat->ctx)) { + return FCHECK_CONTINUE; + } + status = mcsat_satellite_check(sat, false, true); switch (status) { case YICES_STATUS_UNSAT: diff --git a/src/solvers/simplex/simplex.c b/src/solvers/simplex/simplex.c index 4a5c4aeee..f952068ca 100644 --- a/src/solvers/simplex/simplex.c +++ b/src/solvers/simplex/simplex.c @@ -12673,6 +12673,15 @@ bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, rational_t *v) } +/* + * Check whether x is 0 in the solver's current (mid-search) candidate + * assignment, without requiring a built model. + */ +bool simplex_var_is_zero_in_assignment(simplex_solver_t *solver, thvar_t x) { + return xq_is_zero(arith_var_value(&solver->vtbl, x)); +} + + /* * Get the type of variable x diff --git a/src/solvers/simplex/simplex.h b/src/solvers/simplex/simplex.h index 9a9d4be81..c6345da40 100644 --- a/src/solvers/simplex/simplex.h +++ b/src/solvers/simplex/simplex.h @@ -399,6 +399,14 @@ extern bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, rational extern void simplex_free_model(simplex_solver_t *solver); +/* + * Check whether x is assigned the value 0 in the solver's current + * (possibly partial, mid-search) candidate assignment. + * - unlike simplex_value_in_model, this does not require simplex_build_model + */ +extern bool simplex_var_is_zero_in_assignment(simplex_solver_t *solver, thvar_t x); + + /********************* * GET STATISTICS * From 057204446135873c20b5e3abce2aaa5ac4ba795c Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 2 Jul 2026 02:19:51 -0700 Subject: [PATCH 2/4] Gate reverse zero-lemma clause on all factors being nonzero The reverse clause (z=0 -> some factor=0) was firing whenever z=0 alone, without checking the factors, which is sound (the clause is a tautology) but looser than intended. Only fire it when z=0 and every factor is confirmed nonzero, matching the documented precondition. --- src/context/context.c | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 9afcc5fb7..2157e6d7f 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -3867,7 +3867,7 @@ static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int thvar_t zx, fxi; literal_t lz, *lf, *lits; int_hmap_pair_t *done; - bool z_is_zero, added; + bool z_is_zero, some_factor_zero, added; int32_t forward_i, full_mask; uint32_t i, n; @@ -3893,14 +3893,17 @@ static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int lf = alloc_istack_array(&ctx->istack, n); added = false; forward_i = -1; + some_factor_zero = false; for (i=0; iprod[i].var, &fxi) || !mcsat_relax_cached_zero_atom(ctx, p->prod[i].var, lf+i)) { goto cleanup; } - if (!z_is_zero && forward_i < 0 && (done->val & (1 << i)) == 0 && - simplex_var_is_zero_in_assignment(simplex, fxi)) { - forward_i = (int32_t) i; + if (simplex_var_is_zero_in_assignment(simplex, fxi)) { + if (!z_is_zero && forward_i < 0 && (done->val & (1 << i)) == 0) { + forward_i = (int32_t) i; + } + some_factor_zero = true; } } @@ -3908,7 +3911,7 @@ static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int add_binary_clause(ctx->core, not(lf[forward_i]), lz); done->val |= (1 << forward_i); added = true; - } else if (z_is_zero && (done->val & (1 << 30)) == 0) { + } else if (z_is_zero && !some_factor_zero && (done->val & (1 << 30)) == 0) { lits = alloc_istack_array(&ctx->istack, n+1); lits[0] = not(lz); for (i=0; i Date: Thu, 2 Jul 2026 02:32:46 -0700 Subject: [PATCH 3/4] Move on-demand zero-lemma checking into context_mcsat_relax.c Split the mid-search checking logic (mcsat_relax_check_zero_lemma, context_check_mcsat_relax_zero_lemmas) out of context.c into its own file, following the existing context_solver.c/context_simplifier.c pattern of sharing context_t internals via context_utils.h. Only the atom/monomial construction logic (mcsat_relax_pprod and friends) stays in context.c, since it's tightly coupled to the rest of the internalization pass there. Required exposing three previously-static context.c helpers via context_utils.h: context_mcsat_relaxation_enabled, context_get_mcsat_relax_zero_lemma_done, translate_code_to_arith. --- src/Makefile | 1 + src/context/context.c | 157 +----------------------- src/context/context_mcsat_relax.c | 194 ++++++++++++++++++++++++++++++ src/context/context_utils.h | 26 ++++ 4 files changed, 224 insertions(+), 154 deletions(-) create mode 100644 src/context/context_mcsat_relax.c diff --git a/src/Makefile b/src/Makefile index bf26361f5..dac7456c1 100644 --- a/src/Makefile +++ b/src/Makefile @@ -113,6 +113,7 @@ core_src_c := \ context/common_conjuncts.c \ context/conditional_definitions.c \ context/context.c \ + context/context_mcsat_relax.c \ context/context_simplifier.c \ context/context_solver.c \ context/context_statistics.c \ diff --git a/src/context/context.c b/src/context/context.c index 2157e6d7f..929235a23 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -452,7 +452,7 @@ 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) { +bool context_mcsat_relaxation_enabled(context_t *ctx) { return ctx->mcsat_supplement && context_has_simplex_solver(ctx); } @@ -484,7 +484,7 @@ static int_hmap_t *context_get_mcsat_relax_abstractions(context_t *ctx) { return map; } -static int_hmap_t *context_get_mcsat_relax_zero_lemma_done(context_t *ctx) { +int_hmap_t *context_get_mcsat_relax_zero_lemma_done(context_t *ctx) { int_hmap_t *map; map = ctx->mcsat_relax_zero_lemma_done; @@ -3647,7 +3647,7 @@ static occ_t internalize_to_eterm(context_t *ctx, term_t t) { * - otherwise, x must be the code of an arithmetic variable v, * we return v. */ -static thvar_t translate_code_to_arith(context_t *ctx, int32_t x) { +thvar_t translate_code_to_arith(context_t *ctx, int32_t x) { eterm_t u; thvar_t v; @@ -3804,157 +3804,6 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { -/**************************************************** - * ON-DEMAND ZERO LEMMAS FOR THE MCSAT RELAXATION * - ***************************************************/ - -/* - * thvar_t for term t if t is already internalized to arithmetic, without - * forcing internalization as a side effect of this (read-only) check. - */ -static bool mcsat_relax_term_thvar(context_t *ctx, term_t t, thvar_t *x) { - term_t r; - - r = intern_tbl_get_root(&ctx->intern, t); - if (!intern_tbl_root_is_mapped(&ctx->intern, r)) { - return false; - } - *x = translate_code_to_arith(ctx, intern_tbl_map_of_root(&ctx->intern, r)); - return true; -} - -/* - * Look up (without building) the literal cached by mcsat_relax_cache_zero_atom - * for the atom "t = 0". Read-only: never creates a new atom, which is unsafe - * once the search is past the base level. - */ -static bool mcsat_relax_cached_zero_atom(context_t *ctx, term_t t, literal_t *l) { - int_hmap_pair_t *r; - - if (ctx->mcsat_relax_zero_atoms == NULL) { - return false; - } - r = int_hmap_find(ctx->mcsat_relax_zero_atoms, t); - if (r == NULL) { - return false; - } - *l = r->val; - return true; -} - -/* - * Check monomial (t, z) against the live simplex assignment and add at most - * one zero-lemma clause for it: - * - some factor xi = 0 while z != 0 ==> add not(xi=0) or (z=0) - * - z = 0 while every factor is nonzero ==> add not(z=0) or (x1=0) or ... or (xk=0) - * Returns true if a clause was added. - * - * Only ever combines the literals cached by mcsat_relax_cache_zero_atom - * (built eagerly at base level, see mcsat_relax_pprod) into new clauses; - * it never builds a new atom itself, since that's unsafe mid-search. - * - * Those literals are typically fresh and unassigned, so nothing forces the - * search to change the sampled assignment on its own: without the "done" - * bitmask below, the same violation would be redetected and the same - * clause re-added forever. At most one bit is ever set per call (bits - * 0..n-1 for the forward clauses, bit 30 for the reverse clause), matching - * the one-clause-per-monomial-per-call rule. Once every bit is set, this - * monomial has nothing left to ever contribute and is skipped up front. - */ -static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int_hmap_t *done_map) { - simplex_solver_t *simplex; - pprod_t *p; - thvar_t zx, fxi; - literal_t lz, *lf, *lits; - int_hmap_pair_t *done; - bool z_is_zero, some_factor_zero, added; - int32_t forward_i, full_mask; - uint32_t i, n; - - p = pprod_term_desc(ctx->terms, t); - n = p->len; - assert(n < 30); - full_mask = ((1 << n) - 1) | (1 << 30); - - done = int_hmap_get(done_map, t); - if (done->val < 0) { - done->val = 0; - } - if ((done->val & full_mask) == full_mask) { - return false; - } - - if (!mcsat_relax_term_thvar(ctx, z, &zx) || !mcsat_relax_cached_zero_atom(ctx, z, &lz)) { - return false; - } - simplex = ctx->arith_solver; - z_is_zero = simplex_var_is_zero_in_assignment(simplex, zx); - - lf = alloc_istack_array(&ctx->istack, n); - added = false; - forward_i = -1; - some_factor_zero = false; - for (i=0; iprod[i].var, &fxi) || - !mcsat_relax_cached_zero_atom(ctx, p->prod[i].var, lf+i)) { - goto cleanup; - } - if (simplex_var_is_zero_in_assignment(simplex, fxi)) { - if (!z_is_zero && forward_i < 0 && (done->val & (1 << i)) == 0) { - forward_i = (int32_t) i; - } - some_factor_zero = true; - } - } - - if (forward_i >= 0) { - add_binary_clause(ctx->core, not(lf[forward_i]), lz); - done->val |= (1 << forward_i); - added = true; - } else if (z_is_zero && !some_factor_zero && (done->val & (1 << 30)) == 0) { - lits = alloc_istack_array(&ctx->istack, n+1); - lits[0] = not(lz); - for (i=0; icore, n+1, lits); - free_istack_array(&ctx->istack, lits); - done->val |= (1 << 30); - added = true; - } - - cleanup: - free_istack_array(&ctx->istack, lf); - return added; -} - -/* - * Scan every tracked monomial abstraction once and add at most one zero-lemma - * clause per monomial (batched across monomials, capped per monomial so the - * per-round cost stays bounded as more lemma families are layered on later). - * Returns true if at least one clause was added. - */ -bool context_check_mcsat_relax_zero_lemmas(context_t *ctx) { - int_hmap_t *done_map; - int_hmap_pair_t *r; - bool added; - - if (!context_mcsat_relaxation_enabled(ctx) || ctx->mcsat_relax_abstractions == NULL) { - return false; - } - - done_map = context_get_mcsat_relax_zero_lemma_done(ctx); - added = false; - for (r = int_hmap_first_record(ctx->mcsat_relax_abstractions); - r != NULL; - r = int_hmap_next_record(ctx->mcsat_relax_abstractions, r)) { - if (term_kind(ctx->terms, r->key) == POWER_PRODUCT) { - added |= mcsat_relax_check_zero_lemma(ctx, r->key, r->val, done_map); - } - } - return added; -} - /* * Translate internalization code x to a bitvector variable * - if x is for an egraph term u, then we return the theory variable diff --git a/src/context/context_mcsat_relax.c b/src/context/context_mcsat_relax.c new file mode 100644 index 000000000..7ccbfbbdd --- /dev/null +++ b/src/context/context_mcsat_relax.c @@ -0,0 +1,194 @@ +/* + * 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 . + */ + +/* + * ON-DEMAND ZERO LEMMAS FOR THE MCSAT RELAXATION + * + * context.c's mcsat_relax_pprod abstracts each nonlinear monomial + * x1^e1*...*xk^ek into a fresh simplex variable z, and (at that same, base- + * level point) pre-builds and caches the literals for the atoms "z = 0" and + * "xi = 0" for each factor -- new theory atoms cannot be created later + * mid-search (simplex only allows atom creation at the base decision + * level), so this module may only look up and combine those pre-existing + * literals into new clauses, never create atoms itself. + * + * The zero lemma is z = 0 <-> exists i. xi = 0, split into the clauses: + * - some factor xi = 0 while z != 0 ==> not(xi=0) or (z=0) + * - z = 0 while every factor is nonzero ==> not(z=0) or (x1=0) or ... or (xk=0) + * At most one such clause is added per monomial per call, checked against + * the live simplex assignment from the MCSAT satellite's propagate and + * final_check hooks. + */ + +#include + +#include "context/context_utils.h" +#include "solvers/cdcl/smt_core.h" +#include "solvers/simplex/simplex.h" +#include "terms/power_products.h" +#include "terms/terms.h" +#include "utils/int_hash_map.h" +#include "utils/int_stack.h" + +/* + * thvar_t for term t if t is already internalized to arithmetic, without + * forcing internalization as a side effect of this (read-only) check. + */ +static bool mcsat_relax_term_thvar(context_t *ctx, term_t t, thvar_t *x) { + term_t r; + + r = intern_tbl_get_root(&ctx->intern, t); + if (!intern_tbl_root_is_mapped(&ctx->intern, r)) { + return false; + } + *x = translate_code_to_arith(ctx, intern_tbl_map_of_root(&ctx->intern, r)); + return true; +} + +/* + * Look up (without building) the literal cached by mcsat_relax_cache_zero_atom + * (context.c) for the atom "t = 0". Read-only: never creates a new atom, + * which is unsafe once the search is past the base level. + */ +static bool mcsat_relax_cached_zero_atom(context_t *ctx, term_t t, literal_t *l) { + int_hmap_pair_t *r; + + if (ctx->mcsat_relax_zero_atoms == NULL) { + return false; + } + r = int_hmap_find(ctx->mcsat_relax_zero_atoms, t); + if (r == NULL) { + return false; + } + *l = r->val; + return true; +} + +/* + * Check monomial (t, z) against the live simplex assignment and add at most + * one zero-lemma clause for it: + * - some factor xi = 0 while z != 0 ==> add not(xi=0) or (z=0) + * - z = 0 while every factor is nonzero ==> add not(z=0) or (x1=0) or ... or (xk=0) + * Returns true if a clause was added. + * + * Only ever combines the literals cached by mcsat_relax_cache_zero_atom + * (built eagerly at base level, see mcsat_relax_pprod in context.c) into + * new clauses; it never builds a new atom itself, since that's unsafe + * mid-search. + * + * Those literals are typically fresh and unassigned, so nothing forces the + * search to change the sampled assignment on its own: without the "done" + * bitmask below, the same violation would be redetected and the same + * clause re-added forever. At most one bit is ever set per call (bits + * 0..n-1 for the forward clauses, bit 30 for the reverse clause), matching + * the one-clause-per-monomial-per-call rule. Once every bit is set, this + * monomial has nothing left to ever contribute and is skipped up front. + */ +static bool mcsat_relax_check_zero_lemma(context_t *ctx, term_t t, term_t z, int_hmap_t *done_map) { + simplex_solver_t *simplex; + pprod_t *p; + thvar_t zx, fxi; + literal_t lz, *lf, *lits; + int_hmap_pair_t *done; + bool z_is_zero, some_factor_zero, added; + int32_t forward_i, full_mask; + uint32_t i, n; + + p = pprod_term_desc(ctx->terms, t); + n = p->len; + assert(n < 30); + full_mask = ((1 << n) - 1) | (1 << 30); + + done = int_hmap_get(done_map, t); + if (done->val < 0) { + done->val = 0; + } + if ((done->val & full_mask) == full_mask) { + return false; + } + + if (!mcsat_relax_term_thvar(ctx, z, &zx) || !mcsat_relax_cached_zero_atom(ctx, z, &lz)) { + return false; + } + simplex = ctx->arith_solver; + z_is_zero = simplex_var_is_zero_in_assignment(simplex, zx); + + lf = alloc_istack_array(&ctx->istack, n); + added = false; + forward_i = -1; + some_factor_zero = false; + for (i=0; iprod[i].var, &fxi) || + !mcsat_relax_cached_zero_atom(ctx, p->prod[i].var, lf+i)) { + goto cleanup; + } + if (simplex_var_is_zero_in_assignment(simplex, fxi)) { + if (!z_is_zero && forward_i < 0 && (done->val & (1 << i)) == 0) { + forward_i = (int32_t) i; + } + some_factor_zero = true; + } + } + + if (forward_i >= 0) { + add_binary_clause(ctx->core, not(lf[forward_i]), lz); + done->val |= (1 << forward_i); + added = true; + } else if (z_is_zero && !some_factor_zero && (done->val & (1 << 30)) == 0) { + lits = alloc_istack_array(&ctx->istack, n+1); + lits[0] = not(lz); + for (i=0; icore, n+1, lits); + free_istack_array(&ctx->istack, lits); + done->val |= (1 << 30); + added = true; + } + + cleanup: + free_istack_array(&ctx->istack, lf); + return added; +} + +/* + * Scan every tracked monomial abstraction once and add at most one zero-lemma + * clause per monomial (batched across monomials, capped per monomial so the + * per-round cost stays bounded as more lemma families are layered on later). + * Returns true if at least one clause was added. + */ +bool context_check_mcsat_relax_zero_lemmas(context_t *ctx) { + int_hmap_t *done_map; + int_hmap_pair_t *r; + bool added; + + if (!context_mcsat_relaxation_enabled(ctx) || ctx->mcsat_relax_abstractions == NULL) { + return false; + } + + done_map = context_get_mcsat_relax_zero_lemma_done(ctx); + added = false; + for (r = int_hmap_first_record(ctx->mcsat_relax_abstractions); + r != NULL; + r = int_hmap_next_record(ctx->mcsat_relax_abstractions, r)) { + if (term_kind(ctx->terms, r->key) == POWER_PRODUCT) { + added |= mcsat_relax_check_zero_lemma(ctx, r->key, r->val, done_map); + } + } + return added; +} diff --git a/src/context/context_utils.h b/src/context/context_utils.h index 21adc5140..35cdfaa77 100644 --- a/src/context/context_utils.h +++ b/src/context/context_utils.h @@ -709,4 +709,30 @@ static inline bool context_quant_enabled(context_t *ctx) { } +/* + * MCSAT relaxation internals, shared with context_mcsat_relax.c + */ + +/* + * True if the mcsat-supplement linear relaxation (mcsat_relax_pprod & co., + * in context.c) is active for this context. + */ +extern bool context_mcsat_relaxation_enabled(context_t *ctx); + +/* + * Return ctx->mcsat_relax_zero_lemma_done. Allocate and initialize it if + * necessary. See context_types.h for what this map tracks. + */ +extern int_hmap_t *context_get_mcsat_relax_zero_lemma_done(context_t *ctx); + +/* + * Translate internalization code x to an arithmetic variable + * - if the code is for an egraph term u, then we return the + * theory variable attached to u in the egraph. + * - otherwise, x must be the code of an arithmetic variable v, + * we return v. + */ +extern thvar_t translate_code_to_arith(context_t *ctx, int32_t x); + + #endif /* __CONTEXT_UTILS_H */ From 76bf5724a663a13b1f4beef3a9f198fa0113dfee Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 2 Jul 2026 03:14:45 -0700 Subject: [PATCH 4/4] Restore CONVERSION TO BITVECTOR VARIABLES section banner Collateral damage from an earlier edit that used this comment's text as an anchor and never restored it. --- src/context/context.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/context/context.c b/src/context/context.c index 929235a23..4d1451a24 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -3804,6 +3804,10 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { +/*************************************** + * CONVERSION TO BITVECTOR VARIABLES * + **************************************/ + /* * Translate internalization code x to a bitvector variable * - if x is for an egraph term u, then we return the theory variable