mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

remove a few more inc/dec refs

Browse source
This commit is contained in:
Nuno Lopes 2019-02-19 13:36:39 +00:00
parent edf0df634d
commit 61272fdc0c
4 changed files with 7 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/der.cpp
View file

@ -374,13 +374,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
expr_ref_buffer new_patterns(m_manager); expr_ref_buffer new_patterns(m_manager);
expr_ref_buffer new_no_patterns(m_manager); expr_ref_buffer new_no_patterns(m_manager);
for (unsigned j = 0; j < q->get_num_patterns(); j++) { for (unsigned j = 0; j < q->get_num_patterns(); j++) {
expr_ref new_pat = m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
new_patterns.push_back(new_pat);
} }
for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
expr_ref new_nopat = m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
new_no_patterns.push_back(new_nopat);
} }
r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),

3
src/ast/rewriter/distribute_forall.cpp
View file

@ -126,8 +126,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
br.mk_not(arg, not_arg); br.mk_not(arg, not_arg);
quantifier_ref tmp_q(m_manager); quantifier_ref tmp_q(m_manager);
tmp_q = m_manager.update_quantifier(q, not_arg); tmp_q = m_manager.update_quantifier(q, not_arg);
expr_ref new_q = elim_unused_vars(m_manager, tmp_q, params_ref()); new_args.push_back(elim_unused_vars(m_manager, tmp_q, params_ref()));
new_args.push_back(new_q);
} }
expr_ref result(m_manager); expr_ref result(m_manager);
// m_bsimp.mk_and actually constructs a (not (or ...)) formula, // m_bsimp.mk_and actually constructs a (not (or ...)) formula,

7
src/ast/rewriter/var_subst.cpp
View file

@ -135,17 +135,14 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
return result; return result;
} }
expr_ref tmp(m);
expr_ref_buffer new_patterns(m); expr_ref_buffer new_patterns(m);
expr_ref_buffer new_no_patterns(m); expr_ref_buffer new_no_patterns(m);
for (unsigned i = 0; i < num_patterns; i++) { for (unsigned i = 0; i < num_patterns; i++) {
tmp = m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()); new_patterns.push_back(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
new_patterns.push_back(tmp);
} }
for (unsigned i = 0; i < num_no_patterns; i++) { for (unsigned i = 0; i < num_no_patterns; i++) {
tmp = m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()); new_no_patterns.push_back(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
new_no_patterns.push_back(tmp);
} }
result = m.mk_quantifier(q->get_kind(), result = m.mk_quantifier(q->get_kind(),

6
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -49,8 +49,7 @@ class distribute_forall_tactic : public tactic {
expr * not_arg = m.mk_not(arg); expr * not_arg = m.mk_not(arg);
quantifier_ref tmp_q(m); quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, not_arg); tmp_q = m.update_quantifier(old_q, not_arg);
expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
new_args.push_back(new_q);
} }
result = m.mk_and(new_args.size(), new_args.c_ptr()); result = m.mk_and(new_args.size(), new_args.c_ptr());
return true; return true;
@ -68,8 +67,7 @@ class distribute_forall_tactic : public tactic {
expr * arg = to_app(new_body)->get_arg(i); expr * arg = to_app(new_body)->get_arg(i);
quantifier_ref tmp_q(m); quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, arg); tmp_q = m.update_quantifier(old_q, arg);
expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
new_args.push_back(new_q);
} }
result = m.mk_and(new_args.size(), new_args.c_ptr()); result = m.mk_and(new_args.size(), new_args.c_ptr());
return true; return true;