mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix term indices for the time being when exiting from check()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-20 19:13:13 -07:00
parent 04824e7372
commit 64e542bd70
4 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith_int.h
View file

@ -1387,7 +1387,7 @@ namespace smt {
m_branch_cut_counter++; m_branch_cut_counter++;
// TODO: add giveup code // TODO: add giveup code
if (true || m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) { // remove true :todo if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) {
TRACE("opt_verbose", display(tout);); TRACE("opt_verbose", display(tout););
move_non_base_vars_to_bounds(); move_non_base_vars_to_bounds();
if (!make_feasible()) { if (!make_feasible()) {

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

@ -287,8 +287,6 @@ lia_move int_solver::report_gomory_cut(lar_term& t, mpq& k, mpq &lcm_den, unsign
gomory_cut_adjust_t_and_k_for_size_1(pol, t, k); gomory_cut_adjust_t_and_k_for_size_1(pol, t, k);
else else
gomory_cut_adjust_t_and_k_for_size_gt_1(pol, t, k, num_ints, lcm_den); gomory_cut_adjust_t_and_k_for_size_gt_1(pol, t, k, num_ints, lcm_den);
m_lar_solver->subs_term_columns(t);
lp_assert(current_solution_is_inf_on_cut(t, k));
return lia_move::cut; return lia_move::cut;
} }
@ -323,7 +321,12 @@ lia_move int_solver::mk_gomory_cut(lar_term& t, mpq& k, explanation & expl) {
if (t.is_empty()) if (t.is_empty())
return report_conflict_from_gomory_cut(k); return report_conflict_from_gomory_cut(k);
return report_gomory_cut(t, k, lcm_den, num_ints); auto ret = report_gomory_cut(t, k, lcm_den, num_ints);
// remove this call later :todo
m_lar_solver->subs_term_columns(t);
lp_assert(current_solution_is_inf_on_cut(t, k));
return ret;
} }
@ -398,7 +401,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
return lia_move::ok; return lia_move::ok;
if (true || (++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) { if ((++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) {
move_non_base_vars_to_bounds(); move_non_base_vars_to_bounds();
lp_status st = m_lar_solver->find_feasible_solution(); lp_status st = m_lar_solver->find_feasible_solution();
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
@ -421,15 +424,19 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
TRACE("arith_int", tout << "j" << j << " does not have an integer assignment: " << get_value(j) << "\n";); TRACE("arith_int", tout << "j" << j << " does not have an integer assignment: " << get_value(j) << "\n";);
lp_assert(t.is_empty()); lp_assert(t.is_empty());
t.add_monoid(1, j); t.add_monoid(mpq(1), j);
k = floor(get_value(j)); k = floor(get_value(j));
TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n"; TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
display_column(tout, j); display_column(tout, j);
tout << "k = " << k << std::endl; tout << "k = " << k << std::endl;
); );
// todo: remove this call later when theory_lra handles term indices
m_lar_solver->subs_term_columns(t);
lp_assert(current_solution_is_inf_on_cut(t, k));
return lia_move::branch; return lia_move::branch;
} }
} }
lp_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK()); lp_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
// return true; // return true;
return lia_move::give_up; return lia_move::give_up;

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

@ -468,7 +468,7 @@ public:
} }
mpq v = t.m_v; mpq v = t.m_v;
vector<std::pair<mpq, unsigned>> pol_after_subs; vector<std::pair<mpq, unsigned>> pol_after_subs;
// todo : remove the call to substitute_terms_in_linear_expression // todo : remove the call to substitute_terms_in_linear_expression, when theory_lra handles the terms indices
substitute_terms_in_linear_expression(pol, pol_after_subs, v); substitute_terms_in_linear_expression(pol, pol_after_subs, v);
t.clear(); t.clear();
t = lar_term(pol_after_subs, v); t = lar_term(pol_after_subs, v);

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

@ -205,7 +205,7 @@ public:
max_row_length_for_bound_propagation(300), max_row_length_for_bound_propagation(300),
backup_costs(true), backup_costs(true),
column_number_threshold_for_using_lu_in_lar_solver(4000), column_number_threshold_for_using_lu_in_lar_solver(4000),
m_int_branch_cut_threshold(10000000) m_int_branch_cut_threshold(100)
{} {}
void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; } void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }