Skip to content

Commit 10c2af8

Browse files
try for mixed-mode
1 parent ead8478 commit 10c2af8

File tree

1 file changed

+9
-8
lines changed

1 file changed

+9
-8
lines changed

src/math/lp/int_solver.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -241,30 +241,32 @@ namespace lp {
241241

242242
auto refine_bound = [&](implied_bound const& ib) {
243243
unsigned j = ib.m_j;
244-
auto const& bound = ib.m_bound;
245-
if (!lra.column_is_int(j)) // for now, ignore non-integers.
246-
return l_undef;
244+
rational bound = ib.m_bound;
247245
if (ib.m_is_lower_bound) {
246+
if (lra.column_is_int(j))
247+
bound = ceil(bound);
248248
if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) >= bound)
249249
return l_undef;
250250
auto d = ib.explain_implied();
251-
if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) < ceil(bound)) {
251+
if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) < bound) {
252252
set_conflict(j, d, lra.get_column_upper_bound_witness(j));
253253
return l_false;
254254
}
255255

256-
lra.update_column_type_and_bound(j, lconstraint_kind::GE, ceil(bound), d);
256+
lra.update_column_type_and_bound(j, ib.m_strict ? lconstraint_kind::GT : lconstraint_kind::GE, bound, d);
257257
++num_refined_bounds;
258258
} else {
259+
if (lra.column_is_int(j))
260+
bound = floor(bound);
259261
if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) <= bound)
260262
return l_undef;
261263
auto d = ib.explain_implied();
262-
if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) > floor(bound)) {
264+
if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) > bound) {
263265
set_conflict(j, d, lra.get_column_lower_bound_witness(j));
264266
return l_false;
265267
}
266268

267-
lra.update_column_type_and_bound(j, lconstraint_kind::LE, floor(bound), d);
269+
lra.update_column_type_and_bound(j, ib.m_strict ? lconstraint_kind::LT : lconstraint_kind::LE, bound, d);
268270
++num_refined_bounds;
269271
}
270272
return l_true;
@@ -284,7 +286,6 @@ namespace lp {
284286
ibounds.clear();
285287
}
286288

287-
verbose_stream() << num_refined_bounds << "\n";
288289
return num_refined_bounds > 0 ? lia_move::continue_with_check : lia_move::undef;
289290
}
290291

0 commit comments

Comments
 (0)