mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-03 22:05:45 +00:00
Code Activity

propagate monomial is nla

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-05 18:49:59 -07:00
parent 318d7d7564
commit 41f59cb1ed
11 changed files with 210 additions and 115 deletions
Download patch file Download diff file Expand all files Collapse all files

132
src/math/lp/monomial_bounds.cpp
View file

@ -258,51 +258,113 @@ namespace nla {
}
}
void monomial_bounds::unit_propagate() {
for (auto const& m : c().m_emons)
unit_propagate(m);
bool monomial_bounds::unit_propagate() {
unsigned sz = 0;
vector<lpvar> monics_vars;
for (auto const& m : c().m_emons) {
monics_vars.push_back(m.var());
sz++;
}
unsigned l = this->random();
for (unsigned i = 0; i < sz; ++i) {
lpvar v = monics_vars[(i + l) % sz];
if (!unit_propagate(c().m_emons[v])) {
return false;
}
}
return true;
}
void monomial_bounds::unit_propagate(monic const& m) {
// returns false if and only if there is a conflict
bool monomial_bounds::unit_propagate(monic const& m) {
m_propagated.reserve(m.var() + 1, false);
if (m_propagated[m.var()])
return;
return true;
if (!is_linear(m))
return;
return true;
c().trail().push(set_bitvector_trail(m_propagated, m.var()));
rational k = fixed_var_product(m);
new_lemma lemma(c(), "fixed-values");
if (k == 0) {
for (auto v : m) {
if (c().var_is_fixed(v) && c().val(v).is_zero()) {
lemma.explain_fixed(v);
lpvar zero_fixed = null_lpvar, non_fixed = null_lpvar;
// find a zero fixed variable and a non-fixed variable
for (lpvar v : m) {
if (c().var_is_fixed(v)) {
if (c().val(v).is_zero()) {
zero_fixed = v;
break;
}
}
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
}
else {
for (auto v : m)
if (c().var_is_fixed(v))
lemma.explain_fixed(v);
lpvar w = non_fixed_var(m);
if (w != null_lpvar) {
lp::lar_term term;
term.add_var(m.var());
term.add_monomial(-k, w);
lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
} else {
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
else {
non_fixed = v;
}
}
if (zero_fixed != null_lpvar) {
// the m.var() has to have a zero value
u_dependency* d = this->dep.mk_join(c().lra.get_column_lower_bound_witness(zero_fixed),
c().lra.get_column_upper_bound_witness(zero_fixed));
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, mpq(0), d);
} else if (non_fixed != null_lpvar) {
u_dependency* d = nullptr;
rational k(1);
for (auto v : m)
if (v != non_fixed) {
d = this->dep.mk_join(d, c().lra.get_column_upper_bound_witness(v));
d = this->dep.mk_join(d, c().lra.get_column_lower_bound_witness(v));
k *= c().val(v);
}
SASSERT(k.is_pos() || k.is_neg());
// we have m = k* non_fixed: m.var() getting the bounds witnesses of non_fixed
if (k.is_pos()) {
d = c().lra.get_column_upper_bound_witness(non_fixed);
if (d) {
const auto& b = c().lra.get_column_value(non_fixed);
bool strict = b.y.is_neg();
c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE, k * b.x, d);
}
d = c().lra.get_column_lower_bound_witness(non_fixed);
if (d) {
const auto& b = c().lra.get_column_value(non_fixed);
bool strict = b.y.is_pos();
c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE, k * b.x, d);
}
} else {
d = c().lra.get_column_upper_bound_witness(non_fixed);
if (d) {
const auto& b = c().lra.get_column_value(non_fixed);
bool strict = b.y.is_neg();
c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::GT : lp::lconstraint_kind::GE, k * b.x, d);
}
d = c().lra.get_column_lower_bound_witness(non_fixed);
if (d) {
const auto& b = c().lra.get_column_value(non_fixed);
bool strict = b.y.is_pos();
c().lra.update_column_type_and_bound(m.var(), strict ? lp::lconstraint_kind::LT : lp::lconstraint_kind::LE, k * b.x, d);
}
}
} else {
SASSERT(non_fixed == null_lpvar && zero_fixed == null_lpvar);
rational k(1);
u_dependency* d = nullptr;
for (auto v : m) {
SASSERT(c().var_is_fixed(v));
d = this->dep.mk_join(d, c().lra.get_column_upper_bound_witness(v));
d = this->dep.mk_join(d, c().lra.get_column_lower_bound_witness(v));
k *= c().val(v);
}
SASSERT(k.is_pos() || k.is_neg());
// we have m = k: m.var() getting the bounds witnesses of all fixed variables
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, d);
}
if (c().lra.get_status() == lp::lp_status::INFEASIBLE) {
TRACE("nla_solver", tout << "conflict in unit_propagate\n";);
return false;
}
return true;
}
bool monomial_bounds::is_linear(monic const& m) {
unsigned non_fixed = 0;
for (lpvar v : m) {
@ -324,12 +386,6 @@ namespace nla {
return r;
}
lpvar monomial_bounds::non_fixed_var(monic const& m) {
for (lpvar v : m)
if (!c().var_is_fixed(v))
return v;
return null_lpvar;
}
}