From 7ce88d4da9d985380bb3cb033a9e3113e8779703 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 21 Apr 2013 14:36:39 -0700 Subject: [PATCH] fix a few compilation warnings - remove unused variables and class fields - add support for gcc 4.5 & clang's __builtin_unreachable - fix 2 bugs related to strict aliasing - remove a few unused function parameters Signed-off-by: Nuno Lopes --- src/ast/ast.cpp | 2 +- src/ast/ast.h | 1 - src/ast/dl_decl_plugin.cpp | 1 + src/ast/float_decl_plugin.cpp | 1 + src/ast/func_decl_dependencies.cpp | 5 ++--- src/ast/macros/quasi_macros.cpp | 3 +-- src/ast/macros/quasi_macros.h | 3 +-- src/ast/recurse_expr.h | 2 +- src/ast/substitution/matcher.cpp | 4 ---- src/ast/substitution/matcher.h | 3 +-- src/ast/substitution/substitution.cpp | 2 +- src/math/subpaving/subpaving.cpp | 4 ---- src/muz_qe/dl_context.cpp | 1 - src/muz_qe/dl_interval_relation.cpp | 16 ++++++---------- src/muz_qe/dl_mk_bit_blast.cpp | 1 - src/muz_qe/dl_mk_explanations.cpp | 3 +-- src/muz_qe/dl_mk_karr_invariants.cpp | 7 ++----- src/muz_qe/dl_mk_subsumption_checker.cpp | 4 +--- src/muz_qe/dl_relation_manager.cpp | 4 +--- src/muz_qe/dl_relation_manager.h | 8 +++----- src/muz_qe/dl_util.h | 4 +--- src/muz_qe/nlarith_util.cpp | 1 - src/muz_qe/pdr_context.cpp | 2 +- src/muz_qe/pdr_farkas_learner.cpp | 5 ++--- src/muz_qe/qe.cpp | 5 +---- src/muz_qe/qe_dl_plugin.cpp | 2 -- src/muz_qe/tab_context.cpp | 4 ---- src/parsers/smt/smtparser.cpp | 8 +++----- src/parsers/smt2/smt2scanner.cpp | 1 - src/parsers/smt2/smt2scanner.h | 1 - src/smt/asserted_formulas.cpp | 2 +- src/smt/database.h | 2 +- src/smt/expr_context_simplifier.cpp | 2 +- src/smt/expr_context_simplifier.h | 2 -- src/smt/mam.cpp | 2 -- src/smt/theory_dl.cpp | 9 +++------ src/tactic/ufbv/quasi_macros_tactic.cpp | 2 +- src/tactic/ufbv/ufbv_rewriter.cpp | 14 ++++++-------- src/test/matcher.cpp | 2 +- src/util/bit_util.cpp | 14 +++++++++++++- src/util/debug.cpp | 4 ++-- src/util/debug.h | 11 +++++++++++ src/util/gparams.cpp | 4 ++-- src/util/hwf.h | 15 ++++++++++----- src/util/memory_manager.cpp | 16 ++++++++-------- src/util/warning.cpp | 10 +++++----- 46 files changed, 97 insertions(+), 122 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fefb400ed..0555e5fc8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -300,7 +300,7 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) { // // ----------------------------------- -char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" }; +static char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" }; char const * get_ast_kind_name(ast_kind k) { return g_ast_kind_names[k]; diff --git a/src/ast/ast.h b/src/ast/ast.h index 4c924691c..ef4ab3b55 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1193,7 +1193,6 @@ enum pattern_op_kind { heurisitic quantifier instantiation. */ class pattern_decl_plugin : public decl_plugin { - sort * m_list; public: virtual decl_plugin * mk_fresh() { return alloc(pattern_decl_plugin); } diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index d8e2385ec..4f0c9a75d 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -326,6 +326,7 @@ namespace datalog { } unsigned index0; sort* last_sort = 0; + SASSERT(num_params > 0); for (unsigned i = 0; i < num_params; ++i) { parameter const& p = params[i]; if (!p.is_int()) { diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 26131bc28..2a090fc39 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -200,6 +200,7 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par } else { m_manager->raise_exception("sort of floating point constant was not specified"); + UNREACHABLE(); } SASSERT(is_sort_of(s, m_family_id, FLOAT_SORT)); diff --git a/src/ast/func_decl_dependencies.cpp b/src/ast/func_decl_dependencies.cpp index 5e054d5d9..162efb0dd 100644 --- a/src/ast/func_decl_dependencies.cpp +++ b/src/ast/func_decl_dependencies.cpp @@ -79,7 +79,6 @@ void func_decl_dependencies::collect_ng_func_decls(expr * n, func_decl_set * s) */ class func_decl_dependencies::top_sort { enum color { OPEN, IN_PROGRESS, CLOSED }; - ast_manager & m_manager; dependency_graph & m_deps; typedef obj_map color_map; @@ -177,7 +176,7 @@ class func_decl_dependencies::top_sort { } public: - top_sort(ast_manager & m, dependency_graph & deps):m_manager(m), m_deps(deps) {} + top_sort(dependency_graph & deps) : m_deps(deps) {} bool operator()(func_decl * new_decl) { @@ -198,7 +197,7 @@ bool func_decl_dependencies::insert(func_decl * f, func_decl_set * s) { m_deps.insert(f, s); - top_sort cycle_detector(m_manager, m_deps); + top_sort cycle_detector(m_deps); if (cycle_detector(f)) { m_deps.erase(f); dealloc(s); diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 1b0f0b621..084a33ebf 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -22,10 +22,9 @@ Revision History: #include"uint_set.h" #include"var_subst.h" -quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s) : +quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s) : m_manager(m), m_macro_manager(mm), - m_bsimp(p), m_simplifier(s), m_new_vars(m), m_new_eqs(m), diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h index 1731774b2..c5e6b6d4f 100644 --- a/src/ast/macros/quasi_macros.h +++ b/src/ast/macros/quasi_macros.h @@ -32,7 +32,6 @@ class quasi_macros { ast_manager & m_manager; macro_manager & m_macro_manager; - basic_simplifier_plugin & m_bsimp; simplifier & m_simplifier; occurrences_map m_occurrences; ptr_vector m_todo; @@ -57,7 +56,7 @@ class quasi_macros { void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); public: - quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s); + quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s); ~quasi_macros(); /** diff --git a/src/ast/recurse_expr.h b/src/ast/recurse_expr.h index 9cb71872b..6b3220d40 100644 --- a/src/ast/recurse_expr.h +++ b/src/ast/recurse_expr.h @@ -30,7 +30,7 @@ class recurse_expr : public Visitor { vector m_results2; bool is_cached(expr * n) const { T c; return m_cache.find(n, c); } - T get_cached(expr * n) const { T c; m_cache.find(n, c); return c; } + T get_cached(expr * n) const { return m_cache.find(n); } void cache_result(expr * n, T c) { m_cache.insert(n, c); } void visit(expr * n, bool & visited); diff --git a/src/ast/substitution/matcher.cpp b/src/ast/substitution/matcher.cpp index a5560c6a2..ce9bdcb3e 100644 --- a/src/ast/substitution/matcher.cpp +++ b/src/ast/substitution/matcher.cpp @@ -18,10 +18,6 @@ Revision History: --*/ #include"matcher.h" -matcher::matcher(ast_manager & m): - m_manager(m) { -} - bool matcher::operator()(expr * e1, expr * e2, substitution & s) { reset(); m_subst = &s; diff --git a/src/ast/substitution/matcher.h b/src/ast/substitution/matcher.h index 1a71a51ed..84a62e874 100644 --- a/src/ast/substitution/matcher.h +++ b/src/ast/substitution/matcher.h @@ -30,7 +30,6 @@ class matcher { typedef pair_hash, obj_ptr_hash > expr_pair_hash; typedef hashtable > cache; - ast_manager & m_manager; substitution * m_subst; // cache m_cache; svector m_todo; @@ -38,7 +37,7 @@ class matcher { void reset(); public: - matcher(ast_manager & m); + matcher() {} /** \brief Return true if e2 is an instance of e1. diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 11bca0133..be293c5a8 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -148,7 +148,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e expr * arg = to_app(e)->get_arg(i); expr * new_arg; - m_apply_cache.find(expr_offset(arg, off), new_arg); + VERIFY(m_apply_cache.find(expr_offset(arg, off), new_arg)); new_args.push_back(new_arg); if (arg != new_arg) has_new_args = true; diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index 0bbabc683..ad0819ad8 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -85,7 +85,6 @@ namespace subpaving { }; class context_mpf_wrapper : public context_wrapper { - f2n & m_fm; unsynch_mpq_manager & m_qm; scoped_mpf m_c; scoped_mpf_vector m_as; @@ -103,7 +102,6 @@ namespace subpaving { public: context_mpf_wrapper(f2n & fm, params_ref const & p, small_object_allocator * a): context_wrapper(fm, p, a), - m_fm(fm), m_qm(fm.m().mpq_manager()), m_c(fm.m()), m_as(fm.m()), @@ -145,7 +143,6 @@ namespace subpaving { }; class context_hwf_wrapper : public context_wrapper { - f2n & m_fm; unsynch_mpq_manager & m_qm; hwf m_c; svector m_as; @@ -166,7 +163,6 @@ namespace subpaving { public: context_hwf_wrapper(f2n & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a): context_wrapper(fm, p, a), - m_fm(fm), m_qm(qm) { } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 73ddd22e5..df293aeba 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -647,7 +647,6 @@ namespace datalog { } } ast_manager& m = get_manager(); - datalog::rule_manager& rm = get_rule_manager(); contains_pred contains_p(*this); check_pred check_pred(contains_p, get_manager()); diff --git a/src/muz_qe/dl_interval_relation.cpp b/src/muz_qe/dl_interval_relation.cpp index 3397f2db0..4c8171bc7 100644 --- a/src/muz_qe/dl_interval_relation.cpp +++ b/src/muz_qe/dl_interval_relation.cpp @@ -99,11 +99,9 @@ namespace datalog { } class interval_relation_plugin::rename_fn : public convenient_relation_rename_fn { - interval_relation_plugin& m_plugin; public: - rename_fn(interval_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) - : convenient_relation_rename_fn(orig_sig, cycle_len, cycle), - m_plugin(p){ + rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) + : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) { } virtual relation_base * operator()(const relation_base & _r) { @@ -120,7 +118,7 @@ namespace datalog { if(!check_kind(r)) { return 0; } - return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle); + return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle); } interval interval_relation_plugin::unite(interval const& src1, interval const& src2) { @@ -194,11 +192,9 @@ namespace datalog { } class interval_relation_plugin::union_fn : public relation_union_fn { - interval_relation_plugin& m_plugin; bool m_is_widen; public: - union_fn(interval_relation_plugin& p, bool is_widen) : - m_plugin(p), + union_fn(bool is_widen) : m_is_widen(is_widen) { } @@ -223,7 +219,7 @@ namespace datalog { if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { return 0; } - return alloc(union_fn, *this, false); + return alloc(union_fn, false); } relation_union_fn * interval_relation_plugin::mk_widen_fn( @@ -232,7 +228,7 @@ namespace datalog { if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { return 0; } - return alloc(union_fn, *this, true); + return alloc(union_fn, true); } class interval_relation_plugin::filter_identical_fn : public relation_mutator_fn { diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 3f92bbce8..51a9d5927 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -141,7 +141,6 @@ namespace datalog { func_decl_ref_vector const& new_funcs() const { return m_new_funcs; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - rule_manager& rm = m_context.get_rule_manager(); bool found = false; for (unsigned j = 0; !found && j < num; ++j) { found = m_util.is_mkbv(args[j]); diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index bf3548a7a..004b1823d 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -527,11 +527,10 @@ namespace datalog { } class explanation_relation_plugin::intersection_filter_fn : public relation_intersection_filter_fn { - explanation_relation_plugin & m_plugin; func_decl_ref m_union_decl; public: intersection_filter_fn(explanation_relation_plugin & plugin) - : m_plugin(plugin), m_union_decl(plugin.m_union_decl) {} + : m_union_decl(plugin.m_union_decl) {} virtual void operator()(relation_base & tgt0, const relation_base & src0) { explanation_relation & tgt = static_cast(tgt0); diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index c8e350eeb..9109f1bda 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -938,11 +938,8 @@ namespace datalog { class karr_relation_plugin::union_fn : public relation_union_fn { - karr_relation_plugin& m_plugin; public: - union_fn(karr_relation_plugin& p) : - m_plugin(p) { - } + union_fn() {} virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) { @@ -966,7 +963,7 @@ namespace datalog { if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { return 0; } - return alloc(union_fn, *this); + return alloc(union_fn); } class karr_relation_plugin::filter_identical_fn : public relation_mutator_fn { diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index f50bd104c..0e94ba3b9 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -320,9 +320,7 @@ namespace datalog { if(!m_ground_unconditional_rule_heads.contains(pred)) { m_ground_unconditional_rule_heads.insert(pred, alloc(obj_hashtable)); } - obj_hashtable * head_store; - m_ground_unconditional_rule_heads.find(pred, head_store); - head_store->insert(head); + m_ground_unconditional_rule_heads.find(pred)->insert(head); next_rule:; } diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index d92ae7dcc..ef8e6ddd4 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -1090,12 +1090,10 @@ namespace datalog { class relation_manager::default_table_rename_fn : public convenient_table_rename_fn, auxiliary_table_transformer_fn { - const unsigned m_cycle_len; public: default_table_rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) - : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle), - m_cycle_len(permutation_cycle_len) { + : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) { SASSERT(permutation_cycle_len>=2); } diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index 8715e5cff..26008a830 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -661,17 +661,15 @@ namespace datalog { SASSERT(res_idxinsert(m_allocated_kinds[res_idx], spec); } return m_allocated_kinds[res_idx]; } void get_relation_spec(const relation_signature & sig, family_id kind, Spec & spec) { - family_id2spec * idspecs; - VERIFY( m_kind_specs.find(sig, idspecs) ); - VERIFY( idspecs->find(kind, spec) ); + family_id2spec * idspecs = m_kind_specs.find(sig); + spec = idspecs->find(kind); } }; diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index c3644cd74..974ab5862 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -198,8 +198,6 @@ namespace datalog { { bool values_match(const expr * v1, const expr * v2); - ast_manager & m_manager; - unsigned_vector m_args1; unsigned_vector m_args2; @@ -211,7 +209,7 @@ namespace datalog { static unsigned expr_cont_get_size(const ptr_vector & v) { return v.size(); } static expr * expr_cont_get(const ptr_vector & v, unsigned i) { return v[i]; } public: - variable_intersection(ast_manager & m) : m_manager(m), m_consts(m) {} + variable_intersection(ast_manager & m) : m_consts(m) {} unsigned size() const { return m_args1.size(); diff --git a/src/muz_qe/nlarith_util.cpp b/src/muz_qe/nlarith_util.cpp index 5f8a24e99..c555b71f1 100644 --- a/src/muz_qe/nlarith_util.cpp +++ b/src/muz_qe/nlarith_util.cpp @@ -1028,7 +1028,6 @@ namespace nlarith { }; class sqrt_subst : public isubst { - bool m_even; sqrt_form const& m_s; public: sqrt_subst(imp& i, sqrt_form const& s): isubst(i), m_s(s) {} diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index d4027d73d..a240a9aef 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1285,7 +1285,7 @@ namespace pdr { obj_hashtable::iterator itf = deps.begin(), endf = deps.end(); for (; itf != endf; ++itf) { TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";); - VERIFY (rels.find(*itf, pt_user)); + pt_user = rels.find(*itf); pt_user->add_use(pt); } } diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 489b2437e..393090299 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -418,11 +418,10 @@ namespace pdr { class farkas_learner::constant_replacer_cfg : public default_rewriter_cfg { - ast_manager& m; const obj_map& m_translation; public: - constant_replacer_cfg(ast_manager& m, const obj_map& translation) - : m(m), m_translation(translation) + constant_replacer_cfg(const obj_map& translation) + : m_translation(translation) { } bool get_subst(expr * s, expr * & t, proof * & t_pr) { diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index bb65f8bf8..894a935b5 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -1093,8 +1093,7 @@ namespace qe { bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); } search_tree* child(rational const& branch_id) const { - unsigned idx; - VERIFY(m_branch_index.find(branch_id, idx)); + unsigned idx = m_branch_index.find(branch_id); return m_children[idx]; } @@ -1963,7 +1962,6 @@ namespace qe { expr_ref m_assumption; bool m_produce_models; ptr_vector m_plugins; - unsigned m_name_counter; // fresh-id volatile bool m_cancel; bool m_eliminate_variables_as_block; @@ -1973,7 +1971,6 @@ namespace qe { m_fparams(p), m_assumption(m), m_produce_models(m_fparams.m_model), - m_name_counter(0), m_cancel(false), m_eliminate_variables_as_block(true) { diff --git a/src/muz_qe/qe_dl_plugin.cpp b/src/muz_qe/qe_dl_plugin.cpp index 15e972e88..61466795b 100644 --- a/src/muz_qe/qe_dl_plugin.cpp +++ b/src/muz_qe/qe_dl_plugin.cpp @@ -12,14 +12,12 @@ namespace qe { // dl_plugin class eq_atoms { - ast_manager& m; expr_ref_vector m_eqs; expr_ref_vector m_neqs; app_ref_vector m_eq_atoms; app_ref_vector m_neq_atoms; public: eq_atoms(ast_manager& m): - m(m), m_eqs(m), m_neqs(m), m_eq_atoms(m), diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 44d9d94e2..653f5f188 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -740,7 +740,6 @@ namespace tb { typedef svector double_vector; typedef obj_map score_map; typedef obj_map pred_map; - datalog::context& m_ctx; ast_manager& m; datatype_util dt; score_map m_score_map; @@ -750,19 +749,16 @@ namespace tb { pred_map m_pred_map; expr_ref_vector m_refs; double m_weight_multiply; - unsigned m_num_invocations; unsigned m_update_frequency; unsigned m_next_update; public: selection(datalog::context& ctx): - m_ctx(ctx), m(ctx.get_manager()), dt(m), m_refs(m), m_weight_multiply(1.0), - m_num_invocations(0), m_update_frequency(20), m_next_update(20) { set_strategy(ctx.get_params().tab_selection()); diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp index b6b40c01a..d26190541 100644 --- a/src/parsers/smt/smtparser.cpp +++ b/src/parsers/smt/smtparser.cpp @@ -1472,7 +1472,7 @@ private: SASSERT(sorts.size() > 0); - idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope, current); + idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope); expr_ref_vector * empty_v = alloc(expr_ref_vector, m_manager); up.push_back(new (region) parse_frame(current, pop_q, empty_v, 0, m_binding_level)); @@ -2522,7 +2522,7 @@ private: class pop_quantifier : public idbuilder { public: pop_quantifier(smtparser * smt, bool is_forall, int weight, symbol const& qid, symbol const& skid, expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, sort_ref_buffer & sorts, - svector& vars, symbol_table & local_scope, proto_expr* p_expr): + svector& vars, symbol_table & local_scope): m_smt(smt), m_is_forall(is_forall), m_weight(weight), @@ -2531,8 +2531,7 @@ private: m_patterns(m_smt->m_manager), m_no_patterns(m_smt->m_manager), m_sorts(m_smt->m_manager), - m_local_scope(local_scope), - m_p_expr(p_expr) { + m_local_scope(local_scope) { SASSERT(sorts.size() == vars.size()); m_vars.append(vars); @@ -2619,7 +2618,6 @@ private: sort_ref_buffer m_sorts; svector m_vars; symbol_table& m_local_scope; - proto_expr* m_p_expr; }; class builtin_builder : public idbuilder { diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 0f6101a93..f653cbb25 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -243,7 +243,6 @@ namespace smt2 { } scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive): - m_ctx(ctx), m_interactive(interactive), m_spos(0), m_curr(0), // avoid Valgrind warning diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h index 7b74c752f..631c71f17 100644 --- a/src/parsers/smt2/smt2scanner.h +++ b/src/parsers/smt2/smt2scanner.h @@ -31,7 +31,6 @@ namespace smt2 { class scanner { private: - cmd_context & m_ctx; bool m_interactive; int m_spos; // position in the current line of the stream char m_curr; // current char; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index c5d3c08cf..4775e44a4 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -408,7 +408,7 @@ void asserted_formulas::apply_quasi_macros() { TRACE("before_quasi_macros", display(tout);); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); - quasi_macros proc(m_manager, m_macro_manager, *m_bsimp, m_simplifier); + quasi_macros proc(m_manager, m_macro_manager, m_simplifier); while (proc(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, diff --git a/src/smt/database.h b/src/smt/database.h index 2e71cbae4..1975fe3c3 100644 --- a/src/smt/database.h +++ b/src/smt/database.h @@ -1,4 +1,4 @@ -char const * g_pattern_database = +static char const * g_pattern_database = "(benchmark patterns \n" " :status unknown \n" " :logic ALL \n" diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index b23bb3bdc..66252c3cf 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -311,7 +311,7 @@ bool expr_context_simplifier::is_false(expr* e) const { // expr_strong_context_simplifier::expr_strong_context_simplifier(smt_params& p, ast_manager& m): - m_manager(m), m_params(p), m_arith(m), m_id(0), m_fn(0,m), m_solver(m, p) { + m_manager(m), m_arith(m), m_fn(0,m), m_solver(m, p) { sort* i_sort = m_arith.mk_int(); m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort()); } diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h index 982b65878..a1d01b78c 100644 --- a/src/smt/expr_context_simplifier.h +++ b/src/smt/expr_context_simplifier.h @@ -57,9 +57,7 @@ private: class expr_strong_context_simplifier { ast_manager& m_manager; - smt_params & m_params; arith_util m_arith; - unsigned m_id; func_decl_ref m_fn; smt::kernel m_solver; diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index c9d6ead88..d92eef5b8 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1849,11 +1849,9 @@ namespace smt { unsigned m_curr_max_generation; // temporary var used to store a copy of m_max_generation unsigned m_num_args; unsigned m_oreg; - unsigned m_ireg; enode * m_n1; enode * m_n2; enode * m_app; - instruction * m_alt; const bind * m_b; ptr_vector m_used_enodes; unsigned m_curr_used_enodes_size; diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 758f78c2c..9c3489aec 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -68,14 +68,11 @@ namespace smt { bv_util& b() { return m_bv; } class dl_value_proc : public smt::model_value_proc { - smt::model_generator & m_mg; theory_dl& m_th; smt::enode* m_node; public: - dl_value_proc(smt::model_generator & m, theory_dl& th, smt::enode* n): - m_mg(m), m_th(th), m_node(n) - { } + dl_value_proc(theory_dl& th, smt::enode* n) : m_th(th), m_node(n) {} virtual void get_dependencies(buffer & result) {} @@ -165,8 +162,8 @@ namespace smt { m.register_factory(alloc(dl_factory, m_util, m.get_model())); } - virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator & m) { - return alloc(dl_value_proc, m, *this, n); + virtual smt::model_value_proc * mk_value(smt::enode * n) { + return alloc(dl_value_proc, *this, n); } virtual void apply_sort_cnstr(enode * n, sort * s) { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index d7e55379a..393a40603 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -67,7 +67,7 @@ class quasi_macros_tactic : public tactic { simp.register_plugin(bvsimp); macro_manager mm(m_manager, simp); - quasi_macros qm(m_manager, mm, *bsimp, simp); + quasi_macros qm(m_manager, mm, simp); bool more = true; expr_ref_vector forms(m_manager), new_forms(m_manager); diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp index e4ed2ec01..40fdf5e3e 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/tactic/ufbv/ufbv_rewriter.cpp @@ -442,11 +442,10 @@ expr * ufbv_rewriter::rewrite(expr * n) { } class ufbv_rewriter::add_back_idx_proc { - ast_manager & m_manager; back_idx_map & m_back_idx; expr * m_expr; public: - add_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {} + add_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {} void operator()(var * n) {} void operator()(quantifier * n) {} void operator()(app * n) { @@ -469,11 +468,10 @@ public: }; class ufbv_rewriter::remove_back_idx_proc { - ast_manager & m_manager; back_idx_map & m_back_idx; expr * m_expr; public: - remove_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {} + remove_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {} void operator()(var * n) {} void operator()(quantifier * n) {} void operator()(app * n) { @@ -511,7 +509,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) { expr * p = *sit; // remove p from m_processed and m_back_idx m_processed.remove(p); - remove_back_idx_proc proc(m_manager, m_back_idx, p); // this could change it->m_value, thus we need the `temp' set. + remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set. for_each_expr(proc, p); // insert p into m_todo m_todo.push_back(p); @@ -619,7 +617,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { // remove d from m_back_idx // just remember it here, because otherwise it and/or esit might become invalid? // to_remove.insert(d); - remove_back_idx_proc proc(m_manager, m_back_idx, d); + remove_back_idx_proc proc(m_back_idx, d); for_each_expr(proc, d); // insert d into m_todo m_todo.push_back(d); @@ -674,7 +672,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * // insert n' into m_processed m_processed.insert(np); // update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx) - add_back_idx_proc proc(m_manager, m_back_idx, np); + add_back_idx_proc proc(m_back_idx, np); for_each_expr(proc, np); } else { // np is a demodulator that allows us to replace 'large' with 'small'. @@ -702,7 +700,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * insert_fwd_idx(large, small, to_quantifier(np)); // update m_back_idx - add_back_idx_proc proc(m_manager, m_back_idx, np); + add_back_idx_proc proc(m_back_idx, np); for_each_expr(proc, np); } } diff --git a/src/test/matcher.cpp b/src/test/matcher.cpp index 05d971e24..598a82ae3 100644 --- a/src/test/matcher.cpp +++ b/src/test/matcher.cpp @@ -26,7 +26,7 @@ void tst_match(ast_manager & m, app * t, app * i) { substitution s(m); s.reserve(2, 10); // reserving a big number of variables to be safe. - matcher match(m); + matcher match; std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n"; if (match(t, i, s)) { std::cout << "yes\n"; diff --git a/src/util/bit_util.cpp b/src/util/bit_util.cpp index 32861f754..0f1fd294d 100644 --- a/src/util/bit_util.cpp +++ b/src/util/bit_util.cpp @@ -19,6 +19,7 @@ Revision History: #include"bit_util.h" #include"util.h" #include"debug.h" +#include /** \brief (Debugging version) Return the position of the most significant (set) bit of a @@ -67,7 +68,11 @@ unsigned msb_pos(unsigned v) { */ unsigned nlz_core(unsigned x) { SASSERT(x != 0); +#ifdef __GNUC__ + return __builtin_clz(x); +#else return 31 - msb_pos(x); +#endif } /** @@ -92,8 +97,15 @@ unsigned nlz(unsigned sz, unsigned const * data) { */ unsigned ntz_core(unsigned x) { SASSERT(x != 0); +#ifdef __GNUC__ + return __builtin_ctz(x); +#else float f = static_cast(x & static_cast(-static_cast(x))); - return (*reinterpret_cast(&f) >> 23) - 0x7f; + unsigned u; + SASSERT(sizeof(u) == sizeof(f)); + memcpy(&u, &f, sizeof(u)); + return (u >> 23) - 0x7f; +#endif } /** diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 75ea8586a..c336ddb73 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -24,7 +24,7 @@ Revision History: #include"str_hashtable.h" #include"z3_exception.h" -volatile bool g_enable_assertions = true; +static volatile bool g_enable_assertions = true; void enable_assertions(bool f) { g_enable_assertions = f; @@ -41,7 +41,7 @@ void notify_assertion_violation(const char * fileName, int line, const char * co std::cerr << condition << "\n"; } -str_hashtable* g_enabled_debug_tags = 0; +static str_hashtable* g_enabled_debug_tags = 0; static void init_debug_table() { if (!g_enabled_debug_tags) { diff --git a/src/util/debug.h b/src/util/debug.h index c45ee5aa6..9e519982f 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -29,6 +29,10 @@ bool assertions_enabled(); #include #endif +#ifndef __has_builtin +# define __has_builtin(x) 0 +#endif + #include"error_codes.h" #include"warning.h" @@ -53,7 +57,14 @@ bool is_debug_enabled(const char * tag); #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); }) + +#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable) +// only available in gcc >= 4.5 and in newer versions of clang +# define UNREACHABLE() __builtin_unreachable() +#else #define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();) +#endif + #define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) #ifdef Z3DEBUG diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 3b2e8edc1..1d9426390 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -22,7 +22,7 @@ Notes: extern void gparams_register_modules(); -char const * g_old_params_names[] = { +static char const * g_old_params_names[] = { "arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", 0 }; bool is_old_param_name(symbol const & name) { @@ -35,7 +35,7 @@ bool is_old_param_name(symbol const & name) { return false; } -char const * g_params_renames[] = { +static char const * g_params_renames[] = { "proof_mode", "proof", "soft_timeout", "timeout", "mbqi", "smt.mbqi", diff --git a/src/util/hwf.h b/src/util/hwf.h index 3b7a0e94b..9059869a0 100644 --- a/src/util/hwf.h +++ b/src/util/hwf.h @@ -28,6 +28,12 @@ class hwf { friend class hwf_manager; double value; hwf & operator=(hwf const & other) { UNREACHABLE(); return *this; } + uint64 get_raw() const { + uint64 n; + SASSERT(sizeof(n) == sizeof(value)); + memcpy(&n, &value, sizeof(value)); + return n; + } public: hwf() {} @@ -122,16 +128,15 @@ public: bool sgn(hwf const & x) const { - uint64 raw = *reinterpret_cast(&x.value); - return (raw & 0x8000000000000000ull) != 0; + return (x.get_raw() & 0x8000000000000000ull) != 0; } const uint64 sig(hwf const & x) const { - return *reinterpret_cast(&x.value) & 0x000FFFFFFFFFFFFFull; + return x.get_raw() & 0x000FFFFFFFFFFFFFull; } const int exp(hwf const & x) const { - return ((*reinterpret_cast(&x.value) & 0x7FF0000000000000ull) >> 52) - 1023; + return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023; } bool is_nan(hwf const & x); @@ -151,7 +156,7 @@ public: void mk_pinf(hwf & o); void mk_ninf(hwf & o); - unsigned hash(hwf const & a) { return hash_ull(*reinterpret_cast(&a.value)); } + unsigned hash(hwf const & a) { return hash_ull(a.get_raw()); } inline void set_rounding_mode(mpf_rounding_mode rm); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index de4e760d7..f5e5fa9fa 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -27,14 +27,14 @@ void mem_finalize(); out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) { } -volatile bool g_memory_out_of_memory = false; -bool g_memory_initialized = false; -long long g_memory_alloc_size = 0; -long long g_memory_max_size = 0; -long long g_memory_max_used_size = 0; -long long g_memory_watermark = 0; -bool g_exit_when_out_of_memory = false; -char const * g_out_of_memory_msg = "ERROR: out of memory"; +static volatile bool g_memory_out_of_memory = false; +static bool g_memory_initialized = false; +static long long g_memory_alloc_size = 0; +static long long g_memory_max_size = 0; +static long long g_memory_max_used_size = 0; +static long long g_memory_watermark = 0; +static bool g_exit_when_out_of_memory = false; +static char const * g_out_of_memory_msg = "ERROR: out of memory"; void memory::exit_when_out_of_memory(bool flag, char const * msg) { g_exit_when_out_of_memory = flag; diff --git a/src/util/warning.cpp b/src/util/warning.cpp index 0a1ac9bbc..88f807e3c 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -60,11 +60,11 @@ void myInvalidParameterHandler( #define END_ERR_HANDLER() {} #endif -bool g_warning_msgs = true; -bool g_use_std_stdout = false; -std::ostream* g_error_stream = 0; -std::ostream* g_warning_stream = 0; -bool g_show_error_msg_prefix = true; +static bool g_warning_msgs = true; +static bool g_use_std_stdout = false; +static std::ostream* g_error_stream = 0; +static std::ostream* g_warning_stream = 0; +static bool g_show_error_msg_prefix = true; void send_warnings_to_stdout(bool flag) { g_use_std_stdout = flag;