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

make sure that the returned cross nested form is equal to the original

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-19 14:09:41 -07:00
parent 41064f2b25
commit 4e59976c2f
2 changed files with 27 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -43,6 +43,9 @@ class cross_nested {
std::unordered_map<lpvar, unsigned> m_powers; std::unordered_map<lpvar, unsigned> m_powers;
ptr_vector<nex> m_allocated; ptr_vector<nex> m_allocated;
ptr_vector<nex> m_b_split_vec; ptr_vector<nex> m_b_split_vec;
#ifdef Z3DEBUG
nex* m_e_clone;
#endif
public: public:
cross_nested(std::function<bool (const nex*)> call_on_result, cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed): std::function<bool (unsigned)> var_is_fixed):
@ -53,7 +56,10 @@ public:
void run(nex *e) { void run(nex *e) {
m_e = e; m_e = e;
#ifdef Z3DEBUG
m_e_clone = clone(m_e);
m_e_clone = normalize(m_e_clone);
#endif
vector<nex**> front; vector<nex**> front;
explore_expr_on_front_elem(&m_e, front); explore_expr_on_front_elem(&m_e, front);
} }
@ -337,6 +343,13 @@ public:
if(front.empty()) { if(front.empty()) {
TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";); TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
m_done = m_call_on_result(m_e); m_done = m_call_on_result(m_e);
#ifdef Z3DEBUG
nex *ce = clone(m_e);
TRACE("nla_cn", tout << "ce = " << *ce << "\n";);
nex *n = normalize(ce);
TRACE("nla_cn", tout << "n = " << *n << "\nm_e_clone=" << * m_e_clone << "\n";);
SASSERT(*n == *m_e_clone);
#endif
} else { } else {
nex** f = pop_front(front); nex** f = pop_front(front);
explore_expr_on_front_elem(f, front); explore_expr_on_front_elem(f, front);
@ -619,7 +632,9 @@ public:
if ((int)j != sum_j) if ((int)j != sum_j)
b->add_child(a->children()[j]); b->add_child(a->children()[j]);
} }
} b->simplify();
}
TRACE("nla_cn", tout << *r << "\n";);
return normalize_sum(r); return normalize_sum(r);
} }
@ -635,8 +650,9 @@ public:
r = normalize_sum(to_sum(a)); r = normalize_sum(to_sum(a));
} }
r->sort(); r->sort();
return r;
} }
#endif #endif
}; };
} }

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

@ -82,6 +82,9 @@ public:
}; };
#if Z3DEBUG #if Z3DEBUG
bool operator<(const nex& a , const nex& b); bool operator<(const nex& a , const nex& b);
inline bool operator ==(const nex& a , const nex& b) {
return ! (a < b || b < a) ;
}
#endif #endif
std::ostream& operator<<(std::ostream& out, const nex&); std::ostream& operator<<(std::ostream& out, const nex&);
@ -133,6 +136,8 @@ static void promote_children_by_type(ptr_vector<nex> * children, expr_type t) {
} }
} }
} }
children->shrink(children->size() - to_promote.size());
for (nex *e : to_promote) { for (nex *e : to_promote) {
for (nex *ee : *(e->children_ptr())) { for (nex *ee : *(e->children_ptr())) {
@ -218,7 +223,9 @@ public:
} }
void simplify() { void simplify() {
TRACE("nla_cn_details", tout << *this << "\n";);
promote_children_by_type(&m_children, expr_type::MUL); promote_children_by_type(&m_children, expr_type::MUL);
TRACE("nla_cn_details", tout << *this << "\n";);
} }
#ifdef Z3DEBUG #ifdef Z3DEBUG
virtual void sort() { virtual void sort() {
@ -377,7 +384,7 @@ inline bool operator<(const nex& a , const nex& b) {
return to_mul(&a)->children() < to_mul(&b)->children(); return to_mul(&a)->children() < to_mul(&b)->children();
} }
case expr_type::SUM: { case expr_type::SUM: {
return to_mul(&a)->children() < to_mul(&b)->children(); return to_sum(&a)->children() < to_sum(&b)->children();
} }
default: default:
SASSERT(false); SASSERT(false);