Skip to content

Commit

Permalink
Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3…
Browse files Browse the repository at this point in the history 
… into unit_prop_on_monomials
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Sep 24, 2023
2 parents 85eacf9 + a3e2e68 commit 3433366
Show file tree
Hide file tree
Showing 10 changed files with 283 additions and 231 deletions.
48 changes: 23 additions & 25 deletions src/math/lp/bound_analyzer_on_row.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,15 +281,32 @@ public :
// */
// }


void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict)
{
unsigned row_index = this->m_row_index;
auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index,this]() {
return explain_bound_on_var_on_coeff((B*)&m_bp, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index);
auto* lar = &m_bp.lp();
auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;

SASSERT(!tv::is_term(bound_j));
u_dependency* ret = nullptr;
for (auto const& r : lar->get_row(row_index)) {
unsigned j = r.var();
if (j == bound_j)
continue;
mpq const& a = r.coeff();
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->join_deps(ret, witness);
}
return ret;
};
m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain);
}

void advance_u(unsigned j) {
m_column_of_u = (m_column_of_u == -1) ? j : -2;
}
Expand Down Expand Up @@ -320,26 +337,7 @@ public :
break;
}
}
static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
auto& lar = bp->lp();
int bound_sign = (is_lower_bound ? 1 : -1);
int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;

SASSERT(!tv::is_term(bound_j));
u_dependency* ret = nullptr;
for (auto const& r : lar.get_row(row_index)) {
unsigned j = r.var();
if (j == bound_j)
continue;
mpq const& a = r.coeff();
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.join_deps(ret, witness);
}
return ret;
}

};


Expand Down
169 changes: 2 additions & 167 deletions src/math/lp/lp_bound_propagator.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ class lp_bound_propagator {
u_map<unsigned> m_improved_upper_bounds;

T& m_imp;
std_vector<implied_bound> m_ibounds;
std_vector<implied_bound>& m_ibounds;

map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
// works for rows of the form x + y + sum of fixed = 0
Expand Down Expand Up @@ -109,7 +109,7 @@ class lp_bound_propagator {
};

public:
lp_bound_propagator(T& imp) : m_imp(imp) {}
lp_bound_propagator(T& imp, std_vector<implied_bound> & ibounds) : m_imp(imp), m_ibounds(ibounds) {}

const std_vector<implied_bound>& ibounds() const { return m_ibounds; }

Expand All @@ -120,171 +120,6 @@ class lp_bound_propagator {
m_column_types = &lp().get_column_types();
}

bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
zero_var = non_fixed = null_lpvar;
unsigned n_of_non_fixed = 0;
for (lpvar v : m) {
if (!this->column_is_fixed(v)) {
n_of_non_fixed++;
non_fixed = v;
continue;
}
const auto & b = get_lower_bound(v).x;
if (b.is_zero()) {
zero_var = v;
return true;
}

}
return n_of_non_fixed <= 1;
}

void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
auto& lps = lp();
auto lambda = [zero_var,&lps]() {
return lps.get_bound_constraint_witnesses_for_column(zero_var);
};
TRACE("add_bound", lp().print_column_info(zero_var, tout) << std::endl;);
add_lower_bound_monic(monic_var, mpq(0), false, lambda);
add_upper_bound_monic(monic_var, mpq(0), false, lambda);
}

void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {
TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
j = lp().column_to_reported_index(j);
unsigned k;
if (!m_improved_lower_bounds.find(j, k)) {
m_improved_lower_bounds.insert(j,static_cast<unsigned>(m_ibounds.size()));
m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep));
}
else {
auto& found_bound = m_ibounds[k];
if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(v, j, true, is_strict, explain_dep);
TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
}
}
}

void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function <u_dependency* ()> explain_bound) {
j = lp().column_to_reported_index(j);
unsigned k;
if (!m_improved_upper_bounds.find(j, k)) {
m_improved_upper_bounds.insert(j, static_cast<unsigned>(m_ibounds.size()));
m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound));
}
else {
auto& found_bound = m_ibounds[k];
if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) {
found_bound = implied_bound(bound_val, j, false, is_strict, explain_bound);
TRACE("add_bound", lp().print_implied_bound(found_bound, tout););
}
}
}

void propagate_monic(lpvar monic_var, const svector<lpvar>& vars) {
lpvar non_fixed, zero_var;
if (!is_linear(vars, zero_var, non_fixed))
return;

if (zero_var != null_lpvar)
add_bounds_for_zero_var(monic_var, zero_var);
else {
rational k = rational(1);
for (auto v : vars)
if (v != non_fixed) {
k *= lp().get_column_value(v).x;
if (k.is_big()) return;
}

if (non_fixed != null_lpvar)
propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
else // all variables are fixed
propagate_monic_with_all_fixed(monic_var, vars, k);
}
}

void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
lp::impq bound_value;
bool is_strict;
auto& lps = lp();

if (lower_bound_is_available(non_fixed)) {
bound_value = lp().column_lower_bound(non_fixed);
is_strict = !bound_value.y.is_zero();
auto lambda = [vars, non_fixed,&lps]() {
u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed);
for (auto v : vars)
if (v != non_fixed)
dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
return dep;
};
if (k.is_pos())
add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
else
add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
}

if (upper_bound_is_available(non_fixed)) {
bound_value = lp().column_upper_bound(non_fixed);
is_strict = !bound_value.y.is_zero();
auto lambda = [vars, non_fixed,&lps]() {
u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed);
for (auto v : vars)
if (v != non_fixed)
dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
return dep;
};
if (k.is_neg())
add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
else
add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, lambda);
}

if (lower_bound_is_available(monic_var)) {
auto lambda = [vars, monic_var, non_fixed,&lps]() {
u_dependency* dep = lps.get_column_lower_bound_witness(monic_var);
for (auto v : vars) {
if (v != non_fixed) {
dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
}
}
return dep;
};
bound_value = lp().column_lower_bound(monic_var);
is_strict = !bound_value.y.is_zero();
if (k.is_pos())
add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
else
add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
}

if (upper_bound_is_available(monic_var)) {
bound_value = lp().column_upper_bound(monic_var);
is_strict = !bound_value.y.is_zero();
auto lambda = [vars, monic_var, non_fixed,&lps]() {
u_dependency* dep = lps.get_column_upper_bound_witness(monic_var);
for (auto v : vars) {
if (v != non_fixed) {
dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v));
}
}
return dep;
};
if (k.is_neg())
add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
else
add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda);
}
}

void propagate_monic_with_all_fixed(lpvar monic_var, const svector<lpvar>& vars, const rational& k) {
auto& lps = lp();
auto lambda = [vars,&lps]() { return lps.get_bound_constraint_witnesses_for_columns(vars); };
add_lower_bound_monic(monic_var, k, false, lambda);
add_upper_bound_monic(monic_var, k, false, lambda);
}

column_type get_column_type(unsigned j) const {
return (*m_column_types)[j];
}
Expand Down

0 comments on commit 3433366

Please sign in to comment.