fix(kernel/unification_constraint): memory leak
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
7d602c1068
commit
0c21f45292
2 changed files with 12 additions and 19 deletions
|
@ -96,10 +96,10 @@ format unification_constraint_max::pp(formatter const & fmt, options const & opt
|
|||
return add_justification(fmt, opts, body, m_justification, p, include_justification);
|
||||
}
|
||||
|
||||
unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j):
|
||||
unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j):
|
||||
unification_constraint_cell(unification_constraint_kind::Choice, c, j),
|
||||
m_mvar(mvar),
|
||||
m_num_choices(num) {
|
||||
m_choices(choices, choices + num) {
|
||||
}
|
||||
|
||||
unification_constraint_choice::~unification_constraint_choice() {
|
||||
|
@ -111,9 +111,9 @@ format unification_constraint_choice::pp(formatter const & fmt, options const &
|
|||
format eq_op = mk_unification_op(opts);
|
||||
format or_op = unicode ? format("\u2295") : format("OR");
|
||||
format body;
|
||||
for (unsigned i = 0; i < m_num_choices; i++) {
|
||||
for (unsigned i = 0; i < m_choices.size(); i++) {
|
||||
body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, m_choices[i], false, opts))}));
|
||||
if (i + 1 < m_num_choices)
|
||||
if (i + 1 < m_choices.size())
|
||||
body += format{space(), or_op, line()};
|
||||
}
|
||||
body = group(body);
|
||||
|
@ -134,12 +134,7 @@ unification_constraint mk_max_constraint(context const & c, expr const & lhs1, e
|
|||
}
|
||||
|
||||
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j) {
|
||||
char * mem = new char[sizeof(unification_constraint_choice) + num*sizeof(expr)];
|
||||
unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, j));
|
||||
expr * m_choices = to_choice(r)->m_choices;
|
||||
for (unsigned i = 0; i < num; i++)
|
||||
new (m_choices+i) expr(choices[i]);
|
||||
return r;
|
||||
return unification_constraint(new unification_constraint_choice(c, mvar, num, choices, j));
|
||||
}
|
||||
|
||||
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j) {
|
||||
|
|
|
@ -134,18 +134,16 @@ public:
|
|||
\brief Unification constraint of the form <tt>ctx |- mvar == choices[0] OR ... OR mvar == choices[size-1]</tt>.
|
||||
*/
|
||||
class unification_constraint_choice : public unification_constraint_cell {
|
||||
expr m_mvar;
|
||||
unsigned m_num_choices;
|
||||
expr m_choices[0];
|
||||
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
|
||||
expr m_mvar;
|
||||
std::vector<expr> m_choices;
|
||||
public:
|
||||
unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j);
|
||||
unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
|
||||
virtual ~unification_constraint_choice();
|
||||
expr const & get_mvar() const { return m_mvar; }
|
||||
unsigned get_num_choices() const { return m_num_choices; }
|
||||
expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; }
|
||||
expr const * begin_choices() const { return m_choices; }
|
||||
expr const * end_choices() const { return m_choices + m_num_choices; }
|
||||
unsigned get_num_choices() const { return m_choices.size(); }
|
||||
expr const & get_choice(unsigned idx) const { return m_choices[idx]; }
|
||||
std::vector<expr>::const_iterator begin_choices() const { return m_choices.begin(); }
|
||||
std::vector<expr>::const_iterator end_choices() const { return m_choices.end(); }
|
||||
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue