diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 1f93737dc51..ca6f9efaeb4 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -286,23 +286,24 @@ namespace nlsat { } bool check_invariant() const { - DEBUG_CODE( - SASSERT(m_sections.size() == m_sorted_sections.size()); - for (unsigned i = 0; i < m_sorted_sections.size(); i++) { - SASSERT(m_sorted_sections[i] < m_sections.size()); - SASSERT(m_sections[m_sorted_sections[i]].m_pos == i); - } - unsigned total_num_sections = 0; - unsigned total_num_signs = 0; - 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_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size()); - SASSERT(m_info[i].m_first_sign < m_poly_signs.size()); - total_num_sections += m_info[i].m_num_roots; - total_num_signs += m_info[i].m_num_roots + 1; - } - SASSERT(total_num_sections == m_poly_sections.size()); - SASSERT(total_num_signs == m_poly_signs.size());); +#ifdef Z3DEBUG + SASSERT(m_sections.size() == m_sorted_sections.size()); + for (unsigned i = 0; i < m_sorted_sections.size(); i++) { + SASSERT(m_sorted_sections[i] < m_sections.size()); + SASSERT(m_sections[m_sorted_sections[i]].m_pos == i); + } + unsigned total_num_sections = 0; + unsigned total_num_signs = 0; + 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_num_roots == 0 || m_info[i].m_first_section < m_poly_sections.size()); + SASSERT(m_info[i].m_first_sign < m_poly_signs.size()); + total_num_sections += m_info[i].m_num_roots; + total_num_signs += m_info[i].m_num_roots + 1; + } + SASSERT(total_num_sections == m_poly_sections.size()); + SASSERT(total_num_signs == m_poly_signs.size()); +#endif return true; } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 0b76a14efb1..87fda76ef2c 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1531,12 +1531,13 @@ namespace nlsat { m_solver.display(tout, num, ls); m_solver.display(tout);); - DEBUG_CODE( - for (unsigned i = 0; i < num; ++i) { - SASSERT(m_solver.value(ls[i]) == l_true); - atom* a = m_atoms[ls[i].var()]; - SASSERT(!a || m_evaluator.eval(a, ls[i].sign())); - }); +#ifdef Z3DEBUG + for (unsigned i = 0; i < num; ++i) { + SASSERT(m_solver.value(ls[i]) == l_true); + atom* a = m_atoms[ls[i].var()]; + SASSERT(!a || m_evaluator.eval(a, ls[i].sign())); + } +#endif split_literals(x, num, ls, lits); collect_polys(lits.size(), lits.data(), m_ps); var mx_var = max_var(m_ps); @@ -1571,13 +1572,13 @@ namespace nlsat { for (unsigned i = 0; i < result.size(); ++i) { result.set(i, ~result[i]); } - DEBUG_CODE( - TRACE("nlsat", m_solver.display(tout, result.size(), result.data()) << "\n"; ); - for (literal l : result) { - 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)); - }); - +#ifdef Z3DEBUG + TRACE("nlsat", m_solver.display(tout, result.size(), result.data()) << "\n"; ); + for (literal l : result) { + 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)); + } +#endif } void split_literals(var x, unsigned n, literal const* ls, svector& lits) { diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 693690380f1..f928fd5b6cc 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -98,12 +98,13 @@ namespace nlsat { // Check if the intervals are valid, ordered, and are disjoint. bool check_interval_set(anum_manager & am, unsigned sz, interval const * ints) { - DEBUG_CODE( - for (unsigned i = 0; i < sz; i++) { - interval const & curr = ints[i]; - SASSERT(check_interval(am, curr)); - SASSERT(i >= sz - 1 || check_no_overlap(am, curr, ints[i+1])); - }); +#ifdef Z3DEBUG + for (unsigned i = 0; i < sz; i++) { + interval const & curr = ints[i]; + SASSERT(check_interval(am, curr)); + SASSERT(i >= sz - 1 || check_no_overlap(am, curr, ints[i+1])); + } +#endif return true; } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 71a6b7a4744..d99603dcddc 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1868,7 +1868,8 @@ namespace nlsat { 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(); for (unsigned i = 0; i < sz; i++) { literal l = m_lazy_clause[i]; @@ -1881,7 +1882,8 @@ namespace nlsat { SASSERT(l.sign() || m_bvalues[b] == l_true); } } - }); + } +#endif checkpoint(); resolve_clause(b, m_lazy_clause.size(), m_lazy_clause.data()); @@ -2191,19 +2193,20 @@ namespace nlsat { // ----------------------- bool check_watches() const { - DEBUG_CODE( - for (var x = 0; x < num_vars(); x++) { +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { clause_vector const & cs = m_watches[x]; unsigned sz = cs.size(); for (unsigned i = 0; i < sz; i++) { SASSERT(max_var(*(cs[i])) == x); } - }); + } +#endif return true; } bool check_bwatches() const { - DEBUG_CODE( +#ifdef Z3DEBUG for (bool_var b = 0; b < m_bwatches.size(); b++) { clause_vector const & cs = m_bwatches[b]; unsigned sz = cs.size(); @@ -2212,7 +2215,8 @@ namespace nlsat { SASSERT(max_var(c) == null_var); SASSERT(max_bvar(c) == b); } - }); + } +#endif return true; } @@ -2432,11 +2436,11 @@ namespace nlsat { // undo_until_size(0) undo_until_stage(null_var); m_cache.reset(); - DEBUG_CODE({ - for (var x = 0; x < num_vars(); x++) { - SASSERT(m_watches[x].empty()); - } - }); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(m_watches[x].empty()); + } +#endif // update m_perm mapping for (unsigned ext_x = 0; ext_x < sz; ext_x++) { // p: internal -> new pos @@ -2452,12 +2456,12 @@ namespace nlsat { SASSERT(m_infeasible[x] == 0); } m_inv_perm.swap(new_inv_perm); - DEBUG_CODE({ - for (var x = 0; x < num_vars(); x++) { - SASSERT(x == m_inv_perm[m_perm[x]]); - SASSERT(m_watches[x].empty()); - } - }); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(x == m_inv_perm[m_perm[x]]); + SASSERT(m_watches[x].empty()); + } +#endif m_pm.rename(sz, p); TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); reinit_cache(); @@ -2477,12 +2481,12 @@ namespace nlsat { var_vector p; p.append(m_perm); reorder(p.size(), p.data()); - DEBUG_CODE({ - for (var x = 0; x < num_vars(); x++) { - SASSERT(m_perm[x] == x); - SASSERT(m_inv_perm[x] == x); - } - }); +#ifdef Z3DEBUG + for (var x = 0; x < num_vars(); x++) { + SASSERT(m_perm[x] == x); + SASSERT(m_inv_perm[x] == x); + } +#endif } /** diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 3baf9da8765..9426de78ee7 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -125,7 +125,9 @@ class nlsat_tactic : public tactic { continue; // don't care 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)); mc = model2model_converter(md.get()); return ok;