mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

fix up use-list in 3x3 resolution case. Regression RND_3_24.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-28 11:41:57 -07:00
parent 014c693fa5
commit 84aec95eda
2 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/simplex/model_based_opt.cpp
View file

@ -57,6 +57,7 @@ namespace opt {
// variables in each row are sorted and have non-zero coefficients // variables in each row are sorted and have non-zero coefficients
PASSERT(i + 1 == vars.size() || vars[i].m_id < vars[i+1].m_id); PASSERT(i + 1 == vars.size() || vars[i].m_id < vars[i+1].m_id);
PASSERT(!vars[i].m_coeff.is_zero()); PASSERT(!vars[i].m_coeff.is_zero());
PASSERT(index == 0 || m_var2row_ids[vars[i].m_id].contains(index));
} }
PASSERT(r.m_value == get_row_value(r)); PASSERT(r.m_value == get_row_value(r));
@ -522,6 +523,7 @@ namespace opt {
if (c.is_zero()) { if (c.is_zero()) {
return; return;
} }
m_new_vars.reset(); m_new_vars.reset();
row& r1 = m_rows[row_id1]; row& r1 = m_rows[row_id1];
row const& r2 = m_rows[row_id2]; row const& r2 = m_rows[row_id2];
@ -650,7 +652,6 @@ namespace opt {
r.m_coeff += rational::one(); r.m_coeff += rational::one();
r.m_value += rational::one(); r.m_value += rational::one();
} }
SASSERT(invariant(row_id, r));
} }
unsigned model_based_opt::new_row() { unsigned model_based_opt::new_row() {
@ -668,6 +669,17 @@ namespace opt {
return row_id; return row_id;
} }
unsigned model_based_opt::copy_row(unsigned src) {
unsigned dst = new_row();
row const& r = m_rows[src];
set_row(dst, r.m_vars, r.m_coeff, r.m_mod, r.m_type);
for (unsigned i = 0; i < r.m_vars.size(); ++i) {
m_var2row_ids[r.m_vars[i].m_id].push_back(dst);
}
SASSERT(invariant(dst, m_rows[dst]));
return dst;
}
void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, ineq_type rel) { void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, ineq_type rel) {
add_constraint(coeffs, c, rational::zero(), rel); add_constraint(coeffs, c, rational::zero(), rel);
} }
@ -813,9 +825,8 @@ namespace opt {
resolve(row_id1, coeff, row_id2, x); resolve(row_id1, coeff, row_id2, x);
} }
else { else {
row r(m_rows[row_id2]); unsigned row_id3 = copy_row(row_id2);
m_rows.push_back(r); resolve(row_id1, coeff, row_id3, x);
resolve(row_id1, coeff, m_rows.size()-1, x);
} }
} }
} }

2
src/math/simplex/model_based_opt.h
View file

@ -109,6 +109,8 @@ namespace opt {
unsigned new_row(); unsigned new_row();
unsigned copy_row(unsigned row_id);
rational n_sign(rational const& b) const; rational n_sign(rational const& b) const;
void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail); void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);