mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

call power of intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-14 18:17:38 -07:00
parent fbdc28f2ae
commit dd4dc1ad14
3 changed files with 36 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -144,32 +144,42 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) {
m_intervals.set_upper_is_inf(a, false);
}
interv horner::power_with_deps(const interv& a, unsigned n) {
interv b;
interval_deps_combine_rule combine_rule;
m_intervals.power(a, n, b, combine_rule);
TRACE("nla_horner_details", tout << "power of "; m_intervals.display(tout, a) << " = ";
m_intervals.display(tout, b) << "\n";);
return b;
}
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();
if (power != 1) {
return power_with_deps(a, power);
}
return a;
case expr_type::SUM:
{
interv b = interval_of_sum_with_deps(to_sum(e));
if (power != 1)
NOT_IMPLEMENTED_YET();
return power_with_deps(b, power);
return b;
}
case expr_type::MUL:
{
interv b = interval_of_mul_with_deps(to_mul(e));
if (power != 1)
NOT_IMPLEMENTED_YET();
return power_with_deps(b, power);;
return b;
}
case expr_type::VAR:
set_var_interval_with_deps(to_var(e)->var(), a);
if (power != 1)
NOT_IMPLEMENTED_YET();
return power_with_deps(a, power);;
return a;
default:
TRACE("nla_horner_details", tout << e->type() << "\n";);
@ -189,17 +199,17 @@ interv horner::interval_of_expr(const nex* e, unsigned power) {
{
interv b = interval_of_sum(to_sum(e));
if (power != 1) {
NOT_IMPLEMENTED_YET();
return power_with_deps(b, power);;
}
return b;
}
case expr_type::MUL:
{
interv b = interval_of_mul(to_mul(e));
if (power != 1) {
NOT_IMPLEMENTED_YET();
}
return b;
if (power != 1) {
return power_with_deps(b, power);;
}
return b;
}
case expr_type::VAR:
set_var_interval(to_var(e)->var(), a);
@ -210,7 +220,7 @@ interv horner::interval_of_expr(const nex* e, unsigned power) {
return interv();
}
if (power != 1) {
NOT_IMPLEMENTED_YET();
return power_with_deps(a, power);;
}
return a;
}
@ -234,7 +244,7 @@ interv horner::interval_of_mul_with_deps(const nex_mul* e) {
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);
m_intervals.mul_two_intervals(a, b, c, comb_rule);
TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c););
m_intervals.combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
@ -266,7 +276,7 @@ interv horner::interval_of_mul(const nex_mul* e) {
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);
m_intervals.mul_two_intervals(a, b, c, comb_rule);
TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c););
m_intervals.combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
@ -499,7 +509,7 @@ bool horner::interval_from_term(const nex* e, interv & i) const {
set_var_interval(j, i);
interv bi;
m_intervals.mul(a, i, bi, 22);
m_intervals.mul_no_deps(a, i, bi);
m_intervals.add(b, bi);
m_intervals.set(i, bi, 44);

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

@ -68,5 +68,6 @@ public:
bool has_inf_interval(const nex* ) const;
bool mul_has_inf_interval(const nex_mul* ) const;
bool check_cross_nested_expr(const nex*);
interv power_with_deps(const interv& a, unsigned);
}; // end of horner
}

13
src/math/lp/nla_intervals.h
View file

@ -164,7 +164,7 @@ public:
}
}
void mul(const rational& r, const interval& a, interval& b, int foo) const {
void mul_no_deps(const rational& r, const interval& a, interval& b) const {
m_imanager.mul(r.to_mpq(), a, b);
}
@ -190,12 +190,21 @@ public:
m_imanager.set(a, b);
}
void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
void mul_two_intervals(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
SASSERT(&a != &i && &b != &i);
m_config.add_deps(a, b, deps, i);
}
void power(interval const & a, unsigned n, interval & b, interval_deps_combine_rule & b_deps) {
m_imanager.power(a, n, b, b_deps);
}
void power(interval const & a, unsigned n, interval & b) {
m_imanager.power(a, n, b);
}
void update_lower_for_intersection(const interval& a, const interval& b, interval & i) const {
if (a.m_lower_inf) {
if (b.m_lower_inf)