mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 01:02:15 +00:00
Code Activity

add some testing to cross nested expessions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-10 16:40:16 -07:00
parent ee4da1affd
commit bab5c2f078
2 changed files with 29 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/math/lp/horner.cpp
View file

@ -65,7 +65,8 @@ void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& fr
if (occurences.empty()) { if (occurences.empty()) {
if(front.empty()) { if(front.empty()) {
TRACE("nla_cn", tout << "empty front: e=" << e << "\n";); TRACE("nla_cn", tout << "got the cn form: e=" << e << "\n";);
SASSERT(!can_be_cross_nested_more(e));
auto i = interval_of_expr(e); auto i = interval_of_expr(e);
m_intervals.check_interval_for_conflict_on_zero(i); m_intervals.check_interval_for_conflict_on_zero(i);
} else { } else {
@ -140,14 +141,11 @@ void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unord
void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) { void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
SASSERT(e.type() == expr_type::MUL); SASSERT(e.type() == expr_type::MUL);
for (const auto & ce : e.children()) { for (const auto & ce : e.children()) {
if (ce.type() == expr_type::SCALAR) { if (ce.type() == expr_type::VAR) {
} else if (ce.type() == expr_type::VAR) {
process_var_occurences(ce.var(), seen, occurences); process_var_occurences(ce.var(), seen, occurences);
} else if (ce.type() == expr_type::MUL){ } else if (ce.type() == expr_type::MUL){
process_mul_occurences(ce, seen, occurences); process_mul_occurences(ce, seen, occurences);
} else { }
SASSERT(false); // unexpected type
}
} }
} }
@ -170,10 +168,6 @@ vector<lpvar> horner::get_mult_occurences(const nex& e) const {
} }
} else if (ce.type() == expr_type::VAR) { } else if (ce.type() == expr_type::VAR) {
process_var_occurences(ce.var(), seen, occurences); process_var_occurences(ce.var(), seen, occurences);
} else if (ce.type() == expr_type::SCALAR) {
} else {
TRACE("nla_cn_details", tout << "unexpected expression ce = " << ce << std::endl;);
SASSERT(false);
} }
} }
TRACE("nla_cn_details", TRACE("nla_cn_details",
@ -189,7 +183,29 @@ vector<lpvar> horner::get_mult_occurences(const nex& e) const {
} }
return r; return r;
} }
bool horner::can_be_cross_nested_more(const nex& e) const {
switch (e.type()) {
case expr_type::SCALAR:
return false;
case expr_type::SUM: {
return !get_mult_occurences(e).empty();
}
case expr_type::MUL:
{
for (const auto & c: e.children()) {
if (can_be_cross_nested_more(c))
return true;
}
return false;
}
case expr_type::VAR:
return false;
default:
TRACE("nla_cn_details", tout << e.type() << "\n";);
SASSERT(false);
return false;
}
}
void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) { void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";); TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";);
if (!e.is_sum()) if (!e.is_sum())

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

@ -52,6 +52,7 @@ public:
void lemmas_on_expr(nex &); void lemmas_on_expr(nex &);
void cross_nested_of_expr(nex& , vector<nex*>& front); void cross_nested_of_expr(nex& , vector<nex*>& front);
void cross_nested_of_expr_on_front_elem(nex& , nex*, vector<nex*>& front); void cross_nested_of_expr_on_front_elem(nex& , nex*, vector<nex*>& front);
void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front); void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front);
bool can_be_cross_nested_more(const nex&) const;
}; // end of horner }; // end of horner
} }