diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 0d319af39..c74b4f185 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -341,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d } else { SASSERT(u.is_irrational_algebraic_numeral(t)); - anum const & val = u.to_irrational_algebraic_numeral(t); + anum const & val2 = u.to_irrational_algebraic_numeral(t); algebraic_numbers::manager & am = u.am(); format * vf; std::ostringstream buffer; bool is_neg = false; if (decimal) { scoped_anum abs_val(am); - am.set(abs_val, val); - if (am.is_neg(val)) { + am.set(abs_val, val2); + if (am.is_neg(val2)) { is_neg = true; am.neg(abs_val); } am.display_decimal(buffer, abs_val, decimal_prec); } else { - am.display_root_smt2(buffer, val); + am.display_root_smt2(buffer, val2); } vf = mk_string(get_manager(), buffer.str().c_str()); return is_neg ? mk_neg(vf) : vf; diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index d77deca01..79f8f740e 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu return mk_list_assoc_app(m, decl, num_args, args); } -bool is_well_formed_vars(ptr_vector& bound, expr* e) { +bool is_well_formed_vars(ptr_vector& bound, expr * top) { ptr_vector todo; ast_mark mark; - todo.push_back(e); + todo.push_back(top); while (!todo.empty()) { - expr* e = todo.back(); + expr * e = todo.back(); todo.pop_back(); if (mark.is_marked(e)) { continue; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index d707f0178..c185540b7 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -149,10 +149,10 @@ enum status { */ static bool is_recursive_datatype(parameter const * parameters) { unsigned num_types = parameters[0].get_int(); - unsigned tid = parameters[1].get_int(); + unsigned top_tid = parameters[1].get_int(); buffer already_found(num_types, WHITE); buffer todo; - todo.push_back(tid); + todo.push_back(top_tid); while (!todo.empty()) { unsigned tid = todo.back(); if (already_found[tid] == BLACK) { @@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) { */ static sort_size get_datatype_size(parameter const * parameters) { unsigned num_types = parameters[0].get_int(); - unsigned tid = parameters[1].get_int(); + unsigned top_tid = parameters[1].get_int(); buffer szs(num_types, sort_size()); buffer already_found(num_types, WHITE); buffer todo; - todo.push_back(tid); + todo.push_back(top_tid); while (!todo.empty()) { unsigned tid = todo.back(); if (already_found[tid] == BLACK) { @@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) { } } } - return szs[tid]; + return szs[top_tid]; } /** @@ -657,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const { for (unsigned tid = 0; tid < num_types; tid++) { unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset unsigned num_constructors = parameters[o].get_int(); - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o + s].get_int(); + for (unsigned si = 1; si <= num_constructors; si++) { + unsigned k_i = parameters[o + si].get_int(); unsigned num_accessors = parameters[k_i + 2].get_int(); unsigned r = 0; for (; r < num_accessors; r++) { diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp index fbabcb150..097d77cbc 100644 --- a/src/ast/expr2polynomial.cpp +++ b/src/ast/expr2polynomial.cpp @@ -367,16 +367,16 @@ struct expr2polynomial::imp { begin_loop: checkpoint(); frame & fr = m_frame_stack.back(); - app * t = fr.m_curr; - TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";); - unsigned num_args = t->get_num_args(); + app * a = fr.m_curr; + TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";); + unsigned num_args = a->get_num_args(); while (fr.m_idx < num_args) { - expr * arg = t->get_arg(fr.m_idx); + expr * arg = a->get_arg(fr.m_idx); fr.m_idx++; if (!visit(arg)) goto begin_loop; } - process_app(t); + process_app(a); m_frame_stack.pop_back(); } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 16b7cc1da..75e8dfd99 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2219,13 +2219,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * SASSERT(sz == 3); BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned(); - mpf_rounding_mode rm; + mpf_rounding_mode mrm; switch (bv_rm) { - case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break; - case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break; - case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break; - case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break; - case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break; + case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break; + case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break; + case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break; + case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break; + case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break; default: UNREACHABLE(); } @@ -2237,17 +2237,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * return mk_pzero(f, result); else { scoped_mpf v(m_mpf_manager); - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); + m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq()); - - - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); - mk_bias(unbiased_exp, e); + mk_bias(unbiased_exp, exp); - mk_fp(sgn, e, s, result); + mk_fp(sgn, exp, sig, result); } } else if (m_util.au().is_numeral(x)) { @@ -2275,37 +2273,37 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref v1(m), v2(m), v3(m), v4(m); - expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v1); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v1); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v2); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v2); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v3); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v3); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); - mk_bias(unbiased_exp, e); - mk_fp(sgn, e, s, v4); + mk_bias(unbiased_exp, exp); + mk_fp(sgn, exp, sig, v4); sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1); - s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); + sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1); unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits); - mk_bias(unbiased_exp, e); + mk_bias(unbiased_exp, exp); - mk_fp(sgn, e, s, result); + mk_fp(sgn, exp, sig, result); mk_ite(rm_tn, v4, result, result); mk_ite(rm_tp, v3, result, result); mk_ite(rm_nte, v2, result, result); @@ -3350,7 +3348,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref // the maximum shift is `sbits', because after that the mantissa // would be zero anyways. So we can safely cut the shift variable down, // as long as we check the higher bits. - expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m); + expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m); zero_s = m_bv_util.mk_numeral(0, sbits-1); sbits_s = m_bv_util.mk_numeral(sbits, sbits); sh = m_bv_util.mk_extract(ebits-1, sbits, shift); diff --git a/src/ast/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp index 162efb0dd..76f1e3889 100644 --- a/src/ast/func_decl_dependencies.cpp +++ b/src/ast/func_decl_dependencies.cpp @@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort { return false; m_todo.push_back(f); while (!m_todo.empty()) { - func_decl * f = m_todo.back(); + func_decl * cf = m_todo.back(); - switch (get_color(f)) { + switch (get_color(cf)) { case CLOSED: m_todo.pop_back(); break; case OPEN: - set_color(f, IN_PROGRESS); - if (visit_children(f)) { + set_color(cf, IN_PROGRESS); + if (visit_children(cf)) { SASSERT(m_todo.back() == f); m_todo.pop_back(); - set_color(f, CLOSED); + set_color(cf, CLOSED); } break; case IN_PROGRESS: - if (all_children_closed(f)) { - SASSERT(m_todo.back() == f); - set_color(f, CLOSED); + if (all_children_closed(cf)) { + SASSERT(m_todo.back() == cf); + set_color(cf, CLOSED); } else { m_todo.reset(); return true; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index e97933921..9284ff420 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -464,18 +464,18 @@ void bit_blaster_tpl::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr // update p if (i < sz - 1) { for (unsigned j = sz - 1; j > 0; j--) { - expr_ref i(m()); - mk_ite(q, t.get(j-1), p.get(j-1), i); - p.set(j, i); + expr_ref ie(m()); + mk_ite(q, t.get(j-1), p.get(j-1), ie); + p.set(j, ie); } p.set(0, a_bits[sz - i - 2]); } else { // last step: p contains the remainder for (unsigned j = 0; j < sz; j++) { - expr_ref i(m()); - mk_ite(q, t.get(j), p.get(j), i); - p.set(j, i); + expr_ref ie(m()); + mk_ite(q, t.get(j), p.get(j), ie); + p.set(j, ie); } } } diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 92f06679d..be3bfbd0a 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -324,7 +324,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { } result_stack().push_back(def); TRACE("get_macro", tout << "bindings:\n"; - for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";); + for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";); begin_scope(); m_num_qvars = 0; m_root = def; diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h index e135fea84..b522f4a4d 100644 --- a/src/ast/shared_occs.h +++ b/src/ast/shared_occs.h @@ -75,7 +75,7 @@ public: iterator end_shared() const { return m_shared.end(); } void reset(); void cleanup(); - void display(std::ostream & out, ast_manager & m) const; + void display(std::ostream & out, ast_manager & mgr) const; }; #endif diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index 0de507183..dc24a625b 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -34,8 +34,8 @@ struct arith_bounds_tactic : public tactic { bounds_arith_subsumption(in, result); } - virtual tactic* translate(ast_manager& m) { - return alloc(arith_bounds_tactic, m); + virtual tactic* translate(ast_manager & mgr) { + return alloc(arith_bounds_tactic, mgr); } void checkpoint() { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 9765bced5..149cbc272 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -709,8 +709,6 @@ public: tactic_ref_vector ts2; goal_ref_vector g_copies; - ast_manager & m = in->m(); - for (unsigned i = 0; i < r1_size; i++) { ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode()); managers.push_back(new_m);