mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8b9a80e232
commit
7ec02fc11f
|
@ -49,8 +49,8 @@ namespace lp {
|
|||
}
|
||||
|
||||
TRACE("int_solver",
|
||||
lia.display_column(tout << "branching v" << j << " = " << get_value(j) << "\n", j);
|
||||
tout << "k = " << m_k << std::endl;);
|
||||
lia.display_column(tout << "branching v" << j << " = " << lia.get_value(j) << "\n", j);
|
||||
tout << "k = " << lia.m_k << std::endl;);
|
||||
return lia_move::branch;
|
||||
}
|
||||
|
||||
|
@ -114,7 +114,7 @@ namespace lp {
|
|||
inf_int_count++;
|
||||
if (!lia.is_boxed(j))
|
||||
continue;
|
||||
lp_assert(!is_fixed(j));
|
||||
lp_assert(!lia.is_fixed(j));
|
||||
new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
|
||||
if (new_range > small_range_thresold)
|
||||
continue;
|
||||
|
|
|
@ -28,7 +28,7 @@ namespace lp {
|
|||
lia.settings().stats().m_cube_calls++;
|
||||
TRACE("cube",
|
||||
for (unsigned j = 0; j < lra.A_r().column_count(); j++)
|
||||
display_column(tout, j);
|
||||
lia.display_column(tout, j);
|
||||
tout << lra.constraints();
|
||||
);
|
||||
|
||||
|
@ -50,7 +50,7 @@ namespace lp {
|
|||
lra.pop();
|
||||
lra.round_to_integer_solution();
|
||||
lra.set_status(lp_status::FEASIBLE);
|
||||
lp_assert(lia.settings().get_cancel_flag() || is_feasible());
|
||||
lp_assert(lia.settings().get_cancel_flag() || lia.is_feasible());
|
||||
TRACE("cube", tout << "success";);
|
||||
lia.settings().stats().m_cube_success++;
|
||||
return lia_move::sat;
|
||||
|
|
Loading…
Reference in a new issue