diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 94419ddd1..ff38b217f 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -71,14 +71,10 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) { template bool horner::lemmas_on_row(const T& row) { - cross_nested cn( - [this](const nex* n) { return m_intervals->check_nex(n, nullptr); }, - [this](unsigned j) { return c().var_is_fixed(j); }, - [this]() { return c().random(); }, m_nex_creator); - SASSERT (row_is_interesting(row)); c().clear_and_resize_active_var_set(); - create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); + u_dependency* dep = nullptr; + create_sum_from_row(row, m_nex_creator, m_row_sum, dep); c().set_active_vars_weights(m_nex_creator); // without this call the comparisons will be incorrect nex* e = m_nex_creator.simplify(m_row_sum.mk()); TRACE("nla_horner", tout << "e = " << * e << "\n";); @@ -87,6 +83,10 @@ bool horner::lemmas_on_row(const T& row) { if (!e->is_sum()) return false; + cross_nested cn( + [this, dep](const nex* n) { return m_intervals->check_nex(n, dep); }, + [this](unsigned j) { return c().var_is_fixed(j); }, + [this]() { return c().random(); }, m_nex_creator); return lemmas_on_expr(cn, to_sum(e)); } diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index d975f0b56..d8e8fe92d 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -122,13 +122,24 @@ unsigned common::random() { return c().random(); } +void common::add_deps_of_fixed(lpvar j, u_dependency*& dep) { + unsigned lc, uc; + auto& dep_manager = c().m_intervals.get_dep_intervals().dep_manager(); + 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)); +} + + // creates a nex expression for the coeff and var, -nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { +nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_dependency*& dep) { SASSERT(!coeff.is_zero()); if (c().m_nla_settings.horner_subs_fixed() == 1 && c().var_is_fixed(j)) { + add_deps_of_fixed(j, dep); return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x); } if (c().m_nla_settings.horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) { + add_deps_of_fixed(j, dep); return cn.mk_scalar(rational(0)); } @@ -139,11 +150,15 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { const monic& m = c().emons()[j]; nex_creator::mul_factory mf(cn); mf *= coeff; + u_dependency * initial_dep = dep; for (lpvar k : m.vars()) { if (c().m_nla_settings.horner_subs_fixed() && c().var_is_fixed(k)) { + add_deps_of_fixed(k, dep); mf *= c().m_lar_solver.column_lower_bound(k).x; } else if (c().m_nla_settings.horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(k)) { + dep = initial_dep; + add_deps_of_fixed(k, dep); return cn.mk_scalar(rational(0)); } else { @@ -159,52 +174,22 @@ 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_creator::sum_factory& sum - ) { + nex_creator& cn, + nex_creator::sum_factory& sum, + u_dependency*& dep) { TRACE("nla_horner", tout << "row="; m_core->print_row(row, tout) << "\n";); SASSERT(row.size() > 1); sum.reset(); for (const auto &p : row) { - nex* e = nexvar(p.coeff(), p.var(), cn); + nex* e = nexvar(p.coeff(), p.var(), cn, dep); if (!e) continue; sum += e; } } -template -u_dependency* common::get_fixed_vars_dep_from_row(const T& row, u_dependency_manager& dep_manager) { - TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); - u_dependency* dep = nullptr; - for (const auto &p : row) { - lpvar j = p.var(); - if (!c().is_monic_var(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(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)); - } - } - } - return dep; -} - } -template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&); +template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&); diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index bda196ff6..7ef2580f2 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -99,7 +99,7 @@ struct common { std::ostream& print_rooted_monic_with_vars(const monic&, std::ostream& out) const; bool check_monic(const monic&) const; unsigned random(); - + void add_deps_of_fixed(lpvar j, u_dependency*& dep); class ci_value_manager { public: void inc_ref(lp::constraint_index const & v) { @@ -116,10 +116,8 @@ struct common { typedef lp::constraint_index value; }; - nex* nexvar(const rational& coeff, lpvar j, nex_creator&); + nex* nexvar(const rational& coeff, lpvar j, nex_creator&, u_dependency*&); template - void create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&); - template - u_dependency* get_fixed_vars_dep_from_row(const T&, u_dependency_manager& dep_manager); + void create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, u_dependency*&); }; }