mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

pin expressions per Sarah Winkler's memory leak report

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-11 09:46:10 -08:00
parent d4c98c1ab4
commit a156028d82
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/smt_internalizer.cpp
View file

@ -291,15 +291,15 @@ namespace smt {
return; return;
} }
sort * s = m_manager.get_sort(n->get_arg(0)); sort * s = m_manager.get_sort(n->get_arg(0));
sort * u = m_manager.mk_fresh_sort("distinct-elems"); sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager);
func_decl * f = m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u); func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager);
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i); expr * arg = n->get_arg(i);
app * fapp = m_manager.mk_app(f, arg); app_ref fapp(m_manager.mk_app(f, arg), m_manager);
app * val = m_manager.mk_fresh_const("unique-value", u); app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager);
enode * e = mk_enode(val, false, false, true); enode * e = mk_enode(val, false, false, true);
e->mark_as_interpreted(); e->mark_as_interpreted();
app * eq = m_manager.mk_eq(fapp, val); app_ref eq(m_manager.mk_eq(fapp, val), m_manager);
TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";); TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";);
assert_default(eq, 0); assert_default(eq, 0);
mark_as_relevant(eq); mark_as_relevant(eq);
@ -435,7 +435,7 @@ namespace smt {
TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m_manager) << "\n";); TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m_manager) << "\n";);
SASSERT(!b_internalized(n)); SASSERT(!b_internalized(n));
SASSERT(m_manager.is_distinct(n)); SASSERT(m_manager.is_distinct(n));
expr * def = m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()); expr_ref def(m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()), m_manager);
internalize(def, true); internalize(def, true);
bool_var v = mk_bool_var(n); bool_var v = mk_bool_var(n);
literal l(v); literal l(v);
@ -753,8 +753,8 @@ namespace smt {
expr * c = n->get_arg(0); expr * c = n->get_arg(0);
expr * t = n->get_arg(1); expr * t = n->get_arg(1);
expr * e = n->get_arg(2); expr * e = n->get_arg(2);
app * eq1 = mk_eq_atom(n, t); app_ref eq1(mk_eq_atom(n, t), m_manager);
app * eq2 = mk_eq_atom(n, e); app_ref eq2(mk_eq_atom(n, e), m_manager);
mk_enode(n, mk_enode(n,
true /* supress arguments, I don't want to apply CC on ite terms */, true /* supress arguments, I don't want to apply CC on ite terms */,
false /* it is a term, so it should not be merged with true/false */, false /* it is a term, so it should not be merged with true/false */,