diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 8c88028a7..40631dce2 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -330,7 +330,9 @@ private: } void analyze_eq() { - m_bp.try_create_eq(m_row_index); + if (m_bp.lp().settings().cheap_eqs()) { + m_bp.try_create_eq(m_row_index); + } } }; diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index f24cd47a0..049acc7c0 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -26,7 +26,7 @@ namespace lp { bool int_gcd_test::should_apply() { - if (!lia.settings().m_int_run_gcd_test) + if (!lia.settings().int_run_gcd_test()) return false; #if 1 return true; diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 7630adb37..6e4f4cb5e 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -152,9 +152,6 @@ lia_move int_solver::check(lp::explanation * e) { check_return_helper pc(lra); - if (settings().m_int_pivot_fixed_vars_from_basis) - lra.pivot_fixed_vars_from_basis(); - ++m_number_of_calls; if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher(); if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)(); @@ -271,7 +268,7 @@ bool int_solver::should_gomory_cut() { } bool int_solver::should_hnf_cut() { - return settings().m_enable_hnf && m_number_of_calls % m_hnf_cut_period == 0; + return settings().enable_hnf() && m_number_of_calls % m_hnf_cut_period == 0; } lia_move int_solver::hnf_cut() { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 55c8a1461..7025facb6 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -767,7 +767,7 @@ void lar_solver::solve_with_core_solver() { update_x_and_inf_costs_for_columns_with_changed_bounds(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert((((m_settings.m_counter_for_debug++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); + lp_assert((((lp_settings::ddd++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); } @@ -1188,7 +1188,7 @@ std::string lar_solver::get_variable_name(var_index j) const { if (!s.empty()) { return s; } - if (m_settings.m_print_external_var_name) { + if (m_settings.print_external_var_name()) { return std::string("j") + T_to_string(m_var_register.local_to_external(j)); } else { diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index bf0b7413d..6ce54313f 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -62,12 +62,20 @@ class lp_bound_propagator { hashtable m_visited_rows; hashtable m_visited_columns; vector m_vertices; - map, impq_eq> m_offsets_to_verts; + map, impq_eq> m_offset_to_verts; // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_lower_bounds; 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)) {} @@ -154,7 +162,7 @@ public: bool is_offset_row(unsigned row_index, unsigned & x_index, lpvar & y_index, - impq& offset) const { + impq& offset) { x_index = y_index = UINT_MAX; const auto & row = lp().get_row(row_index); for (unsigned k = 0; k < row.size(); k++) { @@ -176,27 +184,31 @@ public: continue; offset += c.coeff() * lp().get_lower_bound(c.var()); } + if (offset.is_zero()) { + lp::explanation ex; + explain_fixed_in_row(row_index, ex); + add_eq_on_columns(ex, row[x_index].var(), row[y_index].var()); + } return true; - } - + } + void check_for_eq_and_add_to_offset_table(const vertex& v) { unsigned k; // the other vertex index - if (m_offsets_to_verts.find(v.offset(), k)) { - if (k != v.id()) + if (m_offset_to_verts.find(v.offset(), k)) { + if (column(m_vertices[k]) != column(v)) report_eq(k, v.id()); } else { TRACE("cheap_eq", tout << "registered offset " << v.offset() << " to " << v.id() << "\n";); - m_offsets_to_verts.insert(v.offset(), v.id()); + m_offset_to_verts.insert(v.offset(), v.id()); } } void clear_for_eq() { - // todo: do not clear the first two? - m_visited_rows.reset(); - m_visited_columns.reset(); + // m_visited_rows.reset(); + // m_visited_columns.reset(); m_vertices.reset(); - m_offsets_to_verts.reset(); + m_offset_to_verts.reset(); } // we have v_i and v_j, indices of vertices at the same offsets @@ -204,42 +216,40 @@ public: SASSERT(v_i != v_j); TRACE("cheap_eq", tout << "v_i = " << v_i << ", v_j = " << v_j << "\nu = "; m_vertices[v_i].print(tout) << "\nv = "; m_vertices[v_j].print(tout) <<"\n";); + svector path; find_path_on_tree(path, v_i, v_j); TRACE("cheap_eq", tout << "path = \n"; - display_row_of_vertex(v_i, tout); for (unsigned k : path) { display_row_of_vertex(k, tout); - } - display_row_of_vertex(v_j, tout); - ); - lp::explanation exp = get_explanation_from_path(v_i, path, v_j); - lpvar v_i_col = get_column(m_vertices[v_i]); - lpvar v_j_col = get_column(m_vertices[v_j]); + }); + lp::explanation exp = get_explanation_from_path(path); + add_eq_on_columns(exp, column(m_vertices[v_i]), column(m_vertices[v_j])); + } + + void add_eq_on_columns(const explanation& exp, lpvar v_i_col, lpvar v_j_col) { + SASSERT(v_i_col != v_j_col); if (lp().column_is_int(v_i_col) != lp().column_is_int(v_j_col)) return; + upair p = v_i_col < v_j_col? upair(v_i_col, v_j_col) :upair(v_j_col, v_i_col); + if (m_reported_pairs.contains(p)) + return; + 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); - m_imp.add_eq(i_e, j_e, exp); + TRACE("cheap_eq", tout << "reporting eq " << i_e << ", " << j_e << "\n";); + m_imp.add_eq(i_e, j_e, exp); } - - explanation get_explanation_from_path(unsigned v_i, - const svector& path, - unsigned v_j) const { + + explanation get_explanation_from_path(const svector& path) const { explanation ex; - unsigned row = m_vertices[v_i].row(); - unsigned prev_row = row; - explain_fixed_in_row(row, ex); + unsigned prev_row = UINT_MAX; for (unsigned k : path) { - row = m_vertices[k].row(); + unsigned row = m_vertices[k].row(); if (row == prev_row) continue; - prev_row = row; - explain_fixed_in_row(row, ex); + explain_fixed_in_row(prev_row = row, ex); } - row = m_vertices[v_j].row(); - if (prev_row != row) - explain_fixed_in_row(row, ex); return ex; } @@ -259,10 +269,12 @@ public: m_vertices[k].print(out); return lp().get_int_solver()->display_row_info(out,m_vertices[k].row() ); } - // the path will not include the start and the end + void find_path_on_tree(svector & path, unsigned u_i, unsigned v_i) const { const vertex* u = &m_vertices[u_i]; const vertex* v = &m_vertices[v_i]; + path.push_back(u->id()); + path.push_back(v->id()); // equalize the levels while (u->level() > v->level()) { u = &m_vertices[u->parent()]; @@ -326,11 +338,13 @@ public: } return out; } - lpvar get_column(const vertex& v) const { + lpvar column(const vertex& v) const { return lp().get_row(v.row())[v.index_in_row()].var(); } - void try_create_eq(unsigned row_index) { + void try_create_eq(unsigned row_index) { + if (m_visited_rows.contains(row_index)) + return; TRACE("cheap_eq", tout << "row_index = " << row_index << "\n";); clear_for_eq(); unsigned x_index, y_index; @@ -350,7 +364,7 @@ public: } void go_over_vertex_column(vertex & v) { - lpvar j = get_column(v); + lpvar j = column(v); if (m_visited_columns.contains(j)) return; m_visited_columns.insert(j); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 0cd0305fc..bbf212303 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -142,6 +142,10 @@ private: random_gen m_rand; public: + bool enable_hnf() const { return m_enable_hnf; } + bool& enable_hnf() { return m_enable_hnf; } + bool int_run_gcd_test() const { return m_int_run_gcd_test; } + bool& int_run_gcd_test() { return m_int_run_gcd_test; } unsigned reps_in_scaler; // when the absolute value of an element is less than pivot_epsilon // in pivoting, we treat it as a zero @@ -194,18 +198,19 @@ public: unsigned m_int_find_cube_period; private: unsigned m_hnf_cut_period; -public: bool m_int_run_gcd_test; - bool m_int_pivot_fixed_vars_from_basis; +public: unsigned limit_on_rows_for_hnf_cutter; unsigned limit_on_columns_for_hnf_cutter; +private: bool m_enable_hnf; bool m_print_external_var_name; -#ifdef Z3DEBUG - unsigned m_counter_for_debug; -#endif - - + 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; } + 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(); } @@ -267,14 +272,11 @@ public: m_int_find_cube_period(4), m_hnf_cut_period(4), m_int_run_gcd_test(true), - m_int_pivot_fixed_vars_from_basis(false), limit_on_rows_for_hnf_cutter(75), limit_on_columns_for_hnf_cutter(150), m_enable_hnf(true), m_print_external_var_name(false) -#ifdef Z3DEBUG - , m_counter_for_debug(0) -#endif + {} void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; } diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h index 94c4bd34b..4b5bc6db7 100644 --- a/src/math/lp/lp_solver_def.h +++ b/src/math/lp/lp_solver_def.h @@ -29,7 +29,7 @@ template column_info * lp_solver::get_or_creat template std::string lp_solver::get_variable_name(unsigned j) const { // j here is the core solver index - if (!m_settings.m_print_external_var_name) + if (!m_settings.print_external_var_name()) return std::string("j")+T_to_string(j); auto it = this->m_core_solver_columns_to_external_columns.find(j); if (it == this->m_core_solver_columns_to_external_columns.end()) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 02f90e5a1..241948c41 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -171,7 +171,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const { bool first = true; for (lpvar v : m) { if (!first) out << "*"; else first = false; - if (lp_settings().m_print_external_var_name) + if (lp_settings().print_external_var_name()) out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")"; else out << "(j" << v << " = " << val(v) << ")"; @@ -217,7 +217,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) } std::ostream& core::print_monic(const monic& m, std::ostream& out) const { - if (lp_settings().m_print_external_var_name) + if (lp_settings().print_external_var_name()) out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = "; else out << "(j" << m.var() << " = " << val(m.var()) << " = "; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 15c271218..560643a47 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -41,6 +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.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 386441c51..4ad6fe49b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -344,8 +344,8 @@ class theory_lra::imp { lp().settings().set_resource_limit(m_resource_limit); lp().settings().simplex_strategy() = static_cast(lpar.arith_simplex_strategy()); lp().settings().bound_propagation() = BP_NONE != propagation_mode(); - lp().settings().m_enable_hnf = lpar.arith_enable_hnf(); - lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names(); + lp().settings().enable_hnf() = lpar.arith_enable_hnf(); + lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names(); lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows()); lp().settings().report_frequency = lpar.arith_rep_freq(); lp().settings().print_statistics = lpar.arith_print_stats(); @@ -354,7 +354,7 @@ class theory_lra::imp { unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; lp().set_cut_strategy(branch_cut_ratio); - lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; + lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); get_one(true); @@ -985,17 +985,18 @@ public: lp().settings().set_resource_limit(m_resource_limit); lp().settings().simplex_strategy() = static_cast(lpar.arith_simplex_strategy()); lp().settings().bound_propagation() = BP_NONE != propagation_mode(); - lp().settings().m_enable_hnf = lpar.arith_enable_hnf(); - lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names(); + lp().settings().enable_hnf() = lpar.arith_enable_hnf(); + lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names(); lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows()); lp().settings().report_frequency = lpar.arith_rep_freq(); lp().settings().print_statistics = lpar.arith_print_stats(); + lp().settings().cheap_eqs() = lpar.arith_cheap_eqs(); // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; lp().set_cut_strategy(branch_cut_ratio); - lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; + lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); get_one(true);