mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

fixes in the interval processing in horner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-23 17:22:37 -07:00
parent ba2dbabe21
commit 2a02d04259
4 changed files with 45 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -39,9 +39,9 @@ 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_horner", tout << "e = " << e << "\n";);
cross_nested cn(e, [this](const nex& n) { cross_nested cn(e, [this](const nex& n) {
TRACE("nla_cn", tout << "callback n = " << n << "\n";); TRACE("nla_horner", tout << "callback n = " << n << "\n";);
auto i = interval_of_expr(n); auto i = interval_of_expr(n);
m_intervals.check_interval_for_conflict_on_zero(i);} ); m_intervals.check_interval_for_conflict_on_zero(i);} );
cn.run(); cn.run();
@ -83,7 +83,7 @@ nex horner::nexvar(lpvar j) const {
} }
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_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
SASSERT(row.size() > 1); SASSERT(row.size() > 1);
nex e(expr_type::SUM); nex e(expr_type::SUM);
for (const auto &p : row) { for (const auto &p : row) {
@ -104,91 +104,93 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) {
interv horner::interval_of_expr(const nex& e) { interv horner::interval_of_expr(const nex& e) {
TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;); TRACE("nla_horner_details", tout << e.type() << " e=" << e << std::endl;);
interv a; interv a;
switch (e.type()) { switch (e.type()) {
case expr_type::SCALAR: case expr_type::SCALAR:
set_interval_for_scalar(a, e.value()); set_interval_for_scalar(a, e.value());
return a; return a;
case expr_type::SUM: case expr_type::SUM:
return interval_of_sum(e.children()); return interval_of_sum(e);
case expr_type::MUL: case expr_type::MUL:
return interval_of_mul(e.children()); return interval_of_mul(e);
case expr_type::VAR: case expr_type::VAR:
set_var_interval(e.var(), a); set_var_interval(e.var(), a);
return a; return a;
default: default:
TRACE("nla_cn_details", tout << e.type() << "\n";); TRACE("nla_horner_details", tout << e.type() << "\n";);
SASSERT(false); SASSERT(false);
return interv(); return interv();
} }
} }
template <typename V> interv horner::interval_of_mul(const nex& e) {
interv horner::interval_of_mul(const V& es) { SASSERT(e.is_mul());
auto & es = e.children();
SASSERT(es.size()); SASSERT(es.size());
TRACE("nla_horner_details", tout << "e=" << e << "\n";);
interv a = interval_of_expr(es[0]); interv a = interval_of_expr(es[0]);
// std::cout << "a" << std::endl; TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
TRACE("nla_cn_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
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]);
interv c; interv c;
interval_deps deps; interval_deps deps;
m_intervals.mul(a, b, c, deps); m_intervals.mul(a, b, c, deps);
m_intervals.set(a, c); TRACE("nla_horner_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";);
m_intervals.add_deps(a, b, deps, a); m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn_details", tout << "es["<< k << "] = " << es[k] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";); m_intervals.set(a, c);
TRACE("nla_horner_details", tout << "es[" << k << "]=" << es[k] << ", a = "; m_intervals.display(tout, a); );
if (m_intervals.is_zero(a)) { if (m_intervals.is_zero(a)) {
TRACE("nla_cn_details", tout << "got zero\n"; ); TRACE("nla_horner_details", tout << "got zero\n"; );
break; break;
} }
} }
TRACE("nla_cn_details", TRACE("nla_horner_details", tout << "e=" << e << "\n";
for (const auto &e : es) { tout << " interv = "; m_intervals.display(tout, a););
tout << "("<< e << ")";
}
tout << " interv a = ";
m_intervals.display(tout, a) << "\n";);
return a; return a;
} }
template <typename V> interv horner::interval_of_sum(const nex& e) {
interv horner::interval_of_sum(const V& es) { TRACE("nla_horner_details", tout << "e=" << e << "\n";);
SASSERT(e.is_sum());
auto & es = e.children();
interv a = interval_of_expr(es[0]); interv a = interval_of_expr(es[0]);
TRACE("nla_cn_details", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";);
if (m_intervals.is_inf(a)) { if (m_intervals.is_inf(a)) {
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " interv = "; m_intervals.display(tout, a););
return a; return a;
} }
for (unsigned k = 1; k < es.size(); k++) { for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_cn_details", tout << "es[" << k << "]= " << es[k] << "\n";); 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]);
if (m_intervals.is_inf(b)) { if (m_intervals.is_inf(b)) {
TRACE("nla_cn_details", tout << "got inf\n";); TRACE("nla_horner_details", tout << "got inf\n";);
return b; return b;
} }
interv c; interv c;
interval_deps deps; interval_deps deps;
TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";); TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
m_intervals.add(a, b, c, deps); m_intervals.add(a, b, c, deps);
TRACE("nla_cn_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";); TRACE("nla_horner_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";);
m_intervals.set(a, c);
TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a); tout << "\n";);
m_intervals.add_deps(a, b, deps, a); m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";); m_intervals.set(a, c);
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a); tout << "\n";);
// m_intervals.add_deps(a, b, deps, a);
TRACE("nla_horner_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(a)) { if (m_intervals.is_inf(a)) {
TRACE("nla_cn_details", tout << "got infinity\n";); TRACE("nla_horner_details", tout << "got infinity\n";);
return a; return a;
} }
} }
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " interv = "; m_intervals.display(tout, a););
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_horner_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b););
TRACE("nla_cn_details", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b)<< '\n';);
} }
} }

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

