From bd2e73014cfd2345a26c8e9ebe0caf1d898305ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Aug 2021 19:40:33 -0700 Subject: [PATCH] wip Signed-off-by: Nikolaj Bjorner --- src/math/polysat/fixplex.h | 3 +- src/math/polysat/fixplex_def.h | 70 +++++++++++++++----------------- src/math/simplex/sparse_matrix.h | 29 +++++++------ 3 files changed, 49 insertions(+), 53 deletions(-) diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index a68710ff9..cdfd947fb 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -331,8 +331,7 @@ namespace polysat { bool eliminate_var( row const& r_y, - row const& r_z, - numeral const& c, + col_iterator const& z_col, unsigned tz_b, numeral const& old_value_y); }; diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 51e09606e..efbb26e74 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -172,7 +172,6 @@ namespace polysat { } } SASSERT(well_formed()); - std::cout << "non-integral: " << m_num_non_integral << "\n"; if (ineqs_are_violated()) return l_false; if (ineqs_are_satisfied() && m_num_non_integral == 0) @@ -257,9 +256,8 @@ namespace polysat { for (auto col : M.col_entries(v)) { if (r.id() == col.get_row().id()) continue; - numeral c = col.get_row_entry().coeff(); numeral value_v = value(v); - if (!eliminate_var(r, col.get_row(), c, tz_b, value_v)) + if (!eliminate_var(r, col, tz_b, value_v)) return false; } return true; @@ -365,17 +363,12 @@ namespace polysat { numeral new_value = m_vars[x].closest_value(value(x)); numeral b; var_t y = select_pivot_core(x, new_value, b); - - if (y == null_var) { - if (is_infeasible_row(x)) - return l_false; - else - return l_undef; - } - - pivot(x, y, b, new_value); - - return l_true; + if (y != null_var) + return pivot(x, y, b, new_value), l_true; + else if (is_infeasible_row(x)) + return l_false; + else + return l_undef; } template @@ -600,6 +593,13 @@ namespace polysat { template void fixplex::add_ineq(var_t v, var_t w, unsigned dep, bool strict) { + if (inconsistent()) + return; + if (v == w) { + if (strict) + conflict(mk_leaf(dep)); + return; + } ensure_var(v); ensure_var(w); unsigned idx = m_ineqs.size(); @@ -683,7 +683,6 @@ namespace polysat { return false; } - /** * Check if the coefficient b of y has the minimal number of trailing zeros. * In other words, the coefficient b is a multiple of the smallest power of 2. @@ -799,17 +798,17 @@ namespace polysat { */ template void fixplex::pivot(var_t x, var_t y, numeral const& b, numeral const& new_value) { - ++m_stats.m_num_pivots; - TRACE("fixplex", tout << "pivot " << x << " " << y << "\n";); - + ++m_stats.m_num_pivots; SASSERT(is_base(x)); SASSERT(!is_base(y)); var_info& xI = m_vars[x]; var_info& yI = m_vars[y]; unsigned rx = xI.m_base2row; auto& row_x = m_rows[rx]; + row r_x(rx); numeral const& a = row_x.m_base_coeff; numeral old_value_y = yI.m_value; + TRACE("fixplex", display_row(tout << "pivot " << x << " " << y << "\n", r_x);); row_x.m_base = y; row_x.m_value = row_x.m_value - b * old_value_y + a * new_value; row_x.m_base_coeff = b; @@ -819,20 +818,18 @@ namespace polysat { xI.m_is_base = false; xI.m_value = new_value; touch_var(x); - row r_x(rx); add_patch(y); SASSERT(well_formed_row(r_x)); unsigned tz_b = m.trailing_zeros(b); - for (auto col : M.col_entries(y)) { + for (auto const& col : M.col_entries(y)) { row r_z = col.get_row(); unsigned rz = r_z.id(); if (rz == rx) continue; TRACE("fixplex,", display_row(tout << "eliminate ", r_z, false) << "\n";); - numeral c = col.get_row_entry().coeff(); - VERIFY(eliminate_var(r_x, r_z, c, tz_b, old_value_y)); + VERIFY(eliminate_var(r_x, col, tz_b, old_value_y)); TRACE("fixplex,", display_row(tout << "eliminated ", r_z, false) << "\n";); add_patch(row2base(r_z)); } @@ -841,37 +838,34 @@ namespace polysat { /** * r_y - row where y is base variable - * r_z - row that contains y with z base variable, z != y - * c - coefficient of y in r_z + * z_col - column iterator that contains row where z is base variable. * tz_b - number of trailing zeros to coefficient of y in r_y * old_value_y - the value of y used to compute row2value(r_z) * + * Implied variables: + * r_z - row that contains y with z base variable, z != y + * c - coefficient of y in r_z + * * returns true if elimination preserves equivalence (is lossless). */ template bool fixplex::eliminate_var( row const& r_y, - row const& r_z, - numeral const& c, + col_iterator const& z_col, unsigned tz_b, numeral const& old_value_y) { + row const& r_z = z_col.get_row(); + numeral c = z_col.get_row_entry().coeff(); numeral b = row2base_coeff(r_y); - auto z = row2base(r_z); - auto& row_z = m_rows[r_z.id()]; + auto z = row2base(r_z); unsigned tz_c = m.trailing_zeros(c); - numeral b1, c1; - if (tz_b <= tz_c) { - b1 = b >> tz_b; - c1 = 0 - (c >> tz_b); - } - else { - b1 = b >> tz_c; - c1 = 0 - (c >> tz_c); - } - + unsigned tz = std::min(tz_b, tz_c); + numeral b1 = b >> tz; + numeral c1 = 0 - (c >> tz); M.mul(r_z, b1); M.add(r_z, c1, r_y); + auto& row_z = m_rows[r_z.id()]; row_z.m_value = (b1 * (row2value(r_z) - c * old_value_y)) + c1 * row2value(r_y); row_z.m_base_coeff *= b1; set_base_value(z); diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 9c7e46425..ea0cf76fe 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -32,6 +32,8 @@ namespace simplex { typedef typename Ext::manager manager; typedef unsigned var_t; + struct column; + class row_entry { friend class sparse_matrix; numeral m_coeff; @@ -85,8 +87,7 @@ namespace simplex { col_entry(): m_row_id(0), m_row_idx(0) {} bool is_dead() const { return (unsigned) m_row_id == dead_id; } }; - - struct column; + /** \brief A row contains a base variable and set of @@ -110,29 +111,31 @@ namespace simplex { int get_idx_of(var_t v) const; }; + /** - \brief A column stores in which rows a variable occurs. - The column may have free/dead entries. The field m_first_free_idx - is a reference to the first free/dead entry. + \brief A column stores in which rows a variable occurs. + The column may have free/dead entries. The field m_first_free_idx + is a reference to the first free/dead entry. */ struct column { svector m_entries; - unsigned m_size; + unsigned m_size; int m_first_free_idx; mutable unsigned m_refs; - - column():m_size(0), m_first_free_idx(-1), m_refs(0) {} + + column() :m_size(0), m_first_free_idx(-1), m_refs(0) {} unsigned size() const { return m_size; } unsigned num_entries() const { return m_entries.size(); } void reset(); - void compress(vector<_row> & rows); - void compress_if_needed(vector<_row> & rows); + void compress(vector<_row>& rows); + void compress_if_needed(vector<_row>& rows); //void compress_singleton(vector<_row> & rows, unsigned singleton_pos); - col_entry const * get_first_col_entry() const; - col_entry & add_col_entry(int & pos_idx); + col_entry const* get_first_col_entry() const; + col_entry& add_col_entry(int& pos_idx); void del_col_entry(unsigned idx); }; + manager& m; vector<_row> m_rows; svector m_dead_rows; // rows to recycle @@ -258,7 +261,7 @@ namespace simplex { row get_row() const { return row(col().m_entries[m_curr].m_row_id); } - row_entry const& get_row_entry() { + row_entry const& get_row_entry() const { col_entry const& c = col().m_entries[m_curr]; int row_id = c.m_row_id; return m_sm.m_rows[row_id].m_entries[c.m_row_idx];