mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
move unit propagation into monomial_bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c2cbe72b64
commit
ff3268e636
|
@ -17,13 +17,14 @@ namespace nla {
|
|||
common(c),
|
||||
dep(c->m_intervals.get_dep_intervals()) {}
|
||||
|
||||
void monomial_bounds::operator()() {
|
||||
void monomial_bounds::propagate() {
|
||||
for (lpvar v : c().m_to_refine) {
|
||||
monic const& m = c().emons()[v];
|
||||
propagate(m);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool monomial_bounds::is_too_big(mpq const& q) const {
|
||||
return rational(q).bitsize() > 256;
|
||||
}
|
||||
|
@ -257,5 +258,76 @@ namespace nla {
|
|||
}
|
||||
}
|
||||
|
||||
void monomial_bounds::unit_propagate() {
|
||||
for (auto const& m : c().m_emons)
|
||||
unit_propagate(m);
|
||||
}
|
||||
|
||||
void monomial_bounds::unit_propagate(monic const& m) {
|
||||
m_propagated.reserve(m.var() + 1, false);
|
||||
if (m_propagated[m.var()])
|
||||
return;
|
||||
|
||||
if (!is_linear(m))
|
||||
return;
|
||||
|
||||
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);
|
||||
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);
|
||||
SASSERT(w != null_lpvar);
|
||||
|
||||
lp::lar_term term;
|
||||
term.add_monomial(-m.rat_sign(), m.var());
|
||||
term.add_monomial(k, w);
|
||||
lemma |= ineq(term, lp::lconstraint_kind::EQ, 0);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
bool monomial_bounds::is_linear(monic const& m) {
|
||||
unsigned non_fixed = 0;
|
||||
for (lpvar v : m) {
|
||||
if (!c().var_is_fixed(v))
|
||||
++non_fixed;
|
||||
else if (c().val(v).is_zero())
|
||||
return true;
|
||||
}
|
||||
return non_fixed <= 1;
|
||||
}
|
||||
|
||||
|
||||
rational monomial_bounds::fixed_var_product(monic const& m) {
|
||||
rational r(1);
|
||||
for (lpvar v : m) {
|
||||
if (c().var_is_fixed(v))
|
||||
r *= c().lra.get_column_value(v).x;
|
||||
}
|
||||
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;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
|
|
@ -16,6 +16,8 @@ namespace nla {
|
|||
class core;
|
||||
class monomial_bounds : common {
|
||||
dep_intervals& dep;
|
||||
|
||||
|
||||
void var2interval(lpvar v, scoped_dep_interval& i);
|
||||
bool is_too_big(mpq const& q) const;
|
||||
bool propagate_down(monic const& m, lpvar u);
|
||||
|
@ -27,8 +29,17 @@ namespace nla {
|
|||
void analyze_monomial(monic const& m, unsigned& num_free, lpvar& free_v, unsigned& power) const;
|
||||
bool is_free(lpvar v) const;
|
||||
bool is_zero(lpvar v) const;
|
||||
|
||||
// monomial propagation
|
||||
bool_vector m_propagated;
|
||||
void unit_propagate(monic const& m);
|
||||
bool is_linear(monic const& m);
|
||||
rational fixed_var_product(monic const& m);
|
||||
lpvar non_fixed_var(monic const& m);
|
||||
|
||||
public:
|
||||
monomial_bounds(core* core);
|
||||
void operator()();
|
||||
void propagate();
|
||||
void unit_propagate();
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1546,7 +1546,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
|
|||
auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); };
|
||||
|
||||
if (no_effect())
|
||||
m_monomial_bounds();
|
||||
m_monomial_bounds.propagate();
|
||||
|
||||
if (no_effect() && improve_bounds())
|
||||
return l_false;
|
||||
|
@ -1814,79 +1814,14 @@ bool core::improve_bounds() {
|
|||
void core::propagate(vector<lemma>& lemmas) {
|
||||
// disable for now
|
||||
return;
|
||||
|
||||
// propagate linear monomials
|
||||
// propagate linear monomials
|
||||
lemmas.reset();
|
||||
m_lemma_vec = &lemmas;
|
||||
for (auto const& m : m_emons)
|
||||
propagate(m, lemmas);
|
||||
|
||||
m_monomial_bounds.unit_propagate();
|
||||
|
||||
}
|
||||
|
||||
void core::propagate(monic const& m, vector<lemma>& lemmas) {
|
||||
m_propagated.reserve(m.var() + 1, false);
|
||||
if (m_propagated[m.var()])
|
||||
return;
|
||||
|
||||
if (!is_linear(m))
|
||||
return;
|
||||
|
||||
trail().push(set_bitvector_trail(m_propagated, m.var()));
|
||||
|
||||
rational k = fixed_var_product(m);
|
||||
|
||||
new_lemma lemma(*this, "fixed-values");
|
||||
if (k == 0) {
|
||||
for (auto v : m) {
|
||||
if (var_is_fixed(v) && val(v).is_zero()) {
|
||||
lemma.explain_fixed(v);
|
||||
break;
|
||||
}
|
||||
}
|
||||
lemma |= ineq(m.var(), lp::lconstraint_kind::EQ, 0);
|
||||
}
|
||||
else {
|
||||
for (auto v : m)
|
||||
if (var_is_fixed(v))
|
||||
lemma.explain_fixed(v);
|
||||
|
||||
lpvar w = non_fixed_var(m);
|
||||
SASSERT(w != null_lpvar);
|
||||
|
||||
lp::lar_term term;
|
||||
term.add_monomial(mpq(-1), m.var());
|
||||
term.add_monomial(k, w);
|
||||
lemma |= ineq(term, lp::lconstraint_kind::EQ, 0);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
bool core::is_linear(monic const& m) {
|
||||
unsigned non_fixed = 0;
|
||||
for (lpvar v : m) {
|
||||
if (!var_is_fixed(v))
|
||||
++non_fixed;
|
||||
else if (val(v).is_zero())
|
||||
return true;
|
||||
}
|
||||
return non_fixed <= 1;
|
||||
}
|
||||
|
||||
|
||||
rational core::fixed_var_product(monic const& m) {
|
||||
rational r(1);
|
||||
for (lpvar v : m) {
|
||||
if (var_is_fixed(v))
|
||||
r *= lra.get_column_value(v).x;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
lpvar core::non_fixed_var(monic const& m) {
|
||||
for (lpvar v : m)
|
||||
if (!var_is_fixed(v))
|
||||
return v;
|
||||
return null_lpvar;
|
||||
}
|
||||
|
||||
|
||||
} // end of nla
|
||||
|
|
|
@ -436,12 +436,6 @@ private:
|
|||
void save_tableau();
|
||||
bool integrality_holds();
|
||||
|
||||
// monomial propagation
|
||||
bool_vector m_propagated;
|
||||
void propagate(monic const& m, vector<lemma>& lemmas);
|
||||
bool is_linear(monic const& m);
|
||||
rational fixed_var_product(monic const& m);
|
||||
lpvar non_fixed_var(monic const& m);
|
||||
|
||||
}; // end of core
|
||||
|
||||
|
|
Loading…
Reference in a new issue