mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

add a call m_pdd_manager.set_level2var()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-28 13:38:51 -08:00
parent 0bb29bca69
commit c152660911
2 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/nla_core.cpp
View file

@ -1421,6 +1421,7 @@ void core::run_pdd_grobner() {
// m_pdd_manager.resize(m_lar_solver.number_of_vars()); // m_pdd_manager.resize(m_lar_solver.number_of_vars());
create_vars_used_in_mrows(); create_vars_used_in_mrows();
m_pdd_grobner.reset(); m_pdd_grobner.reset();
set_level2var_for_pdd_grobner();
for (unsigned i : m_rows) { for (unsigned i : m_rows) {
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
} }
@ -1589,10 +1590,22 @@ void core::init_nex_grobner(nex_creator & nc) {
void core::set_active_vars_weights(nex_creator& nc) { void core::set_active_vars_weights(nex_creator& nc) {
nc.set_number_of_vars(m_lar_solver.column_count()); nc.set_number_of_vars(m_lar_solver.column_count());
for (lpvar j : active_var_set()) { for (lpvar j : active_var_set()) {
nc.set_var_weight(j, static_cast<unsigned>(get_var_weight(j))); nc.set_var_weight(j, get_var_weight(j));
} }
} }
void core::set_level2var_for_pdd_grobner() {
unsigned_vector level2var(m_lar_solver.column_count());
for (unsigned j = 0; j < level2var.size(); 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 core::get_var_weight(lpvar j) const { unsigned core::get_var_weight(lpvar j) const {
unsigned k; unsigned k;
switch (m_lar_solver.get_column_type(j)) { switch (m_lar_solver.get_column_type(j)) {

1
src/math/lp/nla_core.h
View file

@ -405,6 +405,7 @@ public:
void create_vars_used_in_mrows(); void create_vars_used_in_mrows();
void add_row_vars_to_pdd_grobner(const vector<lp::row_cell<rational>> & row); void add_row_vars_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
dd::pdd pdd_expr(const rational& c, lpvar j); dd::pdd pdd_expr(const rational& c, lpvar j);
void set_level2var_for_pdd_grobner();
}; // end of core }; // end of core
struct pp_mon { struct pp_mon {