diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index fdb2eb092..ffda09020 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -81,7 +81,8 @@ bool horner::check_cross_nested_expr(const nex* n) { } auto interv_wd = interval_of_expr_with_deps(n, 1); TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";); - m_intervals.check_interval_for_conflict_on_zero(interv_wd, m_fixed_var_constraints_for_row); + ci_dependency* dep = get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()); + m_intervals.check_interval_for_conflict_on_zero(interv_wd, dep); m_intervals.reset(); // clean the memory allocated by the interval bound dependencies return true; } @@ -95,8 +96,7 @@ bool horner::lemmas_on_row(const T& row) { SASSERT (row_is_interesting(row)); c().clear_and_resize_active_var_set(); - m_fixed_var_constraints_for_row.clear(); - create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_constraints_for_row); + create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); set_active_vars_weights(); // without this call the comparisons will be incorrect nex* e = m_nex_creator.simplify(&m_row_sum); TRACE("nla_horner", tout << "e = " << * e << "\n";); @@ -131,8 +131,8 @@ void horner::horner_lemmas() { unsigned r = c().random(); unsigned sz = rows.size(); for (unsigned i = 0; i < sz; i++) { - unsigned row_index = rows[(i + r) % sz]; - if (lemmas_on_row(matrix.m_rows[row_index])) { + m_row_index = rows[(i + r) % sz]; + if (lemmas_on_row(matrix.m_rows[m_row_index])) { c().lp_settings().stats().m_horner_conflicts++; break; } diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index a8ee1a8f0..59234cf25 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -30,9 +30,9 @@ class core; class horner : common { - intervals m_intervals; - nex_sum m_row_sum; - svector m_fixed_var_constraints_for_row; + intervals m_intervals; + nex_sum m_row_sum; + unsigned m_row_index; public: typedef intervals::interval interv; horner(core *core); diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 85aee1ded..5f3d33669 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -122,16 +122,11 @@ unsigned common::random() { return c().random(); } -// it also inserts variables into m_active_vars -// and updates fixed_var_deps -nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, - svector & fixed_vars_constraints) { +// creates a nex expression for the coeff and var, +// replaces the fixed vars with scalars +nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { if (!c().is_monic_var(j)) { if (c().var_is_fixed(j)) { - lp::constraint_index lc,uc; - c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); - fixed_vars_constraints.push_back(lc); - fixed_vars_constraints.push_back(uc); return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); } c().insert_to_active_var_set(j); @@ -141,10 +136,6 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); for (lpvar k : m.vars()) { if (c().var_is_fixed(k)) { - lp::constraint_index lc,uc; - c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); - fixed_vars_constraints.push_back(lc); - fixed_vars_constraints.push_back(uc); e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; continue; } @@ -156,16 +147,16 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, } -template void common::create_sum_from_row(const T& row, nex_creator& cn, - nex_sum& sum, - svector & fixed_vars_constraints) { +template void common::create_sum_from_row(const T& row, + nex_creator& cn, + nex_sum& sum) { TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); SASSERT(row.size() > 1); sum.children().clear(); for (const auto &p : row) { - nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints); + nex* e = nexvar(p.coeff(), p.var(), cn); sum.add_child(e); } TRACE("nla_horner", tout << "sum =" << sum << "\n";); @@ -176,25 +167,25 @@ common::ci_dependency* common::get_fixed_vars_dep_from_row(const T& row, ci_depe TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); ci_dependency* dep = nullptr; for (const auto &p : row) { - lpvar j = p.var(); - + lpvar j = p.var(); if (!c().is_monic_var(j)) { - if (c().var_is_fixed(j)) { + if (!c().var_is_fixed(j)) { + continue; + } + lp::constraint_index lc,uc; + c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); + dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); + } + else { + const monic& m = c().emons()[j]; + for (lpvar k : m.vars()) { + if (!c().var_is_fixed(k)) + continue; lp::constraint_index lc,uc; - c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc); + c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); - } else { - const monic& m = c().emons()[j]; - for (lpvar k : m.vars()) { - if (!c().var_is_fixed(k)) - continue; - lp::constraint_index lc,uc; - c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); - c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc); - dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); - dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); - } } } } @@ -238,6 +229,6 @@ var_weight common::get_var_weight(lpvar j) const { } -template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, svector&); - +template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&); +template dependency_manager::dependency* nla::common::get_fixed_vars_dep_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, dependency_manager&); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index e8b810a6e..f0502b2e8 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -118,10 +118,9 @@ struct common { typedef ci_dependency_manager::dependency ci_dependency; // nex* nexvar(lpvar j, nex_creator&, svector & fixed_vars_constraints); - nex* nexvar(const rational& coeff, lpvar j, nex_creator&, svector & fixed_vars_constraints); + nex* nexvar(const rational& coeff, lpvar j, nex_creator&); template - void create_sum_from_row(const T&, nex_creator&, nex_sum&, - svector & fixed_vars_constraints); + void create_sum_from_row(const T&, nex_creator&, nex_sum&); template ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); void set_active_vars_weights(); diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 1c7770e66..48eb8734b 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -183,10 +183,10 @@ void nla_grobner::add_row(unsigned i) { nex_sum * ns = m_nex_creator.mk_sum(); svector fixed_vars_constraints; - create_sum_from_row(row, m_nex_creator, *ns, fixed_vars_constraints); + create_sum_from_row(row, m_nex_creator, *ns); TRACE("nla_grobner", tout << "ns = " << *ns << "\n";); m_tmp_var_set.clear(); - assert_eq_0(ns, dep_from_vector(fixed_vars_constraints)); + assert_eq_0(ns, get_fixed_vars_dep_from_row(row, m_dep_manager)); } void nla_grobner::simplify_equations_to_process() { diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index f9d296f4f..5b7c903bf 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -103,37 +103,32 @@ bool intervals::separated_from_zero_on_upper(const interval& i) const { } -bool intervals::check_interval_for_conflict_on_zero(const interval & i, const svector& cs) { - return check_interval_for_conflict_on_zero_lower(i, cs) || check_interval_for_conflict_on_zero_upper(i, cs); +bool intervals::check_interval_for_conflict_on_zero(const interval & i, ci_dependency* dep) { + return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep); } bool intervals::check_interval_for_conflict_on_zero_upper( const interval & i, - const svector& fixed_vars_constraints) { + ci_dependency* dep) { if (!separated_from_zero_on_upper(i)) return false; add_empty_lemma(); svector expl; - for (auto c : fixed_vars_constraints) { - expl.push_back(c); - } - m_dep_manager.linearize(i.m_upper_dep, expl); + dep = m_dep_manager.mk_join(dep, i.m_upper_dep); + m_dep_manager.linearize(dep, expl); _().current_expl().add_expl(expl); TRACE("nla_solver", print_lemma(tout);); return true; } -bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, const svector& fixed_vars_constraints) { +bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) { if (!separated_from_zero_on_lower(i)) return false; add_empty_lemma(); svector expl; - for (auto c : fixed_vars_constraints) { - expl.push_back(c); - } - - m_dep_manager.linearize(i.m_lower_dep, expl); + dep = m_dep_manager.mk_join(dep, i.m_lower_dep); + m_dep_manager.linearize(dep, expl); _().current_expl().add_expl(expl); TRACE("nla_solver", print_lemma(tout);); return true; @@ -155,7 +150,6 @@ common::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const { return r; } - std::ostream& intervals::display(std::ostream& out, const interval& i) const { if (m_imanager.lower_is_inf(i)) { out << "(-oo"; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 1cc98597e..dc3c262df 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -142,6 +142,7 @@ class intervals : common { mutable interval_manager m_imanager; public: + ci_dependency_manager& dep_manager() { return m_dep_manager; } typedef interval_manager::interval interval; private: ci_dependency* mk_dep(lp::constraint_index ci) const; @@ -428,9 +429,9 @@ public: return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i); } - bool check_interval_for_conflict_on_zero(const interval & i, const svector&); - bool check_interval_for_conflict_on_zero_lower(const interval & i, const svector&); - bool check_interval_for_conflict_on_zero_upper(const interval & i, const svector&); + bool check_interval_for_conflict_on_zero(const interval & i, ci_dependency *); + bool check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency*); + bool check_interval_for_conflict_on_zero_upper(const interval & i, ci_dependency*); mpq const & lower(interval const & a) const { return m_config.lower(a); } mpq const & upper(interval const & a) const { return m_config.upper(a); } inline