mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-24 19:14:00 +00:00
Code Activity

preserve the initial state of the solver with push/pop for multiple objectives (#8264)

Browse source 
* preserve the initial state of the solver with push/pop for multiple objectives

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Fix memory corruption in Z3_polynomial_subresultants

The API function had a memory corruption bug where allocating the result
vector while the default_expr2polynomial converter was still in scope
could corrupt the converter's internal expr2var mapping.

Fixed by restructuring the code to:
1. Complete all polynomial computation in a scoped block
2. Store results in a temporary expr_ref_vector
3. Let the converter go out of scope
4. Then allocate and populate the result vector

Also improved the test to:
- Use randomized testing with 20 iterations
- Test both cases: variable in polynomials and variable not in polynomials
- Use proper reference counting (inc_ref before dec_ref)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
Lev Nachmanson 2026-01-23 08:41:03 -10:00 • committed by GitHub
parent 2a5bfb818b
commit c0583b828d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 107 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/api/api_polynomial.cpp
View file

@ -33,34 +33,48 @@ extern "C" {
LOG_Z3_polynomial_subresultants(c, p, q, x);
RESET_ERROR_CODE();
polynomial::manager & pm = mk_c(c)->pm();
polynomial_ref _p(pm), _q(pm);
polynomial::scoped_numeral d(pm.m());
default_expr2polynomial converter(mk_c(c)->m(), pm);
if (!converter.to_polynomial(to_expr(p), _p, d) ||
!converter.to_polynomial(to_expr(q), _q, d)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return nullptr;
// Compute all polynomial results BEFORE allocating the result vector.
// This avoids a memory corruption issue where allocating API objects
// can interfere with the converter's internal state.
expr_ref_vector results(mk_c(c)->m());
{
polynomial_ref _p(pm), _q(pm);
polynomial::scoped_numeral d(pm.m());
default_expr2polynomial converter(mk_c(c)->m(), pm);
if (!converter.to_polynomial(to_expr(p), _p, d) ||
!converter.to_polynomial(to_expr(q), _q, d)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return nullptr;
}
if (converter.is_var(to_expr(x))) {
expr2var const & mapping = converter.get_mapping();
unsigned v_x = mapping.to_var(to_expr(x));
if (v_x != UINT_MAX) {
polynomial_ref_vector rs(pm);
polynomial_ref r(pm);
expr_ref _r(mk_c(c)->m());
{
cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
pm.psc_chain(_p, _q, v_x, rs);
}
for (unsigned i = 0; i < rs.size(); ++i) {
r = rs.get(i);
converter.to_expr(r, true, _r);
results.push_back(_r);
}
}
}
}
// Converter is now out of scope - safe to allocate result vector
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(result);
if (converter.is_var(to_expr(x))) {
expr2var const & mapping = converter.get_mapping();
unsigned v_x = mapping.to_var(to_expr(x));
polynomial_ref_vector rs(pm);
polynomial_ref r(pm);
expr_ref _r(mk_c(c)->m());
{
cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
pm.psc_chain(_p, _q, v_x, rs);
}
for (unsigned i = 0; i < rs.size(); ++i) {
r = rs.get(i);
converter.to_expr(r, true, _r);
result->m_ast_vector.push_back(_r);
}
for (expr* e : results) {
result->m_ast_vector.push_back(e);
}
RETURN_Z3(of_ast_vector(result));
Z3_CATCH_RETURN(nullptr);

23
src/opt/opt_solver.cpp
View file

@ -202,8 +202,29 @@ namespace opt {
bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
expr_ref blocker(m);
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
if (!maximize_objective(i, blocker))
// Push context to isolate each objective's optimization.
// This prevents bounds created during one objective's optimization
// from affecting subsequent objectives (fixes issue #7677).
m_context.push();
if (!maximize_objective(i, blocker)) {
m_context.pop(1);
return false;
}
// Save results before popping
inf_eps val = m_objective_values[i];
model_ref mdl;
if (m_models[i])
mdl = m_models[i];
m_context.pop(1);
// Restore the computed values after pop
m_objective_values[i] = val;
if (mdl)
m_models.set(i, mdl.get());
blockers.push_back(blocker);
}
return true;

60
src/test/api_polynomial.cpp
View file

@ -19,31 +19,63 @@ Notes:
#include "api/z3.h"
#include "util/trace.h"
#include "util/debug.h"
#include <random>
static void run_single_test(int seed) {
std::mt19937 gen(seed);
std::uniform_int_distribution<> var_choice(0, 2);
void tst_api_polynomial() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
// Create real sort and simple variables
Z3_sort real_sort = Z3_mk_real_sort(ctx);
// Create variables
Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
Z3_symbol y_sym = Z3_mk_string_symbol(ctx, "y");
Z3_symbol z_sym = Z3_mk_string_symbol(ctx, "z");
Z3_ast x = Z3_mk_const(ctx, x_sym, real_sort);
Z3_ast y = Z3_mk_const(ctx, y_sym, real_sort);
Z3_ast z = Z3_mk_const(ctx, z_sym, real_sort);
// Constants
Z3_ast one = Z3_mk_real(ctx, 1, 1);
Z3_ast two = Z3_mk_real(ctx, 2, 1);
// Test Z3_polynomial_subresultants - just try to call it
try {
Z3_ast_vector result = Z3_polynomial_subresultants(ctx, one, two, x);
// If we get here, function executed without major crash
if (result) {
Z3_ast_vector_dec_ref(ctx, result);
}
ENSURE(true); // Test succeeded in calling the function
} catch (...) {
// Even if there's an exception, we tested the function
ENSURE(true);
// Create polynomials: p = x + 1, q = x + 2
Z3_ast add_args1[2] = {x, one};
Z3_ast p = Z3_mk_add(ctx, 2, add_args1);
Z3_ast add_args2[2] = {x, two};
Z3_ast q = Z3_mk_add(ctx, 2, add_args2);
// Choose which variable to use for subresultant
Z3_ast var;
int choice = var_choice(gen);
switch (choice) {
case 0: var = x; break; // x is in the polynomials
case 1: var = y; break; // y is NOT in the polynomials
default: var = z; break; // z is NOT in the polynomials
}
Z3_ast_vector result = Z3_polynomial_subresultants(ctx, p, q, var);
ENSURE(result != nullptr);
Z3_ast_vector_inc_ref(ctx, result); // Take ownership
unsigned size = Z3_ast_vector_size(ctx, result);
// If var is x (in polynomials), expect 1 result; otherwise 0
if (choice == 0) {
ENSURE(size == 1);
} else {
ENSURE(size == 0);
}
Z3_ast_vector_dec_ref(ctx, result); // Release ownership
Z3_del_context(ctx);
}
}
void tst_api_polynomial() {
// Run multiple tests with fresh contexts
for (int i = 0; i < 20; i++) {
run_single_test(i);
}
}