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

Merge pull request #8803 from Z3Prover/mbo_leak

Browse source
This commit is contained in:
Lev Nachmanson 2026-02-27 19:02:56 -10:00 • committed by GitHub
commit 7968669cf2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/model_based_opt.cpp
View file

@ -89,7 +89,7 @@ namespace opt {
}
void model_based_opt::def::dec_ref() {
SASSERT(m_ref_count > 0);
++m_ref_count;
--m_ref_count;
if (m_ref_count == 0)
dealloc(this);
}

19
src/math/simplex/model_based_opt.h
View file

@ -85,6 +85,7 @@ namespace opt {
enum def_t { add_t, mul_t, div_t, const_t, var_t};
struct def {
def() = default;
virtual ~def() = default;
static def* from_row(row const& r, unsigned x);
def_t m_type;
unsigned m_ref_count = 0;
@ -120,6 +121,12 @@ namespace opt {
if (d) d->inc_ref();
m_def = d;
}
def_ref(def_ref const& other) : m_def(other.m_def) {
if (m_def) m_def->inc_ref();
}
def_ref(def_ref&& other) noexcept : m_def(other.m_def) {
other.m_def = nullptr;
}
def_ref& operator=(def* d) {
if (d) d->inc_ref();
if (m_def) m_def->dec_ref();
@ -136,6 +143,15 @@ namespace opt {
return *this;
}
def_ref& operator=(def_ref&& d) noexcept {
if (&d == this)
return *this;
if (m_def) m_def->dec_ref();
m_def = d.m_def;
d.m_def = nullptr;
return *this;
}
def& operator*() { return *m_def; }
def* operator->() { return m_def; }
def const& operator*() const { return *m_def; }
@ -146,15 +162,18 @@ namespace opt {
struct add_def : public def {
def* x, *y;
add_def(def* x, def* y) : x(x), y(y) { m_type = add_t; x->inc_ref(); y->inc_ref(); }
~add_def() override { x->dec_ref(); y->dec_ref(); }
};
struct mul_def : public def {
def* x, *y;
mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t; x->inc_ref(); y->inc_ref(); }
~mul_def() override { x->dec_ref(); y->dec_ref(); }
};
struct div_def : public def {
def* x;
rational m_div{ 1 };
div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); }
~div_def() override { x->dec_ref(); }
};
struct var_def : public def {
var v;