mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

move to lex-leading resolvents

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-29 19:21:30 -07:00
parent fa2d7a1c57
commit 4162d89170
2 changed files with 59 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -469,97 +469,72 @@ namespace nla {
unsigned initial_false_constraints = m_false_constraints.size(); unsigned initial_false_constraints = m_false_constraints.size();
for (unsigned it = 0; it < m_false_constraints.size(); ++it) { for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
if (it > 5*initial_false_constraints) if (it > 5 * initial_false_constraints)
break; break;
auto ci1 = m_false_constraints[it]; auto ci1 = m_false_constraints[it];
auto const &con = m_solver.lra().constraints()[ci1]; auto const &con = m_solver.lra().constraints()[ci1];
for (auto const &cv1 : con.lhs()) { lpvar j = find_max_lex_monomial(con.lhs());
auto j = cv1.j(); if (j == lp::null_lpvar)
if (!is_mon_var(j)) continue;
continue;
auto vars = m_mon2vars[j];
if (vars.size() > m_max_monomial_degree)
continue;
for (auto v : vars) {
if (v >= m_occurs.size())
continue;
svector<lpvar> _vars;
_vars.push_back(v);
for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) {
auto ci2 = m_occurs[v][cidx];
for (auto const & cv2 : m_solver.lra().constraints()[ci2].lhs()) {
auto u = cv2.j();
if (u == v && is_resolvable(ci1, cv1.coeff(), ci2, cv2.coeff()))
resolve(j, ci1, saturate_constraint(ci2, j, _vars));
else if (is_mon_var(u) && is_subset(m_mon2vars[u], vars) &&
is_resolvable(ci1, cv1.coeff(), ci2, cv2.coeff()))
resolve(j, ci1, saturate_constraint(ci2, j, m_mon2vars[u]));
}
}
}
}
}
#if 0
for (unsigned it = 0; it < m_monomials_to_refine.size(); ++it) {
auto j = m_monomials_to_refine[it];
auto vars = m_mon2vars[j]; auto vars = m_mon2vars[j];
TRACE(arith, tout << "j" << j << " " << vars << "\n"); if (vars.size() > m_max_monomial_degree)
continue;
for (auto v : vars) { for (auto v : vars) {
if (v >= m_occurs.size()) if (v >= m_occurs.size())
continue; continue;
svector<lpvar> _vars; svector<lpvar> _vars;
_vars.push_back(v); _vars.push_back(v);
for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) { for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) {
auto ci = m_occurs[v][cidx]; auto ci2 = m_occurs[v][cidx];
for (auto const &cv1 : m_solver.lra().constraints()[ci].lhs()) { if (ci1 == ci2)
auto u = cv1.j(); continue;
for (auto const &cv2 : m_solver.lra().constraints()[ci2].lhs()) {
auto u = cv2.j();
if (u == v) if (u == v)
saturate_constraint(ci, j, _vars); resolve(j, ci1, saturate_constraint(ci2, j, _vars));
else if (is_mon_var(u) && is_subset(m_mon2vars[u], vars)) else if (is_mon_var(u) && is_subset(m_mon2vars[u], vars))
saturate_constraint(ci, j, m_mon2vars[u]); resolve(j, ci1, saturate_constraint(ci2, j, m_mon2vars[u]));
} }
} }
} }
} }
#endif
IF_VERBOSE(5, IF_VERBOSE(5,
c().lra_solver().display(verbose_stream() << "original\n"); c().lra_solver().display(verbose_stream() << "original\n");
c().display(verbose_stream()); c().display(verbose_stream());
display(verbose_stream() << "saturated\n")); display(verbose_stream() << "saturated\n"));
} }
bool stellensatz::is_resolvable(lp::constraint_index ci1, rational const& c1, lp::constraint_index ci2, lpvar stellensatz::find_max_lex_monomial(lp::lar_term const& t) const {
rational const& c2) const { lpvar result = lp::null_lpvar;
SASSERT(c1 != 0); for (auto const &cv : t) {
SASSERT(c2 != 0); auto j = cv.j();
auto const &con1 = m_solver.lra().constraints()[ci1]; if (!is_mon_var(j))
auto const &con2 = m_solver.lra().constraints()[ci2]; continue;
auto k1 = con1.kind(); auto const &vars = m_mon2vars[j];
auto k2 = con2.kind(); if (result == lp::null_lpvar)
for (auto const& cv : con1.lhs()) result = j;
if (is_mon_var(cv.j()) && m_mon2vars[cv.j()].size() > m_max_monomial_degree) else if (std::lexicographical_compare(m_mon2vars[result].begin(), m_mon2vars[result].end(), vars.begin(),
return false; vars.end()))
for (auto const &cv : con2.lhs()) result = j;
if (is_mon_var(cv.j()) && m_mon2vars[cv.j()].size() > m_max_monomial_degree) else if (false && is_lex_greater(vars, m_mon2vars[result]))
return false; result = j;
bool same_sign = (c1.is_pos() == c2.is_pos()); }
if (k1 == lp::lconstraint_kind::EQ) return result;
return true; }
if (k2 == lp::lconstraint_kind::EQ)
return true; bool stellensatz::is_lex_greater(svector<lpvar> const& a, svector<lpvar> const& b) const {
bool is_le1 = (k1 == lp::lconstraint_kind::LE || k1 == lp::lconstraint_kind::LT); if (a.size() != b.size())
bool is_le2 = (k2 == lp::lconstraint_kind::LE || k2 == lp::lconstraint_kind::LT); return a.size() > b.size();
if ((is_le1 == is_le2) && !same_sign) for (unsigned i = a.size(); i-- > 0;) {
return true; if (a[i] != b[i])
if ((is_le1 != is_le2) && same_sign) return a[i] > b[i];
return true; }
return false; return false;
} }
void stellensatz::resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2) { void stellensatz::resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2) {
// resolut of saturate_constraint could swap inequality, // resolut of saturate_constraint could swap inequality,
// so the premise of is_resolveable may not hold. // so the premise of is_resolveable may not hold.
return;
auto const &constraints = m_solver.lra().constraints(); auto const &constraints = m_solver.lra().constraints();
if (!constraints.valid_index(ci1)) if (!constraints.valid_index(ci1))
return; return;
@ -567,15 +542,19 @@ namespace nla {
return; return;
auto const &con1 = constraints[ci1]; auto const &con1 = constraints[ci1];
auto const &con2 = constraints[ci2]; auto const &con2 = constraints[ci2];
for (auto const &cv : con1.lhs())
if (is_mon_var(cv.j()) && m_mon2vars[cv.j()].size() > m_max_monomial_degree)
return;
for (auto const &cv : con2.lhs())
if (is_mon_var(cv.j()) && m_mon2vars[cv.j()].size() > m_max_monomial_degree)
return;
auto k1 = con1.kind(); auto k1 = con1.kind();
auto k2 = con2.kind(); auto k2 = con2.kind();
auto const & lhs1 = con1.lhs(); auto const & lhs1 = con1.lhs();
auto const & lhs2 = con2.lhs(); auto const & lhs2 = con2.lhs();
auto const& c1 = lhs1.get_coeff(j); auto const& c1 = lhs1.get_coeff(j);
auto const& c2 = lhs2.get_coeff(j); auto const& c2 = lhs2.get_coeff(j);
verbose_stream() << "resolve on " << m_mon2vars[j] << " c1: " << c1 << " c2: " << c2 << "\n";
display_constraint(verbose_stream(), ci1) << "\n";
display_constraint(verbose_stream(), ci2) << "\n";
rational mul1, mul2; rational mul1, mul2;
bool is_le1 = (k1 == lp::lconstraint_kind::LE || k1 == lp::lconstraint_kind::LT); bool is_le1 = (k1 == lp::lconstraint_kind::LE || k1 == lp::lconstraint_kind::LT);
bool is_le2 = (k2 == lp::lconstraint_kind::LE || k2 == lp::lconstraint_kind::LT); bool is_le2 = (k2 == lp::lconstraint_kind::LE || k2 == lp::lconstraint_kind::LT);
@ -589,23 +568,30 @@ namespace nla {
mul2 = (c2 > 0 ? -1 : 1) * c1; mul2 = (c2 > 0 ? -1 : 1) * c1;
} }
else if (is_le1 == is_le2) { else if (is_le1 == is_le2) {
SASSERT(c1.is_pos() != c2.is_pos()); if (c1.is_pos() == c2.is_pos())
return;
mul1 = abs(c2); mul1 = abs(c2);
mul2 = abs(c1); mul2 = abs(c1);
} }
else { else {
SASSERT(c1.is_pos() == c2.is_pos()); if (c1.is_pos() != c2.is_pos())
return;
mul1 = abs(c2); mul1 = abs(c2);
mul2 = -abs(c1); mul2 = -abs(c1);
} }
auto lhs = mul1 * lhs1 + mul2 * lhs2; auto lhs = mul1 * lhs1 + mul2 * lhs2;
auto rhs = mul1 * con1.rhs() + mul2 * con2.rhs(); auto rhs = mul1 * con1.rhs() + mul2 * con2.rhs();
if (lhs.size() == 0) // trivial conflict, will be found using LIA
return;
assumptions bounds; assumptions bounds;
bounds.push_back(ci1); bounds.push_back(ci1);
bounds.push_back(ci2); bounds.push_back(ci2);
auto new_ci = add_ineq("resolve", bounds, lhs, k1, rhs); auto new_ci = add_ineq("resolve", bounds, lhs, k1, rhs);
insert_monomials_from_constraint(new_ci); insert_monomials_from_constraint(new_ci);
display_constraint(verbose_stream(), new_ci) << "\n"; IF_VERBOSE(3, verbose_stream() << "resolve on " << m_mon2vars[j] << " c1: " << c1 << " c2: " << c2 << "\n";
display_constraint(verbose_stream(), ci1) << "\n";
display_constraint(verbose_stream(), ci2) << "\n";
display_constraint(verbose_stream(), new_ci) << "\n");
} }
// multiply by remaining vars // multiply by remaining vars

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

