mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

sketch linear monomial propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-31 11:49:05 -07:00
parent 38b131386d
commit c2cbe72b64
2 changed files with 55 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

67
src/math/lp/nla_core.cpp
View file

@ -1817,39 +1817,76 @@ void core::propagate(vector<lemma>& lemmas) {
// propagate linear monomials // propagate linear monomials
lemmas.reset(); lemmas.reset();
m_lemma_vec = &lemmas;
for (auto const& m : m_emons) for (auto const& m : m_emons)
if (propagate(m, lemmas)) propagate(m, lemmas);
break;
} }
bool core::propagate(monic const& m, vector<lemma>& lemmas) { void core::propagate(monic const& m, vector<lemma>& lemmas) {
m_propagated.reserve(m.var() + 1, false); m_propagated.reserve(m.var() + 1, false);
if (m_propagated[m.var()]) if (m_propagated[m.var()])
return false; return;
if (!is_linear(m)) if (!is_linear(m))
return false; return;
trail().push(set_bitvector_trail(m_propagated, m.var())); trail().push(set_bitvector_trail(m_propagated, m.var()));
mpq k = fixed_var_product(m); rational k = fixed_var_product(m);
// todo
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);
}
// return true if m_emons changes (so the iterator is invalid)
return false;
} }
bool core::is_linear(monic const& m) { bool core::is_linear(monic const& m) {
// todo unsigned non_fixed = 0;
return false; for (lpvar v : m) {
if (!var_is_fixed(v))
++non_fixed;
else if (val(v).is_zero())
return true;
}
return non_fixed <= 1;
} }
mpq core::fixed_var_product(monic const& m) { rational core::fixed_var_product(monic const& m) {
// todo rational r(1);
return mpq(0); 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 } // end of nla

5
src/math/lp/nla_core.h
View file

@ -438,9 +438,10 @@ private:
// monomial propagation // monomial propagation
bool_vector m_propagated; bool_vector m_propagated;
bool propagate(monic const& m, vector<lemma>& lemmas); void propagate(monic const& m, vector<lemma>& lemmas);
bool is_linear(monic const& m); bool is_linear(monic const& m);
mpq fixed_var_product(monic const& m); rational fixed_var_product(monic const& m);
lpvar non_fixed_var(monic const& m);
}; // end of core }; // end of core