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

more fixes in simplifying nex expessions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-30 16:53:46 -07:00
parent 5e749045e1
commit 316a0470b1
3 changed files with 70 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nex.h
View file

@ -50,7 +50,6 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) {
} }
class nex; class nex;
bool less_than_nex_standard(const nex* a, const nex* b);
class nex_scalar; class nex_scalar;
// This is the class of non-linear expressions // This is the class of non-linear expressions

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

@ -116,7 +116,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
TRACE("nla_cn_details", print_vector(children, tout);); TRACE("nla_cn_details", print_vector(children, tout););
} }
bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) { bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const {
// the scalar, if it is there, is at the beginning of the children() // the scalar, if it is there, is at the beginning of the children()
TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";); TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";);
SASSERT(is_simplified(a) && is_simplified(b)); SASSERT(is_simplified(a) && is_simplified(b));
@ -170,19 +170,20 @@ bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip
continue; continue;
} }
if (a_pow < b_pow) { if (a_pow < b_pow) {
inside_a_p = false;
inside_b_p = true;
b_pow -= a_pow;
it_a++; it_a++;
if (it_a == a_end) if (it_a == a_end)
return true; return true;
inside_a_p = false;
inside_b_p = true;
b_pow -= a_pow;
} else { } else {
inside_a_p = true; SASSERT(a_pow > b_pow);
inside_b_p = false; a_pow -= b_pow;
SASSERT(b_pow < a_pow);
it_b++; it_b++;
if (it_b == b_end) if (it_b == b_end)
return false; return false;
inside_a_p = true;
inside_b_p = false;
} }
} }
return false; return false;
@ -190,22 +191,68 @@ bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip
} }
bool nex_creator::lt(const nex* a, const nex* b, bool skip_scalar) { bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b, bool skip_scalar) const {
switch(b->type()) {
case expr_type::SCALAR: return false;
case expr_type::VAR:
return less_than(a->var() , to_var(b)->var());
case expr_type::MUL:
{
nex_mul m;
m.add_child(const_cast<nex_var*>(a));
return less_than_on_mul(&m, to_mul(b), skip_scalar);
}
case expr_type::SUM:
{
nex_sum m;
m.add_child(const_cast<nex_var*>(a));
return lt(&m, to_sum(b), skip_scalar);
}
default:
UNREACHABLE();
return false;
}
}
bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b, bool skip_scalar) const {
switch(b->type()) {
case expr_type::SCALAR: return false;
case expr_type::VAR:
{
nex_mul m;
m.add_child(const_cast<nex*>(b));
return less_than_on_mul(a, &m, skip_scalar);
}
case expr_type::MUL:
return less_than_on_mul(a, to_mul(b), skip_scalar);
case expr_type::SUM:
{
const nex* fc = *(to_sum(b)->children().begin());
return lt(a, fc, skip_scalar);
}
default:
UNREACHABLE();
return false;
}
}
bool nex_creator::lt(const nex* a, const nex* b, bool skip_scalar) const {
TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";); TRACE("nla_cn_details", tout << "a = " << *a << ", b = " << *b << ", skip_scalar = " << skip_scalar << "\n";);
int r = (int)(a->type()) - (int)(b->type());
if (r) {
return r < 0;
}
SASSERT(a->type() == b->type());
switch (a->type()) { switch (a->type()) {
case expr_type::VAR: { case expr_type::VAR:
return less_than(to_var(a)->var() , to_var(b)->var()); return less_than_on_var_nex(to_var(a), b, skip_scalar);
}
case expr_type::SCALAR: { case expr_type::SCALAR: {
return to_scalar(a)->value() < to_scalar(b)->value(); if (b->is_scalar())
return
to_scalar(a)->value() < to_scalar(b)->value();
return true; // the scalars are the smallest
} }
case expr_type::MUL: { case expr_type::MUL: {
return less_than_on_mul(to_mul(a), to_mul(b), skip_scalar); return less_than_on_mul_nex(to_mul(a), b, skip_scalar);
} }
case expr_type::SUM: { case expr_type::SUM: {
UNREACHABLE(); UNREACHABLE();
@ -228,6 +275,7 @@ bool nex_creator::is_sorted(const nex_mul* e) const {
return true; return true;
} }
bool nex_creator::less_than_nex(const nex* a, const nex* b) const { bool nex_creator::less_than_nex(const nex* a, const nex* b) const {
int r = (int)(a->type()) - (int)(b->type()); int r = (int)(a->type()) - (int)(b->type());
if (r) { if (r) {

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

@ -223,9 +223,11 @@ public:
bool eat_scalar_pow(nex_scalar *& r, nex_pow& p); bool eat_scalar_pow(nex_scalar *& r, nex_pow& p);
void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar); void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar);
bool lt(const nex* a, const nex* b, bool skip_scalar); bool lt(const nex* a, const nex* b, bool skip_scalar) const;
bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar); bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const;
bool less_than_on_var_nex(const nex_var* a, const nex* b, bool skip_scalar) const;
bool less_than_on_mul_nex(const nex_mul* a, const nex* b, bool skip_scalar) const;
void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children); void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
}; };
} }