From 99538567a7873e78aff07bda98af3f9cf5461ae5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 3 Feb 2025 19:21:24 -1000 Subject: [PATCH] rebase with master Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 2 +- src/math/lp/dioph_eq.cpp | 21 +++++++++++---------- src/math/lp/explanation.h | 4 ++-- src/math/lp/gomory.cpp | 6 +++--- src/math/lp/lar_solver.h | 2 +- 5 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 791e64327..20e45a218 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -300,7 +300,7 @@ private: int a_sign = is_pos(a) ? 1 : -1; int sign = j_sign * a_sign; u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j); - ret = lar->mk_join(ret, witness); + ret = lar->join_deps(ret, witness); } return ret; }; diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index ec9d51a01..b7aac1a2f 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -843,7 +843,8 @@ namespace lp { if (!lia.column_is_int(p.var())) return false; } - return true; + return lia.column_is_int(term.j()); + } void delete_column(unsigned j) { @@ -1470,9 +1471,9 @@ namespace lp { if (lra.has_upper_bound(j, b_dep, rs, is_strict)) { if (m_c > rs || (is_strict && m_c == rs)) { u_dependency* dep = - lra.mk_join(explain_fixed(lra.get_term(j)), + lra.join_deps(explain_fixed(lra.get_term(j)), explain_fixed_in_meta_term(m_term_with_index.m_data)); - dep = lra.mk_join( + dep = lra.join_deps( dep, lra.get_bound_constraint_witnesses_for_column(j)); for (constraint_index ci : lra.flatten(dep)) { m_infeas_explanation.push_back(ci); @@ -1483,9 +1484,9 @@ namespace lp { if (lra.has_lower_bound(j, b_dep, rs, is_strict)) { if (m_c < rs || (is_strict && m_c == rs)) { u_dependency* dep = - lra.mk_join(explain_fixed(lra.get_term(j)), + lra.join_deps(explain_fixed(lra.get_term(j)), explain_fixed_in_meta_term(m_term_with_index.m_data)); - dep = lra.mk_join( + dep = lra.join_deps( dep, lra.get_bound_constraint_witnesses_for_column(j)); for (constraint_index ci : lra.flatten(dep)) { m_infeas_explanation.push_back(ci); @@ -1539,14 +1540,14 @@ namespace lp { lconstraint_kind kind = upper ? lconstraint_kind::LE : lconstraint_kind::GE; u_dependency* dep = prev_dep; - dep = lra.mk_join(dep, explain_fixed_in_meta_term(m_term_with_index.m_data)); + dep = lra.join_deps(dep, explain_fixed_in_meta_term(m_term_with_index.m_data)); u_dependency* j_bound_dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j); - dep = lra.mk_join(dep, j_bound_dep); - dep = lra.mk_join(dep, explain_fixed(lra.get_term(j))); + dep = lra.join_deps(dep, j_bound_dep); + dep = lra.join_deps(dep, explain_fixed(lra.get_term(j))); dep = - lra.mk_join(dep, lra.get_bound_constraint_witnesses_for_column(j)); + lra.join_deps(dep, lra.get_bound_constraint_witnesses_for_column(j)); TRACE("dioph_eq", tout << "jterm:"; print_lar_term_L(lra.get_term(j), tout) << "\ndep:"; print_deps(tout, dep) << std::endl;); @@ -1570,7 +1571,7 @@ namespace lp { if (is_fixed(p.j())) { u_dependency* bound_dep = lra.get_bound_constraint_witnesses_for_column(p.j()); - dep = lra.mk_join(dep, bound_dep); + dep = lra.join_deps(dep, bound_dep); } } return dep; diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index 33542a704..850e59cd4 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -26,10 +26,10 @@ class explanation { typedef vector> pair_vec; typedef hashtable ci_set; // Only one of the fields below is used. The first call adding an entry decides which one it is. -public: vector> m_vector; ci_set m_set; - explanation() {} +public: + explanation() = default; template explanation(const T& t) { diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 442231558..c6f9a4123 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -323,7 +323,7 @@ public: m_dep = nullptr; for (auto c : *m_ex) - m_dep = lia.lra.mk_join(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep); + m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout); lia.lra.display(tout)); @@ -470,10 +470,10 @@ public: if (!p.coeff().is_int()) continue; // the explanation for all above have been already added if (lia.at_lower(j)) - ret = lia.lra.dep_manager().mk_join(lia.column_lower_bound_constraint(j), ret); + ret = lia.lra.join_deps(lia.column_lower_bound_constraint(j), ret); else { SASSERT(lia.at_upper(j)); - ret = lia.lra.dep_manager().mk_join(lia.column_upper_bound_constraint(j), ret); + ret = lia.lra.join_deps(lia.column_upper_bound_constraint(j), ret); } } return ret; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index e7d429cee..ad18947e3 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -606,7 +606,7 @@ public: } void explain_fixed_column(unsigned j, explanation& ex); - u_dependency* mk_join(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } + u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } inline constraint_set const& constraints() const { return m_constraints; } void push(); void pop();