mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 13:19:04 +00:00
Code Activity

handle case where all variables are bounded

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-04 12:58:03 -07:00
parent 98a9a34f2b
commit d7718623a4
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1555,7 +1555,12 @@ void core::refine_pseudo_linear(monic const& m) {
lemma_builder lemma(*this, "nla-pseudo-linear");
lpvar nlvar = null_lpvar;
rational prod(1);
for (auto v : m.vars()) {
for (unsigned i = 0; i < m.vars().size(); ++i) {
auto v = m.vars()[i];
if (i == m.vars().size() - 1 && nlvar == null_lpvar) {
nlvar = v;
break;
}
if (lra.column_is_bounded(v) && lra.var_is_int(v)) {
auto lb = lra.get_lower_bound(v);
auto ub = lra.get_upper_bound(v);
@ -1568,6 +1573,7 @@ void core::refine_pseudo_linear(monic const& m) {
SASSERT(nlvar == null_lpvar);
nlvar = v;
}
SASSERT(nlvar != null_lpvar);
lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
// lemma.display(verbose_stream() << "pseudo-linear lemma\n");
}