mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

handle monomial_bounds::unit_propagate()

Browse source
This commit is contained in:
Lev Nachmanson 2023-08-31 17:35:41 -07:00
parent ff3268e636
commit 5509b468e9
3 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -283,7 +283,7 @@ namespace nla {
break;
}
}
lemma |= ineq(m.var(), lp::lconstraint_kind::EQ, 0);
lemma |= ineq(m.var(), lp::lconstraint_kind::NE, 0);
}
else {
for (auto v : m)
@ -291,12 +291,14 @@ namespace nla {
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);
if (w != null_lpvar) {
lp::lar_term term;
term.add_var(m.var());
term.add_monomial(-k, w);
lemma |= ineq(term, lp::lconstraint_kind::NE, 0);
} else {
lemma |= ineq(m.var(), lp::lconstraint_kind::NE, k);
}
}
}

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

@ -1812,9 +1812,7 @@ bool core::improve_bounds() {
}
void core::propagate(vector<lemma>& lemmas) {
// disable for now
return;
// propagate linear monomials
// propagate linear monomials, those that have all, or all but one, variables fixed
lemmas.reset();
m_lemma_vec = &lemmas;

3
src/smt/theory_lra.cpp
View file

@ -2150,9 +2150,10 @@ public:
case l_true:
propagate_basic_bounds();
propagate_bounds_with_lp_solver();
propagate_nla();
break;
case l_undef:
propagate_nla();
UNREACHABLE();
break;
}
return true;