mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix qsat destructor memory allocation #1948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
45dd820b6c
commit
8248ec879e
|
@ -549,9 +549,15 @@ namespace qe {
|
|||
solver& s() { return *m_solver; }
|
||||
solver const& s() const { return *m_solver; }
|
||||
|
||||
void reset() {
|
||||
void init() {
|
||||
m_solver = mk_smt_solver(m, m_params, symbol::null);
|
||||
}
|
||||
void reset_statistics() {
|
||||
init();
|
||||
}
|
||||
void clear() {
|
||||
m_solver = nullptr;
|
||||
}
|
||||
void assert_expr(expr* e) {
|
||||
m_solver->assert_expr(e);
|
||||
}
|
||||
|
@ -696,7 +702,7 @@ namespace qe {
|
|||
m_level -= num_scopes;
|
||||
}
|
||||
|
||||
void reset() override {
|
||||
void clear() {
|
||||
m_st.reset();
|
||||
m_fa.s().collect_statistics(m_st);
|
||||
m_ex.s().collect_statistics(m_st);
|
||||
|
@ -707,9 +713,15 @@ namespace qe {
|
|||
m_pred_abs.reset();
|
||||
m_vars.reset();
|
||||
m_model = nullptr;
|
||||
m_fa.reset();
|
||||
m_ex.reset();
|
||||
m_free_vars.reset();
|
||||
m_fa.clear();
|
||||
m_ex.clear();
|
||||
}
|
||||
|
||||
void reset() override {
|
||||
clear();
|
||||
m_fa.init();
|
||||
m_ex.init();
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1198,7 +1210,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
~qsat() override {
|
||||
reset();
|
||||
clear();
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) override {
|
||||
|
@ -1294,8 +1306,8 @@ namespace qe {
|
|||
|
||||
void reset_statistics() override {
|
||||
m_stats.reset();
|
||||
m_fa.reset();
|
||||
m_ex.reset();
|
||||
m_fa.reset_statistics();
|
||||
m_ex.reset_statistics();
|
||||
}
|
||||
|
||||
void cleanup() override {
|
||||
|
|
|
@ -350,7 +350,6 @@ class theory_lra::imp {
|
|||
var = m_solver->add_var(v, true);
|
||||
m_theory_var2var_index.setx(v, var, UINT_MAX);
|
||||
m_var_index2theory_var.setx(var, v, UINT_MAX);
|
||||
TRACE("arith", tout << v << " internal: " << var << "\n";);
|
||||
m_var_trail.push_back(v);
|
||||
add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c)));
|
||||
add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c)));
|
||||
|
@ -667,7 +666,6 @@ class theory_lra::imp {
|
|||
m_has_int |= is_int(v);
|
||||
m_theory_var2var_index.setx(v, result, UINT_MAX);
|
||||
m_var_index2theory_var.setx(result, v, UINT_MAX);
|
||||
TRACE("arith", tout << v << " internal: " << result << "\n";);
|
||||
m_var_trail.push_back(v);
|
||||
}
|
||||
return result;
|
||||
|
@ -834,7 +832,6 @@ class theory_lra::imp {
|
|||
SASSERT(!m_left_side.empty());
|
||||
vi = m_solver->add_term(m_left_side);
|
||||
m_theory_var2var_index.setx(v, vi, UINT_MAX);
|
||||
TRACE("arith", tout << v << " internal: " << vi << "\n";);
|
||||
if (m_solver->is_term(vi)) {
|
||||
m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue