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

adjust cuts and branch (m_t and m_k) for terms

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-14 12:39:46 -07:00
parent 257ba6218f
commit 26764b076f
4 changed files with 24 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -383,19 +383,25 @@ typedef monomial mono;
// this will allow to enable and disable tracking of the pivot rows // this will allow to enable and disable tracking of the pivot rows
struct pivoted_rows_tracking_control { struct check_return_helper {
lar_solver * m_lar_solver; lar_solver * m_lar_solver;
bool m_track_pivoted_rows; const lia_move & m_r;
pivoted_rows_tracking_control(lar_solver* ls) : bool m_track_pivoted_rows;
check_return_helper(lar_solver* ls, const lia_move& r) :
m_lar_solver(ls), m_lar_solver(ls),
m_r(r),
m_track_pivoted_rows(ls->get_track_pivoted_rows()) m_track_pivoted_rows(ls->get_track_pivoted_rows())
{ {
TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;); TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
m_lar_solver->set_track_pivoted_rows(false); m_lar_solver->set_track_pivoted_rows(false);
} }
~pivoted_rows_tracking_control() { ~check_return_helper() {
TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;); TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows); m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
if (m_r == lia_move::cut || m_r == lia_move::branch) {
int_solver * s = m_lar_solver->get_int_solver();
m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
}
} }
}; };
@ -615,7 +621,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) {
lia_move r = run_gcd_test(); lia_move r = run_gcd_test();
if (r != lia_move::undef) return r; if (r != lia_move::undef) return r;
pivoted_rows_tracking_control pc(m_lar_solver); check_return_helper pc(m_lar_solver, r);
if(settings().m_int_pivot_fixed_vars_from_basis) if(settings().m_int_pivot_fixed_vars_from_basis)
m_lar_solver->pivot_fixed_vars_from_basis(); m_lar_solver->pivot_fixed_vars_from_basis();

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

@ -160,5 +160,5 @@ public:
bool hnf_has_var_with_non_integral_value() const; bool hnf_has_var_with_non_integral_value() const;
bool hnf_cutter_is_full() const; bool hnf_cutter_is_full() const;
void patch_nbasic_column(unsigned j, bool patch_only_int_vals); void patch_nbasic_column(unsigned j, bool patch_only_int_vals);
}; };
} }

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

@ -2265,6 +2265,16 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) {
} }
} }
void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) {
for (const auto& p : t) {
if (!is_term(p.var())) continue;
const lar_term & p_term = get_term(p.var());
if (p_term.m_v.is_zero()) continue;
rs -= p.coeff() * p_term.m_v;
}
}
} // namespace lp } // namespace lp

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

@ -584,5 +584,6 @@ public:
lar_term get_term_to_maximize(unsigned ext_j) const; lar_term get_term_to_maximize(unsigned ext_j) const;
void set_cut_strategy(unsigned cut_frequency); void set_cut_strategy(unsigned cut_frequency);
bool sum_first_coords(const lar_term& t, mpq & val) const; bool sum_first_coords(const lar_term& t, mpq & val) const;
void adjust_cut_for_terms(const lar_term& t, mpq & rs);
}; };
} }