From 897f2b0f30c46ca4eb07cc7093c2eac1b168a339 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Dec 2025 15:24:41 +0000 Subject: [PATCH] comments Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_stellensatz.cpp | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp index 71459f2f7..09e451444 100644 --- a/src/math/lp/nla_stellensatz.cpp +++ b/src/math/lp/nla_stellensatz.cpp @@ -485,6 +485,18 @@ namespace nla { return new_ci; } + // + // reduce x * y * p >= 0 + // to + // p >= 0 based on assumptions x > 0, y > 0 or x < 0, y < 0 + // -p >= 0 based on assumptions x > 0, y < 0 or x < 0, y > 0 + // + // reduce x * y * p > 0 + // to + // p > 0 based on assumptions x >= 0, y >= 0 or x <= 0, y <= 0 + // -p > 0 based on assumptions x >= 0, y <= 0 or x <= 0, y >= 0 + // + lp::constraint_index stellensatz::factor(lp::constraint_index ci) { auto const &[p, k, j] = m_constraints[ci]; auto [vars, q] = p.var_factors(); // p = vars * q @@ -1833,6 +1845,8 @@ namespace nla { TRACE(arith_verbose, display_constraint(tout << "skip non-maximal ", ci) << "\n"); continue; } + if (!constraint_is_false(ci)) + continue; auto f = factor(v, ci); auto q_ge_0 = vanishing(v, f, ci); if (q_ge_0 != lp::null_ci) { @@ -1876,11 +1890,11 @@ namespace nla { } } } - if (inf == lp::null_ci) - bound_ci = sup; - else if (sup == lp::null_ci) - bound_ci = inf; - else + if (inf == lp::null_ci) + bound_ci = sup; + else if (sup == lp::null_ci) + bound_ci = inf; + else bound_ci = c().random(2) ? inf : sup; return result; }