From e0a08f16d3dd3cb7bec707d2a1ccf673b994f4a1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 1 Nov 2024 12:52:16 -0700 Subject: [PATCH] fix the build Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index efd3fc4e1..b62c17d1c 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -418,7 +418,7 @@ namespace lp { template term_o fix_vars(const T& t) const { term_o ret; - for (auto& p: t) { + for (const auto& p: t) { if (is_fixed(p.var())) { ret.c() += p.coeff() * this->lra.get_lower_bound(p.var()).x; } else { @@ -446,20 +446,6 @@ namespace lp { subs_front_in_indexed_vector(q); } - void debug_remove_fresh_vars(term_o& t) { - std::queue q; - for (const auto& p: t) { - if (is_fresh_var(p.j())) { - q.push(p.j()); - } - } - while (!q.empty()) { - unsigned j = pop_front(q); - - } - - } - lia_move tighten_with_S() { int change = 0; for (unsigned j = 0; j < lra.column_count(); j++) { @@ -1001,7 +987,7 @@ public: return j >= lra.column_count(); } bool can_substitute(unsigned k) { - return k < m_k2s.size() && m_k2s[k] != -1; + return k < m_k2s.size() && m_k2s[k] != UINT_MAX; } u_dependency * eq_deps(const lar_term& t) { NOT_IMPLEMENTED_YET();