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 simplification

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-01 11:18:25 -07:00
parent 9f8f6dee9e
commit f07d9a80c5
4 changed files with 24 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -127,6 +127,7 @@ public:
nex* c_over_f = m_nex_creator.mk_div(*c, f); nex* c_over_f = m_nex_creator.mk_div(*c, f);
c_over_f = m_nex_creator.simplify(c_over_f); c_over_f = m_nex_creator.simplify(c_over_f);
TRACE("nla_cn", tout << "c_over_f =" << *c_over_f << std::endl;);
nex_mul* cm; nex_mul* cm;
*c = cm = m_nex_creator.mk_mul(f, c_over_f); *c = cm = m_nex_creator.mk_mul(f, c_over_f);
TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";); TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";);

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

@ -141,10 +141,18 @@ public:
int& pow() { return m_power; } int& pow() { return m_power; }
std::string to_string() const { std::string to_string() const {
std::stringstream s; std::stringstream s;
if (pow() == 1) { if (pow() == 1) {
s <<"(" << *e() << ")"; if (e()->is_elementary()) {
s << *e();
} else {
s <<"(" << *e() << ")";
}
} else { } else {
s << "(" << *e() << "^" << pow() << ")"; if (e()->is_elementary()){
s << "(" << *e() << "^" << pow() << ")";
} else {
s << "((" << *e() << ")^" << pow() << ")";
}
} }
return s.str(); return s.str();
} }

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

@ -464,7 +464,7 @@ void nex_creator::fill_map_with_children(std::map<nex*, rational, nex_lt> & m, p
} }
} }
if (scalar && scalar->value().is_zero() == false) { if (scalar && scalar->value().is_zero() == false) {
m[scalar] = rational(); m[scalar] = rational(scalar->value());
} }
} }
@ -590,11 +590,17 @@ nex * nex_creator::mk_div(const nex* a, const nex* b) {
} }
nex* nex_creator::simplify(nex* e) { nex* nex_creator::simplify(nex* e) {
nex* es;
TRACE("nla_cn_details", tout << *e << std::endl;);
if (e->is_mul()) if (e->is_mul())
return simplify_mul(to_mul(e)); es = simplify_mul(to_mul(e));
if (e->is_sum()) else if (e->is_sum())
return simplify_sum(to_sum(e)); es = simplify_sum(to_sum(e));
return e; else
es = e;
TRACE("nla_cn_details", tout << "simplified = " << *es << std::endl;);
SASSERT(is_simplified(es));
return es;
} }
bool nex_creator::is_simplified(const nex *e) const bool nex_creator::is_simplified(const nex *e) const

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

@ -68,7 +68,6 @@ public:
const svector<var_weight>& active_vars_weights() const { return m_active_vars_weights;} const svector<var_weight>& active_vars_weights() const { return m_active_vars_weights;}
nex* simplify(nex* e); nex* simplify(nex* e);
rational extract_coeff_from_mul(const nex_mul* m); rational extract_coeff_from_mul(const nex_mul* m);
rational extract_coeff(const nex*); rational extract_coeff(const nex*);
@ -235,6 +234,6 @@ public:
bool less_than_on_mul(const nex_mul* a, const nex_mul* b, bool skip_scalar) const; 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_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; 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);
}; };
} }