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

do not add term to hnf if one of the vars has v.y value

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-10 14:25:22 -07:00
parent 5cfc3591d2
commit 2dfb8f53b6
2 changed files with 23 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2227,6 +2227,17 @@ void lar_solver::round_to_integer_solution() {
update_delta_for_terms(del, j, vars_to_terms[j]); update_delta_for_terms(del, j, vars_to_terms[j]);
} }
} }
// return true if all y coords are zeroes
bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
val = zero_of_type<mpq>();
for (const auto & c : t) {
const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()];
if (!is_zero(x.y))
return false;
val += x.x * c.coeff();
}
return true;
}
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const { bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const {
unsigned tj = term_index + m_terms_start_index; unsigned tj = term_index + m_terms_start_index;
@ -2236,26 +2247,27 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
return false; // the term does not have a bound because it does not correspond to a column return false; // the term does not have a bound because it does not correspond to a column
if (!is_int) // todo - allow for the next version of hnf if (!is_int) // todo - allow for the next version of hnf
return false; return false;
impq term_val; bool rs_is_calculated = false;
bool term_val_ready = false;
mpq b; mpq b;
bool is_strict; bool is_strict;
const lar_term& t = *terms()[term_index];
if (has_upper_bound(j, ci, b, is_strict) && !is_strict) { if (has_upper_bound(j, ci, b, is_strict) && !is_strict) {
lp_assert(b.is_int()); lp_assert(b.is_int());
term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x); if (!sum_first_coords(t, rs))
term_val_ready = true; return false;
if (term_val.x == b) { rs_is_calculated = true;
rs = b; if (rs == b) {
return true; return true;
} }
} }
if (has_lower_bound(j, ci, b, is_strict) && !is_strict) { if (has_lower_bound(j, ci, b, is_strict) && !is_strict) {
if (!term_val_ready) if (!rs_is_calculated){
term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x); if (!sum_first_coords(t, rs))
return false;
}
lp_assert(b.is_int()); lp_assert(b.is_int());
if (term_val.x == b) { if (rs == b) {
rs = b;
return true; return true;
} }
} }

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

@ -577,5 +577,6 @@ public:
bool remove_from_basis(unsigned); bool remove_from_basis(unsigned);
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;
}; };
} }