mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

eq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-29 20:36:12 -07:00
parent e79542cc68
commit dd452e0ac1
3 changed files with 35 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -1911,7 +1911,7 @@ void ast_manager::delete_node(ast * n) {
while ((n = m_ast_table.pop_erase())) {
CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";);
TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id));

113
src/math/grobner/grobner.cpp
View file

@ -65,19 +65,14 @@ void grobner::del_equation(equation * eq) {
}
void grobner::del_monomials(ptr_vector<monomial>& ms) {
ptr_vector<monomial>::iterator it = ms.begin();
ptr_vector<monomial>::iterator end = ms.end();
for (; it != end; ++it) {
del_monomial(*it);
for (auto& m : ms) {
del_monomial(m);
}
ms.reset();
}
void grobner::del_monomial(monomial * m) {
ptr_vector<expr>::iterator it2 = m->m_vars.begin();
ptr_vector<expr>::iterator end2 = m->m_vars.end();
for (; it2 != end2; ++it2) {
expr * v = *it2;
for (expr * v : m->m_vars) {
m_manager.dec_ref(v);
}
dealloc(m);
@ -187,10 +182,8 @@ void grobner::display_equation(std::ostream & out, equation const & eq) const {
void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
if (!v.empty()) {
out << header << "\n";
equation_set::iterator it = v.begin();
equation_set::iterator end = v.end();
for (; it != end; ++it)
display_equation(out, *(*it));
for (equation const* eq : v)
display_equation(out, *eq);
}
}
@ -215,10 +208,7 @@ bool grobner::update_order(equation * eq) {
if (eq->get_num_monomials() == 0)
return false;
monomial * first = eq->m_monomials[0];
ptr_vector<monomial>::iterator it = eq->m_monomials.begin();
ptr_vector<monomial>::iterator end = eq->m_monomials.end();
for (; it != end; ++it) {
monomial * m = *it;
for (monomial* m : eq->m_monomials) {
std::stable_sort(m->m_vars.begin(), m->m_vars.end(), m_var_lt);
}
std::stable_sort(eq->m_monomials.begin(), eq->m_monomials.end(), m_monomial_lt);
@ -227,10 +217,7 @@ bool grobner::update_order(equation * eq) {
void grobner::update_order(equation_set & s, bool processed) {
ptr_buffer<equation> to_remove;
equation_set::iterator it = s.begin();
equation_set::iterator end = s.end();
for (;it != end; ++it) {
equation * eq = *it;
for (equation * eq : s) {
if (update_order(eq)) {
if (processed) {
to_remove.push_back(eq);
@ -238,10 +225,8 @@ void grobner::update_order(equation_set & s, bool processed) {
}
}
}
ptr_buffer<equation>::iterator it2 = to_remove.begin();
ptr_buffer<equation>::iterator end2 = to_remove.end();
for (; it2 != end2; ++it2)
s.erase(*it2);
for (equation* e : to_remove)
s.erase(e);
}
void grobner::update_order() {
@ -582,10 +567,8 @@ void grobner::mul_append(unsigned start_idx, equation const * source, rational c
new_m->m_coeff *= coeff;
new_m->m_vars.append(m->m_vars.size(), m->m_vars.c_ptr());
new_m->m_vars.append(vars.size(), vars.c_ptr());
ptr_vector<expr>::iterator it = new_m->m_vars.begin();
ptr_vector<expr>::iterator end = new_m->m_vars.end();
for (; it != end; ++it)
m_manager.inc_ref(*it);
for (expr* e : new_m->m_vars)
m_manager.inc_ref(e);
std::stable_sort(new_m->m_vars.begin(), new_m->m_vars.end(), m_var_lt);
result.push_back(new_m);
}
@ -597,10 +580,8 @@ void grobner::mul_append(unsigned start_idx, equation const * source, rational c
grobner::monomial * grobner::copy_monomial(monomial const * m) {
monomial * r = alloc(monomial);
r->m_coeff = m->m_coeff;
ptr_vector<expr>::const_iterator it = m->m_vars.begin();
ptr_vector<expr>::const_iterator end = m->m_vars.end();
for (; it != end; ++it)
add_var(r, *it);
for (expr* e : m->m_vars)
add_var(r, e);
return r;
}
@ -692,10 +673,7 @@ grobner::equation * grobner::simplify_using_processed(equation * eq) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using already processed equalities\n";);
do {
simplified = false;
equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end();
for (; it != end; ++it) {
equation const * p = *it;
for (equation const* p : m_processed) {
equation * new_eq = simplify(p, eq);
if (new_eq) {
result = true;
@ -735,19 +713,14 @@ bool grobner::is_better_choice(equation * eq1, equation * eq2) {
grobner::equation * grobner::pick_next() {
equation * r = nullptr;
ptr_buffer<equation> to_delete;
equation_set::iterator it = m_to_process.begin();
equation_set::iterator end = m_to_process.end();
for (; it != end; ++it) {
equation * curr = *it;
for (equation * curr : m_to_process) {
if (is_trivial(curr))
to_delete.push_back(curr);
else if (is_better_choice(curr, r))
r = curr;
}
ptr_buffer<equation>::const_iterator it1 = to_delete.begin();
ptr_buffer<equation>::const_iterator end1 = to_delete.end();
for (; it1 != end1; ++it1)
del_equation(*it1);
for (equation * e : to_delete)
del_equation(e);
if (r)
m_to_process.erase(r);
TRACE("grobner", tout << "selected equation: "; if (!r) tout << "<null>\n"; else display_equation(tout, *r););
@ -791,18 +764,12 @@ bool grobner::simplify_processed(equation * eq) {
if (is_trivial(curr))
to_delete.push_back(curr);
}
ptr_buffer<equation>::const_iterator it1 = to_insert.begin();
ptr_buffer<equation>::const_iterator end1 = to_insert.end();
for (; it1 != end1; ++it1)
m_processed.insert(*it1);
it1 = to_remove.begin();
end1 = to_remove.end();
for (; it1 != end1; ++it1)
m_processed.erase(*it1);
it1 = to_delete.begin();
end1 = to_delete.end();
for (; it1 != end1; ++it1)
del_equation(*it1);
for (equation* eq : to_insert)
m_processed.insert(eq);
for (equation* eq : to_remove)
m_processed.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
return !m_manager.canceled();
}
@ -810,13 +777,10 @@ bool grobner::simplify_processed(equation * eq) {
\brief Use the given equation to simplify to-process terms.
*/
void grobner::simplify_to_process(equation * eq) {
equation_set::iterator it = m_to_process.begin();
equation_set::iterator end = m_to_process.end();
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
for (; it != end; ++it) {
equation * curr = *it;
for (equation* curr : m_to_process) {
equation * new_curr = simplify(eq, curr);
if (new_curr != nullptr && new_curr != curr) {
m_equations_to_unfreeze.push_back(curr);
@ -827,18 +791,12 @@ void grobner::simplify_to_process(equation * eq) {
if (is_trivial(curr))
to_delete.push_back(curr);
}
ptr_buffer<equation>::const_iterator it1 = to_insert.begin();
ptr_buffer<equation>::const_iterator end1 = to_insert.end();
for (; it1 != end1; ++it1)
m_to_process.insert(*it1);
it1 = to_remove.begin();
end1 = to_remove.end();
for (; it1 != end1; ++it1)
m_to_process.erase(*it1);
it1 = to_delete.begin();
end1 = to_delete.end();
for (; it1 != end1; ++it1)
del_equation(*it1);
for (equation* eq : to_insert)
m_to_process.insert(eq);
for (equation* eq : to_remove)
m_to_process.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
}
/**
@ -924,10 +882,7 @@ void grobner::superpose(equation * eq1, equation * eq2) {
\brief Superpose the given equations with the equations in m_processed.
*/
void grobner::superpose(equation * eq) {
equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end();
for (; it != end; ++it) {
equation * curr = *it;
for (equation * curr : m_processed) {
superpose(eq, curr);
}
}
@ -971,10 +926,8 @@ bool grobner::compute_basis(unsigned threshold) {
}
void grobner::copy_to(equation_set const & s, ptr_vector<equation> & result) const {
equation_set::iterator it = s.begin();
equation_set::iterator end = s.end();
for (; it != end; ++it)
result.push_back(*it);
for (equation * e : s)
result.push_back(e);
}
/**

2
src/model/model.cpp
View file

@ -313,7 +313,7 @@ void model::cleanup_interp(top_sort& ts, func_decl* f) {
if (e1 != e2)
fi->set_else(e2);
for (auto& fe : *fi) {
expr_ref e2 = cleanup_expr(ts, fe->get_result(), pid);
e2 = cleanup_expr(ts, fe->get_result(), pid);
if (e2 != fe->get_result()) {
fi->insert_entry(fe->get_args(), e2);
}