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

fix memory alias bug and non-termination bug exposed by issue #184

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-31 14:45:10 -07:00
parent 0ed38ed59b
commit 963981b3a6
3 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -440,7 +440,8 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
unsigned sz = monomials.size(); unsigned sz = monomials.size();
if (sz == 0) if (sz == 0)
return; return;
ptr_vector<monomial>& to_delete = m_tmp_monomials; SASSERT(&m_del_monomials != &monomials);
ptr_vector<monomial>& to_delete = m_del_monomials;
to_delete.reset(); to_delete.reset();
for (unsigned i = 1; i < sz; ++i) { for (unsigned i = 1; i < sz; ++i) {
monomial * m1 = monomials[j]; monomial * m1 = monomials[j];

1
src/math/grobner/grobner.h
View file

@ -110,6 +110,7 @@ protected:
}; };
svector<scope> m_scopes; svector<scope> m_scopes;
ptr_vector<monomial> m_tmp_monomials; ptr_vector<monomial> m_tmp_monomials;
ptr_vector<monomial> m_del_monomials;
ptr_vector<expr> m_tmp_vars1; ptr_vector<expr> m_tmp_vars1;
ptr_vector<expr> m_tmp_vars2; ptr_vector<expr> m_tmp_vars2;
unsigned m_num_new_equations; // temporary variable unsigned m_num_new_equations; // temporary variable

12
src/smt/theory_arith_aux.h
View file

@ -1524,9 +1524,7 @@ namespace smt {
numeral a_ij, curr_a_ij, coeff, curr_coeff; numeral a_ij, curr_a_ij, coeff, curr_coeff;
inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain; inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain;
#ifdef _TRACE
unsigned round = 0; unsigned round = 0;
#endif
max_min_t result = OPTIMIZED; max_min_t result = OPTIMIZED;
has_shared = false; has_shared = false;
unsigned max_efforts = 10 + (ctx.get_random_value() % 20); unsigned max_efforts = 10 + (ctx.get_random_value() % 20);
@ -1535,7 +1533,9 @@ namespace smt {
theory_var x_i = null_theory_var; theory_var x_i = null_theory_var;
max_gain.reset(); max_gain.reset();
min_gain.reset(); min_gain.reset();
TRACE("opt", tout << "round: " << (round++) << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout);); ++round;
TRACE("opt", tout << "round: " << round << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout););
typename vector<row_entry>::const_iterator it = r.begin_entries(); typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries(); typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -1561,7 +1561,7 @@ namespace smt {
best_efforts++; best_efforts++;
} }
else if (curr_x_i == null_theory_var) { else if (curr_x_i == null_theory_var) {
TRACE("opt", tout << "unbounded\n";); TRACE("opt", tout << "v" << curr_x_j << " is unrestricted by other variables\n";);
// we can increase/decrease curr_x_j as much as we want. // we can increase/decrease curr_x_j as much as we want.
x_i = null_theory_var; // unbounded x_i = null_theory_var; // unbounded
x_j = curr_x_j; x_j = curr_x_j;
@ -1592,7 +1592,7 @@ namespace smt {
} }
TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
tout << "best efforts: " << best_efforts << "\n";); tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
if (x_j == null_theory_var) { if (x_j == null_theory_var) {
TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n"; TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";
@ -1610,6 +1610,7 @@ namespace smt {
// can increase/decrease x_j as much as we want. // can increase/decrease x_j as much as we want.
if (inc && upper(x_j)) { if (inc && upper(x_j)) {
if (max_gain.is_zero()) return BEST_EFFORT;
SASSERT(!unbounded_gain(max_gain)); SASSERT(!unbounded_gain(max_gain));
update_value(x_j, max_gain); update_value(x_j, max_gain);
TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
@ -1618,6 +1619,7 @@ namespace smt {
continue; continue;
} }
if (!inc && lower(x_j)) { if (!inc && lower(x_j)) {
if (max_gain.is_zero()) return BEST_EFFORT;
SASSERT(!unbounded_gain(max_gain)); SASSERT(!unbounded_gain(max_gain));
SASSERT(max_gain.is_pos()); SASSERT(max_gain.is_pos());
max_gain.neg(); max_gain.neg();