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

fix crash on arie branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-16 16:58:33 -08:00
parent b835bd4c92
commit 711572e73c
3 changed files with 24 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/rewriter/arith_rewriter.cpp
View file

@ -771,17 +771,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
}
}
if (m_util.is_idiv(arg1, t, e) && is_numeral(e, a1) && a1 > 0) {
// e > 0 => t div e ~ arg2 <=> e * (t div e) ~ e * arg2 <=> t - mod t e ~ e * arg2
if (is_numeral(arg2, a2) && a2 == 0 && (kind == LE || kind == GE)) {
switch (kind) {
case LE: result = m_util.mk_le(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
case GE: result = m_util.mk_ge(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
case EQ: result = m.mk_eq(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
}
}
// generally: result = m_util.mk_sub(t, m_util.mk_mod(t, e));
}
if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
a2.neg();
new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
@ -792,6 +782,14 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
}
}
else if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) {
// e > 0 => t div e ~ arg2 <=> e * (t div e) ~ e * arg2 <=> t - mod t e ~ e * arg2
if (is_numeral(arg2, a2) && a2 == 0 && (kind == LE || kind == GE)) {
switch (kind) {
case LE: result = m_util.mk_le(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
case GE: result = m_util.mk_ge(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
case EQ: result = m.mk_eq(result, m_util.mk_mul(e, arg2)); return BR_REWRITE3;
}
}
// Nothing new; return BR_FAILED to avoid rewriting loops.
return BR_FAILED;
}

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

@ -216,6 +216,7 @@ namespace nla {
ci = m_constraints.size();
m_constraints.push_back({p, k, j });
m_constraint_index.insert({p.index(), k}, ci);
m_tabu.reserve(ci + 1);
return ci;
}
@ -223,7 +224,6 @@ namespace nla {
if (m_active.contains(ci))
return;
m_active.insert(ci);
m_tabu.reserve(ci + 1);
m_tabu[ci] = tabu;
}
@ -284,20 +284,17 @@ namespace nla {
for (unsigned cx = 0; cx < num_x; ++cx) {
auto other_ci = m_occurs[x][cx];
switch (resolve_variable(x, ci, other_ci, p_value, f, _m1, _f_p)) {
case l_false: return l_false;
case l_true: break;
case l_undef: break;
}
if (!resolve_variable(x, ci, other_ci, p_value, f, _m1, _f_p))
return l_false;
}
return l_undef;
}
lbool stellensatz::resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci,
bool stellensatz::resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci,
rational const& p_value,
factorization const &f, unsigned_vector const &_m1, dd::pdd _f_p) {
if (ci == other_ci)
return l_undef;
return true;
auto const &[other_p, other_k, other_j] = m_constraints[other_ci];
auto const &[p, k, j] = m_constraints[ci];
auto g = factor(x, other_ci);
@ -310,13 +307,13 @@ namespace nla {
SASSERT(g.degree > 0);
SASSERT(p_value != 0);
if (g.degree > f.degree) // future: could handle this too by considering tabu to be a map into degrees.
return l_undef;
return true;
if (p_value > 0 && p_value2 > 0)
return l_undef;
return true;
if (p_value < 0 && p_value2 < 0)
return l_undef;
return true;
if (any_of(other_p.free_vars(), [&](unsigned j) { return m_tabu[ci].contains(j); }))
return l_undef;
return true;
TRACE(arith, tout << "factor (" << other_ci << ") " << other_p << " -> j" << x << "^" << g.degree << " * "
<< g.p << " + " << g.q << "\n");
@ -334,9 +331,9 @@ namespace nla {
g_p = g_p.mul(m2);
if (!has_term_offset(f_p))
return l_undef;
return true;
if (!has_term_offset(g_p))
return l_undef;
return true;
TRACE(arith, tout << "m1 " << m1 << " m2 " << m2 << " m1m2: " << m1m2 << "\n");
@ -372,7 +369,7 @@ namespace nla {
auto new_ci = add(ci_a, ci_b);
CTRACE(arith, !is_new_constraint(new_ci), display_constraint(tout << "not new ", new_ci) << "\n");
if (!is_new_constraint(new_ci))
return l_undef;
return true;
if (m_constraints[new_ci].p.degree() <= 3)
init_occurs(new_ci);
TRACE(arith, tout << "eliminate j" << x << ":\n"; display_constraint(tout << "ci: ", ci) << "\n";
@ -381,7 +378,7 @@ namespace nla {
display_constraint(tout << "new_ci: ", new_ci) << "\n");
if (conflict(new_ci))
return l_false;
return false;
if (!constraint_is_true(new_ci)) {
auto const &[new_p, new_k, new_j] = m_constraints[new_ci];
@ -391,7 +388,7 @@ namespace nla {
add_active(new_ci, new_tabu);
}
}
return l_true;
return true;
}
bool stellensatz::conflict(lp::constraint_index ci) {

2
src/math/lp/nla_stellensatz.h
View file

@ -166,7 +166,7 @@ namespace nla {
unsigned degree_of_var_in_constraint(lpvar v, lp::constraint_index ci) const;
factorization factor(lpvar v, lp::constraint_index ci);
lbool resolve_variable(lpvar x, lp::constraint_index ci);
lbool resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, rational const& p_value,
bool resolve_variable(lpvar x, lp::constraint_index ci, lp::constraint_index other_ci, rational const& p_value,
factorization const& f, unsigned_vector const& m1, dd::pdd _f_p);
bool constraint_is_true(lp::constraint_index ci) const;