mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

adjust hnf

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

change in settings + random in adding terms to hnf

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

add terms in hnf from the beginning

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

adjusting settings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

remove non used determinant()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-22 09:51:33 -07:00
parent eeaca949e0
commit e5eea467b7
9 changed files with 36 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_internalizer.cpp
View file

@ -849,7 +849,7 @@ namespace smt {
std::cerr << v << " ::=\n" << mk_ll_pp(n, m_manager) << "<END-OF-FORMULA>\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);

18
src/smt/theory_lra.cpp
View file

@ -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);

38
src/test/lp/lp.cpp
View file

@ -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<unsigned> 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<unsigned> 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) {

20
src/util/lp/hnf.h
View file

@ -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<unsigned> & 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 <typename M>
mpq determinant(const M& m) {
lp_assert(m.row_count() == m.column_count());
auto mc = m;
svector<unsigned> basis_rows;
mpq d = determinant_of_rectangular_matrix(mc, basis_rows);
return basis_rows.size() < m.row_count() ? zero_of_type<mpq>() : d;
}
} // end of namespace hnf_calc
template <typename M> // M is the matrix type

10
src/util/lp/int_solver.cpp
View file

@ -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<mpq> * 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);
}

2
src/util/lp/int_solver.h
View file

@ -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

16
src/util/lp/lar_solver.cpp
View file

@ -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

1
src/util/lp/lar_solver.h
View file

@ -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);
};
}

8
src/util/lp/lp_settings.h
View file

@ -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),