From dd30b5e3af7ef8753416300953b5f55f41446572 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 8 Jun 2020 21:16:23 -0700 Subject: [PATCH] some simplifications in cheap eqs Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 12 ++++++++++-- src/math/lp/lp_bound_propagator.h | 29 +++++++++++++--------------- src/math/lp/lp_settings.h | 6 +++--- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/theory_lra.cpp | 13 +++++++++++++ 5 files changed, 40 insertions(+), 22 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 40631dce2..5929bafd0 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -330,11 +330,19 @@ private: } void analyze_eq() { - if (m_bp.lp().settings().cheap_eqs()) { + switch (m_bp.lp().settings().cheap_eqs()) { + case 0: + return; + case 1: m_bp.try_create_eq(m_row_index); + break; + case 2: + m_bp.try_create_eq_table(m_row_index); + break; + default: + UNREACHABLE(); } } - }; } diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index ca7e27529..c9018bfd4 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -9,6 +9,11 @@ namespace lp { template class lp_bound_propagator { + typedef std::pair var_offset; + typedef pair_hash > var_offset_hash; + typedef map > var_offset2row_id; + var_offset2row_id m_var_offset2row_id; + struct impq_eq { bool operator()(const impq& a, const impq& b) const {return a == b;}}; // vertex represents a pair (row,x) or (row,y) for an offset row. @@ -62,14 +67,6 @@ class lp_bound_propagator { std::unordered_map m_improved_upper_bounds; T& m_imp; impq m_zero; - typedef std::pair upair; - struct uphash { - unsigned operator()(const upair& p) const { return combine_hash(p.first, p.second); } - }; - struct upeq { - unsigned operator()(const upair& p, const upair& q) const { return p == q; } - }; - hashtable m_reported_pairs; // contain the pairs of columns (first < second) public: vector m_ibounds; lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {} @@ -156,7 +153,7 @@ public: offset += c.coeff() * lp().get_lower_bound(c.var()); } if (offset.is_zero() && - !pair_is_reported(row[x_index].var(), row[y_index].var())) { + !pair_is_reported_or_congruent(row[x_index].var(), row[y_index].var())) { lp::explanation ex; explain_fixed_in_row(row_index, ex); add_eq_on_columns(ex, row[x_index].var(), row[y_index].var()); @@ -164,17 +161,16 @@ public: return true; } - bool pair_is_reported(lpvar j, lpvar k) const { - return j < k? m_reported_pairs.contains(std::make_pair(j, k)) : - m_reported_pairs.contains(std::make_pair(k, j)); + bool pair_is_reported_or_congruent(lpvar j, lpvar k) const { + return m_imp.congruent_or_irrelevant(lp().column_to_reported_index(j), lp().column_to_reported_index(k)); } void check_for_eq_and_add_to_offset_table(vertex* v) { - vertex *k; // the other vertex index + vertex *k; // the other vertex if (m_offset_to_verts.find(v->offset(), k)) { if (column(k) != column(v) && - !pair_is_reported(column(k),column(v))) + !pair_is_reported_or_congruent(column(k),column(v))) report_eq(k, v); } else { TRACE("cheap_eq", tout << "registered offset " << v->offset() << " to " << v << "\n";); @@ -211,8 +207,6 @@ public: void add_eq_on_columns(const explanation& exp, lpvar v_i_col, lpvar v_j_col) { SASSERT(v_i_col != v_j_col); - upair p = v_i_col < v_j_col? upair(v_i_col, v_j_col) :upair(v_j_col, v_i_col); - m_reported_pairs.insert(p); unsigned i_e = lp().column_to_reported_index(v_i_col); unsigned j_e = lp().column_to_reported_index(v_j_col); TRACE("cheap_eq", tout << "reporting eq " << i_e << ", " << j_e << "\n"; @@ -222,6 +216,9 @@ public: m_imp.add_eq(i_e, j_e, exp); } + + void try_create_eq_table(unsigned row_index) { + } explanation get_explanation_from_path(const ptr_vector& path) const { explanation ex; diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index bbf212303..3fcd8a8e3 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -205,12 +205,12 @@ public: private: bool m_enable_hnf; bool m_print_external_var_name; - bool m_cheap_eqs; + unsigned 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; } - bool cheap_eqs() const { return m_cheap_eqs;} - bool& cheap_eqs() { return m_cheap_eqs;} + unsigned cheap_eqs() const { return m_cheap_eqs;} + unsigned& 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 560643a47..8027f5540 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', BOOL, True, 'true for extracting cheap equalities'), + ('arith.cheap_eqs', UINT, 0, '0 - do not run, 1 - use tree, 2 - use table'), ('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.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 4ad6fe49b..62ab6bec0 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1592,6 +1592,19 @@ public: void reset_variable_values() { m_variable_values.clear(); } + + bool congruent_or_irrelevant(lpvar k, lpvar j) { + theory_var kv = lp().local_to_external(k); + if (kv == null_theory_var) + return true; + theory_var jv = lp().local_to_external(j); + if (jv == null_theory_var) + return true; + + enode * n0 = get_enode(kv); + enode * n1 = get_enode(jv); + return n0->get_root() == n1->get_root(); + } void random_update() { if (m_nla)