mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

debug sorting of nex expressions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-28 20:12:31 -07:00
parent 019ba1e942
commit 4c1a120391
3 changed files with 27 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

22
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::mul_simplify_lt(const nex_mul* a, const nex_mul* b) { bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
@ -135,7 +135,7 @@ bool nex_creator::sum_simplify_lt(const nex* a, const nex* b) {
return to_scalar(a)->value() < to_scalar(b)->value(); return to_scalar(a)->value() < to_scalar(b)->value();
} }
case expr_type::MUL: { case expr_type::MUL: {
return mul_simplify_lt(to_mul(a), to_mul(b)); return less_than_on_mul(to_mul(a), to_mul(b));
} }
case expr_type::SUM: { case expr_type::SUM: {
UNREACHABLE(); UNREACHABLE();
@ -229,7 +229,7 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
return e; return e;
} }
bool nex_creator::sum_is_simplified(nex_sum* e) const { bool nex_creator::sum_is_simplified(const nex_sum* e) const {
if (e->size() < 2) return false; if (e->size() < 2) return false;
for (nex * ee : e->children()) { for (nex * ee : e->children()) {
if (ee->is_sum()) if (ee->is_sum())
@ -470,4 +470,20 @@ nex * nex_creator::mk_div(const nex* a, const nex* b) {
return mk_div_by_mul(a, to_mul(b)); return mk_div_by_mul(a, to_mul(b));
} }
nex* nex_creator::simplify(nex* e) {
if (e->is_mul())
return simplify_mul(to_mul(e));
if (e->is_sum())
return simplify_sum(to_sum(e));
return e;
}
bool nex_creator::is_simplified(const nex *e) const
{
if (e->is_mul())
return mul_is_simplified(to_mul(e));
if (e->is_sum())
return sum_is_simplified(to_sum(e));
return true;
}
} }

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

@ -60,17 +60,11 @@ public:
svector<var_weight>& active_vars_weights() { return m_active_vars_weights;} svector<var_weight>& active_vars_weights() { return m_active_vars_weights;}
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);
NOT_IMPLEMENTED_YET();
}
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*);
bool is_simplified(const nex *e) {
NOT_IMPLEMENTED_YET();
}
bool less_than(lpvar j, lpvar k) const{ bool less_than(lpvar j, lpvar k) const{
unsigned wj = (unsigned)m_active_vars_weights[j]; unsigned wj = (unsigned)m_active_vars_weights[j];
unsigned wk = (unsigned)m_active_vars_weights[k]; unsigned wk = (unsigned)m_active_vars_weights[k];
@ -210,11 +204,12 @@ public:
nex * simplify_mul(nex_mul *e); nex * simplify_mul(nex_mul *e);
bool is_sorted(const nex_mul * e) const; bool is_sorted(const nex_mul * e) const;
bool mul_is_simplified(const nex_mul*e ) const;
nex* simplify_sum(nex_sum *e); nex* simplify_sum(nex_sum *e);
bool sum_is_simplified(nex_sum* e) const; bool is_simplified(const nex *e) const;
bool sum_is_simplified(const nex_sum* e) const;
bool mul_is_simplified(const nex_mul*e ) const;
void mul_to_powers(vector<nex_pow>& children); void mul_to_powers(vector<nex_pow>& children);
@ -230,7 +225,7 @@ public:
bool sum_simplify_lt(const nex* a, const nex* b); bool sum_simplify_lt(const nex* a, const nex* b);
bool mul_simplify_lt(const nex_mul* a, const nex_mul* b); bool less_than_on_mul(const nex_mul* a, const nex_mul* b);
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);
}; };
} }

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

@ -86,6 +86,9 @@ void test_simplify() {
enable_trace("nla_cn"); enable_trace("nla_cn");
enable_trace("nla_cn_details"); enable_trace("nla_cn_details");
nex_creator & r = cn.get_nex_creator(); nex_creator & r = cn.get_nex_creator();
r.active_vars_weights().resize(3);
for (unsigned j = 0; j < r.active_vars_weights().size(); j++)
r.active_vars_weights()[j] = static_cast<var_weight>(5 - j);
nex_var* a = r.mk_var(0); nex_var* a = r.mk_var(0);
nex_var* b = r.mk_var(1); nex_var* b = r.mk_var(1);
nex_var* c = r.mk_var(2); nex_var* c = r.mk_var(2);