mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-25 05:26:51 +00:00
Code Activity

comments

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-12-13 15:24:41 +00:00
parent 16bad349ce
commit 897f2b0f30
1 changed files with 19 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/lp/nla_stellensatz.cpp
View file

@ -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;
}