mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix nex order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-11 18:14:42 -07:00
parent d5f574ffc5
commit eaba70e916
1 changed files with 31 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/math/lp/nex_creator.cpp
View file

@ -118,46 +118,49 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const { bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
const nex* ae = nullptr;
const nex* be = nullptr;
auto it_a = a->begin(); auto it_a = a->begin();
auto it_b = b->begin(); auto it_b = b->begin();
auto a_end = a->end(); auto a_end = a->end();
auto b_end = b->end(); auto b_end = b->end();
unsigned a_pow, b_pow; unsigned a_pow, b_pow;
bool ret;
for (; ;) { do {
if (!inside_a_p) { if (!inside_a_p) { a_pow = it_a->pow(); }
ae = it_a->e(); if (!inside_b_p) { b_pow = it_b->pow(); }
a_pow = it_a->pow(); if (lt(it_a->e(), it_b->e())){
ret = true;
break;
} }
if (!inside_b_p) { if (lt(it_b->e(), it_a->e())) {
be = it_b->e(); ret = false;
b_pow = it_b->pow(); break;
} }
if (lt(ae, be))
return true;
if (lt(be, ae))
return false;
if (a_pow == b_pow) { if (a_pow == b_pow) {
inside_a_p = inside_b_p = false; inside_a_p = inside_b_p = false;
it_a++; it_b++; it_a++; it_b++;
if (it_a == a_end) { if (it_a == a_end) {
if (it_b != b_end) { if (it_b != b_end) {
return true; ret = true;
break;
} }
return a->coeff() < b->coeff(); SASSERT(it_a == a_end && it_b == b_end);
} else if (it_b == b_end) { ret = a->coeff() < b->coeff();
return false; break;
}
if (it_b == b_end) {
ret = false;
break;
} }
// no iterator reached the end // no iterator reached the end
continue; continue;
} }
if (a_pow < b_pow) { if (a_pow < b_pow) {
it_a++; it_a++;
if (it_a == a_end) if (it_a == a_end) {
return true; ret = true;
break;
}
inside_a_p = false; inside_a_p = false;
inside_b_p = true; inside_b_p = true;
b_pow -= a_pow; b_pow -= a_pow;
@ -165,15 +168,17 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
SASSERT(a_pow > b_pow); SASSERT(a_pow > b_pow);
a_pow -= b_pow; a_pow -= b_pow;
it_b++; it_b++;
if (it_b == b_end) if (it_b == b_end) {
return false; ret = false;
break;
}
inside_a_p = true; inside_a_p = true;
inside_b_p = false; inside_b_p = false;
} }
} } while (true);
TRACE("nla_cn_details", tout << "a = " << *a << " >= b = " << *b << "\n";);
return false;
TRACE("nla_cn_details", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
return ret;
} }
bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const { bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {