From 6c22edc98830bafa91305010174b283a163d2fad Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sat, 16 May 2015 11:44:58 +0100 Subject: [PATCH] fix assorted compiler warnings Signed-off-by: Nuno Lopes --- src/math/polynomial/upolynomial_factorization.cpp | 3 +-- src/muz/ddnf/ddnf.cpp | 5 +---- src/muz/fp/datalog_parser.cpp | 4 ++-- src/muz/pdr/pdr_context.cpp | 7 ++----- src/muz/pdr/pdr_prop_solver.cpp | 3 +-- src/muz/pdr/pdr_prop_solver.h | 3 +-- src/opt/hitting_sets.cpp | 7 +++---- src/opt/opt_context.cpp | 1 - src/opt/opt_solver.cpp | 2 +- src/opt/opt_solver.h | 1 - src/shell/opt_frontend.cpp | 1 - src/tactic/nlsat_smt/nl_purify_tactic.cpp | 4 ++-- src/util/inf_rational.h | 5 +---- src/util/rational.cpp | 12 +++++++++--- 14 files changed, 24 insertions(+), 34 deletions(-) diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 7d5a23d99..0b2977a22 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -719,12 +719,11 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C, // we create a new Z_p manager, since we'll be changing the input one zp_manager zp_upm(nm); zp_upm.set_zp(zpe_upm.m().p()); - zp_numeral_manager & zp_nm = zp_upm.m(); // get the U, V, such that A*U + B*V = 1 (mod p) scoped_mpz_vector U(nm), V(nm), D(nm); zp_upm.ext_gcd(A.size(), A.c_ptr(), B.size(), B.c_ptr(), U, V, D); - SASSERT(D.size() == 1 && zp_nm.is_one(D[0])); + SASSERT(D.size() == 1 && zp_upm.m().is_one(D[0])); // we start lifting from (a = p, b = p, r = p) scoped_mpz_vector A_lifted(nm), B_lifted(nm); diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 14f4a2b75..6545d4282 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -54,7 +54,6 @@ namespace datalog { typedef ptr_hashtable ddnf_nodes; private: - ddnf_mgr& m; tbv_manager& tbvm; tbv const& m_tbv; ddnf_node_vector m_children; @@ -68,7 +67,6 @@ namespace datalog { public: ddnf_node(ddnf_mgr& m, tbv_manager& tbvm, tbv const& tbv, unsigned id): - m(m), tbvm(tbvm), m_tbv(tbv), m_children(m), @@ -130,7 +128,6 @@ namespace datalog { void reset() { memset(this, 0, sizeof(*this)); } }; - unsigned m_num_bits; ddnf_node* m_root; ddnf_node_vector m_noderefs; bool m_internalized; @@ -141,7 +138,7 @@ namespace datalog { svector m_marked; stats m_stats; public: - ddnf_mgr(unsigned n): m_num_bits(n), m_noderefs(*this), m_internalized(false), m_tbv(n), + ddnf_mgr(unsigned n): m_noderefs(*this), m_internalized(false), m_tbv(n), m_hash(m_tbv), m_eq(m_tbv), m_nodes(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq) { tbv* bX = m_tbv.allocateX(); diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 1567dff4f..58bc79e7a 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -89,8 +89,8 @@ public: :m_eof(false), m_eof_behind_buffer(false), m_next_index(0), - m_data_size(0), - m_ok(true) { + m_ok(true), + m_data_size(0) { m_data.resize(2*s_expansion_step); resize_data(0); #if _WINDOWS diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 3b7d5c056..134c0746d 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -80,7 +80,7 @@ namespace pdr { pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), - m_sig(m), m_solver(pm, ctx.get_params().pdr_try_minimize_core(), head->get_name()), + m_sig(m), m_solver(pm, head->get_name()), m_invariants(m), m_transition(m), m_initial_state(m), m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().pdr_cache_mode()) {} @@ -150,9 +150,9 @@ namespace pdr { } datalog::rule const& pred_transformer::find_rule(model_core const& model) const { - datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); obj_map::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); TRACE("pdr_verbose", + datalog::rule_manager& rm = ctx.get_context().get_rule_manager(); for (; it != end; ++it) { expr* pred = it->m_key; tout << mk_pp(pred, m) << ":\n"; @@ -1137,9 +1137,6 @@ namespace pdr { if (n->get_model_ptr()) { models.insert(n->state(), n->get_model_ptr()); rules.insert(n->state(), n->get_rule()); - pred_transformer& pt = n->pt(); - context& ctx = pt.get_context(); - datalog::context& dctx = ctx.get_context(); } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index a7d0a02bf..9ba976254 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -225,12 +225,11 @@ namespace pdr { }; - prop_solver::prop_solver(manager& pm, bool try_minimize_core, symbol const& name) : + prop_solver::prop_solver(manager& pm, symbol const& name) : m_fparams(pm.get_fparams()), m(pm.get_manager()), m_pm(pm), m_name(name), - m_try_minimize_core(try_minimize_core), m_ctx(pm.mk_fresh()), m_pos_level_atoms(m), m_neg_level_atoms(m), diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h index d7f13a603..a44ac7e5a 100644 --- a/src/muz/pdr/pdr_prop_solver.h +++ b/src/muz/pdr/pdr_prop_solver.h @@ -40,7 +40,6 @@ namespace pdr { ast_manager& m; manager& m_pm; symbol m_name; - bool m_try_minimize_core; scoped_ptr m_ctx; decl_vector m_level_preds; app_ref_vector m_pos_level_atoms; // atoms used to identify level @@ -74,7 +73,7 @@ namespace pdr { public: - prop_solver(pdr::manager& pm, bool try_minimize_core, symbol const& name); + prop_solver(pdr::manager& pm, symbol const& name); /** return true is s is a symbol introduced by prop_solver */ bool is_aux_symbol(func_decl * s) const { diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index 8c10d3640..30ed1287a 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -149,13 +149,12 @@ namespace opt { m_max_weight(0), m_denominator(1), m_alloc("hitting-sets"), - m_weights_var(0), m_qhead(0), - m_scope_lvl(0), m_conflict_j(justification(justification::AXIOM)), m_inconsistent(false), - m_compare_scores(), - m_heap(0, m_compare_scores) { + m_scope_lvl(0), + m_heap(0, m_compare_scores), + m_weights_var(0) { m_enable_simplex = true; m_compare_scores.m_imp = this; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3cae51bc2..857b57296 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1343,7 +1343,6 @@ namespace opt { break; } case O_MAXSMT: { - maxsmt& ms = *m_maxsmts.find(obj.m_id); rational value(0); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { VERIFY(m_model->eval(obj.m_terms[i], val)); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 4f268268d..d505a9ffb 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -41,9 +41,9 @@ namespace opt { m_params(p), m_context(mgr, m_params), m(mgr), - m_dump_benchmarks(false), m_fm(fm), m_objective_sorts(m), + m_dump_benchmarks(false), m_first(true) { m_params.updt_params(p); m_params.m_relevancy_lvl = 0; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index f3a4099d0..19205ddd9 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -73,7 +73,6 @@ namespace opt { filter_model_converter& m_fm; progress_callback * m_callback; symbol m_logic; - bool m_objective_enabled; svector m_objective_vars; vector m_objective_values; sref_vector m_models; diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 616fc1962..a7b4f807e 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -340,7 +340,6 @@ unsigned parse_opt(char const* file_name, bool is_wcnf) { g_start_time = static_cast(clock()); register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); - unsigned result = 0; if (file_name) { std::ifstream in(file_name); if (in.bad() || in.fail()) { diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 5f0163077..9b84654b9 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -631,11 +631,11 @@ public: m(m), m_util(m), m_params(p), + m_fmc(0), + m_cancel(false), m_nl_tac(mk_nlsat_tactic(m, p)), m_nl_g(0), m_solver(mk_smt_solver(m, p, symbol::null)), - m_fmc(0), - m_cancel(false), m_eq_preds(m), m_new_reals(m), m_new_preds(m), diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index 2da99cca5..e1060a7b0 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -63,10 +63,7 @@ class inf_rational { return s; } - inf_rational(): - m_first(rational()), - m_second(rational()) - {} + inf_rational() {} inf_rational(const inf_rational & r): m_first(r.m_first), diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 122db7217..743038972 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -24,9 +24,9 @@ Revision History: #endif synch_mpq_manager * rational::g_mpq_manager = 0; -rational rational::m_zero(0); -rational rational::m_one(1); -rational rational::m_minus_one(-1); +rational rational::m_zero; +rational rational::m_one; +rational rational::m_minus_one; vector rational::m_powers_of_two; void mk_power_up_to(vector & pws, unsigned n) { @@ -56,11 +56,17 @@ rational rational::power_of_two(unsigned k) { void rational::initialize() { if (!g_mpq_manager) { g_mpq_manager = alloc(synch_mpq_manager); + m().set(m_zero.m_val, 0); + m().set(m_one.m_val, 1); + m().set(m_minus_one.m_val, -1); } } void rational::finalize() { m_powers_of_two.finalize(); + m_zero.~rational(); + m_one.~rational(); + m_minus_one.~rational(); dealloc(g_mpq_manager); g_mpq_manager = 0; }