mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-29 07:13:37 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-05 06:13:37 -10:00
parent 8577877d13
commit 412ed2aa7f
2 changed files with 0 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_explain.cpp
View file

@ -1143,7 +1143,6 @@ namespace nlsat {
bool first = true; bool first = true;
if (ps.empty()) if (ps.empty())
return; return;
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
m_todo.reset(); m_todo.reset();
for (unsigned i = 0; i < ps.size(); ++i) { for (unsigned i = 0; i < ps.size(); ++i) {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
@ -1161,10 +1160,7 @@ namespace nlsat {
if (levelwise_ok) if (levelwise_ok)
return; return;
} }
TRACE(nlsat_explain, ::nlsat::display(tout << "ps before extract:", m_solver, ps)<< "\n";);
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);

8
src/nlsat/nlsat_solver.cpp
View file

@ -1173,10 +1173,6 @@ namespace nlsat {
for (var v : vars) for (var v : vars)
used_vars[v] = true; used_vars[v] = true;
} }
if (m_lemma_count >= 7 && false) {
enable_trace("lws");
enable_trace("nlsat_explain");
}
display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n"; display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
if (m_log_lemma_smtrat) if (m_log_lemma_smtrat)
out << "(set-logic NRA)\n"; out << "(set-logic NRA)\n";
@ -1191,10 +1187,6 @@ namespace nlsat {
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
display_smt2(out << "(assert ", ~cls[i]) << ")\n"; display_smt2(out << "(assert ", ~cls[i]) << ")\n";
out << "(check-sat)\n(reset)\n"; out << "(check-sat)\n(reset)\n";
if (m_lemma_count == 10 && false) {
std::cout << "early exit\n";
exit(1);
}
} }
clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {