mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

integrating NB suggestions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-11 10:47:15 -10:00
parent 617e1387f4
commit 7642f74142
2 changed files with 32 additions and 117 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -125,127 +125,42 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
TRACE("grobner_d", print_vector(children, tout););
}
bool nex_creator:: gt_on_powers_mul_same_degree(const vector<nex_pow>& 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_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a.begin();
auto it_b = b.begin();
auto a_end = a.end();
auto b_end = b.end();
unsigned a_pow, b_pow;
lbool ret = l_undef;
while (true) {
if (!inside_a_p) { a_pow = it_a->pow(); }
if (!inside_b_p) { b_pow = it_b->pow(); }
template <typename T>
bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) const {
bool ret = false;
unsigned a_pow = a.begin()->pow();
unsigned b_pow = b.begin()->pow();
for (auto it_a = a.begin(), it_b = b.begin(); it_a != a.end() && it_b != b.end(); ) {
if (gt(it_a->e(), it_b->e())){
ret = l_true;
ret = true;
break;
}
if (gt(it_b->e(), it_a->e())) {
ret = l_false;
if (gt(it_b->e(), it_a->e())){
ret = false;
break;
}
if (a_pow == b_pow) {
inside_a_p = inside_b_p = false;
it_a++; it_b++;
if (it_a == a_end) {
ret = l_false;
break;
}
if (it_b == b_end) { // it_a is not at the end
ret = l_false;
break;
}
// no iterator reached the end
continue;
}
if (a_pow > b_pow) {
it_a++;
if (it_a == a_end) {
ret = l_true;
break;
}
inside_a_p = false;
inside_b_p = true;
if (a_pow > b_pow) { // b should be advanced
b_pow -= a_pow;
} else {
SASSERT(a_pow < b_pow);
a_pow -= b_pow;
it_b++;
if (it_b == b_end) {
ret = l_false;
break;
}
inside_a_p = true;
inside_b_p = false;
++it_b;
if (it_b != b.end()) b_pow = it_b->pow();
ret = true;
}
else if (a_pow < b_pow) { // a should be advanced
b_pow -= a_pow;
++it_a;
if (it_a != a.end()) a_pow = it_a->pow();
ret = false;
}
else {
++it_a;
++it_b;
if (it_a != a.end()) a_pow = it_a->pow();
if (it_b != b.end()) b_pow = it_b->pow();
}
}
TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret != l_false?" < ":" >= ") << b << "\n";);
return ret != l_false;
}
bool nex_creator::gt_on_mul_mul_same_degree(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_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a.begin();
auto it_b = b.begin();
auto a_end = a.end();
auto b_end = b.end();
unsigned a_pow, b_pow;
lbool ret = l_undef;
while (true) {
if (!inside_a_p) { a_pow = it_a->pow(); }
if (!inside_b_p) { b_pow = it_b->pow(); }
if (gt(it_a->e(), it_b->e())){
ret = l_true;
break;
}
if (gt(it_b->e(), it_a->e())) {
ret = l_false;
break;
}
if (a_pow == b_pow) {
inside_a_p = inside_b_p = false;
it_a++; it_b++;
if (it_a == a_end) {
if (it_b != b_end) {
ret = l_false;
break;
}
SASSERT(it_a == a_end && it_b == b_end);
ret = to_lbool(a.coeff() > b.coeff());
break;
}
if (it_b == b_end) { // it_a is not at the end
ret = l_false;
break;
}
// no iterator reached the end
continue;
}
if (a_pow > b_pow) {
it_a++;
if (it_a == a_end) {
ret = l_true;
break;
}
inside_a_p = false;
inside_b_p = true;
b_pow -= a_pow;
} else {
SASSERT(a_pow < b_pow);
a_pow -= b_pow;
it_b++;
if (it_b == b_end) {
ret = l_false;
break;
}
inside_a_p = true;
inside_b_p = false;
}
}
TRACE("grobner_d", tout << "a = " << a << (ret != l_false?" < ":" >= ") << b << "\n";);
return ret != l_false;
TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret?" > ":" <= ") << b << "\n";);
return ret;
}
bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
@ -269,7 +184,7 @@ bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
SASSERT(is_simplified(&a) && is_simplified(&b));
unsigned a_deg = a.get_degree();
unsigned b_deg = b.get_degree();
return a_deg == b_deg ? gt_on_mul_mul_same_degree(a, b) : a_deg > b_deg;
return a_deg == b_deg ? gt_on_powers_mul_same_degree(a, b) : a_deg > b_deg;
}
bool nex_creator::gt_on_var_nex(const nex_var* a, const nex* b) const {

6
src/math/lp/nex_creator.h
View file

@ -244,11 +244,11 @@ public:
bool children_are_simplified(const vector<nex_pow>& children) const;
bool gt(const nex* a, const nex* b) const;
bool gt_nex_powers(const vector<nex_pow>&, const nex* b) const;
bool gt_on_powers_mul(const vector<nex_pow>&, const nex_mul& b) const;
bool gt_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul& b) const;
bool gt_on_powers_mul(const vector<nex_pow>&, const nex_mul& b) const;
template <typename T>
bool gt_on_powers_mul_same_degree(const T&, const nex_mul& b) const;
bool gt_for_sort_join_sum(const nex* a, const nex* b) const;
bool gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const;
bool gt_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const;
bool gt_on_var_nex(const nex_var* a, const nex* b) const;
bool gt_on_mul_nex(const nex_mul* a, const nex* b) const;
bool gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const;