mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 20:16:00 +00:00
Code Activity

fixup loop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-20 07:46:53 -07:00
parent 4b4e8cbc6e
commit 964dd2a71a
2 changed files with 22 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/nlsat_explain.cpp
View file

@ -1303,7 +1303,8 @@ namespace nlsat {
// Temporarily unassign x, s.t. isolate_roots does not assume p as constant. // Temporarily unassign x, s.t. isolate_roots does not assume p as constant.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
unsigned num_roots = roots.size(); unsigned num_roots = roots.size();
if (num_roots == 0) continue; if (num_roots == 0)
continue;
// find p's smallest root above the sample // find p's smallest root above the sample
unsigned i = 0; unsigned i = 0;
@ -1319,7 +1320,8 @@ namespace nlsat {
p_lower = p; p_lower = p;
i_lower = i+1; i_lower = i+1;
break; // TODO: choose the best among multiple section polynomials? break; // TODO: choose the best among multiple section polynomials?
} else if (s < 0) { }
else if (s < 0) {
// x_val < roots[i] // x_val < roots[i]
ps_above.push_back(p); ps_above.push_back(p);
if (upper_inf || m_am.lt(roots[i], upper)) { if (upper_inf || m_am.lt(roots[i], upper)) {
@ -1348,7 +1350,8 @@ namespace nlsat {
if (!m_am.is_rational(x_val)) { if (!m_am.is_rational(x_val)) {
// TODO: FAIL // TODO: FAIL
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} else if (m_pm.total_degree(p_lower) > 1) { }
else if (m_pm.total_degree(p_lower) > 1) {
rational bound; rational bound;
m_am.to_rational(x_val, bound); m_am.to_rational(x_val, bound);
p_lower = m_pm.mk_polynomial(x); p_lower = m_pm.mk_polynomial(x);
@ -1446,7 +1449,8 @@ namespace nlsat {
// section // section
lb = ps_equal_sample.back(); lb = ps_equal_sample.back();
psc_resultants_with(ps, lb, x); psc_resultants_with(ps, lb, x);
} else { }
else {
if (!ps_below_sample.empty()) { if (!ps_below_sample.empty()) {
lb = ps_below_sample.back(); lb = ps_below_sample.back();
psc_resultants_with(ps_below_sample, lb, x); psc_resultants_with(ps_below_sample, lb, x);

31
src/nlsat/nlsat_solver.cpp
View file

@ -2044,22 +2044,24 @@ namespace nlsat {
literal best_literal = null_literal; literal best_literal = null_literal;
unsigned sz = m_clauses.size(); unsigned sz = m_clauses.size();
lbool satisfied = l_true; lbool satisfied = l_true;
for (unsigned i = 0; i < sz; i++) { for (auto cp : m_clauses) {
bool c_satisfied = false; auto& c = *cp;
clause const & c = *(m_clauses[i]); bool is_false = all_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_false; });
for (literal l : c) { bool is_true = any_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_true; });
if (const_cast<imp*>(this)->value(l) != l_false) { if (is_true)
c_satisfied = true; continue;
break;
if (!is_false) {
satisfied = l_undef;
continue;
} }
}
if (c_satisfied) continue;
// take best literal from c // take best literal from c
for (literal l : c) { for (literal l : c) {
if (best_literal == null_literal) { if (best_literal == null_literal) {
best_literal = l; best_literal = l;
} else { }
else {
bool_var b_best = best_literal.var(); bool_var b_best = best_literal.var();
bool_var b_l = l.var(); bool_var b_l = l.var();
if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) { if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) {
@ -2070,14 +2072,9 @@ namespace nlsat {
} }
} }
if (satisfied == l_true) { if (best_literal == null_literal)
// nothing to do return satisfied;
return l_true;
}
if (satisfied == l_undef) {
// nothing to do?
return l_undef; return l_undef;
}
// assignment does not satisfy the constraints -> create lemma // assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal); SASSERT(best_literal != null_literal);