mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-02-13 10:51:44 -10:00
parent f1d97c7a3a
commit 4d06c399cc
5 changed files with 70 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/nlsat/nlsat_evaluator.cpp
View file

@ -286,23 +286,24 @@ namespace nlsat {
} }
bool check_invariant() const { bool check_invariant() const {
DEBUG_CODE( #ifdef Z3DEBUG
SASSERT(m_sections.size() == m_sorted_sections.size()); SASSERT(m_sections.size() == m_sorted_sections.size());
for (unsigned i = 0; i < m_sorted_sections.size(); i++) { for (unsigned i = 0; i < m_sorted_sections.size(); i++) {
SASSERT(m_sorted_sections[i] < m_sections.size()); SASSERT(m_sorted_sections[i] < m_sections.size());
SASSERT(m_sections[m_sorted_sections[i]].m_pos == i); SASSERT(m_sections[m_sorted_sections[i]].m_pos == i);
} }
unsigned total_num_sections = 0; unsigned total_num_sections = 0;
unsigned total_num_signs = 0; unsigned total_num_signs = 0;
for (unsigned i = 0; i < m_info.size(); i++) { for (unsigned i = 0; i < m_info.size(); i++) {
SASSERT(m_info[i].m_first_section <= m_poly_sections.size()); SASSERT(m_info[i].m_first_section <= m_poly_sections.size());
SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size()); SASSERT(m_info[i].m_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size());
SASSERT(m_info[i].m_first_sign < m_poly_signs.size()); SASSERT(m_info[i].m_first_sign < m_poly_signs.size());
total_num_sections += m_info[i].m_num_roots; total_num_sections += m_info[i].m_num_roots;
total_num_signs += m_info[i].m_num_roots + 1; total_num_signs += m_info[i].m_num_roots + 1;
} }
SASSERT(total_num_sections == m_poly_sections.size()); SASSERT(total_num_sections == m_poly_sections.size());
SASSERT(total_num_signs == m_poly_signs.size());); SASSERT(total_num_signs == m_poly_signs.size());
#endif
return true; return true;
} }

27
src/nlsat/nlsat_explain.cpp
View file

