From b5364b787cb76d002b129489caa73f8fb782a428 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 28 Dec 2019 13:53:04 -0800 Subject: [PATCH] set level2var for m_pdd_manager of pdd_grobner Signed-off-by: Lev Nachmanson --- src/math/dd/dd_pdd.h | 1 + src/math/lp/nla_core.cpp | 9 ++++++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 1168952d4..6c7750b90 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -259,6 +259,7 @@ namespace dd { void reset(unsigned_vector const& level2var); void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; } unsigned_vector const& get_level2var() const { return m_level2var; } + unsigned_vector& get_level2var() { return m_level2var; } pdd mk_var(unsigned i); pdd mk_val(rational const& r); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cc08b0d0a..741558f35 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1595,15 +1595,18 @@ void core::set_active_vars_weights(nex_creator& nc) { } void core::set_level2var_for_pdd_grobner() { - unsigned_vector level2var(m_lar_solver.column_count()); - for (unsigned j = 0; j < level2var.size(); j++) + unsigned n = m_pdd_manager.get_level2var().size(); + unsigned_vector level2var(n); + for (unsigned j = 0; j < n; j++) level2var[j] = j; // sort that the larger weights are in beginning std::sort(level2var.begin(), level2var.end(), [this](unsigned a, unsigned b) { unsigned wa = get_var_weight(a); unsigned wb = get_var_weight(b); return wa > wb || (wa == wb && a > b); }); - m_pdd_manager.set_level2var(level2var); + unsigned_vector& l2v = m_pdd_manager.get_level2var(); + for (unsigned j = 0; j < n; j++) + l2v[j] = level2var[j]; } unsigned core::get_var_weight(lpvar j) const {