mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-05 17:14:51 -07:00
parent 71ff987f6b
commit 7cd901019f
2 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -166,7 +166,7 @@ namespace opt {
return true; return true;
} }
#define PASSERT(_e_) if (!(_e_)) { TRACE("opt1", display(tout, r); display(tout);); SASSERT(_e_); } #define PASSERT(_e_) { CTRACE("qe", !(_e_), display(tout, r); display(tout);); SASSERT(_e_); }
bool model_based_opt::invariant(unsigned index, row const& r) { bool model_based_opt::invariant(unsigned index, row const& r) {
vector<var> const& vars = r.m_vars; vector<var> const& vars = r.m_vars;
@ -424,6 +424,13 @@ namespace opt {
return val; return val;
} }
rational model_based_opt::eval(vector<var> const& coeffs) const {
rational val(0);
for (var const& v : coeffs)
val += v.m_coeff * eval(v.m_id);
return val;
}
rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) const { rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) const {
return m_rows[row_id].get_coefficient(var_id); return m_rows[row_id].get_coefficient(var_id);
} }
@ -1193,7 +1200,7 @@ namespace opt {
row& r1 = m_rows[row_id1]; row& r1 = m_rows[row_id1];
vector<var> coeffs; vector<var> coeffs;
mk_coeffs_without(coeffs, r1.m_vars, x); mk_coeffs_without(coeffs, r1.m_vars, x);
rational c = r1.m_coeff; rational c = mod(-eval(coeffs), a);
add_divides(coeffs, c, a); add_divides(coeffs, c, a);
} }
unsigned_vector const& row_ids = m_var2row_ids[x]; unsigned_vector const& row_ids = m_var2row_ids[x];

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

@ -105,6 +105,8 @@ namespace opt {
rational eval(def const& d) const; rational eval(def const& d) const;
rational eval(vector<var> const& coeffs) const;
void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x); void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);
void solve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x); void solve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);