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

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-01 17:52:30 +01:00
parent 336fa6ae83 963981b3a6
commit 5b8d0617d4
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();
if (sz == 0)
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();
for (unsigned i = 1; i < sz; ++i) {
monomial * m1 = monomials[j];

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

@ -110,6 +110,7 @@ protected:
};
svector<scope> m_scopes;
ptr_vector<monomial> m_tmp_monomials;
ptr_vector<monomial> m_del_monomials;
ptr_vector<expr> m_tmp_vars1;
ptr_vector<expr> m_tmp_vars2;
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;
inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain;
#ifdef _TRACE
unsigned round = 0;
#endif
max_min_t result = OPTIMIZED;
has_shared = false;
unsigned max_efforts = 10 + (ctx.get_random_value() % 20);
@ -1535,7 +1533,9 @@ namespace smt {
theory_var x_i = null_theory_var;
max_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 end = r.end_entries();
for (; it != end; ++it) {
@ -1561,7 +1561,7 @@ namespace smt {
best_efforts++;
}
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.
x_i = null_theory_var; // unbounded
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";
tout << "best efforts: " << best_efforts << "\n";);
tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
if (x_j == null_theory_var) {
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.
if (inc && upper(x_j)) {
if (max_gain.is_zero()) return BEST_EFFORT;
SASSERT(!unbounded_gain(max_gain));
update_value(x_j, max_gain);
TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
@ -1618,6 +1619,7 @@ namespace smt {
continue;
}
if (!inc && lower(x_j)) {
if (max_gain.is_zero()) return BEST_EFFORT;
SASSERT(!unbounded_gain(max_gain));
SASSERT(max_gain.is_pos());
max_gain.neg();