mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
avoid big nums in is_offset_row in cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
713eb6319d
commit
50b9915c57
|
@ -144,7 +144,6 @@ bool lar_solver::row_has_a_big_num(unsigned i) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
|
||||
void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
|
||||
// todo : create a map from term basic vars to the rows where they are used
|
||||
unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i];
|
||||
|
|
|
@ -151,8 +151,12 @@ public:
|
|||
x = y = null_lpvar;
|
||||
for (auto& c : lp().get_row(r)) {
|
||||
lpvar v = c.var();
|
||||
if (column_is_fixed(v))
|
||||
if (column_is_fixed(v)) {
|
||||
// if (get_lower_bound_rational(c.var()).is_big())
|
||||
// return false;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (c.coeff().is_one() && x == null_lpvar) {
|
||||
x = v;
|
||||
continue;
|
||||
|
@ -173,6 +177,8 @@ public:
|
|||
if (!column_is_fixed(c.var()))
|
||||
continue;
|
||||
k -= c.coeff() * get_lower_bound_rational(c.var());
|
||||
if (k.is_big())
|
||||
return false;
|
||||
}
|
||||
|
||||
if (y == null_lpvar)
|
||||
|
@ -184,7 +190,7 @@ public:
|
|||
return true;
|
||||
}
|
||||
|
||||
if (/*r.get_base_var() != x &&*/ x > y) {
|
||||
if (!lp().is_base(x) && x > y) {
|
||||
std::swap(x, y);
|
||||
k.neg();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue