mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

persist

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-12 11:53:25 -07:00
parent 92769469df
commit 24d70abfd8
2 changed files with 180 additions and 164 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -23,193 +23,209 @@
namespace nla { namespace nla {
class cross_nested { class cross_nested {
typedef nla_expr<rational> nex; typedef nla_expr<rational> nex;
std::function<void (unsigned)> m_call_on_result; nex& m_e;
std::function<void (const nex&)> m_call_on_result;
public: public:
cross_nested(std::function<void (unsigned)> call_on_result): m_call_on_result(call_on_result) {} cross_nested(nex &e, std::function<void (const nex&)> call_on_result): m_e(e), m_call_on_result(call_on_result) {}
void cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& front) { void run() {
vector<nex*> front;
cross_nested_of_expr_on_front_elem(&m_e, front);
}
static nex* pop_back(vector<nex*>& front) {
nex* c = front.back();
front.pop_back();
return c;
}
void cross_nested_of_expr_on_front_elem(nex* c, vector<nex*>& front) {
SASSERT(c->is_sum()); SASSERT(c->is_sum());
vector<lpvar> occurences = get_mult_occurences(*c); vector<lpvar> occurences = get_mult_occurences(*c);
TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\noccurences="; print_vector(occurences, tout) << "\nfront:"; print_vector_of_ptrs(front, tout) << "\n";); TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << "\noccurences="; print_vector(occurences, tout) << "\nfront:"; print_vector_of_ptrs(front, tout) << "\n";);
if (occurences.empty()) { if (occurences.empty()) {
if(front.empty()) { if(front.empty()) {
TRACE("nla_cn_cn", tout << "got the cn form: e=" << e << "\n";); TRACE("nla_cn_cn", tout << "got the cn form: m_e=" << m_e << "\n";);
SASSERT(!can_be_cross_nested_more(e)); SASSERT(!can_be_cross_nested_more(m_e));
auto i = interval_of_expr(e); m_call_on_result(m_e);
m_intervals.check_interval_for_conflict_on_zero(i);
} else { } else {
nex* c = pop_back(front); nex* c = pop_back(front);
cross_nested_of_expr_on_front_elem(e, c, front); cross_nested_of_expr_on_front_elem(c, front);
} }
} else { } else {
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";);
nex copy_of_c = *c; nex copy_of_c = *c;
vector<nex> copy_of_front;
for (nex* n: front)
copy_of_front.push_back(*n);
for(lpvar j : occurences) { for(lpvar j : occurences) {
cross_nested_of_expr_on_sum_and_var(e, c, j, front); cross_nested_of_expr_on_sum_and_var(c, j, front);
*c = copy_of_c; *c = copy_of_c;
TRACE("nla_cn", tout << "restore c=" << *c << ", e=" << e << "\n";); TRACE("nla_cn", tout << "restore c=" << *c << ", m_e=" << m_e << "\n";);
for (unsigned i = 0; i < front.size(); i++)
*(front[i]) = copy_of_front[i];
} }
} }
TRACE("nla_cn", tout << "exit\n";); TRACE("nla_cn", tout << "exit\n";);
} }
// e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form // e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form
void horner::cross_nested_of_expr_on_sum_and_var(nex& e, nex* c, lpvar j, vector<nex*>& front) { void cross_nested_of_expr_on_sum_and_var(nex* c, lpvar j, vector<nex*> front) {
TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\nj = v" << j << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";); TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << "\nj = v" << j << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
split_with_var(*c, j, front); split_with_var(*c, j, front);
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";);
do { do {
nex* n = pop_back(front); nex* n = pop_back(front);
cross_nested_of_expr_on_front_elem(e, n, front); cross_nested_of_expr_on_front_elem(n, front);
} while (!front.empty()); } while (!front.empty());
}
void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
if (seen.find(j) != seen.end()) return;
seen.insert(j);
auto it = occurences.find(j);
if (it == occurences.end())
occurences[j] = 1;
else
it->second ++;
}
void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
SASSERT(e.type() == expr_type::MUL);
for (const auto & ce : e.children()) {
if (ce.type() == expr_type::VAR) {
process_var_occurences(ce.var(), seen, occurences);
} else if (ce.type() == expr_type::MUL){
process_mul_occurences(ce, seen, occurences);
}
} }
} void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) const {
if (seen.find(j) != seen.end()) return;
seen.insert(j);
// j -> the number of expressions j appears in as a multiplier auto it = occurences.find(j);
vector<lpvar> horner::get_mult_occurences(const nex& e) const { if (it == occurences.end())
std::unordered_map<lpvar, unsigned> occurences; occurences[j] = 1;
SASSERT(e.type() == expr_type::SUM); else
for (const auto & ce : e.children()) { it->second ++;
std::unordered_set<lpvar> seen; }
if (ce.type() == expr_type::MUL) {
for (const auto & cce : ce.children()) { void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) const {
if (cce.type() == expr_type::VAR) { SASSERT(e.type() == expr_type::MUL);
process_var_occurences(cce.var(), seen, occurences); for (const auto & ce : e.children()) {
} else if (cce.type() == expr_type::MUL) { if (ce.type() == expr_type::VAR) {
process_mul_occurences(cce, seen, occurences); process_var_occurences(ce.var(), seen, occurences);
} else { } else if (ce.type() == expr_type::MUL){
continue; process_mul_occurences(ce, seen, occurences);
} }
}
} else if (ce.type() == expr_type::VAR) {
process_var_occurences(ce.var(), seen, occurences);
} }
} }
TRACE("nla_cn_details",
tout << "{";
for(auto p: occurences) { // j -> the number of expressions j appears in as a multiplier
tout << "(v" << p.first << "->" << p.second << ")"; vector<lpvar> get_mult_occurences(const nex& e) const {
} std::unordered_map<lpvar, unsigned> occurences;
tout << "}" << std::endl;); SASSERT(e.type() == expr_type::SUM);
vector<lpvar> r; for (const auto & ce : e.children()) {
for(auto p: occurences) { std::unordered_set<lpvar> seen;
if (p.second > 1) if (ce.type() == expr_type::MUL) {
r.push_back(p.first); for (const auto & cce : ce.children()) {
} if (cce.type() == expr_type::VAR) {
return r; process_var_occurences(cce.var(), seen, occurences);
} } else if (cce.type() == expr_type::MUL) {
bool horner::can_be_cross_nested_more(const nex& e) const { process_mul_occurences(cce, seen, occurences);
switch (e.type()) { } else {
case expr_type::SCALAR: continue;
return false; }
case expr_type::SUM: { }
return !get_mult_occurences(e).empty(); } else if (ce.type() == expr_type::VAR) {
} process_var_occurences(ce.var(), seen, occurences);
case expr_type::MUL:
{
for (const auto & c: e.children()) {
if (can_be_cross_nested_more(c))
return true;
} }
}
TRACE("nla_cn_details",
tout << "{";
for(auto p: occurences) {
tout << "(v" << p.first << "->" << p.second << ")";
}
tout << "}" << std::endl;);
vector<lpvar> r;
for(auto p: occurences) {
if (p.second > 1)
r.push_back(p.first);
}
return r;
}
bool 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; return false;
} }
case expr_type::VAR:
return false;
default:
TRACE("nla_cn_details", tout << e.type() << "\n";);
SASSERT(false);
return false;
} }
} void 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()) return;
return; nex a, b;
nex a, b; for (const nex & ce: e.children()) {
for (const nex & ce: e.children()) { if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) {
if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) { a.add_child(ce / j);
a.add_child(ce / j); } else {
} else { b.add_child(ce);
b.add_child(ce); }
} }
} a.type() = expr_type::SUM;
a.type() = expr_type::SUM; TRACE("nla_cn_details", tout << "a = " << a << "\n";);
TRACE("nla_cn_details", tout << "a = " << a << "\n";); SASSERT(a.children().size() >= 2);
SASSERT(a.children().size() >= 2);
if (b.children().size() == 1) { if (b.children().size() == 1) {
nex t = b.children()[0]; nex t = b.children()[0];
b = t; b = t;
} else if (b.children().size() > 1) { } else if (b.children().size() > 1) {
b.type() = expr_type::SUM; b.type() = expr_type::SUM;
}
if (b.is_undef()) {
SASSERT(b.children().size() == 0);
e = nex(expr_type::MUL);
e.add_child(nex::var(j));
e.add_child(a);
if (a.size() > 1) {
front.push_back(&e.children().back());
TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
} }
if (b.is_undef()) {
SASSERT(b.children().size() == 0);
e = nex(expr_type::MUL);
e.add_child(nex::var(j));
e.add_child(a);
if (a.size() > 1) {
front.push_back(&e.children().back());
TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
}
} else { } else {
TRACE("nla_cn_details", tout << "b = " << b << "\n";); TRACE("nla_cn_details", tout << "b = " << b << "\n";);
e = nex::sum(nex::mul(nex::var(j), a), b); e = nex::sum(nex::mul(nex::var(j), a), b);
if (a.is_sum()) { if (a.is_sum()) {
front.push_back(&(e.children()[0].children()[1])); front.push_back(&(e.children()[0].children()[1]));
TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";); TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";);
} }
if (b.is_sum()) { if (b.is_sum()) {
front.push_back(&(e.children()[1])); front.push_back(&(e.children()[1]));
TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";); TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";);
}
} }
} }
} std::set<lpvar> get_vars_of_expr(const nex &e ) const {
std::set<lpvar> horner::get_vars_of_expr(const nex &e ) const { std::set<lpvar> r;
std::set<lpvar> r; switch (e.type()) {
switch (e.type()) { case expr_type::SCALAR:
case expr_type::SCALAR: return r;
return r; case expr_type::SUM:
case expr_type::SUM: case expr_type::MUL:
case expr_type::MUL: {
{ for (const auto & c: e.children())
for (const auto & c: e.children()) for ( lpvar j : get_vars_of_expr(c))
for ( lpvar j : get_vars_of_expr(c)) r.insert(j);
r.insert(j); }
return r;
case expr_type::VAR:
r.insert(e.var());
return r;
default:
TRACE("nla_cn_details", tout << e.type() << "\n";);
SASSERT(false);
return r;
} }
return r;
case expr_type::VAR:
r.insert(e.var());
return r;
default:
TRACE("nla_cn_details", tout << e.type() << "\n";);
SASSERT(false);
return r;
}
} }
}; };
} }

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

