mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-24 21:03:32 +00:00
Code Activity

replace with e

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-12 10:17:46 -07:00
parent 276b00db5b
commit 1576824675
1 changed files with 4 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/lp/dioph_eq.cpp
View file

@ -238,18 +238,13 @@ namespace lp {
r.c() -= b.c(); r.c() -= b.c();
return r; return r;
} }
#if Z3DEBUG
friend bool operator==(const term_o& a, const term_o& b) { friend bool eq(const term_o& a, const term_o& b) {
term_o t = a.clone(); term_o t = a.clone();
t += mpq(-1) * b; t += mpq(-1) * b;
return t.c() == mpq(0) && t.size() == 0; return t.c() == mpq(0) && t.size() == 0;
} }
friend bool operator!=(const term_o& a, const term_o& b) {
return ! (a == b);
}
#endif
term_o& operator+=(const term_o& t) { term_o& operator+=(const term_o& t) {
for (const auto& p : t) { for (const auto& p : t) {
add_monomial(p.coeff(), p.j()); add_monomial(p.coeff(), p.j());
@ -1541,7 +1536,7 @@ namespace lp {
term_o t1 = open_ml(t0); term_o t1 = open_ml(t0);
t1.add_monomial(mpq(1), j); t1.add_monomial(mpq(1), j);
term_o rs = fix_vars(t1); term_o rs = fix_vars(t1);
if (ls != rs) { if (!eq(ls, rs)) {
TRACE(dio, tout << "ls:"; print_term_o(ls, tout) << "\n"; TRACE(dio, tout << "ls:"; print_term_o(ls, tout) << "\n";
tout << "rs:"; print_term_o(rs, tout) << "\n";); tout << "rs:"; print_term_o(rs, tout) << "\n";);
return false; return false;
@ -2351,7 +2346,7 @@ namespace lp {
return false; return false;
} }
bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei])); bool ret = eq(ls, fix_vars(open_ml(m_l_matrix.m_rows[ei])));
if (!ret) { if (!ret) {
CTRACE(dio, !ret, CTRACE(dio, !ret,
{ {