From b996bc1f02671bc65357f768d8ebaa6c9a663ac1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 30 Jun 2020 13:17:33 -0700 Subject: [PATCH] remove cheap equalities with the table Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.h | 6 +- src/math/lp/lp_bound_propagator.h | 132 +-------------------------- src/math/lp/lp_settings.h | 6 +- src/smt/params/smt_params_helper.pyg | 2 +- 4 files changed, 10 insertions(+), 136 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 79c6fcefb..1400c1ee9 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -373,11 +373,7 @@ public: } template void calculate_cheap_eqs_for_row(unsigned i, lp_bound_propagator & bp) { - if (settings().cheap_eqs() == 1) { - bp.cheap_eq_tree(i); - } else { - bp.cheap_eq_table(i); - } + bp.cheap_eq_tree(i); } bool is_fixed(column_index const& j) const { return column_is_fixed(j); } diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 9fa8d0d62..250180e86 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -180,59 +180,6 @@ public: m_imp.consume(a, ci); } - bool is_offset_row(unsigned r, lpvar & x, lpvar & y, mpq & k) const { - if (r >= lp().row_count()) - return false; - x = y = null_lpvar; - for (auto& c : lp().get_row(r)) { - lpvar v = c.var(); - if (column_is_fixed(v)) { - // if (get_lower_bound_rational(c.var()).is_big()) - // return false; - continue; - } - - if (c.coeff().is_one() && x == null_lpvar) { - x = v; - continue; - } - if (c.coeff().is_minus_one() && y == null_lpvar) { - y = v; - continue; - } - return false; - } - - if (x == null_lpvar && y == null_lpvar) { - return false; - } - - k = mpq(0); - for (const auto& c : lp().get_row(r)) { - if (!column_is_fixed(c.var())) - continue; - k -= c.coeff() * get_lower_bound_rational(c.var()); - if (k.is_big()) - return false; - } - - if (y == null_lpvar) - return true; - - if (x == null_lpvar) { - std::swap(x, y); - k.neg(); - return true; - } - - if (!lp().is_base(x) && x > y) { - std::swap(x, y); - k.neg(); - } - return true; - } - - bool set_sign_and_column(signed_column& i, const row_cell & c) const { if (c.coeff().is_one()) { i.sign() = false; @@ -352,7 +299,7 @@ public: return m_imp.is_equal(col_to_imp(j), col_to_imp(k)); } - void check_for_eq_and_add_to_offset_table(vertex* v, map, mpq_eq>& table) { + void check_for_eq_and_add_to_val_table(vertex* v, map, mpq_eq>& table) { vertex *k; // the other vertex if (table.find(val(v), k)) { TRACE("cheap_eq", tout << "found k " ; k->print(tout) << "\n";); @@ -366,12 +313,12 @@ public: } } - void check_for_eq_and_add_to_offsets(vertex* v) { + void check_for_eq_and_add_to_val_tables(vertex* v) { TRACE("cheap_eq_det", v->print(tout) << "\n";); if (v->neg()) - check_for_eq_and_add_to_offset_table(v, m_vals_to_verts_neg); + check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg); else - check_for_eq_and_add_to_offset_table(v, m_vals_to_verts); + check_for_eq_and_add_to_val_table(v, m_vals_to_verts); } void clear_for_eq() { @@ -452,75 +399,6 @@ public: return lp().column_is_int(j); } - void cheap_eq_table(unsigned rid) { - TRACE("cheap_eqs", tout << "checking if row " << rid << " can propagate equality.\n"; print_row(tout, rid);); - unsigned x = 0, y = 0; - mpq k; - if (is_offset_row(rid, x, y, k)) { - if (y == null_lpvar) { - // x is an implied fixed var at k. - unsigned x2 = null_lpvar; - if (lp().find_in_fixed_tables(k, is_int(x), x2) && - !is_equal(x, x2)) { - SASSERT(is_int(x) == is_int(x2) && lp().column_is_fixed(x2) && - get_lower_bound_rational(x2) == k); - explanation ex; - constraint_index lc, uc; - lp().get_bound_constraint_witnesses_for_column(x2, lc, uc); - ex.push_back(lc); - ex.push_back(uc); - explain_fixed_in_row(rid, ex); - add_eq_on_columns(ex, x, x2); - } - } - if (k.is_zero() && y != null_lpvar && !is_equal(x, y) && - is_int(x) == is_int(y)) { - explanation ex; - explain_fixed_in_row(rid, ex); - add_eq_on_columns(ex, x, y); - } - - unsigned row_id; - var_offset key(y, k); - if (m_var_offset2row_id.find(key, row_id)) { - if (row_id == rid) { // it is the same row. - return; - } - unsigned x2, y2; - mpq k2; - if (is_offset_row(row_id, x2, y2, k2)) { - bool new_eq = false; - if (y == y2 && k == k2) { - new_eq = true; - } - else if (y2 != null_lpvar && x2 == y && k == - k2) { - std::swap(x2, y2); - new_eq = true; - } - - if (new_eq) { - if (!is_equal(x, x2) && is_int(x) == is_int(x2)) { - // SASSERT(y == y2 && k == k2 ); - explanation ex; - explain_fixed_in_row(rid, ex); - explain_fixed_in_row(row_id, ex); - TRACE("arith_eq", tout << "propagate eq two rows:\n"; - tout << "x : v" << x << "\n"; - tout << "x2 : v" << x2 << "\n"; - print_row(tout, rid); - print_row(tout, row_id);); - add_eq_on_columns(ex, x, x2); - } - return; - } - } - // the original row was deleted or it is not offset row anymore ===> remove it from table - } - // add new entry - m_var_offset2row_id.insert(key, rid); - } - } - explanation get_explanation_from_path(const ptr_vector& path) const { explanation ex; unsigned prev_row = UINT_MAX; @@ -731,7 +609,7 @@ public: } void explore_under(vertex * v) { - check_for_eq_and_add_to_offsets(v); + check_for_eq_and_add_to_val_tables(v); go_over_vertex_column(v); // v might change in m_vertices expansion for (vertex* c : v->children()) { diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 4026cb97a..fec783961 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -206,12 +206,12 @@ public: private: bool m_enable_hnf; bool m_print_external_var_name; - unsigned m_cheap_eqs; + bool m_cheap_eqs; public: bool print_external_var_name() const { return m_print_external_var_name; } bool& print_external_var_name() { return m_print_external_var_name; } - unsigned cheap_eqs() const { return m_cheap_eqs;} - unsigned& cheap_eqs() { return m_cheap_eqs;} + bool cheap_eqs() const { return m_cheap_eqs;} + bool& cheap_eqs() { return m_cheap_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; } void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; } unsigned random_next() { return m_rand(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 982446932..8aa37e1b2 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -41,7 +41,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.cheap_eqs', UINT, 1, '0 - do not run, 1 - use tree, 2 - use table'), + ('arith.cheap_eqs', BOOL, True, 'false - do not run, true - run cheap equality heuristic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental lianirization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),