@ -1531,12 +1531,13 @@ namespace nlsat {
m_solver.display(tout, num, ls); m_solver.display(tout, num, ls);
m_solver.display(tout);); m_solver.display(tout););
DEBUG_CODE( #ifdef Z3DEBUG
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
SASSERT(m_solver.value(ls[i]) == l_true); SASSERT(m_solver.value(ls[i]) == l_true);
atom* a = m_atoms[ls[i].var()]; atom* a = m_atoms[ls[i].var()];
SASSERT(!a || m_evaluator.eval(a, ls[i].sign())); SASSERT(!a || m_evaluator.eval(a, ls[i].sign()));
}); }
#endif
split_literals(x, num, ls, lits); split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.data(), m_ps); collect_polys(lits.size(), lits.data(), m_ps);
var mx_var = max_var(m_ps); var mx_var = max_var(m_ps);
@ -1571,13 +1572,13 @@ namespace nlsat {
for (unsigned i = 0; i < result.size(); ++i) { for (unsigned i = 0; i < result.size(); ++i) {
result.set(i, ~result[i]); result.set(i, ~result[i]);
} }
DEBUG_CODE( #ifdef Z3DEBUG
TRACE("nlsat", m_solver.display(tout, result.size(), result.data()) << "\n"; ); TRACE("nlsat", m_solver.display(tout, result.size(), result.data()) << "\n"; );
for (literal l : result) { for (literal l : result) {
CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";); CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
SASSERT(l_true == m_solver.value(l)); SASSERT(l_true == m_solver.value(l));
}); }
#endif
} }
void split_literals(var x, unsigned n, literal const* ls, svector<literal>& lits) { void split_literals(var x, unsigned n, literal const* ls, svector<literal>& lits) {

13
src/nlsat/nlsat_interval_set.cpp
View file

@ -98,12 +98,13 @@ namespace nlsat {
// Check if the intervals are valid, ordered, and are disjoint. // Check if the intervals are valid, ordered, and are disjoint.
bool check_interval_set(anum_manager & am, unsigned sz, interval const * ints) { bool check_interval_set(anum_manager & am, unsigned sz, interval const * ints) {
DEBUG_CODE( #ifdef Z3DEBUG
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
interval const & curr = ints[i]; interval const & curr = ints[i];
SASSERT(check_interval(am, curr)); SASSERT(check_interval(am, curr));
SASSERT(i >= sz - 1 || check_no_overlap(am, curr, ints[i+1])); SASSERT(i >= sz - 1 || check_no_overlap(am, curr, ints[i+1]));
}); }
#endif
return true; return true;
} }

52
src/nlsat/nlsat_solver.cpp
View file

@ -1868,7 +1868,8 @@ namespace nlsat {
m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr)); m_valids.push_back(mk_clause_core(m_lazy_clause.size(), m_lazy_clause.data(), false, nullptr));
} }
DEBUG_CODE({ #ifdef Z3DEBUG
{
unsigned sz = m_lazy_clause.size(); unsigned sz = m_lazy_clause.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
literal l = m_lazy_clause[i]; literal l = m_lazy_clause[i];
@ -1881,7 +1882,8 @@ namespace nlsat {
SASSERT(l.sign() || m_bvalues[b] == l_true); SASSERT(l.sign() || m_bvalues[b] == l_true);
} }
} }
}); }
#endif
checkpoint(); checkpoint();
resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.data()); resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.data());
@ -2191,19 +2193,20 @@ namespace nlsat {
// ----------------------- // -----------------------
bool check_watches() const { bool check_watches() const {
DEBUG_CODE( #ifdef Z3DEBUG
for (var x = 0; x < num_vars(); x++) { for (var x = 0; x < num_vars(); x++) {
clause_vector const & cs = m_watches[x]; clause_vector const & cs = m_watches[x];
unsigned sz = cs.size(); unsigned sz = cs.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
SASSERT(max_var(*(cs[i])) == x); SASSERT(max_var(*(cs[i])) == x);
} }
}); }
#endif
return true; return true;
} }
bool check_bwatches() const { bool check_bwatches() const {
DEBUG_CODE( #ifdef Z3DEBUG
for (bool_var b = 0; b < m_bwatches.size(); b++) { for (bool_var b = 0; b < m_bwatches.size(); b++) {
clause_vector const & cs = m_bwatches[b]; clause_vector const & cs = m_bwatches[b];
unsigned sz = cs.size(); unsigned sz = cs.size();
@ -2212,7 +2215,8 @@ namespace nlsat {
SASSERT(max_var(c) == null_var); SASSERT(max_var(c) == null_var);
SASSERT(max_bvar(c) == b); SASSERT(max_bvar(c) == b);
} }
}); }
#endif
return true; return true;
} }
@ -2432,11 +2436,11 @@ namespace nlsat {
// undo_until_size(0) // undo_until_size(0)
undo_until_stage(null_var); undo_until_stage(null_var);
m_cache.reset(); m_cache.reset();
DEBUG_CODE({ #ifdef Z3DEBUG
for (var x = 0; x < num_vars(); x++) { for (var x = 0; x < num_vars(); x++) {
SASSERT(m_watches[x].empty()); SASSERT(m_watches[x].empty());
} }
}); #endif
// update m_perm mapping // update m_perm mapping
for (unsigned ext_x = 0; ext_x < sz; ext_x++) { for (unsigned ext_x = 0; ext_x < sz; ext_x++) {
// p: internal -> new pos // p: internal -> new pos
@ -2452,12 +2456,12 @@ namespace nlsat {
SASSERT(m_infeasible[x] == 0); SASSERT(m_infeasible[x] == 0);
} }
m_inv_perm.swap(new_inv_perm); m_inv_perm.swap(new_inv_perm);
DEBUG_CODE({ #ifdef Z3DEBUG
for (var x = 0; x < num_vars(); x++) { for (var x = 0; x < num_vars(); x++) {
SASSERT(x == m_inv_perm[m_perm[x]]); SASSERT(x == m_inv_perm[m_perm[x]]);
SASSERT(m_watches[x].empty()); SASSERT(m_watches[x].empty());
} }
}); #endif
m_pm.rename(sz, p); m_pm.rename(sz, p);
TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout););
reinit_cache(); reinit_cache();
@ -2477,12 +2481,12 @@ namespace nlsat {
var_vector p; var_vector p;
p.append(m_perm); p.append(m_perm);
reorder(p.size(), p.data()); reorder(p.size(), p.data());
DEBUG_CODE({ #ifdef Z3DEBUG
for (var x = 0; x < num_vars(); x++) { for (var x = 0; x < num_vars(); x++) {
SASSERT(m_perm[x] == x); SASSERT(m_perm[x] == x);
SASSERT(m_inv_perm[x] == x); SASSERT(m_inv_perm[x] == x);
} }
}); #endif
} }
/** /**

4
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -125,7 +125,9 @@ class nlsat_tactic : public tactic {
continue; // don't care continue; // don't care
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false()); md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
} }
DEBUG_CODE(eval_model(*md.get(), g);); #ifdef Z3DEBUG
eval_model(*md.get(), g);
#endif
// VERIFY(eval_model(*md.get(), g)); // VERIFY(eval_model(*md.get(), g));
mc = model2model_converter(md.get()); mc = model2model_converter(md.get());
return ok; return ok;