Skip to content

Commit b0383da

Browse files
committed
fix a bug in dio
1 parent 7fe703e commit b0383da

File tree

1 file changed

+9
-8
lines changed

1 file changed

+9
-8
lines changed

src/math/lp/dioph_eq.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -233,9 +233,7 @@ namespace lp {
233233
// {coeff*lar.get_term(k)})
234234

235235
std_vector<unsigned> m_k2s;
236-
std_vector<unsigned> m_fresh_definitions; // seems only needed in the debug
237-
// version in remove_fresh_vars
238-
236+
std_vector<unsigned> m_fresh_definitions;
239237
unsigned m_conflict_index = -1; // m_entries[m_conflict_index] gives the conflict
240238
unsigned m_max_number_of_iterations = 100;
241239
unsigned m_number_of_iterations;
@@ -304,7 +302,7 @@ namespace lp {
304302
void fill_entry(const lar_term& t) {
305303
TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;);
306304
entry te = {lar_term(t.j()), mpq(0), entry_status::F};
307-
unsigned entry_index = m_entries.size();
305+
unsigned entry_index = (unsigned)m_entries.size();
308306
m_f.push_back(entry_index);
309307
m_entries.push_back(te);
310308
entry& e = m_entries.back();
@@ -928,7 +926,10 @@ namespace lp {
928926
}
929927
TRACE("dio_br", lra.print_column_info(b.m_j, tout) <<"add bound" << std::endl;);
930928
if (lra.column_is_fixed(b.m_j)) {
931-
if (fix_var(lar_solver_to_local(b.m_j)) == lia_move::conflict) {
929+
unsigned local_b_mj;
930+
if (!m_var_register.external_is_used(b.m_j, local_b_mj))
931+
return lia_move::undef;
932+
if (fix_var(local_b_mj) == lia_move::conflict) {
932933
TRACE("dio_br", tout << "conflict in fix_var" << std::endl;) ;
933934
return lia_move::conflict;
934935
}
@@ -1024,7 +1025,7 @@ namespace lp {
10241025
}
10251026

10261027
unsigned get_number_of_int_inf() const {
1027-
return std::count_if(
1028+
return (unsigned)std::count_if(
10281029
lra.r_basis().begin(), lra.r_basis().end(),
10291030
[this](unsigned j) {
10301031
return lia.column_is_int_inf(j);
@@ -1165,7 +1166,7 @@ namespace lp {
11651166
[ei](const auto& cell) {
11661167
return cell.var() == ei;
11671168
});
1168-
unsigned pivot_col_cell_index = std::distance(column.begin(), it);
1169+
unsigned pivot_col_cell_index = (unsigned) std::distance(column.begin(), it);
11691170
if (pivot_col_cell_index != 0) {
11701171
// swap the pivot column cell with the head cell
11711172
auto c = column[0];
@@ -1328,7 +1329,7 @@ namespace lp {
13281329
m_e_matrix.add_new_element(fresh_row, i, q);
13291330
}
13301331

1331-
m_k2s.resize(std::max(k + 1, xt + 1), -1);
1332+
m_k2s.resize(k + 1, -1);
13321333
m_k2s[k] = fresh_row;
13331334
m_fresh_definitions.resize(xt + 1, -1);
13341335
m_fresh_definitions[xt] = fresh_row;

0 commit comments

Comments
 (0)