@ -40,16 +40,13 @@ bool horner::row_is_interesting(const T& row) const {
void horner::lemmas_on_expr(nex& e) { void horner::lemmas_on_expr(nex& e) {
TRACE("nla_cn", tout << "e = " << e << "\n";); TRACE("nla_cn", tout << "e = " << e << "\n";);
TRACE("nla_cn_cn", tout << "e = " << e << "\n";); TRACE("nla_cn_cn", tout << "e = " << e << "\n";);
vector<nex*> front; cross_nested cn(e, [this](const nex& n) {
cross_nested_of_expr_on_front_elem(e, &e, front); auto i = interval_of_expr(n);
m_intervals.check_interval_for_conflict_on_zero(i);} );
} }
nex* pop_back(vector<nex*>& front) {
nex* c = front.back();
front.pop_back();
return c;
}
template <typename T> template <typename T>
void horner::lemmas_on_row(const T& row) { void horner::lemmas_on_row(const T& row) {
@ -71,6 +68,8 @@ void horner::horner_lemmas() {
} }
} }
typedef nla_expr<rational> nex;
nex horner::nexvar(lpvar j) const { nex horner::nexvar(lpvar j) const {
// todo: consider deepen the recursion // todo: consider deepen the recursion
if (!c().is_monomial_var(j)) if (!c().is_monomial_var(j))
@ -83,7 +82,6 @@ nex horner::nexvar(lpvar j) const {
return e; return e;
} }
template <typename T> nex horner::create_sum_from_row(const T& row) { template <typename T> nex horner::create_sum_from_row(const T& row) {
TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";); TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
SASSERT(row.size() > 1); SASSERT(row.size() > 1);
@ -191,3 +189,5 @@ void horner::set_var_interval(lpvar v, interv& b) {
} }
} }
auto i = interval_of_expr(e);
m_intervals.check_interval_for_conflict_on_zero(i);