mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

add stub for cheap equality propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-30 15:36:17 -07:00
parent 6a45c5d17c
commit d372af4782
13 changed files with 131 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

50
src/math/lp/bound_analyzer_on_row.h
View file

@ -55,6 +55,17 @@ public :
m_rs(rs)
{}
static void analyze_row(const C & row,
unsigned bj, // basis column for the row
const numeric_pair<mpq>& rs,
unsigned row_or_term_index,
lp_bound_propagator & bp) {
bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
a.analyze();
// TBD: a.analyze_eq();
}
private:
void analyze() {
for (const auto & c : m_row) {
@ -73,6 +84,37 @@ public :
limit_all_monoids_from_above();
}
void analyze_eq() {
lpvar x = null_lpvar, y = null_lpvar;
for (const auto & c : m_row) {
if (m_bp.get_column_type(c.var()) == column_type::fixed)
continue;
if (x == null_lpvar && c.coeff().is_one())
x = c.var();
else if (y == null_lpvar && c.coeff().is_minus_one())
y = c.var();
else
return;
}
if (x == null_lpvar || y == null_lpvar)
return;
impq value;
for (const auto & c : m_row) {
if (m_bp.get_column_type(c.var()) == column_type::fixed)
value += c.coeff() * lb(c.var());
}
if (!value.is_zero()) {
// insert / check offset table to infer equalities
// of the form y = z from offset table collision:
// value = (x - y)
// value = (x - z)
}
else {
// m_bp.try_add_fixed(x, y, m_row_or_term_index);
}
}
bool bound_is_available(unsigned j, bool lower_bound) {
return (lower_bound && lower_bound_is_available(j)) ||
(!lower_bound && upper_bound_is_available(j));
@ -319,14 +361,6 @@ public :
}
}
static void analyze_row(const C & row,
unsigned bj, // basis column for the row
const numeric_pair<mpq>& rs,
unsigned row_or_term_index,
lp_bound_propagator & bp) {
bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
a.analyze();
}
};
}

2
src/math/lp/lar_core_solver.h
View file

@ -631,7 +631,7 @@ public:
for (unsigned i = 0; i < m_r_A.row_count(); i++) {
auto & row = m_r_A.m_rows[i];
for (row_cell<mpq> & c : row) {
A.add_new_element(i, c.var(), c.get_val().get_double());
A.add_new_element(i, c.var(), c.coeff().get_double());
}
}
}

2
src/math/lp/lar_core_solver_def.h
View file

@ -227,7 +227,7 @@ void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() {
m_infeasible_sum_sign = m_r_solver.inf_sign_of_column(bj);
m_infeasible_linear_combination.clear();
for (auto & rc : m_r_solver.m_A.m_rows[m_r_solver.m_inf_row_index_for_tableau]) {
m_infeasible_linear_combination.push_back(std::make_pair( rc.get_val(), rc.var()));
m_infeasible_linear_combination.push_back(std::make_pair(rc.coeff(), rc.var()));
}
}

25
src/math/lp/lar_solver.cpp
View file

