mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 05:36:41 +00:00
Code Activity

update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-14 16:37:00 -08:00
parent d081321384
commit 072f1deccc
1 changed files with 38 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -236,7 +236,6 @@ namespace nla {
// find complementary constraints that contain x^k for k = 0 .. degree -1 // find complementary constraints that contain x^k for k = 0 .. degree -1
// eliminate x (and other variables) by combining ci with complementary constraints. // eliminate x (and other variables) by combining ci with complementary constraints.
auto ci = m_active.elem_at(0); auto ci = m_active.elem_at(0);
auto tabu = m_tabu[ci];
m_active.remove(ci); m_active.remove(ci);
switch (factor(ci)) { switch (factor(ci)) {
@ -279,7 +278,7 @@ namespace nla {
continue; continue;
if (p_value < 0 && p_value2 < 0) if (p_value < 0 && p_value2 < 0)
continue; continue;
if (any_of(other_ineq.p.free_vars(), [&](unsigned j) { return tabu.contains(j); })) if (any_of(other_ineq.p.free_vars(), [&](unsigned j) { return m_tabu[ci].contains(j); }))
continue; continue;
TRACE(arith, tout << "factor (" << other_ci << ") " << other_ineq.p << " -> j" << x << "^" << g.degree TRACE(arith, tout << "factor (" << other_ci << ") " << other_ineq.p << " -> j" << x << "^" << g.degree
@ -317,12 +316,6 @@ namespace nla {
// //
lp::constraint_index ci_a, ci_b; lp::constraint_index ci_a, ci_b;
auto aj = assumption_justification(); auto aj = assumption_justification();
if (f_p.is_val())
ci_b = multiply(other_ci, pddm.mk_val(f_p.val()));
else if (sign_f)
ci_b = multiply(other_ci, add_constraint(f_p, lp::lconstraint_kind::LT, aj));
else
ci_b = multiply(other_ci, add_constraint(f_p, lp::lconstraint_kind::GT, aj));
if (g_p.is_val()) if (g_p.is_val())
ci_a = multiply(ci, pddm.mk_val(g_p.val())); ci_a = multiply(ci, pddm.mk_val(g_p.val()));
@ -331,6 +324,13 @@ namespace nla {
else else
ci_a = multiply(ci, add_constraint(g_p, lp::lconstraint_kind::GT, aj)); ci_a = multiply(ci, add_constraint(g_p, lp::lconstraint_kind::GT, aj));
if (f_p.is_val())
ci_b = multiply(other_ci, pddm.mk_val(f_p.val()));
else if (sign_f)
ci_b = multiply(other_ci, add_constraint(f_p, lp::lconstraint_kind::LT, aj));
else
ci_b = multiply(other_ci, add_constraint(f_p, lp::lconstraint_kind::GT, aj));
auto new_ci = add(ci_a, ci_b); auto new_ci = add(ci_a, ci_b);
CTRACE(arith, !is_new_constraint(new_ci), display_constraint(tout << "not new ", new_ci) << "\n"); CTRACE(arith, !is_new_constraint(new_ci), display_constraint(tout << "not new ", new_ci) << "\n");
if (!is_new_constraint(new_ci)) if (!is_new_constraint(new_ci))
@ -351,7 +351,7 @@ namespace nla {
auto const &p = m_constraints[ci].p; auto const &p = m_constraints[ci].p;
auto const &[new_p, new_k, new_j] = m_constraints[new_ci]; auto const &[new_p, new_k, new_j] = m_constraints[new_ci];
if (new_p.degree() <= 3 && !new_p.free_vars().contains(x)) { if (new_p.degree() <= 3 && !new_p.free_vars().contains(x)) {
uint_set new_tabu(tabu), fv; uint_set new_tabu(m_tabu[ci]), fv;
for (auto v : new_p.free_vars()) for (auto v : new_p.free_vars())
fv.insert(v); fv.insert(v);
for (auto v : p.free_vars()) for (auto v : p.free_vars())
@ -382,34 +382,35 @@ namespace nla {
} }
bool stellensatz::vanishing(lpvar x, factorization const &f, lp::constraint_index ci) { bool stellensatz::vanishing(lpvar x, factorization const &f, lp::constraint_index ci) {
if (f.q.is_zero())
return false;
if (f.p.is_zero())
return false;
auto p_value = cvalue(f.p); auto p_value = cvalue(f.p);
if (!f.p.is_zero() && p_value == 0) { if (p_value != 0)
// add p = 0 as assumption and reduce to q. return false;
auto p_is_0 = assume(f.p, lp::lconstraint_kind::EQ);
if (!f.q.is_zero()) {
// ci & -p_is_0*x^f.degree => new_ci
dd::pdd r = pddm.mk_val(rational(-1));
for (unsigned i = 0; i < f.degree; ++i)
r = r * pddm.mk_var(x);
p_is_0 = multiply(p_is_0, r);
auto new_ci = add(ci, p_is_0);
TRACE(arith, display_constraint(tout << "reduced", new_ci) << "\n"); // add p = 0 as assumption and reduce to q.
if (!is_new_constraint(new_ci)) auto p_is_0 = assume(f.p, lp::lconstraint_kind::EQ);
return false; // ci & -p_is_0*x^f.degree => new_ci
init_occurs(new_ci); dd::pdd r = pddm.mk_val(rational(-1));
uint_set new_tabu(m_tabu[ci]); for (unsigned i = 0; i < f.degree; ++i)
uint_set q_vars; r = r * pddm.mk_var(x);
for (auto j : f.q.free_vars()) p_is_0 = multiply(p_is_0, r);
q_vars.insert(j); auto new_ci = add(ci, p_is_0);
for (auto j : f.p.free_vars()) TRACE(arith, display_constraint(tout << "reduced", new_ci) << "\n");
if (!q_vars.contains(j)) if (!is_new_constraint(new_ci))
new_tabu.insert(j); return false;
add_active(new_ci, new_tabu); init_occurs(new_ci);
} uint_set new_tabu(m_tabu[ci]);
return true; uint_set q_vars;
} for (auto j : f.q.free_vars())
return false; q_vars.insert(j);
for (auto j : f.p.free_vars())
if (!q_vars.contains(j))
new_tabu.insert(j);
add_active(new_ci, new_tabu);
return true;
} }
lbool stellensatz::factor(lp::constraint_index ci) { lbool stellensatz::factor(lp::constraint_index ci) {