mirror of
https://github.com/Z3Prover/z3
synced 2026-02-14 21:01:49 +00:00
c0583b828d
* 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>
83 lines
2.7 KiB
C++
83 lines
2.7 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
api_polynomial.cpp
|
|
|
|
Abstract:
|
|
|
|
Polynomial manager and caches for the external API.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2012-12-08
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#include "api/z3.h"
|
|
#include "api/api_log_macros.h"
|
|
#include "api/api_context.h"
|
|
#include "api/api_polynomial.h"
|
|
#include "api/api_ast_vector.h"
|
|
#include "ast/expr2polynomial.h"
|
|
#include "util/cancel_eh.h"
|
|
#include "util/scoped_timer.h"
|
|
#include "ast/expr2var.h"
|
|
|
|
extern "C" {
|
|
|
|
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {
|
|
Z3_TRY;
|
|
LOG_Z3_polynomial_subresultants(c, p, q, x);
|
|
RESET_ERROR_CODE();
|
|
polynomial::manager & pm = mk_c(c)->pm();
|
|
|
|
// 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);
|
|
for (expr* e : results) {
|
|
result->m_ast_vector.push_back(e);
|
|
}
|
|
RETURN_Z3(of_ast_vector(result));
|
|
Z3_CATCH_RETURN(nullptr);
|
|
}
|
|
|
|
};
|