From a3d0372e3dc79a1f8cebb15cb38f8471b72e405e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Sep 2019 16:11:51 -0700 Subject: [PATCH] move the nex object creation from a row to nla_common Signed-off-by: Lev Nachmanson --- src/math/lp/horner.cpp | 40 ------------------------------------- src/math/lp/horner.h | 4 ---- src/math/lp/nex_creator.h | 2 +- src/math/lp/nla_common.cpp | 40 +++++++++++++++++++++++++++++++++++++ src/math/lp/nla_common.h | 5 +++++ src/math/lp/nla_grobner.cpp | 10 ++++------ 6 files changed, 50 insertions(+), 51 deletions(-) diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 7433b687d..ea78ab9ee 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -131,46 +131,6 @@ void horner::horner_lemmas() { } } -nex * horner::nexvar(lpvar j, nex_creator& cn) const { - // todo: consider deepen the recursion - if (!c().is_monic_var(j)) - return cn.mk_var(j); - const monic& m = c().emons()[j]; - nex_mul * e = cn.mk_mul(); - for (lpvar k : m.vars()) { - e->add_child(cn.mk_var(k)); - CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); - } - return e; -} - -nex * horner::nexvar(const rational & coeff, lpvar j, nex_creator& cn) const { - // todo: consider deepen the recursion - if (!c().is_monic_var(j)) - return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); - const monic& m = c().emons()[j]; - nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); - for (lpvar k : m.vars()) { - e->add_child(cn.mk_var(k)); - CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); - } - return e; -} - - -template void horner::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) { - if (p.coeff().is_one()) - sum.add_child(nexvar(p.var(), cn)); - else { - sum.add_child(nexvar(p.coeff(), p.var(), cn)); - } - } -} - void horner::set_interval_for_scalar(interv& a, const rational& v) { m_intervals.set_lower(a, v); diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h index a38a41801..d35e252a5 100644 --- a/src/math/lp/horner.h +++ b/src/math/lp/horner.h @@ -39,8 +39,6 @@ public: template // T has an iterator of (coeff(), var()) bool lemmas_on_row(const T&); template bool row_is_interesting(const T&) const; - template - void create_sum_from_row(const T&, nex_creator&, nex_sum&); intervals::interval interval_of_expr_with_deps(const nex* e); intervals::interval interval_of_expr(const nex* e); intervals::interval interval_of_sum(const nex_sum*); @@ -51,8 +49,6 @@ public: bool interval_from_term(const nex* e, interv&) const; - nex* nexvar(lpvar j, nex_creator& ) const; - nex* nexvar(const rational& coeff, lpvar j, nex_creator&) const; intervals::interval interval_of_sum_with_deps(const nex_sum*); intervals::interval interval_of_sum_no_term_with_deps(const nex_sum*); intervals::interval interval_of_mul_with_deps(const nex_mul*); diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h index 4a2ec04d1..1d8330639 100644 --- a/src/math/lp/nex_creator.h +++ b/src/math/lp/nex_creator.h @@ -18,7 +18,7 @@ --*/ #pragma once - +#include "math/lp/nex.h" namespace nla { struct occ { diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index eacb83916..09ec84e27 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -122,5 +122,45 @@ unsigned common::random() { return c().random(); } +nex * common::nexvar(lpvar j, nex_creator& cn) const { + // todo: consider deepen the recursion + if (!c().is_monic_var(j)) + return cn.mk_var(j); + const monic& m = c().emons()[j]; + nex_mul * e = cn.mk_mul(); + for (lpvar k : m.vars()) { + e->add_child(cn.mk_var(k)); + CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); + } + return e; } +nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) const { + // todo: consider deepen the recursion + if (!c().is_monic_var(j)) + return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); + const monic& m = c().emons()[j]; + nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff)); + for (lpvar k : m.vars()) { + e->add_child(cn.mk_var(k)); + CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); + } + return e; +} + + +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) { + if (p.coeff().is_one()) + sum.add_child(nexvar(p.var(), cn)); + else { + sum.add_child(nexvar(p.coeff(), p.var(), cn)); + } + } +} +} +template void nla::common::create_sum_from_row, true, unsigned int> >(old_vector, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&); + diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h index e82ea16ca..0465ab3c6 100644 --- a/src/math/lp/nla_common.h +++ b/src/math/lp/nla_common.h @@ -26,6 +26,7 @@ #include "math/lp/factorization.h" #include "util/dependency.h" #include "util/region.h" +#include "math/lp/nex_creator.h" namespace nla { @@ -114,6 +115,10 @@ struct common { typedef dependency_manager ci_dependency_manager; typedef ci_dependency_manager::dependency ci_dependency; + nex* nexvar(lpvar j, nex_creator& ) const; + nex* nexvar(const rational& coeff, lpvar j, nex_creator&) const; + template + void create_sum_from_row(const T&, nex_creator&, nex_sum&); }; } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index df1f9273d..fa7670ca4 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -199,13 +199,11 @@ nex * nla_grobner::mk_monomial_in_row(rational coeff, lpvar j, ci_dependency * & } -void nla_grobner::add_row(unsigned i) { - NOT_IMPLEMENTED_YET(); - /* - const auto& row = c().m_lar_solver.A_r().m_rows[i]; +void nla_grobner::add_row(unsigned i) { + const auto& row = c().m_lar_solver.A_r().m_rows[i]; TRACE("non_linear", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout);); - nex * row_nex; - v_dependency * dep = nullptr; + nex * row_nex = nullptr; + /* v_dependency * dep = nullptr; m_tmp_var_set.reset(); for (const auto & p : row) { rational coeff = p.coeff();