mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
propagate lineal monomial
This commit is contained in:
parent
5509b468e9
commit
d3258e7084
|
@ -283,7 +283,7 @@ namespace nla {
|
|||
break;
|
||||
}
|
||||
}
|
||||
lemma |= ineq(m.var(), lp::lconstraint_kind::NE, 0);
|
||||
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0);
|
||||
}
|
||||
else {
|
||||
for (auto v : m)
|
||||
|
@ -295,9 +295,9 @@ namespace nla {
|
|||
lp::lar_term term;
|
||||
term.add_var(m.var());
|
||||
term.add_monomial(-k, w);
|
||||
lemma |= ineq(term, lp::lconstraint_kind::NE, 0);
|
||||
lemma += ineq(term, lp::lconstraint_kind::EQ, 0);
|
||||
} else {
|
||||
lemma |= ineq(m.var(), lp::lconstraint_kind::NE, k);
|
||||
lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -1056,6 +1056,17 @@ new_lemma& new_lemma::operator|=(ineq const& ineq) {
|
|||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
// Contrary to new_lemma::operator|=, this method does not assert that the model does not satisfy the ineq.
|
||||
// If ineq holds then it is a nop.
|
||||
new_lemma& new_lemma::operator+=(ineq const& ineq) {
|
||||
if (c.ineq_holds(ineq)) return *this;
|
||||
|
||||
if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
|
||||
current().push_back(ineq);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
||||
new_lemma::~new_lemma() {
|
||||
|
|
|
@ -83,6 +83,7 @@ namespace nla {
|
|||
new_lemma& operator&=(const factorization& f);
|
||||
new_lemma& operator&=(lpvar j);
|
||||
new_lemma& operator|=(ineq const& i);
|
||||
new_lemma& operator+=(ineq const& i);
|
||||
new_lemma& explain_fixed(lpvar j);
|
||||
new_lemma& explain_equiv(lpvar u, lpvar v);
|
||||
new_lemma& explain_var_separated_from_zero(lpvar j);
|
||||
|
|
Loading…
Reference in a new issue