diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index d377e5355..ae023078a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -849,7 +849,7 @@ namespace smt { std::cerr << v << " ::=\n" << mk_ll_pp(n, m_manager) << "\n"; } #endif - TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";); + TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << " " << n->get_id() << "\n";); TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";); set_bool_var(id, v); m_bdata.reserve(v+1); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 512bf7787..03431c8b7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -306,13 +306,13 @@ class theory_lra::imp { reset_variable_values(); m_solver->settings().bound_propagation() = BP_NONE != propagation_mode(); m_solver->set_track_pivoted_rows(lp.bprop_on_pivoted_rows()); - m_solver->settings().m_int_gomory_cut_period = ctx().get_fparams().m_arith_branch_cut_ratio; - m_solver->settings().m_hnf_cut_period = ctx().get_fparams().m_arith_branch_cut_ratio; - m_solver->settings().m_int_chase_cut_solver_period = std::max(8u, ctx().get_fparams().m_arith_branch_cut_ratio); + + // 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; + m_solver->set_cut_strategy(branch_cut_ratio); + m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; - m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed); - //m_solver->settings().set_ostream(0); m_lia = alloc(lp::int_solver, m_solver.get()); } @@ -1297,7 +1297,7 @@ public: return FC_CONTINUE; case l_undef: TRACE("arith", tout << "check-lia giveup\n";); - st = FC_GIVEUP; + st = FC_CONTINUE; break; } @@ -1400,6 +1400,8 @@ public: case lp::lia_move::undef: TRACE("arith", tout << "lia undef\n";); return l_undef; + case lp::lia_move::continue_with_check: + return l_undef; default: UNREACHABLE(); } @@ -2873,10 +2875,6 @@ public: st.update("arith-make-feasible", m_solver->settings().st().m_make_feasible); st.update("arith-max-columns", m_solver->settings().st().m_max_cols); st.update("arith-max-rows", m_solver->settings().st().m_max_rows); - st.update("cut-solver-calls", m_solver->settings().st().m_chase_cut_solver_calls); - st.update("cut-solver-true", m_solver->settings().st().m_chase_cut_solver_true); - st.update("cut-solver-false", m_solver->settings().st().m_chase_cut_solver_false); - st.update("cut-solver-undef", m_solver->settings().st().m_chase_cut_solver_undef); st.update("gcd-calls", m_solver->settings().st().m_gcd_calls); st.update("gcd-conflict", m_solver->settings().st().m_gcd_conflicts); st.update("cube-calls", m_solver->settings().st().m_cube_calls); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 76f9bd7f2..35c9aeccb 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -3286,44 +3286,6 @@ void cutting_the_mix_example_1() { std::cout << "d = " << d << ", u = " << u << ", vv = " << vv << std::endl; } -void test_determinant() { -#ifdef Z3DEBUG - { - auto M = general_matrix(4); - M[0][0] = 1; M[0][1] = -1; M[0][2] = 1; M[0][3] = 1; - M[1][0] = 1; M[1][1] = 0; M[1][2] = 0; M[1][3] = 0; - M[2][0] = 0; M[2][1] = 1; M[2][2] = 4; M[2][3] = 0; - M[3][0] = 0; M[3][1] = 0; M[3][2] = 0; M[3][3] = 4; - std::cout << "M = "; M.print(std::cout, 4); endl(std::cout); - mpq d = hnf_calc::determinant(M); - std::cout << "det M = " << d << std::endl; - } - { - auto M = general_matrix(3); - M[0][0] = 3; M[0][1] = -1; M[0][2] = 1; - M[1][0] = 1; M[1][1] = 0; M[1][2] = 0; - M[2][0] = 0; M[2][1] = 1; M[2][2] = 4; - svector r; - std::cout << "M = "; M.print(std::cout, 4); endl(std::cout); - mpq d = hnf_calc::determinant_of_rectangular_matrix(M, r, mpq((int)100000)); - std::cout << "det M = " << d << std::endl; - std::cout << "rank = " << r.size() << std::endl; - } - { - auto M = general_matrix(4, 6); - M[0][0] = 3; M[0][1] = -1; M[0][2] = 1; M[0][3] = 1; M[0][4] = 3; M[0][5] = -1; - M[1][0] = 1; M[1][1] = 0; M[1][2] = 0; M[1][3] = 0; M[1][4] = 2; M[1][5] = 7; - M[2][0] = 0; M[2][1] = 1; M[2][2] = 4; M[2][3] = 0; M[2][4] = 2; M[2][5] = 8; - M[3][0] = 6; M[3][1] = -2; M[3][2] = 2; M[3][3] = 2; M[3][4] = 6; M[3][5] = -2; - svector r; - std::cout << "M = "; M.print(std::cout, 4); endl(std::cout); - mpq d = hnf_calc::determinant_of_rectangular_matrix(M, r, mpq((int)1000000)); - std::cout << "det M = " << d << std::endl; - std::cout << "rank = " << r.size() << std::endl; - } -#endif -} - #ifdef Z3DEBUG void fill_general_matrix(general_matrix & M) { diff --git a/src/util/lp/hnf.h b/src/util/lp/hnf.h index 0e14972da..3cdeac466 100644 --- a/src/util/lp/hnf.h +++ b/src/util/lp/hnf.h @@ -130,15 +130,13 @@ void pivot_column_non_fractional(M &m, unsigned r, bool & overflow, const mpq & lp_assert(!is_zero(m[r][r])); for (unsigned j = r + 1; j < m.column_count(); j++) { for (unsigned i = r + 1; i < m.row_count(); i++) { - m[i][j] = - (r > 0) ? - (m[r][r]*m[i][j] - m[i][r]*m[r][j]) / m[r-1][r-1] : - (m[r][r]*m[i][j] - m[i][r]*m[r][j]); - if (m[i][j] >= big_number) { + if ( + (m[i][j] = (r > 0) ? (m[r][r]*m[i][j] - m[i][r]*m[r][j]) / m[r-1][r-1] : + (m[r][r]*m[i][j] - m[i][r]*m[r][j])) + >= big_number) { overflow = true; return; } - lp_assert(is_int(m[i][j])); } } @@ -201,16 +199,6 @@ mpq determinant_of_rectangular_matrix(const M& m, svector & basis_rows TRACE("hnf_calc", tout << "basis_rows = "; print_vector(basis_rows, tout); m_copy.print(tout, "m_copy = ");); return gcd_of_row_starting_from_diagonal(m_copy, rank - 1); } - -template -mpq determinant(const M& m) { - lp_assert(m.row_count() == m.column_count()); - auto mc = m; - svector basis_rows; - mpq d = determinant_of_rectangular_matrix(mc, basis_rows); - return basis_rows.size() < m.row_count() ? zero_of_type() : d; -} - } // end of namespace hnf_calc template // M is the matrix type diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 5033f2852..3f69e616b 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -463,7 +463,7 @@ bool int_solver::tighten_terms_for_cube() { } lia_move int_solver::find_cube() { - if (m_branch_cut_counter % settings().m_int_find_cube_period != 0) + if (m_number_of_calls % settings().m_int_find_cube_period != 0) return lia_move::undef; settings().st().m_cube_calls++; @@ -510,7 +510,7 @@ lia_move int_solver::run_gcd_test() { } lia_move int_solver::gomory_cut() { - if ((m_branch_cut_counter) % settings().m_int_gomory_cut_period != 0) + if ((m_number_of_calls) % settings().m_int_gomory_cut_period != 0) return lia_move::undef; if (move_non_basic_columns_to_bounds()) { @@ -598,7 +598,7 @@ lia_move int_solver::make_hnf_cut() { } lia_move int_solver::hnf_cut() { - if ((m_branch_cut_counter) % settings().m_hnf_cut_period == 0) { + if ((m_number_of_calls) % settings().m_hnf_cut_period == 0) { return make_hnf_cut(); } return lia_move::undef; @@ -618,7 +618,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) { r = patch_nbasic_columns(); if (r != lia_move::undef) return r; - ++m_branch_cut_counter; + ++m_number_of_calls; r = find_cube(); if (r != lia_move::undef) return r; @@ -936,7 +936,7 @@ linear_combination_iterator * int_solver::get_column_iterator(unsigned j) { int_solver::int_solver(lar_solver* lar_slv) : m_lar_solver(lar_slv), - m_branch_cut_counter(0), + m_number_of_calls(0), m_hnf_cutter(settings()) { m_lar_solver->set_int_solver(this); } diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 13db7470e..65c818d1e 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -38,7 +38,7 @@ class int_solver { public: // fields lar_solver *m_lar_solver; - unsigned m_branch_cut_counter; + unsigned m_number_of_calls; lar_term *m_t; // the term to return in the cut mpq *m_k; // the right side of the cut explanation *m_ex; // the conflict explanation diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 1fd124ab2..7e529758b 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -2240,6 +2240,22 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term return false; } +void lar_solver::set_cut_strategy(unsigned cut_frequency) { + if (cut_frequency < 4) { // enable only gomory cut + settings().m_int_gomory_cut_period = 2; + settings().m_hnf_cut_period = 100000000; + settings().m_int_find_cube_period = 100000000; + } else if (cut_frequency == 4) { // enable all cuts and cube equally + settings().m_int_gomory_cut_period = 4; + settings().m_hnf_cut_period = 4; + settings().m_int_find_cube_period = 4; + } else { + // disable all heuristics + settings().m_int_gomory_cut_period = 10000000; + settings().m_hnf_cut_period = 100000000; + settings().m_int_find_cube_period = 100000000; + } +} } // namespace lp diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index d7f0fb076..7209efced 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -577,5 +577,6 @@ public: bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci) const; bool remove_from_basis(unsigned); lar_term get_term_to_maximize(unsigned ext_j) const; + void set_cut_strategy(unsigned cut_frequency); }; } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 0ef385cab..b2e785064 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -102,10 +102,6 @@ struct stats { unsigned m_need_to_solve_inf; unsigned m_max_cols; unsigned m_max_rows; - unsigned m_chase_cut_solver_calls; - unsigned m_chase_cut_solver_true; - unsigned m_chase_cut_solver_false; - unsigned m_chase_cut_solver_undef; unsigned m_gcd_calls; unsigned m_gcd_conflicts; unsigned m_cube_calls; @@ -192,11 +188,9 @@ public: bool backup_costs; unsigned column_number_threshold_for_using_lu_in_lar_solver; unsigned m_int_gomory_cut_period; - unsigned m_int_chase_cut_solver_period; unsigned m_int_find_cube_period; unsigned m_hnf_cut_period; bool m_int_run_gcd_test; - unsigned m_chase_cut_solver_cycle_on_var; bool m_int_pivot_fixed_vars_from_basis; bool m_int_patch_only_integer_values; unsigned limit_on_rows_for_hnf_cutter; @@ -258,11 +252,9 @@ public: backup_costs(true), column_number_threshold_for_using_lu_in_lar_solver(4000), m_int_gomory_cut_period(4), - m_int_chase_cut_solver_period(8), m_int_find_cube_period(4), m_hnf_cut_period(4), m_int_run_gcd_test(true), - m_chase_cut_solver_cycle_on_var(10), m_int_pivot_fixed_vars_from_basis(false), m_int_patch_only_integer_values(true), limit_on_rows_for_hnf_cutter(75),