@ -55,6 +55,8 @@ namespace nla {
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon; map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
u_map<unsigned_vector> m_mon2vars; u_map<unsigned_vector> m_mon2vars;
bool is_mon_var(lpvar v) const { return m_mon2vars.contains(v); } bool is_mon_var(lpvar v) const { return m_mon2vars.contains(v); }
lpvar find_max_lex_monomial(lp::lar_term const &t) const;
bool is_lex_greater(svector<lpvar> const &a, svector<lpvar> const &b) const;
unsigned m_max_monomial_degree = 0; unsigned m_max_monomial_degree = 0;
@ -107,7 +109,6 @@ namespace nla {
lbool add_bounds(svector<lpvar> const &vars, assumptions &bounds); lbool add_bounds(svector<lpvar> const &vars, assumptions &bounds);
void saturate_constraints(); void saturate_constraints();
lp::constraint_index saturate_constraint(lp::constraint_index con_id, lp::lpvar mi, svector<lpvar> const & xs); lp::constraint_index saturate_constraint(lp::constraint_index con_id, lp::lpvar mi, svector<lpvar> const & xs);
bool is_resolvable(lp::constraint_index ci1, rational const& c1, lp::constraint_index ci2, rational const& c2) const;
void resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2); void resolve(lpvar j, lp::constraint_index ci1, lp::constraint_index ci2);
void saturate_basic_linearize(); void saturate_basic_linearize();