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

fix interval calculations to accomodate changes in nex expressions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2019-10-14 17:24:52 -07:00 • committed by Lev Nachmanson
parent dc39ef761c
commit fbdc28f2ae
4 changed files with 82 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,6 +63,8 @@ public:
m_e = e;
#ifdef Z3DEBUG
m_e_clone = m_nex_creator.clone(m_e);
TRACE("nla_cn", tout << "m_e_clone = " << * m_e_clone << "\n";);
#endif
vector<nex**> front;
explore_expr_on_front_elem(&m_e, front);
@ -254,7 +256,7 @@ public:
TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
m_done = m_call_on_result(m_e) || ++m_reported > 100;
#ifdef Z3DEBUG
TRACE("nla_cn", tout << "m_e_clone" << *m_e_clone << "\n";);
TRACE("nla_cn", tout << "m_e_clone " << *m_e_clone << "\n";);
SASSERT(nex_creator::equal(m_e, m_e_clone));
#endif
} else {
@ -280,7 +282,11 @@ public:
return;
TRACE("nla_cn", tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
if (front.empty()) {
TRACE("nla_cn", tout << "got the cn form: =" << *m_e << ", clone = " << *m_e_clone << "\n";);
m_done = m_call_on_result(m_e) || ++m_reported > 100;
#ifdef Z3DEBUG
SASSERT(nex_creator::equal(m_e, m_e_clone));
#endif
return;
}
auto n = pop_front(front);

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

@ -71,16 +71,16 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
bool horner::check_cross_nested_expr(const nex* n) {
TRACE("nla_horner", tout << "cross-nested n = " << *n << "\n";);
TRACE("nla_horner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
c().lp_settings().stats().m_cross_nested_forms++;
auto i = interval_of_expr(n);
auto i = interval_of_expr(n, 1);
TRACE("nla_horner", tout << "callback n = " << *n << "\ni="; m_intervals.display(tout, i) << "\n";);
if (!m_intervals.separated_from_zero(i)) {
m_intervals.reset();
return false;
}
auto id = interval_of_expr_with_deps(n);
auto id = interval_of_expr_with_deps(n, 1);
TRACE("nla_horner", tout << "conflict: id = "; m_intervals.display(tout, id ) << *n << "\n";);
m_intervals.check_interval_for_conflict_on_zero(id);
m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
@ -144,18 +144,32 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) {
m_intervals.set_upper_is_inf(a, false);
}
interv horner::interval_of_expr_with_deps(const nex* e) {
interv horner::interval_of_expr_with_deps(const nex* e, unsigned power) {
interv a;
switch (e->type()) {
case expr_type::SCALAR:
set_interval_for_scalar(a, to_scalar(e)->value());
if (power != 1)
NOT_IMPLEMENTED_YET();
return a;
case expr_type::SUM:
return interval_of_sum_with_deps(to_sum(e));
{
interv b = interval_of_sum_with_deps(to_sum(e));
if (power != 1)
NOT_IMPLEMENTED_YET();
return b;
}
case expr_type::MUL:
return interval_of_mul_with_deps(to_mul(e));
case expr_type::VAR:
{
interv b = interval_of_mul_with_deps(to_mul(e));
if (power != 1)
NOT_IMPLEMENTED_YET();
return b;
}
case expr_type::VAR:
set_var_interval_with_deps(to_var(e)->var(), a);
if (power != 1)
NOT_IMPLEMENTED_YET();
return a;
default:
TRACE("nla_horner_details", tout << e->type() << "\n";);
@ -164,43 +178,60 @@ interv horner::interval_of_expr_with_deps(const nex* e) {
}
}
interv horner::interval_of_expr(const nex* e) {
interv horner::interval_of_expr(const nex* e, unsigned power) {
TRACE("nla_horner_details", tout << "e = " << *e << "\n";);
interv a;
switch (e->type()) {
case expr_type::SCALAR:
set_interval_for_scalar(a, to_scalar(e)->value());
return a;
break;
case expr_type::SUM:
return interval_of_sum(to_sum(e));
{
interv b = interval_of_sum(to_sum(e));
if (power != 1) {
NOT_IMPLEMENTED_YET();
}
return b;
}
case expr_type::MUL:
return interval_of_mul(to_mul(e));
{
interv b = interval_of_mul(to_mul(e));
if (power != 1) {
NOT_IMPLEMENTED_YET();
}
return b;
}
case expr_type::VAR:
set_var_interval(to_var(e)->var(), a);
return a;
break;
default:
TRACE("nla_horner_details", tout << e->type() << "\n";);
SASSERT(false);
return interv();
}
if (power != 1) {
NOT_IMPLEMENTED_YET();
}
return a;
}
interv horner::interval_of_mul_with_deps(const nex_mul* e) {
const nex * zero_interval_child = get_zero_interval_child(e);
if (zero_interval_child) {
interv a = interval_of_expr_with_deps(zero_interval_child);
interv a = interval_of_expr_with_deps(zero_interval_child, 1);
m_intervals.set_zero_interval_deps_for_mult(a);
TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); );
return a;
}
SASSERT(e->is_mul());
auto & es = to_mul(e)->children();
interv a = interval_of_expr_with_deps(es[0].e());
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr_with_deps(es[k].e());
TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
interv a;
set_interval_for_scalar(a, e->coeff());
TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); );
for (const auto & ep : *e) {
interv b = interval_of_expr_with_deps(ep.e(), ep.pow());
TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); );
interv c;
interval_deps_combine_rule comb_rule;
m_intervals.mul(a, b, c, comb_rule);
@ -217,21 +248,22 @@ interv horner::interval_of_mul_with_deps(const nex_mul* e) {
}
interv horner::interval_of_mul(const nex_mul* e) {
TRACE("nla_horner_details", tout << "e = " << *e << "\n";);
const nex * zero_interval_child = get_zero_interval_child(e);
if (zero_interval_child) {
interv a = interval_of_expr(zero_interval_child);
interv a = interval_of_expr(zero_interval_child, 1);
m_intervals.set_zero_interval_deps_for_mult(a);
TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); );
return a;
}
SASSERT(e->is_mul());
auto & es = to_mul(e)->children();
interv a = interval_of_expr(es[0].e());
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k].e());
TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
interv a;
set_interval_for_scalar(a, e->coeff());
TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); );
for (const auto & ep : *e) {
interv b = interval_of_expr(ep.e(), ep.pow() );
TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); );
interv c;
interval_deps_combine_rule comb_rule;
m_intervals.mul(a, b, c, comb_rule);
@ -248,38 +280,20 @@ interv horner::interval_of_mul(const nex_mul* e) {
}
void horner::add_mul_to_vector(const nex_mul* e, vector<std::pair<rational, lpvar>> &v) {
void horner::add_mul_of_degree_one_to_vector(const nex_mul* e, vector<std::pair<rational, lpvar>> &v) {
TRACE("nla_horner_details", tout << *e << "\n";);
SASSERT(e->size() > 0);
if (e->size() == 1) {
add_linear_to_vector(e->children().begin()->e(), v);
return;
}
rational r;
lpvar j = -1;
for (const auto & p: e->children()) {
const nex * c = p.e();
switch (c->type()) {
case expr_type::SCALAR:
r = to_scalar(c)->value();
break;
case expr_type::VAR:
j = to_var(c)->var();
break;
default:
TRACE("nla_horner_details", tout << e->type() << "\n";);
SASSERT(false);
}
}
SASSERT((j + 1) && !(r.is_zero() || r.is_one()));
v.push_back(std::make_pair(r, j));
SASSERT(e->size() == 1);
SASSERT((*e)[0].pow() == 1);
const nex *ev = (*e)[0].e();
lpvar j = to_var(ev)->var();
v.push_back(std::make_pair(e->coeff(), j));
}
void horner::add_linear_to_vector(const nex* e, vector<std::pair<rational, lpvar>> &v) {
TRACE("nla_horner_details", tout << *e << "\n";);
switch (e->type()) {
case expr_type::MUL:
add_mul_to_vector(to_mul(e), v);
add_mul_of_degree_one_to_vector(to_mul(e), v);
break;
case expr_type::VAR:
v.push_back(std::make_pair(rational(1), to_var(e)->var()));
@ -402,10 +416,10 @@ interv horner::interval_of_sum_no_term_with_deps(const nex_sum* e) {
return interv();
}
auto & es = e->children();
interv a = interval_of_expr_with_deps(es[0]);
interv a = interval_of_expr_with_deps(es[0], 1);
for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";);
interv b = interval_of_expr_with_deps(es[k]);
interv b = interval_of_expr_with_deps(es[k], 1);
interv c;
interval_deps_combine_rule combine_rule;
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
@ -426,10 +440,10 @@ interv horner::interval_of_sum_no_term(const nex_sum* e) {
return interv();
}
auto & es = e->children();
interv a = interval_of_expr(es[0]);
interv a = interval_of_expr(es[0], 1);
for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << *es[k] << "\n";);
interv b = interval_of_expr(es[k]);
interv b = interval_of_expr(es[k], 1);
interv c;
interval_deps_combine_rule combine_rule;
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);

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

@ -39,8 +39,8 @@ public:
template <typename T> // T has an iterator of (coeff(), var())
bool lemmas_on_row(const T&);
template <typename T> bool row_is_interesting(const T&) const;
intervals::interval interval_of_expr_with_deps(const nex* e);
intervals::interval interval_of_expr(const nex* e);
intervals::interval interval_of_expr_with_deps(const nex* e, unsigned power);
intervals::interval interval_of_expr(const nex* e, unsigned power);
intervals::interval interval_of_sum(const nex_sum*);
intervals::interval interval_of_sum_no_term(const nex_sum*);
intervals::interval interval_of_mul(const nex_mul*);
@ -60,7 +60,7 @@ public:
lpvar find_term_column(const lp::lar_term &, rational & a) const;
static lp::lar_term expression_to_normalized_term(const nex_sum*, rational& a, rational & b);
static void add_linear_to_vector(const nex*, vector<std::pair<rational, lpvar>> &);
static void add_mul_to_vector(const nex_mul*, vector<std::pair<rational, lpvar>> &);
static void add_mul_of_degree_one_to_vector(const nex_mul*, vector<std::pair<rational, lpvar>> &);
bool interval_from_term_with_deps(const nex* e, interv&) const;
const nex* get_zero_interval_child(const nex_mul*) const;
const nex* get_inf_interval_child(const nex_sum*) const;

2
src/math/lp/nex_creator.cpp
View file

@ -266,6 +266,8 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
bool nex_creator::lt(const nex* a, const nex* b) const {
TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";);
if (a == b)
return false;
bool ret;
switch (a->type()) {
case expr_type::VAR: