mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

reverse the order in nex expressions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-15 14:40:10 -07:00
parent 4daa841116
commit 0f948d7a07
3 changed files with 29 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -145,7 +145,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
break;
}
SASSERT(it_a == a_end && it_b == b_end);
ret = a->coeff() < b->coeff();
ret = a->coeff() > b->coeff();
break;
}
if (it_b == b_end) { // it_a is not at the end
@ -155,7 +155,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
// no iterator reached the end
continue;
}
if (a_pow < b_pow) {
if (a_pow > b_pow) {
it_a++;
if (it_a == a_end) {
ret = true;
@ -165,7 +165,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
inside_b_p = true;
b_pow -= a_pow;
} else {
SASSERT(a_pow > b_pow);
SASSERT(a_pow < b_pow);
a_pow -= b_pow;
it_b++;
if (it_b == b_end) {
@ -194,9 +194,9 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
unsigned b_deg = b->get_degree();
bool ret;
if (a_deg > b_deg) {
ret = false;
} else if (a_deg < b_deg) {
ret = true;
} else if (a_deg < b_deg) {
ret = false;
} else {
ret = less_than_on_mul_mul_same_degree(a, b);
}
@ -207,13 +207,13 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
switch(b->type()) {
case expr_type::SCALAR: return false;
case expr_type::SCALAR: return true;
case expr_type::VAR:
return less_than(a->var() , to_var(b)->var());
case expr_type::MUL:
{
if (b->get_degree() > 1)
return true;
return false;
auto it = to_mul(b)->begin();
const nex_pow & c = *it;
const nex * f = c.e();
@ -236,10 +236,12 @@ bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
case expr_type::VAR:
{
if (a->get_degree() > 1)
return false;
return true;
auto it = a->begin();
const nex_pow & c = *it;
SASSERT(c.pow() == 1);
const nex * f = c.e();
SASSERT(!f->is_scalar());
return lt(f, b);
}
case expr_type::MUL:
@ -260,7 +262,7 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
if (lt((*b)[j], (*a)[j]))
return false;
}
return size < b->size();
return size > b->size();
}
@ -275,9 +277,9 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
break;
case expr_type::SCALAR: {
if (b->is_scalar())
ret = to_scalar(a)->value() < to_scalar(b)->value();
ret = to_scalar(a)->value() > to_scalar(b)->value();
else
ret = true; // the scalars are the smallest
ret = false; // the scalars are the largest
break;
}
case expr_type::MUL: {

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

@ -86,11 +86,11 @@ public:
bool less_than(lpvar j, lpvar k) const{
unsigned wj = (unsigned)m_active_vars_weights[j];
unsigned wk = (unsigned)m_active_vars_weights[k];
return wj != wk ? wj < wk : j < k;
return wj != wk ? wj > wk : j > k;
}
bool less_than_on_nex_pow(const nex_pow & a, const nex_pow& b) const {
return (a.pow() < b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e()));
return (a.pow() > b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e()));
}
void simplify_children_of_mul(vector<nex_pow> & children, rational&);

19
src/test/lp/lp.cpp
View file

@ -82,11 +82,16 @@ void test_nex_order() {
nex_creator r;
r.set_number_of_vars(3);
for (unsigned j = 0; j < r.get_number_of_vars(); j++)
r.set_var_weight(j, j);
r.set_var_weight(j, 10 - j);
nex_var* a = r.mk_var(0);
nex_var* b = r.mk_var(1);
nex_var* c = r.mk_var(2);
SASSERT(r.lt(a, b));
SASSERT(r.lt(b, c));
SASSERT(r.lt(a, c));
nex* ab = r.mk_mul(a, b);
nex* ba = r.mk_mul(b, a);
nex* ac = r.mk_mul(a, c);
@ -96,14 +101,18 @@ void test_nex_order() {
nex* _2ab = r.mk_mul(rational(2), a, b);
SASSERT(r.lt(ab, _3ac));
SASSERT(!r.lt(_3ac, ab));
SASSERT(r.lt(a, ab));
SASSERT(!r.lt(ab, a));
SASSERT(!r.lt(a, ab));
SASSERT(r.lt(ab, a));
SASSERT(r.lt(_2ab, _3ac));
SASSERT(!r.lt(_3ac, _2ab));
nex* _2a = r.mk_mul(rational(2), a);
SASSERT(r.lt(_2a, _2ab));
SASSERT(!r.lt(_2ab, _2a));
SASSERT(!r.lt(_2a, _2ab));
SASSERT(r.lt(_2ab, _2a));
SASSERT(nex_creator::equal(ab, ba));
nex_sum * five_a_pl_one = r.mk_sum(r.mk_mul(rational(5), a), r.mk_scalar(rational(1)));
nex_mul * poly = r.mk_mul(five_a_pl_one, b);
nex * p = r.simplify(poly);
std::cout << "poly = " << *poly << " , p = " << *p << "\n";
}
void test_simplify() {