mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

detect non integral terms in dio

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-14 05:17:33 -10:00 committed by Lev Nachmanson
parent a62d664ae4
commit 7c12a029e2
3 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/math/lp/dioph_eq.cpp
View file

@ -331,6 +331,7 @@ namespace lp {
return out; return out;
} }
bool m_has_non_integral_term = false;
std_vector<mpq> m_sum_of_fixed; std_vector<mpq> m_sum_of_fixed;
var_register m_var_register; var_register m_var_register;
// the terms are stored in m_A and m_c // the terms are stored in m_A and m_c
@ -740,6 +741,7 @@ namespace lp {
TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;); TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
if (!lra.column_is_int(j)) { if (!lra.column_is_int(j)) {
TRACE("dio", tout << "ignored a non-integral column" << std::endl;); TRACE("dio", tout << "ignored a non-integral column" << std::endl;);
m_has_non_integral_term = true;
return; return;
} }
@ -2622,7 +2624,9 @@ namespace lp {
// needed for the template bound_analyzer_on_row.h // needed for the template bound_analyzer_on_row.h
const lar_solver& lp() const { return lra; } const lar_solver& lp() const { return lra; }
lar_solver& lp() {return lra;} lar_solver& lp() {return lra;}
bool has_non_integral_term() const {
return m_has_non_integral_term;
}
}; };
// Constructor definition // Constructor definition
dioph_eq::dioph_eq(int_solver& lia) { dioph_eq::dioph_eq(int_solver& lia) {
@ -2640,4 +2644,9 @@ namespace lp {
m_imp->explain(ex); m_imp->explain(ex);
} }
bool dioph_eq::has_non_integral_term() const {
return m_imp->has_non_integral_term();
}
} // namespace lp } // namespace lp

1
src/math/lp/dioph_eq.h
View file

@ -30,5 +30,6 @@ namespace lp {
~dioph_eq(); ~dioph_eq();
lia_move check(); lia_move check();
void explain(lp::explanation&); void explain(lp::explanation&);
bool has_non_integral_term() const;
}; };
} }

6
src/math/lp/int_solver.cpp
View file

@ -189,8 +189,10 @@ namespace lp {
} }
bool should_gomory_cut() { bool should_gomory_cut() {
return (!all_columns_are_integral() ||(!settings().dio_eqs() || settings().dio_enable_gomory_cuts())) bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
&& m_number_of_calls % settings().m_int_gomory_cut_period == 0; m_dio.has_non_integral_term();
return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
} }
bool should_solve_dioph_eq() { bool should_solve_dioph_eq() {