mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-23 08:47:37 +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 • committed by Nikolaj Bjorner
parent a3e7bbb92f
commit 9152013fbd
8 changed files with 42 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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));
}
}