mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

add comments and more efficient code in cross_nested

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-23 10:36:01 -07:00
parent 84e9e4ca9a
commit ba2dbabe21
2 changed files with 29 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -30,7 +30,7 @@ public:
void run() { void run() {
vector<nex*> front; vector<nex*> front;
explore_of_expr_on_front_elem(&m_e, front, true); // true for trivial form - no change explore_expr_on_front_elem(&m_e, front, true); // true for trivial form - no change
} }
static nex* pop_back(vector<nex*>& front) { static nex* pop_back(vector<nex*>& front) {
@ -69,6 +69,18 @@ public:
return !f.children().empty(); return !f.children().empty();
} }
static bool has_common_factor(const nex& c) {
TRACE("nla_cn", tout << "c=" << c << "\n";);
SASSERT(c.is_sum());
unsigned size = c.children().size();
for(const auto & p : get_mult_occurences(c)) {
if (p.second.m_occs == size) {
return true;
}
}
return false;
}
bool proceed_with_common_factor(nex* c, vector<nex*>& front, const std::unordered_map<lpvar, occ> & occurences) { bool proceed_with_common_factor(nex* c, vector<nex*>& front, const std::unordered_map<lpvar, occ> & occurences) {
TRACE("nla_cn", tout << "c=" << *c << "\n";); TRACE("nla_cn", tout << "c=" << *c << "\n";);
SASSERT(c->is_sum()); SASSERT(c->is_sum());
@ -80,7 +92,7 @@ public:
f.simplify(); f.simplify();
* c = nex::mul(f, *c); * c = nex::mul(f, *c);
TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";); TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";);
explore_of_expr_on_front_elem(&(c->children()[1]), front, false); explore_expr_on_front_elem(&(c->children()[1]), front, false);
return true; return true;
} }
@ -102,7 +114,7 @@ public:
*(front[i]) = copy[i]; *(front[i]) = copy[i];
} }
void explore_of_expr_on_front_elem_occs(nex* c, vector<nex*>& front, const std::unordered_map<lpvar, occ> & occurences) { void explore_expr_on_front_elem_occs(nex* c, vector<nex*>& front, const std::unordered_map<lpvar, occ> & occurences) {
if (proceed_with_common_factor(c, front, occurences)) if (proceed_with_common_factor(c, front, occurences))
return; return;
TRACE("nla_cn", tout << "save c=" << *c << "; front:"; print_vector_of_ptrs(front, tout) << "\n";); TRACE("nla_cn", tout << "save c=" << *c << "; front:"; print_vector_of_ptrs(front, tout) << "\n";);
@ -130,7 +142,7 @@ public:
return out; return out;
} }
void explore_of_expr_on_front_elem(nex* c, vector<nex*>& front, bool trivial_form) { void explore_expr_on_front_elem(nex* c, vector<nex*>& front, bool trivial_form) {
SASSERT(c->is_sum()); SASSERT(c->is_sum());
auto occurences = get_mult_occurences(*c); auto occurences = get_mult_occurences(*c);
TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences="; TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences=";
@ -144,10 +156,10 @@ public:
m_call_on_result(m_e); m_call_on_result(m_e);
} else { } else {
nex* c = pop_back(front); nex* c = pop_back(front);
explore_of_expr_on_front_elem(c, front, trivial_form); explore_expr_on_front_elem(c, front, trivial_form);
} }
} else { } else {
explore_of_expr_on_front_elem_occs(c, front, occurences); explore_expr_on_front_elem_occs(c, front, occurences);
} }
} }
static char ch(unsigned j) { static char ch(unsigned j) {
@ -161,7 +173,7 @@ public:
TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";); TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
SASSERT(front.size()); SASSERT(front.size());
nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";); nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";);
explore_of_expr_on_front_elem(n, front, false); // we got a non-trivial_form explore_expr_on_front_elem(n, front, false); // we got a non-trivial_form
} }
static void process_var_occurences(lpvar j, std::unordered_map<lpvar, occ>& occurences) { static void process_var_occurences(lpvar j, std::unordered_map<lpvar, occ>& occurences) {
auto it = occurences.find(j); auto it = occurences.find(j);
@ -303,8 +315,15 @@ public:
if (!e.is_sum()) return false; if (!e.is_sum()) return false;
nex a, b; nex a, b;
pre_split(e, j, a, b); pre_split(e, j, a, b);
nex f; /*
if (extract_common_factor(&a, f, get_mult_occurences(a))) When we have e without a non-trivial common factor then
there is a variable j such that e = jP + Q, where Q has all members
of e that do not have j as a factor, and
P also does not have a non-trivial common factor. It is enough
to explore only such variables to create all cross-nested forms.
*/
if (has_common_factor(a))
return false; return false;
update_front_with_split(e, j, front, a, b); update_front_with_split(e, j, front, a, b);
return true; return true;

2
src/math/lp/nla_expr.h
View file

@ -155,7 +155,7 @@ public:
case expr_type::MUL: case expr_type::MUL:
return print_mul(out); return print_mul(out);
case expr_type::VAR: case expr_type::VAR:
out << (char)('a'+ m_j); out << 'v' << m_j;
return out; return out;
case expr_type::SCALAR: case expr_type::SCALAR:
out << m_v; out << m_v;