From 6f2a6da600c3a5f0cb756052b7a41a62bb120b93 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Aug 2022 18:50:54 -0700
Subject: [PATCH] address unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/pp.cpp | 3 ---
src/math/lp/emonics.cpp | 1 +
src/model/model_evaluator.cpp | 8 +++-----
src/nlsat/nlsat_evaluator.cpp | 33 +++++++++++++++++----------------
4 files changed, 21 insertions(+), 24 deletions(-)
diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp
index e307989c9..091b50c97 100644
--- a/src/ast/pp.cpp
+++ b/src/ast/pp.cpp
@@ -66,7 +66,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
bool single_line = p.single_line();
unsigned pos = 0;
- unsigned ribbon_pos = 0;
unsigned line = 0;
unsigned len;
unsigned i;
@@ -92,7 +91,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
break;
}
pos += len;
- ribbon_pos += len;
out << f->get_decl()->get_parameter(0).get_symbol();
break;
case OP_INDENT:
@@ -121,7 +119,6 @@ void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p)
break;
}
pos = indent;
- ribbon_pos = 0;
line++;
if (line < max_num_lines) {
out << "\n";
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 0f1956a2b..060c2b1b9 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -546,6 +546,7 @@ bool emonics::invariant() const {
}
CTRACE("nla_solver_mons", !found, tout << "not found v" << v << ": " << m << "\n";);
SASSERT(found);
+ (void)found;
c = c->m_next;
}
while (c != ht.m_head);
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 5c6d0f311..2d9b1ccae 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -566,14 +566,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
SASSERT(m_ar.is_array(a));
- bool are_values = true;
are_unique = true;
TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
while (m_ar.is_store(a)) {
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
- are_values &= args_are_values(store, are_unique);
+ args_are_values(store, are_unique);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
@@ -584,9 +583,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
if (m_ar_rw.has_index_set(a, else_case, stores)) {
- for (auto const& store : stores) {
- are_values &= args_are_values(store, are_unique);
- }
+ for (auto const& store : stores)
+ args_are_values(store, are_unique);
return true;
}
if (!m_ar.is_as_array(a)) {
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index f7b8f2797..97e0e3d72 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -286,22 +286,23 @@ namespace nlsat {
}
bool check_invariant() const {
- 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());
+ 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()););
return true;
}