From bc50b6bea2d52ae5964fe697e2cde15162ece3b9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 9 Oct 2019 14:09:33 +0100 Subject: [PATCH] fix a few warnings --- src/ast/datatype_decl_plugin.cpp | 3 +-- src/ast/fpa/bv2fpa_converter.cpp | 25 ++++++++++--------------- src/ast/fpa/fpa2bv_converter.cpp | 2 +- src/nlsat/nlsat_explain.cpp | 1 + src/nlsat/nlsat_solver.cpp | 1 + 5 files changed, 14 insertions(+), 18 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 22f328988..73efa7874 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1129,7 +1129,6 @@ namespace datatype { // 2) each type T_i is not recursive or contains a constructor that does not depend on T ptr_vector const& constructors = *get_datatype_constructors(ty); - unsigned sz = constructors.size(); array_util autil(m); cnstr_depth result(nullptr, 0); if (m_datatype2nonrec_constructor.find(ty, result)) @@ -1138,7 +1137,7 @@ namespace datatype { tout << "forbidden: "; for (sort* s : forbidden_set) tout << sort_ref(s, m) << " "; tout << "\n"; - tout << "constructors: " << sz << "\n"; + tout << "constructors: " << constructors.size() << "\n"; for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n"; ); unsigned min_depth = INT_MAX; diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index f1c2b1a14..8386f8960 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -156,10 +156,9 @@ expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * bv) { expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) { expr_ref res(m); - rational bv_val(0); - unsigned sz = 0; + rational bv_val; - if (m_bv_util.is_numeral(bv_rm, bv_val, sz)) { + if (m_bv_util.is_numeral(bv_rm, bv_val)) { SASSERT(bv_val.is_uint64()); switch (bv_val.get_uint64()) { case BV_RM_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break; @@ -266,7 +265,6 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * if (bv_fi) { fpa_rewriter rw(m); - expr_ref ai(m); for (unsigned i = 0; i < bv_fi->num_entries(); i++) { func_entry const * bv_fe = bv_fi->get_entry(i); @@ -276,14 +274,14 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * for (unsigned j = 0; j < arity; j++) { sort * ft_dj = dmn[j]; expr * bv_aj = bv_args[j]; - ai = rebuild_floats(mc, ft_dj, to_app(bv_aj)); + expr_ref ai = rebuild_floats(mc, ft_dj, to_app(bv_aj)); m_th_rw(ai); - new_args.push_back(ai); + new_args.push_back(std::move(ai)); } - expr_ref bv_fres(m), ft_fres(m); + expr_ref bv_fres(m); bv_fres = bv_fe->get_result(); - ft_fres = rebuild_floats(mc, rng, to_app(bv_fres)); + expr_ref ft_fres = rebuild_floats(mc, rng, to_app(bv_fres)); m_th_rw(ft_fres); TRACE("bv2fpa", for (unsigned i = 0; i < new_args.size(); i++) @@ -303,10 +301,9 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * } app_ref bv_els(m); - expr_ref ft_els(m); bv_els = (app*)bv_fi->get_else(); if (bv_els != 0) { - ft_els = rebuild_floats(mc, rng, bv_els); + expr_ref ft_els = rebuild_floats(mc, rng, bv_els); m_th_rw(ft_els); result->set_else(ft_els); } @@ -378,8 +375,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model if (!sgn && !sig && !exp) continue; - expr_ref cv(m); - cv = convert_bv2fp(var->get_range(), sgn, exp, sig); + expr_ref cv = convert_bv2fp(var->get_range(), sgn, exp, sig); target_model->register_decl(var, cv); TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;); @@ -396,8 +392,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo expr * val = it->m_value; SASSERT(m_fpa_util.is_bv2rm(val)); expr * bvval = to_app(val)->get_arg(0); - expr_ref fv(m); - fv = convert_bv2rm(mc, to_app(bvval)); + expr_ref fv = convert_bv2rm(mc, to_app(bvval)); TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;); target_model->register_decl(var, fv); seen.insert(to_app(bvval)->get_decl()); @@ -457,7 +452,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode else { // Just keep. SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range())); - expr_ref var(m), val(m); + expr_ref val(m); if (mc->eval(it->m_value, val)) target_model->register_decl(f, val); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index e0c5fd4d8..7849619cc 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -272,7 +272,7 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e { TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; ); - expr_ref fapp(m), feq(m); + expr_ref fapp(m); sort_ref rng(m); app_ref bv_app(m), flt_app(m); rng = f->get_range(); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 3c3120d5d..1e7b0f334 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -986,6 +986,7 @@ namespace nlsat { bool check_already_added() const { for (bool b : m_already_added_literal) { + (void)b; SASSERT(!b); } return true; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 264af8bc7..2709da1e9 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1685,6 +1685,7 @@ namespace nlsat { bool check_marks() { for (unsigned m : m_marks) { + (void)m; SASSERT(m == 0); } return true;