@ -41,10 +41,8 @@ public:
intervals::interval interval_of_expr(const nex& e); intervals::interval interval_of_expr(const nex& e);
nex nexvar(lpvar j) const; nex nexvar(lpvar j) const;
template <typename V> // V is a vector of expressions intervals::interval interval_of_sum(const nex&);
intervals::interval interval_of_sum(const V&); intervals::interval interval_of_mul(const nex&);
template <typename V> // V is a vector of expressions
intervals::interval interval_of_mul(const V&);
void set_interval_for_scalar(intervals::interval&, const rational&); void set_interval_for_scalar(intervals::interval&, const rational&);
void set_var_interval(lpvar j, intervals::interval&); void set_var_interval(lpvar j, intervals::interval&);
std::set<lpvar> get_vars_of_expr(const nex &) const; std::set<lpvar> get_vars_of_expr(const nex &) const;

3
src/math/lp/nla_intervals.cpp
View file

@ -94,10 +94,9 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
m_dep_manager.linearize(i.m_upper_dep, expl); m_dep_manager.linearize(i.m_upper_dep, expl);
{ {
lp::explanation e(expl); lp::explanation e(expl);
out << "\n)\nupper constraints (\n"; out << "upper constraints\n";
m_core->print_explanation(e, out); m_core->print_explanation(e, out);
} }
out << ")\n";
return out; return out;
} }

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

@ -75,12 +75,11 @@ class intervals : common {
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 {
ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps); i.m_lower_dep = mk_dependency(a, b, deps.m_lower_deps);
ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps); i.m_upper_dep = mk_dependency(a, b, deps.m_upper_deps);
i.m_lower_dep = lo;
i.m_upper_dep = hi;
} }
// Should be NOOPs for precise mpq types. // Should be NOOPs for precise mpq types.
// For imprecise types (e.g., floats) it should set the rounding mode. // For imprecise types (e.g., floats) it should set the rounding mode.
void round_to_minus_inf() {} void round_to_minus_inf() {}
@ -149,13 +148,7 @@ public:
typedef interval_manager<im_config>::interval interval; typedef interval_manager<im_config>::interval interval;
private: private:
void set_var_interval(lpvar v, interval & b) const; void set_var_interval(lpvar v, interval & b) const;
void set_var_interval_signs(lpvar v, interval & b) const;
void set_var_interval_deps(lpvar v, interval & b) const;
ci_dependency* mk_dep(lp::constraint_index ci) const; ci_dependency* mk_dep(lp::constraint_index ci) const;
lp::lar_solver& ls(); lp::lar_solver& ls();
const lp::lar_solver& ls() const; const lp::lar_solver& ls() const;
public: public:
@ -167,8 +160,6 @@ public:
m_imanager(lim, im_config(m_num_manager, m_dep_manager)) m_imanager(lim, im_config(m_num_manager, m_dep_manager))
{} {}
interval mul(const svector<lpvar>&) const; interval mul(const svector<lpvar>&) const;
interval mul_signs(const svector<lpvar>&) const;
interval mul_signs_with_deps(const svector<lpvar>&) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const; void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const; void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const; std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;