From 538ad7701980a16c2ee616e76fe3ef4d59a51604 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 19 Oct 2019 15:54:40 -0700 Subject: [PATCH] fixed vars are treated as scalars optionally Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 6 +++--- src/math/lp/horner.h | 5 +++-- src/math/lp/nla_common.cpp | 12 ++++++------ src/math/lp/nla_common.h | 4 ++-- src/math/lp/nla_grobner.cpp | 2 +- 5 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index ffda09020..15cb0f6e7 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), m_intervals(c, c->reslim()) {} +horner::horner(core * c) : common(c), m_intervals(c, c->reslim()), m_fixed_as_scalars(true) {} template bool horner::row_has_monomial_to_refine(const T& row) const { @@ -81,7 +81,7 @@ 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";); - ci_dependency* dep = get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()); + ci_dependency* dep = m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals.dep_manager()) : nullptr; 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; @@ -96,7 +96,7 @@ bool horner::lemmas_on_row(const T& row) { SASSERT (row_is_interesting(row)); c().clear_and_resize_active_var_set(); - create_sum_from_row(row, cn.get_nex_creator(), m_row_sum); + create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars); 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";); diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index 59234cf25..d3b24de35 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -30,9 +30,10 @@ class core; class horner : common { - intervals m_intervals; - nex_sum m_row_sum; + intervals m_intervals; + nex_sum m_row_sum; unsigned m_row_index; + bool m_fixed_as_scalars; 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 5f3d33669..fb12ed18e 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -124,9 +124,9 @@ unsigned common::random() { // 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) { +nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) { if (!c().is_monic_var(j)) { - if (c().var_is_fixed(j)) { + if (fixed_as_scalars && c().var_is_fixed(j)) { return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x); } c().insert_to_active_var_set(j); @@ -135,7 +135,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) { const monic& m = c().emons()[j]; nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); for (lpvar k : m.vars()) { - if (c().var_is_fixed(k)) { + if (fixed_as_scalars && c().var_is_fixed(k)) { e->coeff() *= c().m_lar_solver.get_lower_bound(k).x; continue; } @@ -149,14 +149,14 @@ 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) { + nex_sum& sum, bool fixed_as_scalars) { 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); + nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars); sum.add_child(e); } TRACE("nla_horner", tout << "sum =" << sum << "\n";); @@ -229,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&); +template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool); 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 f0502b2e8..7389a3e01 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -118,9 +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&); + nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool); template - void create_sum_from_row(const T&, nex_creator&, nex_sum&); + void create_sum_from_row(const T&, nex_creator&, nex_sum&, bool); 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 48eb8734b..d2871df6b 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -183,7 +183,7 @@ 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); + create_sum_from_row(row, m_nex_creator, *ns, true); // true to treat fixed vars as scalars TRACE("nla_grobner", tout << "ns = " << *ns << "\n";); m_tmp_var_set.clear(); assert_eq_0(ns, get_fixed_vars_dep_from_row(row, m_dep_manager));