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

save

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-02 12:52:25 -07:00
parent e3a8522885
commit 7bac714762
2 changed files with 38 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -235,9 +235,14 @@ intervals::interval horner::interval_of_expr(const nex& e) {
template <typename T> template <typename T>
interv horner::interval_of_mul(const vector<nla_expr<T>>& es) { interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
interv a = interval_of_expr(es[0]); interv a = interval_of_expr(es[0]);
if (m_intervals.is_zero(a)) {
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
return a;
}
for (unsigned k = 1; k < es.size(); k++) { for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k]); interv b = interval_of_expr(es[k]);
if (m_intervals.is_zero(b)) { if (m_intervals.is_zero(b)) {
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, b); tout << "\n";);
return b; return b;
} }
interv c; interv c;
@ -245,29 +250,49 @@ interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
m_intervals.mul(a, b, c, deps); m_intervals.mul(a, b, c, deps);
m_intervals.set(a, c); m_intervals.set(a, c);
m_intervals.add_deps(a, b, deps, a); m_intervals.add_deps(a, b, deps, a);
if (m_intervals.is_zero(a))
return a;
} }
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
return a; return a;
} }
template <typename T> template <typename T>
interv horner::interval_of_sum(const vector<nla_expr<T>>& es) { interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
TRACE("nla_cn", tout << "es[0]= " << es[0] << "\n";);
interv a = interval_of_expr(es[0]); interv a = interval_of_expr(es[0]);
for (unsigned k = 1; k < es.size(); k++) { TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
interv b = interval_of_expr(es[k]); if (m_intervals.is_inf(a)) {
interv c; return a;
m_intervals.add(a, b, c);
m_intervals.set(a, c);
} }
for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_cn", tout << "es[k]= " << es[k] << "\n";);
interv b = interval_of_expr(es[k]);
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(b)) {
return a;
}
interv c;
interval_deps deps;
m_intervals.add(a, b, c, deps);
m_intervals.set(a, c);
m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(a)) {
return a;
}
}
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
return a; return a;
} }
// sets the dependencies also // sets the dependencies also
void horner::set_var_interval(lpvar v, interv& b) { void horner::set_var_interval(lpvar v, interv& b) {
m_intervals.set_var_interval_with_deps(v, b); m_intervals.set_var_interval_with_deps(v, b);
TRACE("nla_cn", tout << "v = "; print_var(v, tout); tout << "\n";);
} }
void horner::check_interval_for_conflict(const intervals::interval&) { void horner::check_interval_for_conflict(const intervals::interval& i) {
TRACE("nla_cn", tout << "interval = "; m_intervals.display(tout, i); );
SASSERT(false); SASSERT(false);
} }
} }

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

@ -96,10 +96,12 @@ class intervals : common {
bool upper_is_open(interval const & a) const { return a.m_upper_open; } bool upper_is_open(interval const & a) const { return a.m_upper_open; }
bool lower_is_inf(interval const & a) const { return a.m_lower_inf; } bool lower_is_inf(interval const & a) const { return a.m_lower_inf; }
bool upper_is_inf(interval const & a) const { return a.m_upper_inf; } bool upper_is_inf(interval const & a) const { return a.m_upper_inf; }
bool is_inf(interval const & a) const { return upper_is_inf(a) && lower_is_inf(a); }
bool is_zero(interval const & a) const { bool is_zero(interval const & a) const {
return unsynch_mpq_manager::is_zero(a.m_lower) return unsynch_mpq_manager::is_zero(a.m_lower)
&& unsynch_mpq_manager::is_zero(a.m_upper); } && unsynch_mpq_manager::is_zero(a.m_upper); }
// Setters // Setters
void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); } void set_lower(interval & a, mpq const & n) const { m_manager.set(a.m_lower, n); }
void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); } void set_upper(interval & a, mpq const & n) const { m_manager.set(a.m_upper, n); }
@ -178,11 +180,13 @@ public:
bool is_zero(const interval& a) const { return m_config.is_zero(a); } bool is_zero(const interval& a) const { return m_config.is_zero(a); }
void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); } void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); } void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
void add(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.add(a, b, c, deps); }
void set(interval& a, const interval& b) { m_imanager.set(a, b); } void set(interval& a, const interval& b) { m_imanager.set(a, b); }
void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); } void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); }
void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
m_config.add_deps(a, b, deps, i); m_config.add_deps(a, b, deps, i);
} }
void set_var_interval_with_deps(lpvar, interval &); void set_var_interval_with_deps(lpvar, interval &);
bool is_inf(const interval& i) const { return m_config.is_inf(i); }
}; // end of intervals }; // end of intervals
} // end of namespace nla } // end of namespace nla