mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-18 14:44:21 +00:00
Code Activity

remove a few copies

Browse source
This commit is contained in:
Nuno Lopes 2026-02-10 09:52:03 +00:00
parent 617c621cc0
commit 915ad35012
8 changed files with 42 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/explanation.h
View file

@ -124,14 +124,12 @@ public:
struct equality {
lp::lpvar i, j;
lp::explanation e;
equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {}
};
struct fixed_equality {
lp::lpvar v;
rational k;
lp::explanation e;
fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {}
};
}

9
src/math/lp/monomial_bounds.cpp
View file

@ -423,8 +423,7 @@ namespace nla {
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep);
// propagate fixed equality
auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), rational(0), exp);
c().add_fixed_equality(m.var(), rational(0), get_explanation(dep));
}
void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
@ -433,8 +432,7 @@ namespace nla {
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
// propagate fixed equality
auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), k, exp);
c().add_fixed_equality(m.var(), k, get_explanation(dep));
}
void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
@ -447,8 +445,7 @@ namespace nla {
c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, mpq(0), dep);
if (k == 1) {
lp::explanation exp = get_explanation(dep);
c().add_equality(m.var(), w, exp);
c().add_equality(m.var(), w, get_explanation(dep));
}
}

4
src/math/lp/nla_core.h
View file

@ -443,8 +443,8 @@ public:
vector<lp::fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
bool should_check_feasible() const { return m_check_feasible; }
void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation && e) { m_fixed_equalities.push_back({v, k, std::move(e)}); }
void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation && e) { m_equalities.push_back({i, j, std::move(e)}); }
bool throttle_enabled() const { return m_throttle_enabled; }
nla_throttle& throttle() { return m_throttle; }