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

fixes in nex order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-11 17:36:30 -07:00
parent f71cd72d7b
commit d5f574ffc5
3 changed files with 34 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -115,29 +115,17 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
TRACE("nla_cn_details", print_vector(children, tout);); TRACE("nla_cn_details", print_vector(children, tout););
} }
bool nex_creator::less_than_on_mul_mul(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 {
SASSERT(is_simplified(a)); bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
SASSERT(is_simplified(b)); bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
unsigned a_deg = a->get_degree(); const nex* ae = nullptr;
unsigned b_deg = b->get_degree(); const nex* be = nullptr;
if (a_deg > b_deg)
return true;
if (a_deg < b_deg)
return false;
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 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
const nex* ae = nullptr;
const nex *be = nullptr;
if (it_a == a_end) {
return it_b != b_end;
}
if (it_b == b_end)
return false;
for (; ;) { for (; ;) {
if (!inside_a_p) { if (!inside_a_p) {
ae = it_a->e(); ae = it_a->e();
@ -185,6 +173,28 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
} }
TRACE("nla_cn_details", tout << "a = " << *a << " >= b = " << *b << "\n";); TRACE("nla_cn_details", tout << "a = " << *a << " >= b = " << *b << "\n";);
return false; return false;
}
bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {
SASSERT(a->get_degree() == b->get_degree());
SASSERT(a->size() && b->size());
return less_than_on_mul_mul_same_degree_iterate(a, b);
}
bool nex_creator::less_than_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();
bool ret;
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);
}
return ret;
} }
@ -752,8 +762,8 @@ bool nex_creator::equal(const nex* a, const nex* b) {
} }
nex * ca = cn.canonize(a); nex * ca = cn.canonize(a);
nex * cb = cn.canonize(b); nex * cb = cn.canonize(b);
TRACE("nla_cn_test", tout << "a = " << *a << ", canonized a = " << *ca << "\n";); TRACE("nla_cn_details", tout << "a = " << *a << ", canonized a = " << *ca << "\n";);
TRACE("nla_cn_test", tout << "b = " << *b << ", canonized b = " << *cb << "\n";); TRACE("nla_cn_details", tout << "b = " << *b << ", canonized b = " << *cb << "\n";);
return !(cn.lt(ca, cb) || cn.lt(cb, ca)); return !(cn.lt(ca, cb) || cn.lt(cb, ca));
} }
#endif #endif

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

@ -95,7 +95,6 @@ public:
void simplify_children_of_mul(vector<nex_pow> & children, rational&); void simplify_children_of_mul(vector<nex_pow> & children, rational&);
nex * clone(const nex* a) { nex * clone(const nex* a) {
switch (a->type()) { switch (a->type()) {
case expr_type::VAR: { case expr_type::VAR: {
@ -253,6 +252,8 @@ public:
bool lt(const nex* a, const nex* b) const; bool lt(const nex* a, const nex* b) const;
bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const; bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_var_nex(const nex_var* a, const nex* b) const; bool less_than_on_var_nex(const nex_var* a, const nex* b) const;
bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const; bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const;
bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const; bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const;

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

@ -184,9 +184,9 @@ void test_cn_shorter() {
bcg->add_child(min_1); bcg->add_child(min_1);
nex* abcd = cr.mk_mul(a, b, c, d); nex* abcd = cr.mk_mul(a, b, c, d);
nex* eae = cr.mk_mul(e, a, e); nex* eae = cr.mk_mul(e, a, e);
nex* eac = cr.mk_mul(e, a, c); nex* three_eac = cr.mk_mul(e, a, c); to_mul(three_eac)->coeff() = rational(3);
nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d); nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d);
clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, eac))); clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, three_eac)));
clone = to_sum(cr.simplify(clone)); clone = to_sum(cr.simplify(clone));
TRACE("nla_test", tout << "clone = " << *clone << "\n";); TRACE("nla_test", tout << "clone = " << *clone << "\n";);
// test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);