diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 4e6935c22..4c6996327 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -25,7 +25,7 @@ namespace nla { typedef intervals::interval interv; -horner::horner(core * c) : common(c) {} +horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {} template bool horner::row_has_monomial_to_refine(const T& row) const { @@ -67,13 +67,12 @@ bool horner::lemmas_on_expr(nex& e) { TRACE("nla_horner", tout << "e = " << e << "\n";); bool conflict = false; cross_nested cn(e, [this, & conflict](const nex& n) { - intervals ivs(&c(), c().reslim()); - set_intervals(& ivs); TRACE("nla_horner", tout << "cross-nested n = " << n << "\n";); auto i = interval_of_expr(n); - TRACE("nla_horner", tout << "callback n = " << n << "\ni="; ivs.display(tout, i) << "\n";); + TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";); - conflict = ivs.check_interval_for_conflict_on_zero(i); + conflict = m_intervals.check_interval_for_conflict_on_zero(i); + m_intervals.reset(); // clean the memory allocated by the interval bound dependencies return conflict; }, [this](unsigned j) { return c().var_is_fixed(j); } @@ -145,12 +144,12 @@ template nex horner::create_sum_from_row(const T& row) { void horner::set_interval_for_scalar(interv& a, const rational& v) { - m_intervals->set_lower(a, v); - m_intervals->set_upper(a, v); - m_intervals->set_lower_is_open(a, false); - m_intervals->set_lower_is_inf(a, false); - m_intervals->set_upper_is_open(a, false); - m_intervals->set_upper_is_inf(a, false); + m_intervals.set_lower(a, v); + m_intervals.set_upper(a, v); + m_intervals.set_lower_is_open(a, false); + m_intervals.set_lower_is_inf(a, false); + m_intervals.set_upper_is_open(a, false); + m_intervals.set_upper_is_inf(a, false); } interv horner::interval_of_expr(const nex& e) { @@ -176,33 +175,33 @@ interv horner::interval_of_mul(const nex& e) { SASSERT(e.is_mul()); auto & es = e.children(); interv a = interval_of_expr(es[0]); - if (m_intervals->is_zero(a)) { - m_intervals->set_zero_interval_deps_for_mult(a); - TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals->display(tout, a); ); + if (m_intervals.is_zero(a)) { + m_intervals.set_zero_interval_deps_for_mult(a); + TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); ); return a; } - TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals->display(tout, a); ); + 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]); - if (m_intervals->is_zero(b)) { - m_intervals->set_zero_interval_deps_for_mult(b); - TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals->display(tout, b); ); + if (m_intervals.is_zero(b)) { + m_intervals.set_zero_interval_deps_for_mult(b); + TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals.display(tout, b); ); TRACE("nla_horner_details", tout << "got zero\n"; ); return b; } - TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals->display(tout, b); ); + TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); ); interv c; interval_deps_combine_rule comb_rule; - m_intervals->mul(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);); - TRACE("nla_horner_details", tout << "c "; m_intervals->display(tout, c);); - m_intervals->set(a, c); - TRACE("nla_horner_details", tout << "part mult "; m_intervals->display(tout, a);); + m_intervals.mul(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);); + TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c);); + m_intervals.set(a, c); + TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a);); } TRACE("nla_horner_details", tout << "e=" << e << "\n"; - tout << " return "; m_intervals->display(tout, a);); + tout << " return "; m_intervals.display(tout, a);); return a; } @@ -307,34 +306,34 @@ lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const { interv horner::interval_of_sum_no_terms(const nex& e) { auto & es = e.children(); interv a = interval_of_expr(es[0]); - 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);); + tout << " interv = "; m_intervals.display(tout, a);); return a; } 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]); - if (m_intervals->is_inf(b)) { + if (m_intervals.is_inf(b)) { TRACE("nla_horner_details", tout << "got inf\n";); return b; } 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";); - m_intervals->add(a, b, c, combine_rule); - m_intervals->combine_deps(a, b, combine_rule, c); - m_intervals->set(a, c); + 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, combine_rule); + m_intervals.combine_deps(a, b, combine_rule, c); + m_intervals.set(a, c); TRACE("nla_horner_details_sum", tout << es[k] << ", "; - m_intervals->display(tout, a); tout << "\n";); - if (m_intervals->is_inf(a)) { + m_intervals.display(tout, a); tout << "\n";); + if (m_intervals.is_inf(a)) { TRACE("nla_horner_details", tout << "got infinity\n";); return a; } } TRACE("nla_horner_details", tout << "e=" << e << "\n"; - tout << " interv = "; m_intervals->display(tout, a);); + tout << " interv = "; m_intervals.display(tout, a);); return a; } @@ -347,14 +346,14 @@ bool horner::interval_from_term(const nex& e, interv & i) const { set_var_interval(j, i); interv bi; - m_intervals->mul(a, i, bi); - m_intervals->add(b, bi); - m_intervals->set(i, bi); + m_intervals.mul(a, i, bi); + m_intervals.add(b, bi); + m_intervals.set(i, bi); TRACE("nla_horner", c().m_lar_solver.print_column_info(j, tout) << "\n"; tout << "a=" << a << ", b=" << b << "\n"; - tout << e << ", interval = "; m_intervals->display(tout, i);); + tout << e << ", interval = "; m_intervals.display(tout, i);); return true; } @@ -366,9 +365,9 @@ interv horner::interval_of_sum(const nex& e) { if (e.sum_is_a_linear_term()) { interv i_from_term ; if (interval_from_term(e, i_from_term)) { - interv r = m_intervals->intersect(i_e, i_from_term); - TRACE("nla_horner_details", tout << "intersection="; m_intervals->display(tout, r) << "\n";); - if (m_intervals->is_empty(r)) { + interv r = m_intervals.intersect(i_e, i_from_term); + TRACE("nla_horner_details", tout << "intersection="; m_intervals.display(tout, r) << "\n";); + if (m_intervals.is_empty(r)) { SASSERT(false); // not implemented } return r; @@ -380,8 +379,8 @@ interv horner::interval_of_sum(const nex& e) { // sets the dependencies also void horner::set_var_interval(lpvar v, interv& b) const{ - m_intervals->set_var_interval_with_deps(v, b); - TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals->display(tout, b);); + m_intervals.set_var_interval_with_deps(v, b); + TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b);); } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 2dad6e7d7..f5944b24c 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -28,13 +28,10 @@ class core; class horner : common { - intervals *m_intervals; + intervals m_intervals; public: typedef nla_expr nex; typedef intervals::interval interv; - void set_intervals( intervals * i) { - m_intervals = i; - } horner(core *core); void horner_lemmas(); template // T has an iterator of (coeff(), var()) diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 0e34371a3..2cde3e45b 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -19,7 +19,7 @@ --*/ #pragma once #include "util/dependency.h" -#include "util/small_object_allocator.h" +#include "util/region.h" #include "math/lp/nla_common.h" #include "math/lp/lar_solver.h" #include "math/interval/interval.h" @@ -40,7 +40,7 @@ class intervals : common { struct ci_dependency_config { typedef ci_value_manager value_manager; - typedef small_object_allocator allocator; + typedef region allocator; static const bool ref_count = false; typedef lp::constraint_index value; }; @@ -135,13 +135,13 @@ class intervals : common { } }; - small_object_allocator m_alloc; - ci_value_manager m_val_manager; + region m_alloc; + ci_value_manager m_val_manager; mutable unsynch_mpq_manager m_num_manager; mutable ci_dependency_manager m_dep_manager; im_config m_config; mutable interval_manager m_imanager; - region m_region; + region m_region; public: typedef interval_manager::interval interval; @@ -153,7 +153,7 @@ private: public: intervals(core* c, reslimit& lim) : common(c), - m_alloc("intervals"), + m_alloc(), m_dep_manager(m_val_manager, m_alloc), m_config(m_num_manager, m_dep_manager), m_imanager(lim, im_config(m_num_manager, m_dep_manager)) @@ -319,6 +319,6 @@ public: return true; return false; } - + void reset() { m_alloc.reset(); } }; // end of intervals } // end of namespace nla