From 97b480ded34183201fbb3fd371f19cfead7cf696 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 24 May 2020 17:06:39 -0700 Subject: [PATCH] Expl (#4462) * cleaner API for explanation Signed-off-by: Lev Nachmanson * remove an unnecessery check Signed-off-by: Lev Nachmanson * expl Signed-off-by: Lev Nachmanson --- src/math/lp/explanation.h | 85 ++++++++++++++++++++++++-------------- src/math/lp/lar_solver.cpp | 6 +-- src/smt/theory_lra.cpp | 2 +- src/test/lp/gomory_test.h | 8 ++-- 4 files changed, 63 insertions(+), 38 deletions(-) diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index c80b94eaf..1b4bd9ddb 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -20,68 +20,93 @@ Revision History: #pragma once #include "math/lp/lp_utils.h" #include "util/map.h" -#include "util/optional.h" +#include "util/hashtable.h" namespace lp { class explanation { - u_map> m_j_to_mpq; + 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. + vector> m_vector; + ci_set m_set; public: explanation() {} + template explanation(const T& t) { - for ( unsigned c : t) + for (unsigned c : t) push_back(c); } - void clear() { m_j_to_mpq.reset(); } - void add_with_coeff(constraint_index j, const mpq& v) { - SASSERT(m_j_to_mpq.contains(j) == false); // if we hit the assert then we - // might start using summation - m_j_to_mpq.insert(j, optional(v)); + void clear() { m_vector.clear(); m_set.reset(); } + void add_pair(constraint_index j, const mpq& v) { + SASSERT(m_set.empty()); + m_vector.push_back(std::make_pair(j, v)); } // this signature is needed to use it in a template that also works for the vector type void push_back(constraint_index j) { - if (m_j_to_mpq.contains(j)) - return; - m_j_to_mpq.insert(j, optional()); + SASSERT(m_vector.empty()); + m_set.insert(j); } void add_expl(const explanation& e) { - for (const auto& p: e.m_j_to_mpq) { - m_j_to_mpq.insert(p.m_key, p.m_value); + if (e.m_vector.empty()) { + for (constraint_index j : e.m_set) + push_back(j); + } else { + for (const auto & p : e.m_vector) { + add_pair(p.first, p.second); + } } } - void add_pair(const std::pair& j) { - add_with_coeff(j.second, j.first); - } - - bool empty() const { return m_j_to_mpq.empty(); } - size_t size() const { return m_j_to_mpq.size(); } + bool empty() const { return m_vector.empty() || m_set.empty(); } + size_t size() const { return std::max(m_vector.size(), m_set.size()); } class cimpq { constraint_index m_var; - const optional & m_coeff; + const mpq& m_coeff; public: - cimpq(constraint_index var, const optional & val) : m_var(var), m_coeff(val) { } + cimpq(constraint_index var, const mpq & val) : m_var(var), m_coeff(val) { } constraint_index ci() const { return m_var; } - mpq coeff() const { return m_coeff.initialized()? *m_coeff: one_of_type(); } + const mpq &coeff() const { return m_coeff; } }; class iterator { - u_map>::iterator m_it; + bool m_run_on_vector; + pair_vec::const_iterator m_vi; + ci_set::iterator m_ci; public: cimpq operator*() const { - return cimpq(m_it->m_key, m_it->m_value); + return m_run_on_vector? + cimpq( m_vi->first, m_vi->second) : + cimpq( *m_ci, one_of_type()); } - iterator operator++() { iterator i = *this; m_it++; return i; } - iterator operator++(int) { m_it++; return *this; } - iterator(u_map>::iterator it) : m_it(it) {} - bool operator==(const iterator &other) const { return m_it == other.m_it; } + iterator operator++() { + if (m_run_on_vector) + m_vi++; + else + m_ci++; + return *this; + } + iterator operator++(int) { + iterator i = *this; ++(*this); return i; + } + iterator(bool run_on_vector, pair_vec::const_iterator vi, ci_set::iterator cii) : + m_run_on_vector(run_on_vector), m_vi(vi), m_ci(cii) + {} + bool operator==(const iterator &other) const { + SASSERT(m_run_on_vector == other.m_run_on_vector); + return m_run_on_vector? m_vi == other.m_vi : m_ci == other.m_ci; + } bool operator!=(const iterator &other) const { return !(*this == other); } }; - iterator begin() const { return iterator(m_j_to_mpq.begin()); } - iterator end() const { return iterator(m_j_to_mpq.end()); } + iterator begin() const { + return iterator( !m_vector.empty(), m_vector.begin(), m_set.begin()); + } + iterator end() const { + return iterator(!m_vector.empty(), m_vector.end(), m_set.end()); + } }; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f9f2e0696..dfc69fe48 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -307,8 +307,8 @@ void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evide // this is the case when the lower bound is in conflict with the upper one const ul_pair & ul = m_columns_to_ul_pairs[m_crossed_bounds_column]; - evidence.add_with_coeff(ul.upper_bound_witness(), numeric_traits::one()); - evidence.add_with_coeff(ul.lower_bound_witness(), -numeric_traits::one()); + evidence.add_pair(ul.upper_bound_witness(), numeric_traits::one()); + evidence.add_pair(ul.lower_bound_witness(), -numeric_traits::one()); } @@ -1195,7 +1195,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign( constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); lp_assert(m_constraints.valid_index(bound_constr_i)); - exp.add_with_coeff(bound_constr_i, coeff); + exp.add_pair(bound_constr_i, coeff); } } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b5595749b..f9352d798 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2344,7 +2344,7 @@ public: void consume(rational const& v, lp::constraint_index j) override { m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs); - m_imp.m_explanation.add_with_coeff(j, v); + m_imp.m_explanation.add_pair(j, v); } }; diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 4c2d68c5f..c7b0002cd 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -67,7 +67,7 @@ struct gomory_test { } k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than // k += lower_bound(x_j).x * new_a; - expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a); + expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { lp_assert(at_upper(x_j)); @@ -79,7 +79,7 @@ struct gomory_test { new_a = a / (mpq(1) - f_0); } k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; - expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a); + expl.add_pair(column_upper_bound_constraint(x_j), new_a); } TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << k << "\n";); pol.add_monomial(new_a, x_j); @@ -107,7 +107,7 @@ struct gomory_test { new_a = (1 - f_j) / f_0; } k.addmul(new_a, lower_bound(x_j).x); - expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a); + expl.add_pair(column_lower_bound_constraint(x_j), new_a); } else { lp_assert(at_upper(x_j)); @@ -119,7 +119,7 @@ struct gomory_test { } new_a.neg(); // the upper terms are inverted k.addmul(new_a, upper_bound(x_j).x); - expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a); + expl.add_pair(column_upper_bound_constraint(x_j), new_a); } TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << k << "\n";); t.add_monomial(new_a, x_j);