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

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-27 08:06:24 -08:00
parent 25d0386ade
commit 97c28cb226
2 changed files with 16 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/nlsat/nlsat_explain.cpp
View file

@ -1199,31 +1199,29 @@ namespace nlsat {
for (auto p: m_todo.m_set) for (auto p: m_todo.m_set)
ps.push_back(p); ps.push_back(p);
var x = m_todo.extract_max_polys(ps); m_todo.extract_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am); levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am);
auto cell = lws.single_cell(); auto cell = lws.single_cell();
TRACE(lws, for (unsigned i = 0; i < cell.size(); i++) TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";); display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
if (x < max_x) // Enumerate all intervals in the computed cell and add literals for each non-trivial interval.
cac_add_cell_lits(ps, x); // Non-trivial = section, or sector with at least one finite bound (ignore (-oo,+oo)).
for (auto const & I : cell) {
while (true) { if (I.is_section()) {
if (all_univ(ps, x) && m_todo.empty()) { if (I.l && I.l_index) // root indices start at 1
m_todo.reset(); add_root_literal(atom::ROOT_EQ, max_var(I.l.get()), I.l_index, I.l.get());
break; continue;
} }
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x); tout << "\npolynomials\n"; if (I.l_inf() && I.u_inf())
display(tout, m_solver, ps); tout << "\n";); continue; // skip whole-line sector
add_lcs(ps, x); if (!I.l_inf() && I.l_index)
psc_discriminant(ps, x); add_root_literal(m_full_dimensional ? atom::ROOT_GE :
psc_resultant(ps, x); atom::ROOT_GT, max_var(I.l.get()), I.l_index, I.l.get());
if (!I.u_inf() && I.u_index && I.u)
if (m_todo.empty()) add_root_literal(m_full_dimensional ? atom::ROOT_LE :
break; atom::ROOT_LT, max_var(I.u.get()), I.u_index, I.u.get());
x = m_todo.extract_max_polys(ps);
cac_add_cell_lits(ps, x);
} }
} }

2
src/nlsat/nlsat_solver.cpp
View file

@ -2221,8 +2221,6 @@ namespace nlsat {
// lazy clause is a valid clause // lazy clause is a valid clause
TRACE(nlsat_mathematica, display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data());); TRACE(nlsat_mathematica, display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data()););
std::cout << "early exit!!!\n";
exit(0);
if (m_dump_mathematica) { if (m_dump_mathematica) {
// verbose_stream() << "lazy clause\n"; // verbose_stream() << "lazy clause\n";
display_mathematica_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data()) << std::endl; display_mathematica_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data()) << std::endl;