@ -141,14 +141,16 @@ void lar_solver::analyze_new_bounds_on_row(
lp_bound_propagator & bp) {
lp_assert(!use_tableau());
unsigned j = m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row
bound_analyzer_on_row<indexed_vector<mpq>>
ra_pos(m_mpq_lar_core_solver.get_pivot_row(),
j,
zero_of_type<numeric_pair<mpq>>(),
row_index,
bp
);
ra_pos.analyze();
bound_analyzer_on_row<indexed_vector<mpq>>::analyze_row(
m_mpq_lar_core_solver.get_pivot_row(),
j,
zero_of_type<numeric_pair<mpq>>(),
row_index,
bp
);
// ra_pos.analyze();
}
bool lar_solver::row_has_a_big_num(unsigned i) const {
@ -167,6 +169,7 @@ void lar_solver::analyze_new_bounds_on_row_tableau(
|| row_has_a_big_num(row_index))
return;
lp_assert(use_tableau());
bound_analyzer_on_row<row_strip<mpq>>::analyze_row(A_r().m_rows[row_index],
null_ci,
zero_of_type<numeric_pair<mpq>>(),
@ -227,7 +230,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
for (auto const& r : A_r().m_rows[i]) {
unsigned j = r.var();
if (j == bound_j) continue;
mpq const& a = r.get_val();
mpq const& a = r.coeff();
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;
const ul_pair & ul = m_columns_to_ul_pairs[j];
@ -948,7 +951,7 @@ void lar_solver::copy_from_mpq_matrix(static_matrix<U, V> & matr) {
matr.m_columns.resize(A_r().column_count());
for (unsigned i = 0; i < matr.row_count(); i++) {
for (auto & it : A_r().m_rows[i]) {
matr.set(i, it.var(), convert_struct<U, mpq>::convert(it.get_val()));
matr.set(i, it.var(), convert_struct<U, mpq>::convert(it.coeff()));
}
}
}
@ -1399,7 +1402,7 @@ void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) {
for (unsigned k = last_row.size(); k-- > 0;) {
auto &rc = last_row[k];
if (cost_is_nz) {
m_mpq_lar_core_solver.m_r_solver.m_d[rc.var()] += cost_j*rc.get_val();
m_mpq_lar_core_solver.m_r_solver.m_d[rc.var()] += cost_j * rc.coeff();
}
A_r().remove_element(last_row, rc);
}

1
src/math/lp/lp_bound_propagator.h
View file

@ -18,6 +18,7 @@ public:
const impq & get_lower_bound(unsigned) const;
const impq & get_upper_bound(unsigned) const;
void try_add_bound(mpq const & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict);
void try_add_eq(lpvar x, lpvar y, unsigned row_or_term_index) {} // TBD
virtual bool bound_is_interesting(unsigned vi,
lp::lconstraint_kind kind,
const rational & bval) {return true;}

16
src/math/lp/lp_core_solver_base_def.h
View file

@ -95,7 +95,7 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
return;
for (const row_cell<T> & r: m_A.m_rows[i]){
if (r.var() != j)
m_d[r.var()] -= a * r.get_val();
m_d[r.var()] -= a * r.coeff();
}
a = zero_of_type<T>(); // zero the pivot column's m_d finally
}
@ -304,7 +304,7 @@ calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
for (auto & c : m_A.m_rows[i]) {
unsigned j = c.var();
if (m_basis_heading[j] < 0) {
m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.get_val() * pi_1);
m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1);
}
}
}
@ -444,7 +444,7 @@ rs_minus_Anx(vector<X> & rs) {
for (auto & it : m_A.m_rows[row]) {
unsigned j = it.var();
if (m_basis_heading[j] < 0) {
rsv -= m_x[j] * it.get_val();
rsv -= m_x[j] * it.coeff();
}
}
}
@ -630,8 +630,8 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
column[0] = column[pivot_col_cell_index];
column[pivot_col_cell_index] = c;
m_A.m_rows[piv_row_index][column[0].m_offset].m_offset = 0;
m_A.m_rows[c.var()][c.m_offset].m_offset = pivot_col_cell_index;
m_A.m_rows[piv_row_index][column[0].offset()].offset() = 0;
m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
}
while (column.size() > 1) {
auto & c = column.back();
@ -761,7 +761,7 @@ fill_reduced_costs_from_m_y_by_rows() {
for (row_cell<T> & c : m_A.m_rows[i]) {
j = c.var();
if (m_basis_heading[j] < 0) {
m_d[j] -= y * c.get_val();
m_d[j] -= y * c.coeff();
}
}
}
@ -804,7 +804,7 @@ find_error_in_BxB(vector<X>& rs){
for (auto & it : m_A.m_rows[row]) {
unsigned j = it.var();
if (m_basis_heading[j] >= 0) {
rsv -= m_x[j] * it.get_val();
rsv -= m_x[j] * it.coeff();
}
}
}
@ -1046,7 +1046,7 @@ void lp_core_solver_base<T, X>::calculate_pivot_row(unsigned i) {
unsigned basic_j = m_basis[i];
for (auto & c : m_A.m_rows[i]) {
if (c.var() != basic_j)
m_pivot_row.set_value(c.get_val(), c.var());
m_pivot_row.set_value(c.coeff(), c.var());
}
return;
}

14
src/math/lp/lp_primal_core_solver.h
View file

@ -180,19 +180,19 @@ public:
case column_type::fixed:
return false;
case column_type::lower_bound:
if (is_pos(rc.get_val())) {
if (is_pos(rc.coeff())) {
return this->x_above_lower_bound(j);
}
return true;
case column_type::upper_bound:
if (is_pos(rc.get_val())) {
if (is_pos(rc.coeff())) {
return true;
}
return this->x_below_upper_bound(j);
case column_type::boxed:
if (is_pos(rc.get_val())) {
if (is_pos(rc.coeff())) {
return this->x_above_lower_bound(j);
}
@ -213,19 +213,19 @@ public:
case column_type::fixed:
return false;
case column_type::lower_bound:
if (is_neg(rc.get_val())) {
if (is_neg(rc.coeff())) {
return this->x_above_lower_bound(j);
}
return true;
case column_type::upper_bound:
if (is_neg(rc.get_val())) {
if (is_neg(rc.coeff())) {
return true;
}
return this->x_below_upper_bound(j);
case column_type::boxed:
if (is_neg(rc.get_val())) {
if (is_neg(rc.coeff())) {
return this->x_above_lower_bound(j);
}
@ -923,7 +923,7 @@ public:
unsigned k = rc.var();
if (k == j)
continue;
this->m_d[k] += delta * rc.get_val();
this->m_d[k] += delta * rc.coeff();
}
}

2
src/math/lp/lu_def.h
View file

@ -391,7 +391,7 @@ void lu< M>::find_error_of_yB_indexed(const indexed_vector<T>& y, const vector<i
if (hj < 0) continue;
if (m_ii.m_data[hj] == 0)
m_ii.set_value(1, hj);
m_y_copy.m_data[hj] -= c.get_val() * y_k;
m_y_copy.m_data[hj] -= c.coeff() * y_k;
}
}
// add the index of m_y_copy to m_ii

68
src/math/lp/static_matrix.h
View file

@ -1,21 +1,10 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#pragma once
@ -30,27 +19,26 @@ Revision History:
namespace lp {
template <typename T>
struct row_cell {
unsigned m_j; // points to the column
unsigned m_offset; // offset in column
T m_value;
row_cell(unsigned j, unsigned offset, T const & val) : m_j(j), m_offset(offset), m_value(val) {
class row_cell {
unsigned m_j; // points to the column
unsigned m_offset; // offset in column
T m_coeff; // coefficient
public:
row_cell(unsigned j, unsigned offset, T const & val) : m_j(j), m_offset(offset), m_coeff(val) {
}
row_cell(unsigned j, unsigned offset) : m_j(j), m_offset(offset) {
}
const T & get_val() const { return m_value;}
T & get_val() { return m_value;}
const T & coeff() const { return m_value;}
T & coeff() { return m_value;}
unsigned var() const { return m_j;}
unsigned & var() { return m_j;}
unsigned offset() const { return m_offset;}
unsigned & offset() { return m_offset;}
inline const T & coeff() const { return m_coeff; }
inline T & coeff() { return m_coeff; }
inline unsigned var() const { return m_j; }
inline unsigned & var() { return m_j; }
inline unsigned offset() const { return m_offset; }
inline unsigned & offset() { return m_offset; }
};
template <typename T>
std::ostream& operator<<(std::ostream& out, const row_cell<T>& rc) {
return out << "(m_j=" << rc.m_j << ", m_offset= " << rc.m_offset << ", m_value=" << rc.m_value << ")";
return out << "(j=" << rc.var() << ", offset= " << rc.offset() << ", coeff=" << rc.coeff() << ")";
}
struct empty_struct {};
typedef row_cell<empty_struct> column_cell;
@ -102,11 +90,11 @@ public:
public:
const T & get_val(const column_cell & c) const {
return m_rows[c.var()][c.m_offset].get_val();
return m_rows[c.var()][c.offset()].coeff();
}
column_cell & get_column_cell(const row_cell<T> &rc) {
return m_columns[rc.m_j][rc.m_offset];
return m_columns[rc.var()][rc.offset()];
}
void init_row_columns(unsigned m, unsigned n);
@ -243,7 +231,7 @@ public:
void pop_row_columns(const vector<row_cell<T>> & row) {
for (auto & c : row) {
unsigned j = c.m_j;
unsigned j = c.var();
auto & col = m_columns[j];
lp_assert(col[col.size() - 1].var() == m_rows.size() -1 ); // todo : start here!!!!
col.pop_back();
@ -277,13 +265,13 @@ public:
void multiply_row(unsigned row, T const & alpha) {
for (auto & t : m_rows[row]) {
t.m_value *= alpha;
t.coeff() *= alpha;
}
}
void divide_row(unsigned row, T const & alpha) {
for (auto & t : m_rows[row]) {
t.m_value /= alpha;
t.coeff() /= alpha;
}
}
@ -306,12 +294,12 @@ public:
m_rows[ii] = t;
// now fix the columns
for (auto & rc : m_rows[i]) {
column_cell & cc = m_columns[rc.m_j][rc.m_offset];
column_cell & cc = m_columns[rc.var()][rc.offset()];
lp_assert(cc.var() == ii);
cc.var() = i;
}
for (auto & rc : m_rows[ii]) {
column_cell & cc = m_columns[rc.m_j][rc.m_offset];
column_cell & cc = m_columns[rc.var()][rc.offset()];
lp_assert(cc.var() == i);
cc.var() = ii;
}
@ -326,17 +314,17 @@ public:
return;
for (const auto & c : m_rows[row_index]) {
if (c.m_j == j) {
if (c.var() == j) {
continue;
}
T & wv = m_work_vector.m_data[c.m_j];
T & wv = m_work_vector.m_data[c.var()];
bool was_zero = is_zero(wv);
wv -= alpha * c.m_value;
wv -= alpha * c.coeff();
if (was_zero)
m_work_vector.m_index.push_back(c.m_j);
m_work_vector.m_index.push_back(c.var());
else {
if (is_zero(wv)) {
m_work_vector.erase_from_index(c.m_j);
m_work_vector.erase_from_index(c.var());
}
}
}
@ -390,7 +378,7 @@ public:
L ret = zero_of_type<L>();
lp_assert(row < m_rows.size());
for (auto & it : m_rows[row]) {
ret += w[it.m_j] * it.get_val();
ret += w[it.var()] * it.coeff();
}
return ret;
}
@ -402,7 +390,7 @@ public:
column_cell_plus(const column_cell & c, const static_matrix& A) :
m_c(c), m_A(A) {}
unsigned var() const { return m_c.var(); }
const T & coeff() const { return m_A.m_rows[var()][m_c.m_offset].get_val(); }
const T & coeff() const { return m_A.m_rows[var()][m_c.offset()].coeff(); }
};

41
src/math/lp/static_matrix_def.h
View file

@ -47,21 +47,21 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
T alpha = -get_val(c);
lp_assert(!is_zero(alpha));
auto & rowii = m_rows[ii];
remove_element(rowii, rowii[c.m_offset]);
remove_element(rowii, rowii[c.offset()]);
scan_row_ii_to_offset_vector(rowii);
unsigned prev_size_ii = rowii.size();
// run over the pivot row and update row ii
for (const auto & iv : m_rows[i]) {
unsigned j = iv.var();
if (j == pivot_col) continue;
T alv = alpha * iv.m_value;
lp_assert(!is_zero(iv.m_value));
T alv = alpha * iv.coeff();
lp_assert(!is_zero(iv.coeff()));
int j_offs = m_vector_of_row_offsets[j];
if (j_offs == -1) { // it is a new element
add_new_element(ii, j, alv);
}
else {
rowii[j_offs].m_value += alv;
rowii[j_offs].coeff() += alv;
}
}
// clean the work vector
@ -71,7 +71,7 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
// remove zeroes
for (unsigned k = rowii.size(); k-- > 0; ) {
if (is_zero(rowii[k].m_value))
if (is_zero(rowii[k].coeff()))
remove_element(rowii, rowii[k]);
}
return !rowii.empty();
@ -188,7 +188,7 @@ template <typename T, typename X> void static_matrix<T, X>::copy_column_to_in
template <typename T, typename X> T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
T ret = numeric_traits<T>::zero();
for (auto & t : m_rows[row]) {
T a = abs(t.get_val());
T a = abs(t.coeff());
if (a > ret) {
ret = a;
}
@ -200,7 +200,7 @@ template <typename T, typename X> T static_matrix<T, X>::get_min_abs_in_row(u
bool first_time = true;
T ret = numeric_traits<T>::zero();
for (auto & t : m_rows[row]) {
T a = abs(t.get_val());
T a = abs(t.coeff());
if (first_time) {
ret = a;
first_time = false;
@ -245,7 +245,7 @@ template <typename T, typename X> void static_matrix<T, X>::check_consistency
for (auto & t : m_rows[i]) {
std::pair<unsigned, unsigned> p(i, t.var());
lp_assert(by_rows.find(p) == by_rows.end());
by_rows[p] = t.get_val();
by_rows[p] = t.coeff();
}
}
std::unordered_map<std::pair<unsigned, unsigned>, T> by_cols;
@ -311,7 +311,7 @@ template <typename T, typename X> void static_matrix<T, X>::cross_out_row_fro
template <typename T, typename X> T static_matrix<T, X>::get_elem(unsigned i, unsigned j) const { // should not be used in efficient code !!!!
for (auto & t : m_rows[i]) {
if (t.var() == j) {
return t.get_val();
return t.coeff();
}
}
return numeric_traits<T>::zero();
@ -329,8 +329,8 @@ template <typename T, typename X> T static_matrix<T, X>::get_balance() const
template <typename T, typename X> T static_matrix<T, X>::get_row_balance(unsigned row) const {
T ret = zero_of_type<T>();
for (auto & t : m_rows[row]) {
if (numeric_traits<T>::is_zero(t.get_val())) continue;
T a = abs(t.get_val());
if (numeric_traits<T>::is_zero(t.coeff())) continue;
T a = abs(t.coeff());
numeric_traits<T>::log(a);
ret += a * a;
}
@ -348,11 +348,11 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
s.insert(rc.var());
if (rc.var() >= m_columns.size())
return false;
if (rc.m_offset >= m_columns[rc.var()].size())
if (rc.offset() >= m_columns[rc.var()].size())
return false;
if (rc.get_val() != get_val(m_columns[rc.var()][rc.m_offset]))
if (rc.coeff() != get_val(m_columns[rc.var()][rc.offset()]))
return false;
if (is_zero(rc.get_val())) {
if (is_zero(rc.coeff())) {
return false;
}
@ -369,24 +369,21 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
s.insert(cc.var());
if (cc.var() >= m_rows.size())
return false;
if (cc.m_offset >= m_rows[cc.var()].size())
if (cc.offset() >= m_rows[cc.var()].size())
return false;
if (get_val(cc) != m_rows[cc.var()][cc.m_offset].get_val())
if (get_val(cc) != m_rows[cc.var()][cc.offset()].coeff())
return false;
}
}
}
return true;
}
template <typename T, typename X>
void static_matrix<T, X>::remove_element(vector<row_cell<T>> & row_vals, row_cell<T> & row_el_iv) {
unsigned column_offset = row_el_iv.m_offset;
unsigned column_offset = row_el_iv.offset();
auto & column_vals = m_columns[row_el_iv.var()];
column_cell& cs = m_columns[row_el_iv.var()][column_offset];
unsigned row_offset = cs.m_offset;
unsigned row_offset = cs.offset();
if (column_offset != column_vals.size() - 1) {
auto & cc = column_vals[column_offset] = column_vals.back(); // copy from the tail
m_rows[cc.var()][cc.offset()].offset() = column_offset;

7
src/smt/seq_regex.cpp
View file

@ -64,22 +64,21 @@ namespace smt {
expr* s = nullptr, *r = nullptr;
expr* e = ctx.bool_var2expr(lit.var());
expr_ref id(a().mk_int(e->get_id()), m);
unsigned idx = 0;
VERIFY(str().is_in_re(e, s, r));
sort* seq_sort = m.get_sort(s);
vector<expr_ref_vector> patterns;
auto mk_cont = [&](unsigned idx) {
auto mk_cont = [&](unsigned idx) {
return sk().mk("seq.cont", id, a().mk_int(idx), seq_sort);
};
unsigned idx = 0;
if (seq_rw().is_re_contains_pattern(r, patterns)) {
expr_ref t(m);
expr_ref_vector ts(m);
ts.push_back(mk_cont(idx));
for (auto const& p : patterns) {
ts.append(p);
ts.push_back(mk_cont(++idx));
}
t = th.mk_concat(ts, seq_sort);
expr_ref t = th.mk_concat(ts, seq_sort);
th.propagate_eq(lit, s, t, true);
return true;
}

5
src/smt/theory_lra.cpp
View file

@ -1012,6 +1012,7 @@ public:
}
bool internalize_atom(app * atom, bool gate_ctx) {
TRACE("arith", tout << mk_pp(atom, m) << "\n";);
SASSERT(!ctx().b_internalized(atom));
expr* n1, *n2;
rational r;
@ -1722,7 +1723,9 @@ public:
final_check_status st = FC_DONE;
switch (is_sat) {
case l_true:
TRACE("arith", display(tout););
TRACE("arith", /*display(tout);*/
ctx().display(tout);
);
switch (check_lia()) {
case l_true:
break;

3
src/smt/theory_seq.cpp
View file

@ -1173,6 +1173,8 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
expr_ref lenl = mk_len(l);
expr_ref lenr = mk_len(r);
literal lit = mk_eq(lenl, lenr, false);
ctx.mark_as_relevant(lit);
if (ctx.get_assignment(lit) == l_true) {
expr_ref_vector lhs(m), rhs(m);
lhs.append(l2, ls2);
@ -2753,7 +2755,6 @@ bool theory_seq::lower_bound(expr* e, rational& lo) const {
VERIFY(m_autil.is_int(e));
bool is_strict = true;
return m_arith_value.get_lo(e, lo, is_strict) && !is_strict && lo.is_int();
}
bool theory_seq::upper_bound(expr* e, rational& hi) const {