From 6ac3075022f217cb2f0bebd42c56d86c3ccd4300 Mon Sep 17 00:00:00 2001 From: davedets Date: Thu, 2 Jul 2026 12:47:29 -0700 Subject: [PATCH] Remove unnecessary semicolons (Attempt 2) (#10020) This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. This is a second version of https://github.com/Z3Prover/z3/pull/9957. I address @NikolajBjorner 's comments about not changing the semicolons after macro invocations, because some editors work better with them present. It now, to the best of my ability, only deletes semis: * after the closing brace of namespace decl. * after the closing brace of an extern "C" decl. * after a function definition. This PR is very large, but it consists entirely of deletions of semicolons in these situations. (If there was a way to update the previous PR, which had been closed, and that is preferable, please let me know. I couldn't figure it out.) --- cmake/compiler_warnings.cmake | 3 ++- src/api/api_algebraic.cpp | 2 +- src/api/api_arith.cpp | 2 +- src/api/api_array.cpp | 2 +- src/api/api_ast.cpp | 2 +- src/api/api_ast_map.cpp | 2 +- src/api/api_ast_vector.cpp | 2 +- src/api/api_ast_vector.h | 2 +- src/api/api_bv.cpp | 2 +- src/api/api_config_params.cpp | 2 +- src/api/api_context.cpp | 4 ++-- src/api/api_context.h | 8 ++++---- src/api/api_datalog.cpp | 4 ++-- src/api/api_datalog.h | 2 +- src/api/api_datatype.cpp | 2 +- src/api/api_finite_set.cpp | 2 +- src/api/api_fpa.cpp | 2 +- src/api/api_goal.cpp | 2 +- src/api/api_model.cpp | 2 +- src/api/api_numeral.cpp | 2 +- src/api/api_opt.cpp | 2 +- src/api/api_params.cpp | 2 +- src/api/api_pb.cpp | 2 +- src/api/api_polynomial.cpp | 2 +- src/api/api_quant.cpp | 2 +- src/api/api_rcf.cpp | 2 +- src/api/api_seq.cpp | 2 +- src/api/api_solver.cpp | 2 +- src/api/api_special_relations.cpp | 2 +- src/api/api_stats.cpp | 2 +- src/api/api_tactic.cpp | 2 +- src/api/api_util.h | 2 +- src/ast/arith_decl_plugin.h | 2 +- src/ast/datatype_decl_plugin.h | 4 ++-- src/ast/dl_decl_plugin.cpp | 4 ++-- src/ast/dl_decl_plugin.h | 2 +- src/ast/euf/euf_ac_plugin.h | 4 ++-- src/ast/euf/euf_etable.cpp | 2 +- src/ast/euf/euf_etable.h | 2 +- src/ast/euf/euf_mam.h | 2 +- src/ast/euf/euf_plugin.h | 2 +- src/ast/for_each_expr.cpp | 2 +- src/ast/format.cpp | 2 +- src/ast/format.h | 2 +- src/ast/fpa/fpa2bv_converter.h | 8 ++++---- src/ast/macros/macro_manager.cpp | 2 +- src/ast/macros/quasi_macros.cpp | 2 +- src/ast/polymorphism_inst.h | 2 +- src/ast/quantifier_stat.cpp | 2 +- src/ast/quantifier_stat.h | 2 +- src/ast/recfun_decl_plugin.h | 4 ++-- src/ast/rewriter/bv_bounds.h | 2 +- src/ast/rewriter/seq_axioms.h | 2 +- src/ast/rewriter/seq_eq_solver.cpp | 2 +- src/ast/rewriter/seq_eq_solver.h | 2 +- src/ast/rewriter/seq_skolem.h | 2 +- src/ast/simplifiers/distribute_forall.cpp | 2 +- src/ast/simplifiers/propagate_values.cpp | 2 +- src/ast/sls/sls_array_plugin.h | 6 +++--- src/ast/sls/sls_bv_lookahead.cpp | 4 ++-- src/ast/sls/sls_bv_tracker.h | 2 +- src/ast/sls/sls_context.h | 6 +++--- src/ast/sls/sls_euf_plugin.h | 4 ++-- src/cmd_context/extra_cmds/dbg_cmds.cpp | 6 +++--- src/math/grobner/pdd_simplifier.cpp | 2 +- src/math/lp/lp_primal_core_solver.h | 2 +- src/math/lp/nla_types.h | 6 +++--- src/math/polynomial/algebraic_numbers.cpp | 2 +- src/math/polynomial/algebraic_numbers.h | 2 +- src/math/polynomial/polynomial.cpp | 2 +- src/math/polynomial/polynomial.h | 4 ++-- src/math/polynomial/polynomial_cache.cpp | 2 +- src/math/polynomial/polynomial_cache.h | 2 +- src/math/polynomial/polynomial_primes.h | 2 +- src/math/polynomial/polynomial_var2value.h | 2 +- src/math/polynomial/rpolynomial.cpp | 2 +- src/math/polynomial/rpolynomial.h | 2 +- src/math/polynomial/upolynomial.cpp | 2 +- src/math/polynomial/upolynomial.h | 2 +- src/math/polynomial/upolynomial_factorization.cpp | 2 +- src/math/polynomial/upolynomial_factorization.h | 2 +- src/math/polynomial/upolynomial_factorization_int.h | 2 +- src/math/realclosure/realclosure.cpp | 2 +- src/math/realclosure/realclosure.h | 2 +- src/math/simplex/simplex.cpp | 2 +- src/math/simplex/simplex.h | 2 +- src/math/simplex/simplex_def.h | 2 +- src/math/simplex/sparse_matrix.h | 2 +- src/math/simplex/sparse_matrix_def.h | 2 +- src/math/subpaving/subpaving.cpp | 2 +- src/math/subpaving/subpaving.h | 2 +- src/math/subpaving/subpaving_hwf.h | 2 +- src/math/subpaving/subpaving_mpf.h | 2 +- src/math/subpaving/subpaving_mpff.h | 2 +- src/math/subpaving/subpaving_mpfx.h | 2 +- src/math/subpaving/subpaving_mpq.h | 2 +- src/math/subpaving/subpaving_t.h | 2 +- src/math/subpaving/subpaving_t_def.h | 2 +- src/muz/base/dl_context.cpp | 2 +- src/muz/base/dl_context.h | 2 +- src/muz/base/dl_costs.cpp | 2 +- src/muz/base/dl_costs.h | 2 +- src/muz/base/dl_rule.cpp | 2 +- src/muz/base/dl_rule.h | 4 ++-- src/muz/base/dl_rule_set.cpp | 2 +- src/muz/base/dl_rule_set.h | 2 +- src/muz/base/dl_rule_subsumption_index.cpp | 2 +- src/muz/base/dl_rule_subsumption_index.h | 2 +- src/muz/base/dl_rule_transformer.cpp | 2 +- src/muz/base/dl_rule_transformer.h | 2 +- src/muz/base/dl_util.cpp | 2 +- src/muz/base/dl_util.h | 2 +- src/muz/bmc/dl_bmc_engine.cpp | 2 +- src/muz/bmc/dl_bmc_engine.h | 2 +- src/muz/clp/clp_context.cpp | 2 +- src/muz/clp/clp_context.h | 2 +- src/muz/ddnf/ddnf.cpp | 2 +- src/muz/ddnf/ddnf.h | 2 +- src/muz/fp/datalog_parser.h | 2 +- src/muz/rel/check_relation.h | 2 +- src/muz/rel/dl_base.h | 6 +++--- src/muz/rel/dl_bound_relation.cpp | 2 +- src/muz/rel/dl_bound_relation.h | 2 +- src/muz/rel/dl_check_table.cpp | 2 +- src/muz/rel/dl_check_table.h | 2 +- src/muz/rel/dl_compiler.h | 2 +- src/muz/rel/dl_external_relation.cpp | 2 +- src/muz/rel/dl_external_relation.h | 2 +- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_finite_product_relation.h | 2 +- src/muz/rel/dl_instruction.h | 2 +- src/muz/rel/dl_interval_relation.cpp | 2 +- src/muz/rel/dl_interval_relation.h | 2 +- src/muz/rel/dl_mk_explanations.cpp | 2 +- src/muz/rel/dl_mk_explanations.h | 2 +- src/muz/rel/dl_mk_similarity_compressor.cpp | 2 +- src/muz/rel/dl_mk_similarity_compressor.h | 2 +- src/muz/rel/dl_mk_simple_joins.cpp | 2 +- src/muz/rel/dl_mk_simple_joins.h | 2 +- src/muz/rel/dl_product_relation.cpp | 2 +- src/muz/rel/dl_product_relation.h | 2 +- src/muz/rel/dl_relation_manager.cpp | 2 +- src/muz/rel/dl_relation_manager.h | 2 +- src/muz/rel/dl_sieve_relation.cpp | 2 +- src/muz/rel/dl_sieve_relation.h | 2 +- src/muz/rel/dl_sparse_table.cpp | 2 +- src/muz/rel/dl_sparse_table.h | 2 +- src/muz/rel/dl_table.cpp | 2 +- src/muz/rel/dl_table.h | 2 +- src/muz/rel/dl_table_relation.cpp | 2 +- src/muz/rel/dl_table_relation.h | 2 +- src/muz/rel/dl_vector_relation.h | 2 +- src/muz/rel/karr_relation.cpp | 2 +- src/muz/rel/karr_relation.h | 2 +- src/muz/rel/rel_context.cpp | 2 +- src/muz/rel/rel_context.h | 2 +- src/muz/rel/udoc_relation.h | 2 +- src/muz/spacer/spacer_concretize.cpp | 2 +- src/muz/spacer/spacer_context.h | 2 +- src/muz/spacer/spacer_convex_closure.h | 2 +- src/muz/spacer/spacer_farkas_learner.cpp | 2 +- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_mbc.cpp | 2 +- src/muz/spacer/spacer_proof_utils.cpp | 2 +- src/muz/spacer/spacer_qe_project.h | 2 +- src/muz/spacer/spacer_sym_mux.h | 2 +- src/muz/spacer/spacer_unsat_core_learner.h | 2 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 2 +- src/muz/spacer/spacer_unsat_core_plugin.h | 8 ++++---- src/muz/tab/tab_context.cpp | 4 ++-- src/muz/tab/tab_context.h | 2 +- src/muz/transforms/dl_mk_array_blast.cpp | 2 +- src/muz/transforms/dl_mk_array_blast.h | 2 +- src/muz/transforms/dl_mk_array_eq_rewrite.h | 2 +- src/muz/transforms/dl_mk_array_instantiation.h | 2 +- src/muz/transforms/dl_mk_backwards.cpp | 2 +- src/muz/transforms/dl_mk_backwards.h | 2 +- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- src/muz/transforms/dl_mk_bit_blast.h | 2 +- src/muz/transforms/dl_mk_coalesce.cpp | 2 +- src/muz/transforms/dl_mk_coalesce.h | 2 +- src/muz/transforms/dl_mk_filter_rules.cpp | 2 +- src/muz/transforms/dl_mk_filter_rules.h | 2 +- src/muz/transforms/dl_mk_interp_tail_simplifier.cpp | 2 +- src/muz/transforms/dl_mk_interp_tail_simplifier.h | 2 +- src/muz/transforms/dl_mk_karr_invariants.cpp | 2 +- src/muz/transforms/dl_mk_karr_invariants.h | 2 +- src/muz/transforms/dl_mk_loop_counter.cpp | 2 +- src/muz/transforms/dl_mk_loop_counter.h | 2 +- src/muz/transforms/dl_mk_magic_sets.cpp | 2 +- src/muz/transforms/dl_mk_magic_sets.h | 2 +- src/muz/transforms/dl_mk_magic_symbolic.cpp | 2 +- src/muz/transforms/dl_mk_magic_symbolic.h | 2 +- src/muz/transforms/dl_mk_quantifier_abstraction.cpp | 2 +- src/muz/transforms/dl_mk_quantifier_abstraction.h | 2 +- src/muz/transforms/dl_mk_quantifier_instantiation.cpp | 2 +- src/muz/transforms/dl_mk_quantifier_instantiation.h | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 2 +- src/muz/transforms/dl_mk_rule_inliner.h | 2 +- src/muz/transforms/dl_mk_scale.cpp | 2 +- src/muz/transforms/dl_mk_scale.h | 2 +- src/muz/transforms/dl_mk_slice.cpp | 2 +- src/muz/transforms/dl_mk_slice.h | 2 +- src/muz/transforms/dl_mk_subsumption_checker.cpp | 2 +- src/muz/transforms/dl_mk_subsumption_checker.h | 2 +- src/muz/transforms/dl_mk_synchronize.cpp | 2 +- src/muz/transforms/dl_mk_synchronize.h | 2 +- src/muz/transforms/dl_mk_unbound_compressor.cpp | 2 +- src/muz/transforms/dl_mk_unbound_compressor.h | 2 +- src/muz/transforms/dl_mk_unfold.cpp | 2 +- src/muz/transforms/dl_mk_unfold.h | 2 +- src/nlsat/nlsat_assignment.h | 2 +- src/nlsat/nlsat_clause.cpp | 2 +- src/nlsat/nlsat_clause.h | 2 +- src/nlsat/nlsat_evaluator.cpp | 2 +- src/nlsat/nlsat_evaluator.h | 2 +- src/nlsat/nlsat_explain.cpp | 2 +- src/nlsat/nlsat_explain.h | 2 +- src/nlsat/nlsat_interval_set.cpp | 2 +- src/nlsat/nlsat_interval_set.h | 2 +- src/nlsat/nlsat_justification.h | 2 +- src/nlsat/nlsat_scoped_literal_vector.h | 2 +- src/nlsat/nlsat_simplify.cpp | 2 +- src/nlsat/nlsat_solver.cpp | 2 +- src/nlsat/nlsat_solver.h | 2 +- src/nlsat/nlsat_types.cpp | 2 +- src/nlsat/nlsat_types.h | 4 ++-- src/opt/maxcore.h | 2 +- src/opt/maxlex.h | 2 +- src/opt/maxsmt.cpp | 6 +++--- src/opt/maxsmt.h | 2 +- src/opt/opt_cores.cpp | 2 +- src/opt/opt_cores.h | 2 +- src/opt/opt_lns.cpp | 2 +- src/opt/opt_lns.h | 2 +- src/opt/opt_preprocess.cpp | 2 +- src/opt/opt_preprocess.h | 2 +- src/opt/optsmt.h | 2 +- src/opt/pb_sls.h | 2 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/parsers/smt2/smt2scanner.cpp | 2 +- src/parsers/smt2/smt2scanner.h | 2 +- src/qe/mbp/mbp_arith.h | 2 +- src/qe/mbp/mbp_arrays.cpp | 2 +- src/qe/mbp/mbp_arrays.h | 2 +- src/qe/mbp/mbp_datatypes.h | 2 +- src/qe/mbp/mbp_euf.h | 2 +- src/qe/mbp/mbp_plugin.h | 2 +- src/qe/mbp/mbp_tg_plugins.h | 8 ++++---- src/qe/nlarith_util.cpp | 2 +- src/qe/nlarith_util.h | 2 +- src/qe/nlqsat.cpp | 2 +- src/qe/qe.h | 2 +- src/qe/qe_mbi.cpp | 2 +- src/qe/qe_mbi.h | 2 +- src/qe/qsat.cpp | 2 +- src/sat/dimacs.h | 4 ++-- src/sat/sat_anf_simplifier.h | 2 +- src/sat/sat_asymm_branch.cpp | 2 +- src/sat/sat_asymm_branch.h | 2 +- src/sat/sat_bcd.cpp | 2 +- src/sat/sat_bcd.h | 2 +- src/sat/sat_big.cpp | 2 +- src/sat/sat_big.h | 2 +- src/sat/sat_clause.cpp | 2 +- src/sat/sat_clause.h | 2 +- src/sat/sat_clause_set.cpp | 2 +- src/sat/sat_clause_set.h | 2 +- src/sat/sat_clause_use_list.cpp | 2 +- src/sat/sat_clause_use_list.h | 2 +- src/sat/sat_cleaner.cpp | 2 +- src/sat/sat_cleaner.h | 2 +- src/sat/sat_config.cpp | 2 +- src/sat/sat_config.h | 2 +- src/sat/sat_elim_eqs.cpp | 2 +- src/sat/sat_elim_eqs.h | 2 +- src/sat/sat_extension.h | 4 ++-- src/sat/sat_integrity_checker.cpp | 2 +- src/sat/sat_integrity_checker.h | 2 +- src/sat/sat_justification.h | 2 +- src/sat/sat_lookahead.h | 2 +- src/sat/sat_model_converter.cpp | 2 +- src/sat/sat_model_converter.h | 2 +- src/sat/sat_mus.h | 2 +- src/sat/sat_parallel.cpp | 2 +- src/sat/sat_parallel.h | 2 +- src/sat/sat_probing.cpp | 2 +- src/sat/sat_probing.h | 2 +- src/sat/sat_scc.cpp | 2 +- src/sat/sat_scc.h | 2 +- src/sat/sat_simplifier.cpp | 2 +- src/sat/sat_simplifier.h | 2 +- src/sat/sat_solver.cpp | 2 +- src/sat/sat_solver.h | 4 ++-- src/sat/sat_solver_core.h | 4 ++-- src/sat/sat_types.h | 4 ++-- src/sat/sat_watched.cpp | 2 +- src/sat/sat_watched.h | 2 +- src/sat/smt/arith_value.cpp | 2 +- src/sat/smt/arith_value.h | 2 +- src/sat/smt/bv_ackerman.h | 2 +- src/sat/smt/bv_delay_internalize.cpp | 4 ++-- src/sat/smt/bv_solver.cpp | 2 +- src/sat/smt/euf_ackerman.h | 2 +- src/sat/smt/euf_solver.h | 2 +- src/sat/smt/fpa_solver.cpp | 2 +- src/sat/smt/intblast_solver.cpp | 2 +- src/sat/smt/pb_constraint.h | 2 +- src/sat/smt/pb_solver.cpp | 2 +- src/sat/smt/pb_solver.h | 2 +- src/sat/smt/q_queue.h | 2 +- src/sat/smt/user_solver.h | 2 +- src/smt/arith_eq_adapter.cpp | 2 +- src/smt/arith_eq_adapter.h | 2 +- src/smt/dyn_ack.cpp | 2 +- src/smt/dyn_ack.h | 2 +- src/smt/fingerprints.cpp | 2 +- src/smt/fingerprints.h | 2 +- src/smt/mam.h | 2 +- src/smt/qi_queue.cpp | 2 +- src/smt/qi_queue.h | 2 +- src/smt/seq_axioms.h | 2 +- src/smt/seq_offset_eq.h | 2 +- src/smt/seq_regex.h | 2 +- src/smt/smt_almost_cg_table.cpp | 2 +- src/smt/smt_almost_cg_table.h | 2 +- src/smt/smt_arith_value.cpp | 2 +- src/smt/smt_arith_value.h | 2 +- src/smt/smt_b_justification.h | 2 +- src/smt/smt_bool_var_data.h | 2 +- src/smt/smt_case_split_queue.h | 2 +- src/smt/smt_cg_table.cpp | 2 +- src/smt/smt_cg_table.h | 2 +- src/smt/smt_checker.cpp | 2 +- src/smt/smt_checker.h | 2 +- src/smt/smt_clause.cpp | 2 +- src/smt/smt_clause.h | 2 +- src/smt/smt_clause_proof.cpp | 2 +- src/smt/smt_clause_proof.h | 2 +- src/smt/smt_conflict_resolution.cpp | 2 +- src/smt/smt_conflict_resolution.h | 2 +- src/smt/smt_context.cpp | 2 +- src/smt/smt_context.h | 2 +- src/smt/smt_context_inv.cpp | 2 +- src/smt/smt_context_pp.cpp | 2 +- src/smt/smt_context_stat.cpp | 2 +- src/smt/smt_enode.cpp | 2 +- src/smt/smt_enode.h | 2 +- src/smt/smt_eq_justification.h | 2 +- src/smt/smt_failure.h | 2 +- src/smt/smt_for_each_relevant_expr.cpp | 2 +- src/smt/smt_for_each_relevant_expr.h | 4 ++-- src/smt/smt_implied_equalities.h | 2 +- src/smt/smt_internalizer.cpp | 2 +- src/smt/smt_justification.cpp | 2 +- src/smt/smt_justification.h | 2 +- src/smt/smt_kernel.cpp | 2 +- src/smt/smt_kernel.h | 2 +- src/smt/smt_literal.cpp | 2 +- src/smt/smt_literal.h | 2 +- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_model_checker.h | 2 +- src/smt/smt_model_finder.h | 4 ++-- src/smt/smt_model_generator.cpp | 2 +- src/smt/smt_model_generator.h | 2 +- src/smt/smt_quantifier.cpp | 2 +- src/smt/smt_quantifier.h | 2 +- src/smt/smt_quick_checker.cpp | 2 +- src/smt/smt_quick_checker.h | 2 +- src/smt/smt_relevancy.cpp | 2 +- src/smt/smt_relevancy.h | 2 +- src/smt/smt_setup.cpp | 2 +- src/smt/smt_setup.h | 2 +- src/smt/smt_statistics.cpp | 2 +- src/smt/smt_statistics.h | 2 +- src/smt/smt_theory.cpp | 2 +- src/smt/smt_theory.h | 2 +- src/smt/smt_types.h | 2 +- src/smt/smt_value_sort.h | 2 +- src/smt/theory_arith.cpp | 2 +- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 4 ++-- src/smt/theory_arith_core.h | 2 +- src/smt/theory_arith_eq.h | 2 +- src/smt/theory_arith_int.h | 2 +- src/smt/theory_arith_inv.h | 2 +- src/smt/theory_arith_nl.h | 2 +- src/smt/theory_arith_pp.h | 2 +- src/smt/theory_array.cpp | 2 +- src/smt/theory_array.h | 2 +- src/smt/theory_array_base.cpp | 2 +- src/smt/theory_array_base.h | 2 +- src/smt/theory_array_full.h | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_bv.h | 2 +- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_datatype.h | 2 +- src/smt/theory_dense_diff_logic.cpp | 2 +- src/smt/theory_dense_diff_logic.h | 2 +- src/smt/theory_dense_diff_logic_def.h | 2 +- src/smt/theory_diff_logic.cpp | 4 ++-- src/smt/theory_diff_logic.h | 2 +- src/smt/theory_dl.cpp | 2 +- src/smt/theory_dl.h | 2 +- src/smt/theory_dummy.cpp | 2 +- src/smt/theory_dummy.h | 2 +- src/smt/theory_fpa.cpp | 2 +- src/smt/theory_fpa.h | 2 +- src/smt/theory_opt.cpp | 2 +- src/smt/theory_pb.h | 2 +- src/smt/theory_polymorphism.h | 2 +- src/smt/theory_seq.h | 2 +- src/smt/theory_seq_empty.h | 2 +- src/smt/theory_user_propagator.h | 2 +- src/smt/theory_utvpi.h | 2 +- src/smt/theory_utvpi_def.h | 2 +- src/smt/theory_wmaxsat.cpp | 2 +- src/smt/theory_wmaxsat.h | 2 +- src/smt/watch_list.cpp | 2 +- src/smt/watch_list.h | 2 +- src/solver/assertions/asserted_formulas.h | 2 +- src/tactic/bv/bv_bound_chk_tactic.cpp | 2 +- src/tactic/core/ctx_simplify_tactic.h | 2 +- src/tactic/core/symmetry_reduce_tactic.cpp | 2 +- src/tactic/tactical.cpp | 2 +- src/util/sat_literal.h | 4 ++-- src/util/sat_sls.h | 2 +- src/util/sign.h | 2 +- src/util/util.h | 2 +- 429 files changed, 477 insertions(+), 476 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 2708725875..9e11d9082b 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -24,8 +24,9 @@ set(CLANG_ONLY_WARNINGS "-Wsuggest-override" "-Winconsistent-missing-override" "-Wno-missing-field-initializers" - "-Wcast-qual" + "-Wcast-qual" ) + set(MSVC_WARNINGS "/W3") ################################################################################ diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index c35d3aa5b6..34a16789ca 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -447,4 +447,4 @@ extern "C" { return _am.get_i(av); Z3_CATCH_RETURN(0); } -}; +} diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 17810a4947..806f720b32 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -235,4 +235,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp index e01248b31a..6b454530ea 100644 --- a/src/api/api_array.cpp +++ b/src/api/api_array.cpp @@ -358,4 +358,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index d7ea3d3c80..f33f93e29f 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1547,4 +1547,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp index 1ebb51fcce..dead361cf7 100644 --- a/src/api/api_ast_map.cpp +++ b/src/api/api_ast_map.cpp @@ -161,4 +161,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp index 46a8894387..b74fecef3b 100644 --- a/src/api/api_ast_vector.cpp +++ b/src/api/api_ast_vector.cpp @@ -135,4 +135,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_ast_vector.h b/src/api/api_ast_vector.h index dc1fcb8e6a..f661b8d8d2 100644 --- a/src/api/api_ast_vector.h +++ b/src/api/api_ast_vector.h @@ -21,7 +21,7 @@ Revision History: namespace api { class context; -}; +} struct Z3_ast_vector_ref : public api::object { ast_ref_vector m_ast_vector; diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 5b627944c7..77e7bfbc29 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -399,4 +399,4 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_CATCH_RETURN(0); } -}; +} diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 02bcde2a93..ba926a967f 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -121,4 +121,4 @@ extern "C" { Z3_CATCH; } -}; +} diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 7fe4e40634..624980d507 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -359,7 +359,7 @@ namespace api { return *(m_rcf_manager.get()); } -}; +} // ------------------------ @@ -531,4 +531,4 @@ extern "C" { Z3_CATCH; } -}; +} diff --git a/src/api/api_context.h b/src/api/api_context.h index 7803725886..80fc90569e 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -45,16 +45,16 @@ Revision History: namespace smtlib { class parser; -}; +} namespace realclosure { class manager; -}; +} namespace smt2 { class parser; void free_parser(parser*); -}; +} namespace api { @@ -267,7 +267,7 @@ namespace api { }; -}; +} inline api::context * mk_c(Z3_context c) { return reinterpret_cast(c); } #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); } diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 61d4aa9fda..072b5c8fff 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -142,7 +142,7 @@ namespace api { void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); } void updt_params(params_ref const& p) { m_context.updt_params(p); } }; -}; +} extern "C" { @@ -705,4 +705,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h index 7f1ceb9bbf..11fbf7e119 100644 --- a/src/api/api_datalog.h +++ b/src/api/api_datalog.h @@ -30,7 +30,7 @@ typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*co namespace api { class fixedpoint_context; class context; -}; +} struct Z3_fixedpoint_ref : public api::object { diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index ee381e3e78..8d9d0dd206 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -687,4 +687,4 @@ extern "C" { } -}; +} diff --git a/src/api/api_finite_set.cpp b/src/api/api_finite_set.cpp index 2a2787e2a2..922ffe3f2c 100644 --- a/src/api/api_finite_set.cpp +++ b/src/api/api_finite_set.cpp @@ -184,4 +184,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index aeeb24c419..8ffbd4f13e 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1337,4 +1337,4 @@ extern "C" { Z3_CATCH_RETURN(false); } -}; +} diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index 7ef619c9b3..ae7d832a93 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -213,4 +213,4 @@ extern "C" { Z3_CATCH_RETURN(""); } -}; +} diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 3e065fb64e..500cbce37e 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -448,4 +448,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index cee60272ef..d6cc5afbcb 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -489,4 +489,4 @@ extern "C" { } #endif -}; +} diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index bf8fc98714..47f9dba6c0 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -503,4 +503,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index efd33cc057..acc3ab7c7a 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -212,4 +212,4 @@ extern "C" { Z3_CATCH_RETURN(""); } -}; +} diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index a51a7c0696..963fe7fa00 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -106,4 +106,4 @@ extern "C" { } -}; +} diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 55d4a43a8e..ba8345aeeb 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -80,4 +80,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 83e2fa5932..de1c6ff48d 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -583,5 +583,5 @@ extern "C" { return Z3_ast_to_string(c, reinterpret_cast(p)); } -}; +} diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index efbeea2e6c..49bc218f3a 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -437,4 +437,4 @@ extern "C" { return from_rcnumeral(rcfm(c).get_sign_condition_coefficient(to_rcnumeral(a), i, j)); Z3_CATCH_RETURN(nullptr); } -}; +} diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 4ceb827397..94756cc584 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -369,4 +369,4 @@ extern "C" { MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP); -}; +} diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 3da3619213..2d39e3287a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -1218,4 +1218,4 @@ extern "C" { -}; +} diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp index f29254cba2..0063fe7863 100644 --- a/src/api/api_special_relations.cpp +++ b/src/api/api_special_relations.cpp @@ -61,4 +61,4 @@ extern "C" { } MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC); -}; +} diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp index a3b8bacf07..b4f97716b7 100644 --- a/src/api/api_stats.cpp +++ b/src/api/api_stats.cpp @@ -133,4 +133,4 @@ extern "C" { return memory::get_allocation_size(); } -}; +} diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index e0038d8b75..8a639727f5 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -669,4 +669,4 @@ extern "C" { -}; +} diff --git a/src/api/api_util.h b/src/api/api_util.h index ee38c4f275..a1715eaa09 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -46,7 +46,7 @@ namespace api { void inc_ref(); void dec_ref(); }; -}; +} inline ast * to_ast(Z3_ast a) { return reinterpret_cast(a); } inline Z3_ast of_ast(ast* a) { return reinterpret_cast(a); } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 5172226aee..cfad378a17 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -24,7 +24,7 @@ class sexpr; namespace algebraic_numbers { class anum; class manager; -}; +} enum arith_sort_kind { REAL_SORT, diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 41ed2036bb..f7d65f2b43 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -171,7 +171,7 @@ namespace datatype { size* subst(obj_map& S) override; sort_size eval(obj_map const& S) override { return S[m_param]; } }; - }; + } class def { ast_manager& m; @@ -465,7 +465,7 @@ namespace datatype { sort_ref mk_tuple_datatype(svector> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs); }; -}; +} typedef datatype::accessor accessor_decl; typedef datatype::constructor constructor_decl; diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index af4d30add8..1be709324c 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -648,7 +648,7 @@ namespace datalog { m_fid = m.mk_family_id(symbol("datalog_relation")); } return m_fid; - }; + } arith_util& dl_decl_util::arith() const { if (!m_arith) m_arith = alloc(arith_util, m); @@ -788,4 +788,4 @@ namespace datalog { return m.mk_app(f, num_args, args); } -}; +} diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 850d181267..2acbb362a6 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -199,5 +199,5 @@ namespace datalog { }; -}; +} diff --git a/src/ast/euf/euf_ac_plugin.h b/src/ast/euf/euf_ac_plugin.h index 99d01791c7..352337a2f1 100644 --- a/src/ast/euf/euf_ac_plugin.h +++ b/src/ast/euf/euf_ac_plugin.h @@ -319,14 +319,14 @@ namespace euf { struct eq_pp { ac_plugin const& p; eq const& e; - eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {}; + eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {} eq_pp(ac_plugin const& p, unsigned eq_id): p(p), e(p.m_active[eq_id]) {} std::ostream& display(std::ostream& out) const { return p.display_equation(out, e); } }; struct eq_pp_ll { ac_plugin const& p; eq const& e; - eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {}; + eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {} eq_pp_ll(ac_plugin const& p, unsigned eq_id) : p(p), e(p.m_active[eq_id]) {} std::ostream& display(std::ostream& out) const { return p.display_equation_ll(out, e); } }; diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index b308523a54..93be311740 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -276,5 +276,5 @@ namespace euf { return find(n) == n; } -}; +} diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index d6b64e7566..ecac03a228 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -179,7 +179,7 @@ namespace euf { }; -}; +} diff --git a/src/ast/euf/euf_mam.h b/src/ast/euf/euf_mam.h index c391f6c09c..a6c20d74b6 100644 --- a/src/ast/euf/euf_mam.h +++ b/src/ast/euf/euf_mam.h @@ -81,5 +81,5 @@ namespace euf { static void ground_subterms(expr* e, ptr_vector& ground); }; -}; +} diff --git a/src/ast/euf/euf_plugin.h b/src/ast/euf/euf_plugin.h index ba6b2d5f93..0a9503ba5d 100644 --- a/src/ast/euf/euf_plugin.h +++ b/src/ast/euf/euf_plugin.h @@ -47,7 +47,7 @@ namespace euf { virtual void merge_eh(enode* n1, enode* n2) = 0; - virtual void diseq_eh(enode* eq) {}; + virtual void diseq_eh(enode* eq) {} virtual void propagate() = 0; diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index ebad5760cb..ee61f7587e 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -94,7 +94,7 @@ namespace has_skolem_functions_ns { void operator()(app const * n) const { if (n->get_decl()->is_skolem() && n->get_num_args() > 0) throw found(); } void operator()(quantifier * n) const {} }; -}; +} bool has_skolem_functions(expr * n) { has_skolem_functions_ns::proc p; diff --git a/src/ast/format.cpp b/src/ast/format.cpp index 6583e9893d..a21f21eebf 100644 --- a/src/ast/format.cpp +++ b/src/ast/format.cpp @@ -195,4 +195,4 @@ namespace format_ns { return fm(m).mk_app(fid(m), OP_NIL); } -}; +} diff --git a/src/ast/format.h b/src/ast/format.h index 2714d54b74..b7356b8029 100644 --- a/src/ast/format.h +++ b/src/ast/format.h @@ -198,6 +198,6 @@ namespace format_ns { return mk_seq4(m, begin, end, proc, static_cast(strlen(lp)), lp, rp); } -}; +} diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index e237c0dcde..0350694082 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -162,10 +162,10 @@ public: void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector m_extra_assertions; - special_t const & get_min_max_specials() const { return m_min_max_ufs; }; - const2bv_t const & get_const2bv() const { return m_const2bv; }; - const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }; - uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; }; + special_t const & get_min_max_specials() const { return m_min_max_ufs; } + const2bv_t const & get_const2bv() const { return m_const2bv; } + const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; } + uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; } protected: void mk_one(func_decl *f, expr_ref & sign, expr_ref & result); diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index a9a0c77fcf..a9a4618909 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -167,7 +167,7 @@ namespace macro_manager_ns { } } }; -}; +} /** \brief Mark all func_decls used in exprs as forbidden. diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index 094a7cabab..a8fa7187ef 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -71,7 +71,7 @@ void quasi_macros::find_occurrences(expr * e) { default: UNREACHABLE(); } } -}; +} bool quasi_macros::is_non_ground_uninterp(expr const * e) const { return is_non_ground(e) && is_uninterp(e); diff --git a/src/ast/polymorphism_inst.h b/src/ast/polymorphism_inst.h index 1d171b3143..d9a6ed943d 100644 --- a/src/ast/polymorphism_inst.h +++ b/src/ast/polymorphism_inst.h @@ -58,7 +58,7 @@ namespace polymorphism { void undo() override { i.m_in_decl_queue.mark(i.m_decl_queue.back(), false); i.m_decl_queue.pop_back(); - }; + } }; struct remove_back : public trail { diff --git a/src/ast/quantifier_stat.cpp b/src/ast/quantifier_stat.cpp index 17efb11e9a..a09d8bd928 100644 --- a/src/ast/quantifier_stat.cpp +++ b/src/ast/quantifier_stat.cpp @@ -115,5 +115,5 @@ namespace q { return r; } -}; +} diff --git a/src/ast/quantifier_stat.h b/src/ast/quantifier_stat.h index 45fd58530c..5bff878f1c 100644 --- a/src/ast/quantifier_stat.h +++ b/src/ast/quantifier_stat.h @@ -149,6 +149,6 @@ namespace q { quantifier_stat * operator()(quantifier * q, unsigned generation); }; -}; +} diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index d9fe07dcf3..f876d3ce89 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -60,7 +60,7 @@ namespace recfun { func_decl_ref m_pred; // interval; typedef obj_map bound_map; - bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {}; + bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {} ~bv_bounds(); public: // bounds addition methods br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result); diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 5838985625..26469ffa2a 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -123,5 +123,5 @@ namespace seq { }; -}; +} diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index e1ffae7431..a77aaa55ba 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -727,5 +727,5 @@ namespace seq { -}; +} diff --git a/src/ast/rewriter/seq_eq_solver.h b/src/ast/rewriter/seq_eq_solver.h index c6c5437b79..a3e8a00d47 100644 --- a/src/ast/rewriter/seq_eq_solver.h +++ b/src/ast/rewriter/seq_eq_solver.h @@ -167,5 +167,5 @@ namespace seq { }; -}; +} diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 4e327f0fa4..39cf2534fe 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -171,5 +171,5 @@ namespace seq { }; -}; +} diff --git a/src/ast/simplifiers/distribute_forall.cpp b/src/ast/simplifiers/distribute_forall.cpp index c7cc6659aa..eb57038103 100644 --- a/src/ast/simplifiers/distribute_forall.cpp +++ b/src/ast/simplifiers/distribute_forall.cpp @@ -101,5 +101,5 @@ void distribute_forall_simplifier::reduce() { if (r != d.fml()) m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep())); } -}; +} diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp index efaf7f244a..36c132295f 100644 --- a/src/ast/simplifiers/propagate_values.cpp +++ b/src/ast/simplifiers/propagate_values.cpp @@ -62,7 +62,7 @@ void propagate_values::add_sub(dependent_expr const& de) { else if (m.is_value(y) && m_shared.is_shared(x)) m_subst.insert(x, y, dep); } -}; +} void propagate_values::reduce() { m_shared.reset(); diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h index 4040e8d57a..84fadc1260 100644 --- a/src/ast/sls/sls_array_plugin.h +++ b/src/ast/sls/sls_array_plugin.h @@ -36,7 +36,7 @@ namespace sls { for (unsigned i = 1; i < a.sel->num_args(); ++i) h ^= a.sel->get_arg(i)->get_root()->hash(); return h; - }; + } }; struct select_args_eq { bool operator()(select_args const& a, select_args const& b) const { @@ -103,13 +103,13 @@ namespace sls { euf::enode* mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel); void resolve_conflict(); - size_t* to_ptr(sat::literal l) { return reinterpret_cast((size_t)(l.index() << 4)); }; + size_t* to_ptr(sat::literal l) { return reinterpret_cast((size_t)(l.index() << 4)); } size_t* to_ptr(euf::enode* t) { return reinterpret_cast((reinterpret_cast(t) << 4) + 1); } size_t* to_ptr(unsigned n) { return reinterpret_cast((size_t)(n << 4) + 3); } bool is_literal(size_t* p) { return (reinterpret_cast(p) & 3) == 0; } bool is_index(size_t* p) { return (reinterpret_cast(p) & 3) == 3; } bool is_enode(size_t* p) { return (reinterpret_cast(p) & 3) == 1; } - sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); }; + sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); } euf::enode* to_enode(size_t* p) { return reinterpret_cast(reinterpret_cast(p) >> 4); } unsigned to_index(size_t* p) { return static_cast(reinterpret_cast(p) >> 4); } diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 87398429e4..b8b46f9d6d 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -871,8 +871,8 @@ namespace sls { if (m_la.m_config.use_top_level_assertions) return m_la.ctx.input_assertions().get(idx); return m_la.ctx.atom(m_la.ctx.root_literals()[idx].var()); - }; + } -} \ No newline at end of file +} diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index a078de5a19..e87190d9b2 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -40,7 +40,7 @@ class sls_tracker { mpz m_zero, m_one, m_two; struct value_score { - value_score() : value(unsynch_mpz_manager::mk_z(0)) {}; + value_score() : value(unsynch_mpz_manager::mk_z(0)) {} value_score(value_score&&) noexcept = default; value_score(const value_score &other) { m = other.m; diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index fae5447eb7..8cad22dc16 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -44,15 +44,15 @@ namespace sls { virtual expr_ref get_value(expr* e) = 0; virtual bool is_fixed(expr* e, expr_ref& value) { return false; } virtual void initialize() = 0; - virtual void start_propagation() {}; + virtual void start_propagation() {} virtual bool propagate() = 0; virtual void propagate_literal(sat::literal lit) = 0; virtual void repair_literal(sat::literal lit) = 0; virtual bool repair_down(app* e) = 0; virtual void repair_up(app* e) = 0; virtual bool is_sat() = 0; - virtual void on_rescale() {}; - virtual void on_restart() {}; + virtual void on_rescale() {} + virtual void on_restart() {} virtual std::ostream& display(std::ostream& out) const = 0; virtual bool set_value(expr* e, expr* v) = 0; virtual void collect_statistics(statistics& st) const = 0; diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h index 45c93a8d06..99523f5077 100644 --- a/src/ast/sls/sls_euf_plugin.h +++ b/src/ast/sls/sls_euf_plugin.h @@ -52,8 +52,8 @@ namespace sls { bool is_user_sort(sort* s) { return s->get_family_id() == user_sort_family_id; } - size_t* to_ptr(sat::literal l) { return reinterpret_cast((size_t)(l.index() << 4)); }; - sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); }; + size_t* to_ptr(sat::literal l) { return reinterpret_cast((size_t)(l.index() << 4)); } + sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast(reinterpret_cast(p) >> 4)); } void validate_model(); void log_clause(sat::literal_vector const& lits); diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index d7316619f7..aaf1f1b479 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -581,7 +581,7 @@ class mbp_qel_cmd : public cmd { ptr_vector m_vars; public: - mbp_qel_cmd() : cmd("mbp-qel"){}; + mbp_qel_cmd() : cmd("mbp-qel"){} char const *get_usage() const override { return "(exprs) (vars)"; } char const *get_descr(cmd_context &ctx) const override { return "Model based projection using e-graphs"; @@ -639,7 +639,7 @@ class qel_cmd : public cmd { ptr_vector m_vars; public: - qel_cmd() : cmd("qel"){}; + qel_cmd() : cmd("qel"){} char const *get_usage() const override { return "(lits) (vars)"; } char const *get_descr(cmd_context &ctx) const override { return "QE lite over e-graphs"; @@ -703,7 +703,7 @@ class qe_lite_cmd : public cmd { ptr_vector m_vars; public: - qe_lite_cmd() : cmd("qe-lite"){}; + qe_lite_cmd() : cmd("qe-lite"){} char const *get_usage() const override { return "(lits) (vars)"; } char const *get_descr(cmd_context &ctx) const override { return "QE lite over e-graphs"; diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp index 8cc47c21e6..df12638d89 100644 --- a/src/math/grobner/pdd_simplifier.cpp +++ b/src/math/grobner/pdd_simplifier.cpp @@ -494,7 +494,7 @@ namespace dd { hash(unsigned_vector& vars):vars(vars) {} bool operator()(mon const& m) const { return unsigned_ptr_hash(vars.data() + m.offset, m.sz, 1); - }; + } }; struct eq { unsigned_vector& vars; diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index d1ac780e84..fe0d403fba 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -267,7 +267,7 @@ namespace lp { unsigned j, const T &m, X &theta, bool &unlimited) { SASSERT(m > 0 && this->m_column_types[j] == column_type::upper_bound); limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited); - }; + } void get_bound_on_variable_and_update_leaving_precisely( unsigned j, vector &leavings, T m, X &t, diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index 89823e4dc3..a57ca15e6b 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -43,9 +43,9 @@ namespace nla { ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {} bool operator==(const ineq& a) const = delete; bool operator!=(const ineq& a) const = delete; - const lp::lar_term& term() const { return m_term; }; - lp::lconstraint_kind cmp() const { return m_cmp; }; - const rational& rs() const { return m_rs; }; + const lp::lar_term& term() const { return m_term; } + lp::lconstraint_kind cmp() const { return m_cmp; } + const rational& rs() const { return m_rs; } }; class lemma { diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index a890913c2d..945b9023dc 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -3511,4 +3511,4 @@ namespace algebraic_numbers { void manager::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); } -}; +} diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index e60f8ea1a9..37c0559728 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -410,7 +410,7 @@ namespace algebraic_numbers { anum& operator=(basic_cell* cell) { SASSERT(is_null()); m_cell = TAG(void*, cell, BASIC); return *this; } anum& operator=(algebraic_cell* cell) { SASSERT(is_null()); m_cell = TAG(void*, cell, ROOT); return *this; } }; -}; +} typedef algebraic_numbers::manager anum_manager; typedef algebraic_numbers::manager::numeral anum; diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 1b06fb2b09..84825baeb8 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -8253,7 +8253,7 @@ namespace polynomial { p->display_smt2(out, m_imp->m_manager, proc); return out; } -}; +} polynomial::polynomial * convert(polynomial::manager & sm, polynomial::polynomial * p, polynomial::manager & tm, polynomial::var x, unsigned max_d) { diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 5774e6e132..9d0bcabcf3 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -36,7 +36,7 @@ class small_object_allocator; namespace algebraic_numbers { class anum; class manager; -}; +} namespace polynomial { typedef unsigned var; @@ -1065,7 +1065,7 @@ namespace polynomial { scoped_set_zp(manager & _m, uint64_t p):m(_m), m_modular(m.modular()), m_p(m.m()) { m_p = m.p(); m.set_zp(p); } ~scoped_set_zp() { if (m_modular) m.set_zp(m_p); else m.set_z(); } }; -}; +} typedef polynomial::polynomial_ref polynomial_ref; typedef polynomial::polynomial_ref_vector polynomial_ref_vector; diff --git a/src/math/polynomial/polynomial_cache.cpp b/src/math/polynomial/polynomial_cache.cpp index 7d3a15ded6..095027bae4 100644 --- a/src/math/polynomial/polynomial_cache.cpp +++ b/src/math/polynomial/polynomial_cache.cpp @@ -256,4 +256,4 @@ namespace polynomial { dealloc(m_imp); m_imp = alloc(imp, _m); } -}; +} diff --git a/src/math/polynomial/polynomial_cache.h b/src/math/polynomial/polynomial_cache.h index a27abf42d1..ae8fa0ed82 100644 --- a/src/math/polynomial/polynomial_cache.h +++ b/src/math/polynomial/polynomial_cache.h @@ -40,4 +40,4 @@ namespace polynomial { void factor(polynomial const * p, polynomial_ref_vector & distinct_factors); void reset(); }; -}; +} diff --git a/src/math/polynomial/polynomial_primes.h b/src/math/polynomial/polynomial_primes.h index ea2baf0dcc..4c9e05e778 100644 --- a/src/math/polynomial/polynomial_primes.h +++ b/src/math/polynomial/polynomial_primes.h @@ -66,5 +66,5 @@ namespace polynomial { }; #endif -}; +} diff --git a/src/math/polynomial/polynomial_var2value.h b/src/math/polynomial/polynomial_var2value.h index 11e8c3bb8e..2897e74149 100644 --- a/src/math/polynomial/polynomial_var2value.h +++ b/src/math/polynomial/polynomial_var2value.h @@ -43,6 +43,6 @@ namespace polynomial { } }; -}; +} diff --git a/src/math/polynomial/rpolynomial.cpp b/src/math/polynomial/rpolynomial.cpp index 67b8825253..17a3be50d4 100644 --- a/src/math/polynomial/rpolynomial.cpp +++ b/src/math/polynomial/rpolynomial.cpp @@ -789,4 +789,4 @@ namespace rpolynomial { } #endif -}; +} diff --git a/src/math/polynomial/rpolynomial.h b/src/math/polynomial/rpolynomial.h index 2a5123a031..ab04c99d63 100644 --- a/src/math/polynomial/rpolynomial.h +++ b/src/math/polynomial/rpolynomial.h @@ -175,7 +175,7 @@ namespace rpolynomial { return out; } }; -}; +} typedef rpolynomial::polynomial_ref rpolynomial_ref; typedef rpolynomial::polynomial_ref_vector rpolynomial_ref_vector; diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index a30691c9df..7ce6aab5a6 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -3142,4 +3142,4 @@ namespace upolynomial { } return out; } -}; +} diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index de29a1cdf4..135422b94f 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -917,4 +917,4 @@ namespace upolynomial { std::ostream& display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name = "x") const; }; -}; +} diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 1ab95def35..34bd83b7ad 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -1299,4 +1299,4 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, return factor_square_free(upm, f, fs, 1, params); } -}; // end upolynomial namespace +} // end upolynomial namespace diff --git a/src/math/polynomial/upolynomial_factorization.h b/src/math/polynomial/upolynomial_factorization.h index 3842665bd1..14ec508c3b 100644 --- a/src/math/polynomial/upolynomial_factorization.h +++ b/src/math/polynomial/upolynomial_factorization.h @@ -90,5 +90,5 @@ namespace upolynomial { That is, the factors of f are inserted as factors of degree k into fs. */ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, unsigned k, factor_params const & ps = factor_params()); -}; +} diff --git a/src/math/polynomial/upolynomial_factorization_int.h b/src/math/polynomial/upolynomial_factorization_int.h index f47610b65d..45f0204441 100644 --- a/src/math/polynomial/upolynomial_factorization_int.h +++ b/src/math/polynomial/upolynomial_factorization_int.h @@ -416,5 +416,5 @@ namespace upolynomial { } } }; -}; +} diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 4ba1c11fa7..427070a85d 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -6486,7 +6486,7 @@ namespace realclosure { { return m_imp->get_sign_condition_coefficient(a, i, j); } -}; +} void pp(realclosure::manager::imp * imp, realclosure::polynomial const & p, realclosure::extension * ext) { imp->display_polynomial_expr(std::cout, p, ext, false, false); diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index a1fae3e2bf..b256ffd15b 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -317,7 +317,7 @@ namespace realclosure { void * data() { return m_value; } static num mk(void * ptr) { num r; r.m_value = reinterpret_cast(ptr); return r; } }; -}; +} typedef realclosure::manager rcmanager; typedef rcmanager::numeral rcnumeral; diff --git a/src/math/simplex/simplex.cpp b/src/math/simplex/simplex.cpp index 6174b81b35..30de88c543 100644 --- a/src/math/simplex/simplex.cpp +++ b/src/math/simplex/simplex.cpp @@ -74,4 +74,4 @@ namespace simplex { } } } -}; +} diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 0405a59d0b..ad194ebe71 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -204,5 +204,5 @@ namespace simplex { void kernel(sparse_matrix& s, vector>& K); void kernel_ffe(sparse_matrix &s, vector> &K); -}; +} diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 69ed434ce6..f7adf424d6 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -1035,6 +1035,6 @@ namespace simplex { } -}; +} diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 942873b5fa..90cd88d142 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -355,4 +355,4 @@ namespace simplex { typedef unsynch_mpq_inf_manager eps_manager; }; -}; +} diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index fd4e7b0c32..430310bc89 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -603,5 +603,5 @@ namespace simplex { -}; +} diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index d531f1bafd..51d7b753e0 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -271,4 +271,4 @@ namespace subpaving { return alloc(context_mpfx_wrapper, lim, m, qm, p, a); } -}; +} diff --git a/src/math/subpaving/subpaving.h b/src/math/subpaving/subpaving.h index b76f5e8313..0c5a76770d 100644 --- a/src/math/subpaving/subpaving.h +++ b/src/math/subpaving/subpaving.h @@ -116,6 +116,6 @@ context * mk_hwf_context(reslimit& lim, f2n & m, unsynch_mpq_manage context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = nullptr); context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = nullptr); -}; +} diff --git a/src/math/subpaving/subpaving_hwf.h b/src/math/subpaving/subpaving_hwf.h index f2378a73a4..49f2dbc5fa 100644 --- a/src/math/subpaving/subpaving_hwf.h +++ b/src/math/subpaving/subpaving_hwf.h @@ -42,5 +42,5 @@ public: context_hwf(reslimit& lim, f2n & m, params_ref const & p, small_object_allocator * a):context_t(lim, config_hwf(m), p, a) {} }; -}; +} diff --git a/src/math/subpaving/subpaving_mpf.h b/src/math/subpaving/subpaving_mpf.h index 213c3c94b6..bc50de6fdf 100644 --- a/src/math/subpaving/subpaving_mpf.h +++ b/src/math/subpaving/subpaving_mpf.h @@ -43,5 +43,5 @@ public: context_mpf(reslimit& lim, f2n & m, params_ref const & p, small_object_allocator * a):context_t(lim, config_mpf(m), p, a) {} }; -}; +} diff --git a/src/math/subpaving/subpaving_mpff.h b/src/math/subpaving/subpaving_mpff.h index 763195cb91..631293be0c 100644 --- a/src/math/subpaving/subpaving_mpff.h +++ b/src/math/subpaving/subpaving_mpff.h @@ -39,5 +39,5 @@ struct config_mpff { typedef context_t context_mpff; -}; +} diff --git a/src/math/subpaving/subpaving_mpfx.h b/src/math/subpaving/subpaving_mpfx.h index 9613aa124d..14611c13a5 100644 --- a/src/math/subpaving/subpaving_mpfx.h +++ b/src/math/subpaving/subpaving_mpfx.h @@ -39,5 +39,5 @@ struct config_mpfx { typedef context_t context_mpfx; -}; +} diff --git a/src/math/subpaving/subpaving_mpq.h b/src/math/subpaving/subpaving_mpq.h index 441fbe0663..7468672a82 100644 --- a/src/math/subpaving/subpaving_mpq.h +++ b/src/math/subpaving/subpaving_mpq.h @@ -37,5 +37,5 @@ struct config_mpq { typedef context_t context_mpq; -}; +} diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 7300e3da3c..3a6081f409 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -845,5 +845,5 @@ public: void operator()(); }; -}; +} diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index b71b10faec..39f4a84f5b 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -1952,4 +1952,4 @@ bool context_t::check_invariant() const { } -}; +} diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 797ce0774c..067ac712ff 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -1360,4 +1360,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 1181cf82bb..3a9bdcf340 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -620,5 +620,5 @@ namespace datalog { void display_rel_decl(std::ostream& out, func_decl* f); }; -}; +} diff --git a/src/muz/base/dl_costs.cpp b/src/muz/base/dl_costs.cpp index 70688cd59c..35eaddce98 100644 --- a/src/muz/base/dl_costs.cpp +++ b/src/muz/base/dl_costs.cpp @@ -157,4 +157,4 @@ namespace datalog { } } -}; +} diff --git a/src/muz/base/dl_costs.h b/src/muz/base/dl_costs.h index ea3efcda99..a4c681af48 100644 --- a/src/muz/base/dl_costs.h +++ b/src/muz/base/dl_costs.h @@ -106,6 +106,6 @@ namespace datalog { void start(accounted_object *); void finish() { start(nullptr); } }; -}; +} diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 0824c84cf5..b23786020c 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -1084,6 +1084,6 @@ namespace datalog { -}; +} diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 87c2637a9b..e5126c778f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -373,7 +373,7 @@ namespace datalog { This possibly returns a ";"-separated list of names. */ - symbol const& name() const { return m_name; } ; + symbol const& name() const { return m_name; } unsigned hash() const; @@ -386,6 +386,6 @@ namespace datalog { unsigned operator()(const rule * r) const; }; -}; +} diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index d621e1b24b..4e0572c978 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -709,4 +709,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index 4afacacf06..be694af461 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -281,5 +281,5 @@ namespace datalog { -}; +} diff --git a/src/muz/base/dl_rule_subsumption_index.cpp b/src/muz/base/dl_rule_subsumption_index.cpp index f3fb545b67..cf41c37f20 100644 --- a/src/muz/base/dl_rule_subsumption_index.cpp +++ b/src/muz/base/dl_rule_subsumption_index.cpp @@ -80,5 +80,5 @@ namespace datalog { return false; } -}; +} diff --git a/src/muz/base/dl_rule_subsumption_index.h b/src/muz/base/dl_rule_subsumption_index.h index 3783be3dc3..5d321fe7aa 100644 --- a/src/muz/base/dl_rule_subsumption_index.h +++ b/src/muz/base/dl_rule_subsumption_index.h @@ -56,6 +56,6 @@ namespace datalog { bool is_subsumed(app * query); }; -}; +} diff --git a/src/muz/base/dl_rule_transformer.cpp b/src/muz/base/dl_rule_transformer.cpp index bcdcc6b5bb..4342e3564a 100644 --- a/src/muz/base/dl_rule_transformer.cpp +++ b/src/muz/base/dl_rule_transformer.cpp @@ -148,4 +148,4 @@ namespace datalog { -}; +} diff --git a/src/muz/base/dl_rule_transformer.h b/src/muz/base/dl_rule_transformer.h index c446593bdd..9ac935357a 100644 --- a/src/muz/base/dl_rule_transformer.h +++ b/src/muz/base/dl_rule_transformer.h @@ -110,6 +110,6 @@ namespace datalog { static void remove_duplicate_tails(app_ref_vector& tail, bool_vector& tail_neg); }; -}; +} diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index 975d4e721b..81740cc86a 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -681,5 +681,5 @@ namespace datalog { stm<; diff --git a/src/muz/bmc/dl_bmc_engine.h b/src/muz/bmc/dl_bmc_engine.h index 05d5707a66..c1631a8319 100644 --- a/src/muz/bmc/dl_bmc_engine.h +++ b/src/muz/bmc/dl_bmc_engine.h @@ -67,7 +67,7 @@ namespace datalog { void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level); expr_ref compile_query(func_decl* query_pred, unsigned level); }; -}; +} diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index ccaf46702b..7683e4dbaa 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -222,4 +222,4 @@ namespace datalog { return m_imp->get_answer(); } -}; +} diff --git a/src/muz/clp/clp_context.h b/src/muz/clp/clp_context.h index 306baf3bd3..4be64b325a 100644 --- a/src/muz/clp/clp_context.h +++ b/src/muz/clp/clp_context.h @@ -38,5 +38,5 @@ namespace datalog { void display_certificate(std::ostream& out) const override; expr_ref get_answer() override; }; -}; +} diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index e692196f26..300edfe239 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -878,4 +878,4 @@ namespace datalog { expr_ref ddnf::get_answer() { return m_imp->get_answer(); } -}; +} diff --git a/src/muz/ddnf/ddnf.h b/src/muz/ddnf/ddnf.h index 6a93ef2305..e25b7a8d08 100644 --- a/src/muz/ddnf/ddnf.h +++ b/src/muz/ddnf/ddnf.h @@ -65,5 +65,5 @@ namespace datalog { void display(std::ostream& out) const; void display_statistics(std::ostream& out) const; }; -}; +} diff --git a/src/muz/fp/datalog_parser.h b/src/muz/fp/datalog_parser.h index e836cbaec8..fcf1a1327f 100644 --- a/src/muz/fp/datalog_parser.h +++ b/src/muz/fp/datalog_parser.h @@ -42,5 +42,5 @@ namespace datalog { virtual bool parse_directory(char const * path) = 0; }; -}; +} diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h index 773b45813f..310e09fe6f 100644 --- a/src/muz/rel/check_relation.h +++ b/src/muz/rel/check_relation.h @@ -164,6 +164,6 @@ namespace datalog { unsigned_vector const& dst_eq, unsigned_vector const& neg_eq); }; -}; +} diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 9c14421850..2592d642ca 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -631,12 +631,12 @@ namespace datalog { class identity_mutator_fn : public mutator_fn { public: - void operator()(base_object & t) override {}; + void operator()(base_object & t) override {} }; class identity_intersection_filter_fn : public intersection_filter_fn { public: - void operator()(base_object & t, const base_object & neg) override {}; + void operator()(base_object & t, const base_object & neg) override {} }; class default_permutation_rename_fn : public transformer_fn { @@ -1258,5 +1258,5 @@ namespace datalog { expr_ref_vector & renaming_arg); -}; +} diff --git a/src/muz/rel/dl_bound_relation.cpp b/src/muz/rel/dl_bound_relation.cpp index 2a078d8f7e..417ae0cb90 100644 --- a/src/muz/rel/dl_bound_relation.cpp +++ b/src/muz/rel/dl_bound_relation.cpp @@ -676,6 +676,6 @@ namespace datalog { } -}; +} diff --git a/src/muz/rel/dl_bound_relation.h b/src/muz/rel/dl_bound_relation.h index 8f852f0ba4..f90d643246 100644 --- a/src/muz/rel/dl_bound_relation.h +++ b/src/muz/rel/dl_bound_relation.h @@ -168,6 +168,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_check_table.cpp b/src/muz/rel/dl_check_table.cpp index 0a6d900274..e036fdb117 100644 --- a/src/muz/rel/dl_check_table.cpp +++ b/src/muz/rel/dl_check_table.cpp @@ -435,5 +435,5 @@ namespace datalog { return result; } -}; +} diff --git a/src/muz/rel/dl_check_table.h b/src/muz/rel/dl_check_table.h index 144d0d6fc4..4e49bd4de9 100644 --- a/src/muz/rel/dl_check_table.h +++ b/src/muz/rel/dl_check_table.h @@ -129,5 +129,5 @@ namespace datalog { unsigned get_size_estimate_bytes() const override { return m_tocheck->get_size_estimate_bytes(); } }; - }; + } diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 106d1b7919..edb7598d68 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -279,6 +279,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_external_relation.cpp b/src/muz/rel/dl_external_relation.cpp index a2e42f6402..bfbd22f4a3 100644 --- a/src/muz/rel/dl_external_relation.cpp +++ b/src/muz/rel/dl_external_relation.cpp @@ -449,4 +449,4 @@ namespace datalog { return alloc(negation_filter_fn, *this, t, negated_obj, joined_col_cnt, t_cols, negated_cols); } -}; +} diff --git a/src/muz/rel/dl_external_relation.h b/src/muz/rel/dl_external_relation.h index c8887eeedb..98fd74992e 100644 --- a/src/muz/rel/dl_external_relation.h +++ b/src/muz/rel/dl_external_relation.h @@ -147,5 +147,5 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 7f3806b91a..61f76c77d6 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -2372,4 +2372,4 @@ namespace datalog { bool_rewriter(m).mk_or(disjs.size(), disjs.data(), fml); } -}; +} diff --git a/src/muz/rel/dl_finite_product_relation.h b/src/muz/rel/dl_finite_product_relation.h index 324564469f..f602e37126 100644 --- a/src/muz/rel/dl_finite_product_relation.h +++ b/src/muz/rel/dl_finite_product_relation.h @@ -359,6 +359,6 @@ namespace datalog { void to_formula(expr_ref& fml) const override; }; -}; +} diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index a008c2b731..4a1da5a791 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -364,6 +364,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_interval_relation.cpp b/src/muz/rel/dl_interval_relation.cpp index 81c630ec6a..39ffdbfcb1 100644 --- a/src/muz/rel/dl_interval_relation.cpp +++ b/src/muz/rel/dl_interval_relation.cpp @@ -648,5 +648,5 @@ namespace datalog { return false; } -}; +} diff --git a/src/muz/rel/dl_interval_relation.h b/src/muz/rel/dl_interval_relation.h index 0bddec4cf8..857a3f3dfd 100644 --- a/src/muz/rel/dl_interval_relation.h +++ b/src/muz/rel/dl_interval_relation.h @@ -134,6 +134,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 9565a71436..67b67bbef5 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -885,5 +885,5 @@ namespace datalog { return res.detach(); } -}; +} diff --git a/src/muz/rel/dl_mk_explanations.h b/src/muz/rel/dl_mk_explanations.h index 33d5cc8eea..ba2bbe082f 100644 --- a/src/muz/rel/dl_mk_explanations.h +++ b/src/muz/rel/dl_mk_explanations.h @@ -79,6 +79,6 @@ namespace datalog { static expr* get_explanation(relation_base const& r); }; -}; +} diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp index 77d106e0cf..39ebbf4344 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.cpp +++ b/src/muz/rel/dl_mk_similarity_compressor.cpp @@ -543,4 +543,4 @@ namespace datalog { reset(); return result; } -}; +} diff --git a/src/muz/rel/dl_mk_similarity_compressor.h b/src/muz/rel/dl_mk_similarity_compressor.h index 394e1a9e62..73ff15339c 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.h +++ b/src/muz/rel/dl_mk_similarity_compressor.h @@ -71,6 +71,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index de10c4f7f0..cf85321226 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -751,5 +751,5 @@ namespace datalog { } -}; +} diff --git a/src/muz/rel/dl_mk_simple_joins.h b/src/muz/rel/dl_mk_simple_joins.h index 6ec66159cd..f4aacdaa9a 100644 --- a/src/muz/rel/dl_mk_simple_joins.h +++ b/src/muz/rel/dl_mk_simple_joins.h @@ -56,6 +56,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp index 7dd9056f6d..9884aea060 100644 --- a/src/muz/rel/dl_product_relation.cpp +++ b/src/muz/rel/dl_product_relation.cpp @@ -1128,7 +1128,7 @@ namespace datalog { } } -}; +} diff --git a/src/muz/rel/dl_product_relation.h b/src/muz/rel/dl_product_relation.h index 63c0004898..e8190a8301 100644 --- a/src/muz/rel/dl_product_relation.h +++ b/src/muz/rel/dl_product_relation.h @@ -184,6 +184,6 @@ namespace datalog { } }; -}; +} diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index dda2704626..ed0c37f4ff 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1689,5 +1689,5 @@ namespace datalog { return res; } -}; +} diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index 58d46347d2..3c480785ae 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -699,6 +699,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index b1e64bd648..19fc688d01 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/src/muz/rel/dl_sieve_relation.cpp @@ -662,4 +662,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h index 0166bec981..71fc8a15a3 100644 --- a/src/muz/rel/dl_sieve_relation.h +++ b/src/muz/rel/dl_sieve_relation.h @@ -190,6 +190,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index b59260863c..8cca81d733 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -1404,5 +1404,5 @@ namespace datalog { } -}; +} diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index c548e3ff06..34f05f4798 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -494,5 +494,5 @@ namespace datalog { bool knows_exact_size() const override { return true; } }; - }; + } diff --git a/src/muz/rel/dl_table.cpp b/src/muz/rel/dl_table.cpp index 62670254d3..36344f5697 100644 --- a/src/muz/rel/dl_table.cpp +++ b/src/muz/rel/dl_table.cpp @@ -292,5 +292,5 @@ namespace datalog { table_base::iterator bitvector_table::end() const { return mk_iterator(alloc(bv_iterator, *this, true)); } -}; +} diff --git a/src/muz/rel/dl_table.h b/src/muz/rel/dl_table.h index 96f68f44cb..becb61d964 100644 --- a/src/muz/rel/dl_table.h +++ b/src/muz/rel/dl_table.h @@ -144,6 +144,6 @@ namespace datalog { -}; +} diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index 4f51001769..c264872c7d 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -489,5 +489,5 @@ namespace datalog { } } -}; +} diff --git a/src/muz/rel/dl_table_relation.h b/src/muz/rel/dl_table_relation.h index bb6368d253..9ff0636283 100644 --- a/src/muz/rel/dl_table_relation.h +++ b/src/muz/rel/dl_table_relation.h @@ -126,6 +126,6 @@ namespace datalog { bool knows_exact_size() const override { return m_table->knows_exact_size(); } }; -}; +} diff --git a/src/muz/rel/dl_vector_relation.h b/src/muz/rel/dl_vector_relation.h index f659831fb3..3f1edd28ee 100644 --- a/src/muz/rel/dl_vector_relation.h +++ b/src/muz/rel/dl_vector_relation.h @@ -397,6 +397,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index c4b6a65b2d..41bd91e31e 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -789,4 +789,4 @@ namespace datalog { } return nullptr; } -}; +} diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h index 33ce1ef984..1aee4595db 100644 --- a/src/muz/rel/karr_relation.h +++ b/src/muz/rel/karr_relation.h @@ -80,6 +80,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 20735cfcc0..4d963b1764 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -630,4 +630,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h index 8d48d2d37d..62f7566b80 100644 --- a/src/muz/rel/rel_context.h +++ b/src/muz/rel/rel_context.h @@ -125,5 +125,5 @@ namespace datalog { lbool saturate() override; }; -}; +} diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index f7a47f0e0e..5c133596be 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -147,6 +147,6 @@ namespace datalog { void disable_fast_pass() { m_disable_fast_pass = true; } }; -}; +} diff --git a/src/muz/spacer/spacer_concretize.cpp b/src/muz/spacer/spacer_concretize.cpp index 9700af1497..d73b3f638e 100644 --- a/src/muz/spacer/spacer_concretize.cpp +++ b/src/muz/spacer/spacer_concretize.cpp @@ -36,7 +36,7 @@ struct proc { } } }; -}; // namespace pattern_var_marker_ns +} // namespace pattern_var_marker_ns namespace spacer { void pob_concretizer::mark_pattern_vars() { pattern_var_marker_ns::proc proc(m_arith, m_var_marks); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 2691421463..0440a0d1e9 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -38,7 +38,7 @@ Notes: namespace datalog { class rule_set; class context; -}; // namespace datalog +} // namespace datalog namespace spacer { diff --git a/src/muz/spacer/spacer_convex_closure.h b/src/muz/spacer/spacer_convex_closure.h index c3676ddf51..da794c4a2d 100644 --- a/src/muz/spacer/spacer_convex_closure.h +++ b/src/muz/spacer/spacer_convex_closure.h @@ -155,7 +155,7 @@ class convex_closure { void add_row(const vector &point) { SASSERT(point.size() == dims()); m_data.add_row(point); - }; + } bool operator()() { return this->compute(); } bool compute(); diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp index 0fa1b74c63..3016b69fe9 100644 --- a/src/muz/spacer/spacer_farkas_learner.cpp +++ b/src/muz/spacer/spacer_farkas_learner.cpp @@ -99,7 +99,7 @@ bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e, ast_manag return false; } return true; -}; +} /** diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 0fa8ae932b..4653d62b91 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -327,4 +327,4 @@ void lemma_eq_generalizer::operator() (lemma_ref &lemma) { } -}; +} diff --git a/src/muz/spacer/spacer_mbc.cpp b/src/muz/spacer/spacer_mbc.cpp index 78c2799ec6..ee4eb0228f 100644 --- a/src/muz/spacer/spacer_mbc.cpp +++ b/src/muz/spacer/spacer_mbc.cpp @@ -66,7 +66,7 @@ public: } - void reset() {reset_partition();}; + void reset() {reset_partition();} void reset_partition() {m_current_part = UINT_MAX;} unsigned partition() {return m_current_part;} bool found_partition() {return m_current_part < UINT_MAX;} diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 383fda4183..eb4d780c98 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -845,4 +845,4 @@ namespace spacer { return res; } -}; +} diff --git a/src/muz/spacer/spacer_qe_project.h b/src/muz/spacer/spacer_qe_project.h index 37d0985406..b48b3aa321 100644 --- a/src/muz/spacer/spacer_qe_project.h +++ b/src/muz/spacer/spacer_qe_project.h @@ -43,5 +43,5 @@ namespace spacer_qe { void array_project_selects (model& model, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars); void array_project (model& model, app_ref_vector& arr_vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects = false); -}; +} diff --git a/src/muz/spacer/spacer_sym_mux.h b/src/muz/spacer/spacer_sym_mux.h index 4ddbeb3e44..549a25b21b 100644 --- a/src/muz/spacer/spacer_sym_mux.h +++ b/src/muz/spacer/spacer_sym_mux.h @@ -35,7 +35,7 @@ private: public: func_decl_ref m_main; func_decl_ref_vector m_variants; - sym_mux_entry(ast_manager &m) : m_main(m), m_variants(m) {}; + sym_mux_entry(ast_manager &m) : m_main(m), m_variants(m) {} }; typedef obj_map decl2entry_map; diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h index 27915b6c9a..fadfe04cfd 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.h +++ b/src/muz/spacer/spacer_unsat_core_learner.h @@ -41,7 +41,7 @@ namespace spacer { public: unsat_core_learner(ast_manager& m, iuc_proof& pr) : - m(m), m_pr(pr), m_unsat_core(m) {}; + m(m), m_pr(pr), m_unsat_core(m) {} virtual ~unsat_core_learner(); ast_manager& get_manager() {return m;} diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 40060629d0..36500eb770 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -35,7 +35,7 @@ Revision History: namespace spacer { unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx): - m(ctx.get_manager()), m_ctx(ctx) {}; + m(ctx.get_manager()), m_ctx(ctx) {} void unsat_core_plugin_lemma::compute_partial_core(proof* step) { SASSERT(m_ctx.is_a(step)); diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index b844cdd469..c327a1fdba 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/src/muz/spacer/spacer_unsat_core_plugin.h @@ -40,7 +40,7 @@ namespace spacer { class unsat_core_plugin_lemma : public unsat_core_plugin { public: - unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; + unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){} void compute_partial_core(proof* step) override; private: void add_lowest_split_to_core(proof* step) const; @@ -53,7 +53,7 @@ namespace spacer { bool use_constant_from_a=true) : unsat_core_plugin(learner), m_split_literals(split_literals), - m_use_constant_from_a(use_constant_from_a) {}; + m_use_constant_from_a(use_constant_from_a) {} void compute_partial_core(proof* step) override; private: bool m_split_literals; @@ -66,7 +66,7 @@ namespace spacer { class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin { public: - unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {}; + unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {} void compute_partial_core(proof* step) override; void finalize() override; protected: @@ -79,7 +79,7 @@ namespace spacer { class unsat_core_plugin_farkas_lemma_bounded : public unsat_core_plugin_farkas_lemma_optimized { public: - unsat_core_plugin_farkas_lemma_bounded(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin_farkas_lemma_optimized(learner, m) {}; + unsat_core_plugin_farkas_lemma_bounded(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin_farkas_lemma_optimized(learner, m) {} void finalize() override; }; diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index a775a7033d..d92d7614ca 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1306,7 +1306,7 @@ namespace tb { } return out << "unmatched instruction"; } -}; +} namespace datalog { @@ -1655,4 +1655,4 @@ namespace datalog { return m_imp->get_answer(); } -}; +} diff --git a/src/muz/tab/tab_context.h b/src/muz/tab/tab_context.h index d5bda040e2..4db6426230 100644 --- a/src/muz/tab/tab_context.h +++ b/src/muz/tab/tab_context.h @@ -39,5 +39,5 @@ namespace datalog { void display_certificate(std::ostream& out) const override; expr_ref get_answer() override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index f0efe2f3ac..5e163f087d 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -333,6 +333,6 @@ namespace datalog { return rules.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h index 12102af73e..04254275b0 100644 --- a/src/muz/transforms/dl_mk_array_blast.h +++ b/src/muz/transforms/dl_mk_array_blast.h @@ -69,6 +69,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/transforms/dl_mk_array_eq_rewrite.h b/src/muz/transforms/dl_mk_array_eq_rewrite.h index eabef4792f..62a9a4e0da 100644 --- a/src/muz/transforms/dl_mk_array_eq_rewrite.h +++ b/src/muz/transforms/dl_mk_array_eq_rewrite.h @@ -44,5 +44,5 @@ namespace datalog { -}; +} diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h index 71924288f9..4b8d8395b9 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.h +++ b/src/muz/transforms/dl_mk_array_instantiation.h @@ -116,5 +116,5 @@ namespace datalog { -}; +} diff --git a/src/muz/transforms/dl_mk_backwards.cpp b/src/muz/transforms/dl_mk_backwards.cpp index a47d0aeebb..b848167026 100644 --- a/src/muz/transforms/dl_mk_backwards.cpp +++ b/src/muz/transforms/dl_mk_backwards.cpp @@ -73,4 +73,4 @@ namespace datalog { return result.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_backwards.h b/src/muz/transforms/dl_mk_backwards.h index 4d1522e021..76aab80af3 100644 --- a/src/muz/transforms/dl_mk_backwards.h +++ b/src/muz/transforms/dl_mk_backwards.h @@ -30,6 +30,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 9ca982776d..d6f07915db 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -334,4 +334,4 @@ namespace datalog { return (*m_impl)(source); } -}; +} diff --git a/src/muz/transforms/dl_mk_bit_blast.h b/src/muz/transforms/dl_mk_bit_blast.h index 3681ecf380..0f7da47680 100644 --- a/src/muz/transforms/dl_mk_bit_blast.h +++ b/src/muz/transforms/dl_mk_bit_blast.h @@ -31,6 +31,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp index 97c4bb3aff..c7e3a1aede 100644 --- a/src/muz/transforms/dl_mk_coalesce.cpp +++ b/src/muz/transforms/dl_mk_coalesce.cpp @@ -194,6 +194,6 @@ namespace datalog { return rules.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_coalesce.h b/src/muz/transforms/dl_mk_coalesce.h index f94ce3465a..07962a006a 100644 --- a/src/muz/transforms/dl_mk_coalesce.h +++ b/src/muz/transforms/dl_mk_coalesce.h @@ -54,6 +54,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index d403f8b953..32b3f63ba5 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -166,4 +166,4 @@ namespace datalog { return m_result; } -}; +} diff --git a/src/muz/transforms/dl_mk_filter_rules.h b/src/muz/transforms/dl_mk_filter_rules.h index 3939c542ba..605fde256f 100644 --- a/src/muz/transforms/dl_mk_filter_rules.h +++ b/src/muz/transforms/dl_mk_filter_rules.h @@ -79,7 +79,7 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 1afb61febc..9d696b7729 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -615,4 +615,4 @@ namespace datalog { return res.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h index f1757dbce7..4658399380 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h @@ -102,6 +102,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp index 71370a0b50..669ea1f2cf 100644 --- a/src/muz/transforms/dl_mk_karr_invariants.cpp +++ b/src/muz/transforms/dl_mk_karr_invariants.cpp @@ -308,5 +308,5 @@ namespace datalog { -}; +} diff --git a/src/muz/transforms/dl_mk_karr_invariants.h b/src/muz/transforms/dl_mk_karr_invariants.h index 9ba579a603..e33ff851cc 100644 --- a/src/muz/transforms/dl_mk_karr_invariants.h +++ b/src/muz/transforms/dl_mk_karr_invariants.h @@ -68,6 +68,6 @@ namespace datalog { }; -}; +} diff --git a/src/muz/transforms/dl_mk_loop_counter.cpp b/src/muz/transforms/dl_mk_loop_counter.cpp index a20224eb29..245ad0b2d2 100644 --- a/src/muz/transforms/dl_mk_loop_counter.cpp +++ b/src/muz/transforms/dl_mk_loop_counter.cpp @@ -153,4 +153,4 @@ namespace datalog { return result; } -}; +} diff --git a/src/muz/transforms/dl_mk_loop_counter.h b/src/muz/transforms/dl_mk_loop_counter.h index b2758df67a..d74a73ffe3 100644 --- a/src/muz/transforms/dl_mk_loop_counter.h +++ b/src/muz/transforms/dl_mk_loop_counter.h @@ -43,6 +43,6 @@ namespace datalog { rule_set * revert(rule_set const& source); }; -}; +} diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index 395aa0d693..f8f34827fd 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -375,5 +375,5 @@ namespace datalog { result->add_rule(back_to_goal_rule); return result.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_magic_sets.h b/src/muz/transforms/dl_mk_magic_sets.h index 3a8a92580d..4e40e057c1 100644 --- a/src/muz/transforms/dl_mk_magic_sets.h +++ b/src/muz/transforms/dl_mk_magic_sets.h @@ -128,6 +128,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_magic_symbolic.cpp b/src/muz/transforms/dl_mk_magic_symbolic.cpp index ed05d2247e..054abf5e7c 100644 --- a/src/muz/transforms/dl_mk_magic_symbolic.cpp +++ b/src/muz/transforms/dl_mk_magic_symbolic.cpp @@ -130,4 +130,4 @@ namespace datalog { return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m); } -}; +} diff --git a/src/muz/transforms/dl_mk_magic_symbolic.h b/src/muz/transforms/dl_mk_magic_symbolic.h index ac29194bcc..1003b2e318 100644 --- a/src/muz/transforms/dl_mk_magic_symbolic.h +++ b/src/muz/transforms/dl_mk_magic_symbolic.h @@ -32,6 +32,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index b2ec2fb297..a12b230bc3 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -361,4 +361,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.h b/src/muz/transforms/dl_mk_quantifier_abstraction.h index 33c70c08b2..40669b02a3 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.h +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.h @@ -55,6 +55,6 @@ namespace datalog { -}; +} diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 9e567c902b..bc1af9c585 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -289,6 +289,6 @@ namespace datalog { } -}; +} diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.h b/src/muz/transforms/dl_mk_quantifier_instantiation.h index 716de11f02..c27058e30f 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.h +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.h @@ -65,6 +65,6 @@ namespace datalog { -}; +} diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 340b0ac569..94c174c1db 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -878,4 +878,4 @@ namespace datalog { return res.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h index c0693fde06..adab914e08 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.h +++ b/src/muz/transforms/dl_mk_rule_inliner.h @@ -199,6 +199,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index b6178bb817..a20b1cbdc2 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -235,4 +235,4 @@ namespace datalog { return result; } -}; +} diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h index fcbf4c2265..39ab3cdce2 100644 --- a/src/muz/transforms/dl_mk_scale.h +++ b/src/muz/transforms/dl_mk_scale.h @@ -45,6 +45,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index ecdf3ab23a..6cfb1e8add 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -854,5 +854,5 @@ namespace datalog { return result.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_slice.h b/src/muz/transforms/dl_mk_slice.h index 807c6dac4e..e619bc90b7 100644 --- a/src/muz/transforms/dl_mk_slice.h +++ b/src/muz/transforms/dl_mk_slice.h @@ -106,6 +106,6 @@ namespace datalog { obj_map const& get_predicates() { return m_predicates; } }; -}; +} diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index c71fddf9ee..c0e499d06e 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -357,4 +357,4 @@ namespace datalog { return res.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_subsumption_checker.h b/src/muz/transforms/dl_mk_subsumption_checker.h index 87c5c8f2e5..e2b21da694 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.h +++ b/src/muz/transforms/dl_mk_subsumption_checker.h @@ -86,6 +86,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index 81c01d7fcc..261768bf7a 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -373,4 +373,4 @@ namespace datalog { return rules; } -}; +} diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 3f3657cae7..c81a3c9c6d 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -128,5 +128,5 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp index 15b619ff85..161af7cea9 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.cpp +++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp @@ -400,4 +400,4 @@ namespace datalog { } -}; +} diff --git a/src/muz/transforms/dl_mk_unbound_compressor.h b/src/muz/transforms/dl_mk_unbound_compressor.h index 63463dc5ce..9102837bf4 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.h +++ b/src/muz/transforms/dl_mk_unbound_compressor.h @@ -88,6 +88,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/muz/transforms/dl_mk_unfold.cpp b/src/muz/transforms/dl_mk_unfold.cpp index 6a1ae1535e..2d71aafcef 100644 --- a/src/muz/transforms/dl_mk_unfold.cpp +++ b/src/muz/transforms/dl_mk_unfold.cpp @@ -59,5 +59,5 @@ namespace datalog { return rules.detach(); } -}; +} diff --git a/src/muz/transforms/dl_mk_unfold.h b/src/muz/transforms/dl_mk_unfold.h index abba64c897..6687e7fadf 100644 --- a/src/muz/transforms/dl_mk_unfold.h +++ b/src/muz/transforms/dl_mk_unfold.h @@ -46,6 +46,6 @@ namespace datalog { rule_set * operator()(rule_set const & source) override; }; -}; +} diff --git a/src/nlsat/nlsat_assignment.h b/src/nlsat/nlsat_assignment.h index d96c8099e9..73d565142e 100644 --- a/src/nlsat/nlsat_assignment.h +++ b/src/nlsat/nlsat_assignment.h @@ -97,5 +97,5 @@ namespace nlsat { bool contains(var x) const override { return x != m_y && m_assignment.is_assigned(x); } anum const & operator()(var x) const override { return m_assignment.value(x); } }; -}; +} diff --git a/src/nlsat/nlsat_clause.cpp b/src/nlsat/nlsat_clause.cpp index 9543c44978..270617d057 100644 --- a/src/nlsat/nlsat_clause.cpp +++ b/src/nlsat/nlsat_clause.cpp @@ -49,4 +49,4 @@ namespace nlsat { return false; } -}; +} diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h index 91467303cd..52afece639 100644 --- a/src/nlsat/nlsat_clause.h +++ b/src/nlsat/nlsat_clause.h @@ -66,5 +66,5 @@ namespace nlsat { typedef ptr_vector clause_vector; -}; +} diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 6520754163..9f97332bb7 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -699,4 +699,4 @@ namespace nlsat { void evaluator::pop(unsigned num_scopes) { // do nothing } -}; +} diff --git a/src/nlsat/nlsat_evaluator.h b/src/nlsat/nlsat_evaluator.h index d2db3f41a6..2ea5bdc4db 100644 --- a/src/nlsat/nlsat_evaluator.h +++ b/src/nlsat/nlsat_evaluator.h @@ -57,5 +57,5 @@ namespace nlsat { void pop(unsigned num_scopes); }; -}; +} diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index d9a0bf131b..0827af809e 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1784,7 +1784,7 @@ namespace nlsat { m_imp->test_root_literal(k, y, i, p, result); } -}; +} #ifdef Z3DEBUG #include void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) { diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 60a7c53e18..44279e8bba 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -108,4 +108,4 @@ namespace nlsat { void test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result); }; -}; +} diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp index 160c8afb66..580aae781a 100644 --- a/src/nlsat/nlsat_interval_set.cpp +++ b/src/nlsat/nlsat_interval_set.cpp @@ -794,4 +794,4 @@ namespace nlsat { out << "*"; return out; } -}; +} diff --git a/src/nlsat/nlsat_interval_set.h b/src/nlsat/nlsat_interval_set.h index 263ab8a103..4efd0c3678 100644 --- a/src/nlsat/nlsat_interval_set.h +++ b/src/nlsat/nlsat_interval_set.h @@ -118,5 +118,5 @@ namespace nlsat { return out; } -}; +} diff --git a/src/nlsat/nlsat_justification.h b/src/nlsat/nlsat_justification.h index d9567ebf93..55501a8aff 100644 --- a/src/nlsat/nlsat_justification.h +++ b/src/nlsat/nlsat_justification.h @@ -106,5 +106,5 @@ namespace nlsat { a.deallocate(obj_sz, ptr); } } -}; +} diff --git a/src/nlsat/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h index d67805c156..ee3a4acd9c 100644 --- a/src/nlsat/nlsat_scoped_literal_vector.h +++ b/src/nlsat/nlsat_scoped_literal_vector.h @@ -107,5 +107,5 @@ namespace nlsat { operator literal const &() const { return m_lit; } void neg() { m_lit.neg(); } }; -}; +} diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp index e1c10d5f51..08e5c3d58b 100644 --- a/src/nlsat/nlsat_simplify.cpp +++ b/src/nlsat/nlsat_simplify.cpp @@ -826,4 +826,4 @@ namespace nlsat { (*m_imp)(); } -}; +} diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6a656b46d4..074b159484 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -4784,4 +4784,4 @@ namespace nlsat { unsigned solver::lws_spt_threshold() const { return m_imp->m_lws_spt_threshold; } bool solver::lws_witness_subs_lc() const { return m_imp->m_lws_witness_subs_lc; } bool solver::lws_witness_subs_disc() const { return m_imp->m_lws_witness_subs_disc; } -}; +} diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index b6e0034733..21d9e42538 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -316,4 +316,4 @@ namespace nlsat { }; -}; +} diff --git a/src/nlsat/nlsat_types.cpp b/src/nlsat/nlsat_types.cpp index 42c41cec14..f2fe6f4287 100644 --- a/src/nlsat/nlsat_types.cpp +++ b/src/nlsat/nlsat_types.cpp @@ -67,4 +67,4 @@ namespace nlsat { return a1->m_kind == a2->m_kind && a1->m_x == a2->m_x && a1->m_i == a2->m_i && a1->m_p == a2->m_p; } -}; +} diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index be8f625c92..ee3b2935bf 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -26,7 +26,7 @@ Revision History: namespace algebraic_numbers { class anum; class manager; -}; +} namespace nlsat { #define NLSAT_VB_LVL 10 @@ -204,5 +204,5 @@ namespace nlsat { if (s == 0) return 0; return 1; } -}; +} diff --git a/src/opt/maxcore.h b/src/opt/maxcore.h index 283fee8506..f16904a21b 100644 --- a/src/opt/maxcore.h +++ b/src/opt/maxcore.h @@ -33,5 +33,5 @@ namespace opt { maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector& soft); -}; +} diff --git a/src/opt/maxlex.h b/src/opt/maxlex.h index fc30b1fd88..4cfa35fe49 100644 --- a/src/opt/maxlex.h +++ b/src/opt/maxlex.h @@ -26,5 +26,5 @@ namespace opt { maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector& soft); -}; +} diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index d1d1506714..665b739783 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -380,12 +380,12 @@ namespace opt { params_ref& params() override { return m_params; } void enable_sls(bool force) override { } // no op symbol const& maxsat_engine() const override { return m_maxsat_engine; } - void get_base_model(model_ref& _m) override { _m = m_model; }; + void get_base_model(model_ref& _m) override { _m = m_model; } smt::context& smt_context() override { throw default_exception("stand-alone maxsat context does not support wmax"); } unsigned num_objectives() override { return 1; } - bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; }; + bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; } void set_model(model_ref& _m) override { m_model = _m; } void model_updated(model* mdl) override { } // no-op rational adjust(unsigned id, rational const& r) override { @@ -419,4 +419,4 @@ namespace opt { } return r; } -}; +} diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 7e75cde450..ca73437d5d 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -211,5 +211,5 @@ namespace opt { model_ref get_model() { return m_model; } }; -}; +} diff --git a/src/opt/opt_cores.cpp b/src/opt/opt_cores.cpp index 049a64da23..7948cdd502 100644 --- a/src/opt/opt_cores.cpp +++ b/src/opt/opt_cores.cpp @@ -394,4 +394,4 @@ namespace opt { } } -}; +} diff --git a/src/opt/opt_cores.h b/src/opt/opt_cores.h index 6dda34fd78..7ba4166913 100644 --- a/src/opt/opt_cores.h +++ b/src/opt/opt_cores.h @@ -68,4 +68,4 @@ namespace opt { void updt_params(params_ref& p); }; -}; +} diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp index 019a60b532..5133ac8c6c 100644 --- a/src/opt/opt_lns.cpp +++ b/src/opt/opt_lns.cpp @@ -269,4 +269,4 @@ namespace opt { return r; } -}; +} diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h index 1bc27f9b13..4dc24d05c6 100644 --- a/src/opt/opt_lns.h +++ b/src/opt/opt_lns.h @@ -77,4 +77,4 @@ namespace opt { void set_conflicts(unsigned c) { m_max_conflicts = c; } unsigned climb(model_ref& mdl); }; -}; +} diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp index 2e1b780707..3a4a712eb0 100644 --- a/src/opt/opt_preprocess.cpp +++ b/src/opt/opt_preprocess.cpp @@ -238,4 +238,4 @@ namespace opt { return false; return true; } -}; +} diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h index 71e06eb2c6..21c9efde9c 100644 --- a/src/opt/opt_preprocess.h +++ b/src/opt/opt_preprocess.h @@ -40,4 +40,4 @@ namespace opt { preprocess(solver& s); bool operator()(vector& soft, rational& lower); }; -}; +} diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index b1198a7f90..385392a1dc 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -93,5 +93,5 @@ namespace opt { }; -}; +} diff --git a/src/opt/pb_sls.h b/src/opt/pb_sls.h index 6537574698..b511a45efa 100644 --- a/src/opt/pb_sls.h +++ b/src/opt/pb_sls.h @@ -44,5 +44,5 @@ namespace smt { }; -}; +} diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index f7bfe6ed53..15f1721b16 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -3333,7 +3333,7 @@ namespace smt2 { }; void free_parser(parser * p) { dealloc(p); } -}; +} bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) { smt2::parser p(ctx, is, interactive, ps, filename); diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 3ab95ab40c..d6edcd0fb0 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -403,5 +403,5 @@ namespace smt2 { m_bend = 0; next(); } -}; +} diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h index dd1aa04c06..fa37870ae3 100644 --- a/src/parsers/smt2/smt2scanner.h +++ b/src/parsers/smt2/smt2scanner.h @@ -104,6 +104,6 @@ namespace smt2 { char const * cached_str(unsigned begin, unsigned end); }; -}; +} diff --git a/src/qe/mbp/mbp_arith.h b/src/qe/mbp/mbp_arith.h index 1323032eba..936b08dbd1 100644 --- a/src/qe/mbp/mbp_arith.h +++ b/src/qe/mbp/mbp_arith.h @@ -51,5 +51,5 @@ namespace mbp { bool arith_project(model& model, app* var, expr_ref_vector& lits); -}; +} diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 2c3e6ddf3b..d6daef7b9f 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -1500,4 +1500,4 @@ namespace mbp { } -}; +} diff --git a/src/qe/mbp/mbp_arrays.h b/src/qe/mbp/mbp_arrays.h index ed06ba78b3..1dced44c8c 100644 --- a/src/qe/mbp/mbp_arrays.h +++ b/src/qe/mbp/mbp_arrays.h @@ -40,5 +40,5 @@ namespace mbp { }; -}; +} diff --git a/src/qe/mbp/mbp_datatypes.h b/src/qe/mbp/mbp_datatypes.h index 28f93089d5..8f667e7b36 100644 --- a/src/qe/mbp/mbp_datatypes.h +++ b/src/qe/mbp/mbp_datatypes.h @@ -39,5 +39,5 @@ namespace mbp { }; -}; +} diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h index 59515e9bd9..1be5cd3387 100644 --- a/src/qe/mbp/mbp_euf.h +++ b/src/qe/mbp/mbp_euf.h @@ -31,5 +31,5 @@ namespace mbp { }; -}; +} diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 5e7dae8c78..67cf396287 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -69,7 +69,7 @@ namespace mbp { virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } virtual family_id get_family_id() { return null_family_id; } - virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; + virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } /** \brief project vars modulo model, return set of definitions for eliminated variables. diff --git a/src/qe/mbp/mbp_tg_plugins.h b/src/qe/mbp/mbp_tg_plugins.h index 3850f11ca1..671f3701ce 100644 --- a/src/qe/mbp/mbp_tg_plugins.h +++ b/src/qe/mbp/mbp_tg_plugins.h @@ -26,9 +26,9 @@ class mbp_tg_plugin { public: // iterate through all terms in m_tg and apply all theory MBP rules once // returns true if any rules were applied - virtual bool apply() { return false; }; + virtual bool apply() { return false; } virtual ~mbp_tg_plugin() = default; - virtual void use_model() { }; - virtual void get_new_vars(app_ref_vector*&) { }; - virtual family_id get_family_id() const { return null_family_id; }; + virtual void use_model() { } + virtual void get_new_vars(app_ref_vector*&) { } + virtual family_id get_family_id() const { return null_family_id; } }; diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index 7e68f33fbe..eda48e607f 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -2022,6 +2022,6 @@ namespace nlarith { void util::get_sign_branches(literal_set& lits, eval& ev, ptr_vector& branches) { m_imp->get_sign_branches(lits, ev, branches); } -}; +} diff --git a/src/qe/nlarith_util.h b/src/qe/nlarith_util.h index dccc4f606f..8f2137a155 100644 --- a/src/qe/nlarith_util.h +++ b/src/qe/nlarith_util.h @@ -143,5 +143,5 @@ namespace nlarith { }; -}; +} diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 263dad43cb..8e168e62fd 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -955,7 +955,7 @@ namespace qe { return alloc(nlqsat, m, m_mode, m_params); } }; -}; +} tactic * mk_nlqsat_tactic(ast_manager & m, params_ref const& p) { return alloc(qe::nlqsat, m, qe::qsat_t, p); diff --git a/src/qe/qe.h b/src/qe/qe.h index 2fd36596d9..6f07b157bf 100644 --- a/src/qe/qe.h +++ b/src/qe/qe.h @@ -367,6 +367,6 @@ namespace qe { }; -}; +} diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index ba8f5faa3b..aab03e9039 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -613,4 +613,4 @@ namespace qe { return pogo(pA, pB, itp); } -}; +} diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 93f7df88d4..18c33cb51a 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -156,4 +156,4 @@ namespace qe { lbool pogo(solver_factory& sf, expr* a, expr* b, expr_ref& itp); }; -}; +} diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 86234962c0..d5ca03096c 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1503,7 +1503,7 @@ namespace qe { void qmax::collect_statistics(statistics& st) const { m_imp->m_qsat.collect_statistics(st); } -}; +} tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) { return alloc(qe::qsat, m, p, qe::qsat_sat); diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h index f6be01ef82..9f43048272 100644 --- a/src/sat/dimacs.h +++ b/src/sat/dimacs.h @@ -97,10 +97,10 @@ namespace dimacs { bool operator!=(iterator const& other) const { return m_eof != other.m_eof; } }; - iterator begin() { return iterator(*this, false); }; + iterator begin() { return iterator(*this, false); } iterator end() { return iterator(*this, true); } void set_read_theory(std::function& r) { m_read_theory_id = r; } }; -}; +} diff --git a/src/sat/sat_anf_simplifier.h b/src/sat/sat_anf_simplifier.h index 0f140d5ab4..8bd30bbe73 100644 --- a/src/sat/sat_anf_simplifier.h +++ b/src/sat/sat_anf_simplifier.h @@ -28,7 +28,7 @@ namespace dd { class pdd; class solver; -}; +} namespace sat { diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 0aed69d616..11a85b79e4 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -497,4 +497,4 @@ namespace sat { m_tr = 0; } -}; +} diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index 20a561214e..7be980477e 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -106,5 +106,5 @@ namespace sat { inline void dec(unsigned c) { m_counter -= c; } }; -}; +} diff --git a/src/sat/sat_bcd.cpp b/src/sat/sat_bcd.cpp index 0b9792ad68..99e0bd4f8f 100644 --- a/src/sat/sat_bcd.cpp +++ b/src/sat/sat_bcd.cpp @@ -353,4 +353,4 @@ namespace sat { m_R.reset(); } -}; +} diff --git a/src/sat/sat_bcd.h b/src/sat/sat_bcd.h index 643a8b8ad4..52d11ba5ed 100644 --- a/src/sat/sat_bcd.h +++ b/src/sat/sat_bcd.h @@ -73,5 +73,5 @@ namespace sat { void operator()(union_find<>& uf); }; -}; +} diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 96ab78cb1a..9469f8431c 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -281,4 +281,4 @@ namespace sat { -}; +} diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 8ee185f16a..a30231c7b0 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -87,5 +87,5 @@ namespace sat { void display(std::ostream& out) const; }; -}; +} diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index c59ce72891..6af39f4cd6 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -249,4 +249,4 @@ namespace sat { return out; } -}; +} diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 0129febbf8..852508a123 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -198,5 +198,5 @@ namespace sat { std::ostream & operator<<(std::ostream & out, clause_wrapper const & c); -}; +} diff --git a/src/sat/sat_clause_set.cpp b/src/sat/sat_clause_set.cpp index c223009d6e..13e08eb54c 100644 --- a/src/sat/sat_clause_set.cpp +++ b/src/sat/sat_clause_set.cpp @@ -88,4 +88,4 @@ namespace sat { return true; } -}; +} diff --git a/src/sat/sat_clause_set.h b/src/sat/sat_clause_set.h index aa0be6b62d..1a2ad3e756 100644 --- a/src/sat/sat_clause_set.h +++ b/src/sat/sat_clause_set.h @@ -50,5 +50,5 @@ namespace sat { bool check_invariant() const; }; -}; +} diff --git a/src/sat/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp index 347e49db99..b00e26e78e 100644 --- a/src/sat/sat_clause_use_list.cpp +++ b/src/sat/sat_clause_use_list.cpp @@ -54,4 +54,4 @@ namespace sat { m_clauses.shrink(m_j); } -}; +} diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index 14961a2236..63b5879568 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -134,5 +134,5 @@ namespace sat { } }; -}; +} diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 46b94b52c4..97abf11be5 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -230,4 +230,4 @@ namespace sat { st.update("sat elim literals", m_elim_literals); } -}; +} diff --git a/src/sat/sat_cleaner.h b/src/sat/sat_cleaner.h index 08d73029af..557b8a0d0b 100644 --- a/src/sat/sat_cleaner.h +++ b/src/sat/sat_cleaner.h @@ -48,5 +48,5 @@ namespace sat { void dec() { m_cleanup_counter--; } }; -}; +} diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 3dfb67f2a4..cf01d39eea 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -259,4 +259,4 @@ namespace sat { sat_params::collect_param_descrs(r); } -}; +} diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 83241fe88a..57076bf6ab 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -196,5 +196,5 @@ namespace sat { static void collect_param_descrs(param_descrs & d); }; -}; +} diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index f761ef9264..ea6ebd495b 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -306,4 +306,4 @@ namespace sat { } (*this)(roots, to_elim); } -}; +} diff --git a/src/sat/sat_elim_eqs.h b/src/sat/sat_elim_eqs.h index 8bfc2c4578..c5000f108b 100644 --- a/src/sat/sat_elim_eqs.h +++ b/src/sat/sat_elim_eqs.h @@ -47,5 +47,5 @@ namespace sat { void operator()(union_find<>& uf); }; -}; +} diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index b42cc33e21..0acfa4ea31 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -77,7 +77,7 @@ namespace sat { solver const& s() const { return *m_solver; } symbol const& name() const { return m_name; } - virtual void set_lookahead(lookahead* s) {}; + virtual void set_lookahead(lookahead* s) {} class scoped_drating { extension& ext; public: @@ -138,5 +138,5 @@ namespace sat { virtual std::string reason_unknown() { return "unknown"; } }; -}; +} diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index b10d243c23..54b0d63d79 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -221,4 +221,4 @@ namespace sat { VERIFY(check_disjoint_clauses()); return true; } -}; +} diff --git a/src/sat/sat_integrity_checker.h b/src/sat/sat_integrity_checker.h index bc7fecf68d..3d8ecd921d 100644 --- a/src/sat/sat_integrity_checker.h +++ b/src/sat/sat_integrity_checker.h @@ -42,4 +42,4 @@ namespace sat { bool check_disjoint_clauses() const; bool operator()() const; }; -}; +} diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h index f83173aa7d..ecffa096fc 100644 --- a/src/sat/sat_justification.h +++ b/src/sat/sat_justification.h @@ -72,5 +72,5 @@ namespace sat { return out; } -}; +} diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 87757ba59d..0aaaf6f04c 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -25,7 +25,7 @@ Notes: namespace pb { class solver; -}; +} namespace sat { diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 67136d79ab..d1b2d38f06 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -455,4 +455,4 @@ namespace sat { } } -}; +} diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 170886aa69..1d44db51ac 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -153,4 +153,4 @@ namespace sat { return out; } -}; +} diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index 672e90185f..b6845c30c5 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -61,5 +61,5 @@ namespace sat { }; }; -}; +} diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 7d5c022ff1..8c9b897098 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -276,5 +276,5 @@ namespace sat { return copied; } -}; +} diff --git a/src/sat/sat_parallel.h b/src/sat/sat_parallel.h index 0fbf4f05d0..948eeaa3f0 100644 --- a/src/sat/sat_parallel.h +++ b/src/sat/sat_parallel.h @@ -112,5 +112,5 @@ namespace sat { bool copy_solver(solver& s); }; -}; +} diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index f1830623a3..b29e9513b1 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -322,4 +322,4 @@ namespace sat { void probing::reset_statistics() { m_num_assigned = 0; } -}; +} diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h index 4b13d6afdd..a7eac7ba8b 100644 --- a/src/sat/sat_probing.h +++ b/src/sat/sat_probing.h @@ -91,5 +91,5 @@ namespace sat { void dec(unsigned c) { m_counter -= c; } }; -}; +} diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 8308a7ea59..21ceb3c6c5 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -282,4 +282,4 @@ namespace sat { sat_scc_params::collect_param_descrs(d); } -}; +} diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index af239c53d9..5b2f0dd260 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -65,5 +65,5 @@ namespace sat { int get_right(literal l) const { return m_big.get_right(l); } bool connected(literal u, literal v) const { return m_big.connected(u, v); } }; -}; +} diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 18e6288208..79c8a723c6 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -2148,4 +2148,4 @@ namespace sat { m_num_bca = 0; m_num_ate = 0; } -}; +} diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index e32c52e4a1..0dd85c6b85 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -250,5 +250,5 @@ namespace sat { bool need_cleanup() const { return m_need_cleanup; } }; -}; +} diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0a109bd0c5..634b09830e 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -4865,4 +4865,4 @@ namespace sat { return true; } -}; +} diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 66352387a2..a64b8fa614 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -48,7 +48,7 @@ Revision History: namespace pb { class solver; -}; +} namespace sat { @@ -895,4 +895,4 @@ namespace sat { std::ostream & operator<<(std::ostream & out, mk_stat const & stat); -}; +} diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index cc0e6e0233..905f9739fd 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -49,7 +49,7 @@ namespace sat { // optional support for user-scopes. Not relevant for sat_tactic integration. // it is only relevant for incremental mode SAT, which isn't wrapped (yet) virtual void user_push() { throw default_exception("optional API not supported"); } - virtual void user_pop(unsigned num_scopes) {}; + virtual void user_pop(unsigned num_scopes) {} virtual unsigned num_user_scopes() const { return 0;} virtual unsigned num_scopes() const { return 0; } @@ -58,5 +58,5 @@ namespace sat { virtual extension* get_extension() const { return nullptr; } virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); } }; -}; +} diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index b027d4f2e1..ce24521cae 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -106,7 +106,7 @@ namespace sat { int m_orig; const proof_hint* m_hint; public: - status(st s, int o, proof_hint const* ps = nullptr) : m_st(s), m_orig(o), m_hint(ps) {}; + status(st s, int o, proof_hint const* ps = nullptr) : m_st(s), m_orig(o), m_hint(ps) {} status(status const& s) : m_st(s.m_st), m_orig(s.m_orig), m_hint(s.m_hint) {} status(status&& s) noexcept { m_st = st::asserted; m_orig = -1; std::swap(m_st, s.m_st); std::swap(m_orig, s.m_orig); std::swap(m_hint, s.m_hint); } status& operator=(status const& other) { m_st = other.m_st; m_orig = other.m_orig; return *this; } @@ -170,7 +170,7 @@ namespace sat { }; -}; +} diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index 5573212f53..865a4b06dc 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -110,4 +110,4 @@ namespace sat { return out; } -}; +} diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 6d91434dba..4e44bbc1b1 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -125,5 +125,5 @@ namespace sat { std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext); void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist); -}; +} diff --git a/src/sat/smt/arith_value.cpp b/src/sat/smt/arith_value.cpp index fb66bdaefd..f6e1e68c79 100644 --- a/src/sat/smt/arith_value.cpp +++ b/src/sat/smt/arith_value.cpp @@ -142,4 +142,4 @@ namespace arith { #endif -}; +} diff --git a/src/sat/smt/arith_value.h b/src/sat/smt/arith_value.h index b858ff8965..89d7c69a36 100644 --- a/src/sat/smt/arith_value.h +++ b/src/sat/smt/arith_value.h @@ -49,4 +49,4 @@ namespace arith { expr_ref get_fixed(expr* e); #endif }; -}; +} diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h index aab4053a28..259e1bfbf8 100644 --- a/src/sat/smt/bv_ackerman.h +++ b/src/sat/smt/bv_ackerman.h @@ -78,4 +78,4 @@ namespace bv { void propagate(); }; -}; +} diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index af3c4abe92..aeda79b5be 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -308,7 +308,7 @@ namespace bv { tmp = m.mk_or(literal2expr(b), tmp); xs.push_back(tmp); } - }; + } /** * The i'th bit in xs is 1 if the least significant bit of x is i or lower. @@ -324,7 +324,7 @@ namespace bv { tmp = m.mk_or(literal2expr(b), tmp); xs.push_back(tmp); } - }; + } /** * Check non-overflow of unsigned multiplication. diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 3ac6da3033..09299bbca6 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -521,7 +521,7 @@ namespace bv { } func_decl* f = m.mk_func_decl(th, sorts.size(), sorts.data(), proof); return m.mk_app(f, args); - }; + } void solver::asserted(literal l) { atom* a = get_bv2a(l.var()); diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h index 846ddb8ae6..37ed814153 100644 --- a/src/sat/smt/euf_ackerman.h +++ b/src/sat/smt/euf_ackerman.h @@ -87,4 +87,4 @@ namespace euf { void propagate(); }; -}; +} diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 69017679c3..72fd6ebabb 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -576,7 +576,7 @@ namespace euf { return p.display(out); } -}; +} inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) { return s.display(out); diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 7f39cd5ed3..238c7d57cc 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -440,4 +440,4 @@ namespace fpa { } } -}; +} diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 39094b9682..2b8468e16b 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -330,7 +330,7 @@ namespace intblast { } } return r; - }; + } bool solver::is_bv(sat::literal lit) { expr* e = ctx.bool_var2expr(lit.var()); diff --git a/src/sat/smt/pb_constraint.h b/src/sat/smt/pb_constraint.h index 4c6f69e077..15e885ae2d 100644 --- a/src/sat/smt/pb_constraint.h +++ b/src/sat/smt/pb_constraint.h @@ -100,7 +100,7 @@ namespace pb { virtual bool validate_unit_propagation(solver_interface const& s, literal alit) const = 0; - virtual bool is_watching(literal l) const { UNREACHABLE(); return false; }; + virtual bool is_watching(literal l) const { UNREACHABLE(); return false; } virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); } virtual void swap(unsigned i, unsigned j) noexcept { UNREACHABLE(); } virtual literal get_lit(unsigned i) const { UNREACHABLE(); return sat::null_literal; } diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 460a051ab2..fd91199bf7 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -3795,6 +3795,6 @@ namespace pb { return true; } -}; +} diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index 67c55c9d58..c73ad8f9ef 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -418,5 +418,5 @@ namespace pb { }; -}; +} diff --git a/src/sat/smt/q_queue.h b/src/sat/smt/q_queue.h index 3750ee31ba..256061aab7 100644 --- a/src/sat/smt/q_queue.h +++ b/src/sat/smt/q_queue.h @@ -26,7 +26,7 @@ Author: namespace euf { class solver; -}; +} namespace q { diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 4bdfcf064f..df56bc1c98 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -169,4 +169,4 @@ namespace user_solver { euf::th_solver* clone(euf::solver& ctx) override; }; -}; +} diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 2bbe7a4e1d..ba578b1850 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -278,5 +278,5 @@ namespace smt { out << "eq_adapter: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n"; } } -}; +} diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h index 7b1c068761..b719d7e451 100644 --- a/src/smt/arith_eq_adapter.h +++ b/src/smt/arith_eq_adapter.h @@ -86,6 +86,6 @@ namespace smt { void collect_statistics(::statistics & st) const; void display_already_processed(std::ostream & out) const; }; -}; +} diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 691bd7fc07..12fcc9754d 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -587,4 +587,4 @@ namespace smt { } #endif -}; +} diff --git a/src/smt/dyn_ack.h b/src/smt/dyn_ack.h index e04f78fd36..6d239d27b2 100644 --- a/src/smt/dyn_ack.h +++ b/src/smt/dyn_ack.h @@ -130,6 +130,6 @@ namespace smt { #endif }; -}; +} diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp index d41e01573f..6a7d176965 100644 --- a/src/smt/fingerprints.cpp +++ b/src/smt/fingerprints.cpp @@ -165,4 +165,4 @@ namespace smt { #endif -}; +} diff --git a/src/smt/fingerprints.h b/src/smt/fingerprints.h index dc1863041e..93f6a115e7 100644 --- a/src/smt/fingerprints.h +++ b/src/smt/fingerprints.h @@ -76,6 +76,6 @@ namespace smt { bool slow_contains(void const * data, unsigned data_hash, unsigned num_args, enode * const * args) const; #endif }; -}; +} diff --git a/src/smt/mam.h b/src/smt/mam.h index e7051b3f76..758d9c684f 100644 --- a/src/smt/mam.h +++ b/src/smt/mam.h @@ -69,5 +69,5 @@ namespace smt { }; mam * mk_mam(context & ctx); -}; +} diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 905644354d..cb803d7559 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -518,5 +518,5 @@ namespace smt { #endif } -}; +} diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h index 13878a158b..7ae92fd16b 100644 --- a/src/smt/qi_queue.h +++ b/src/smt/qi_queue.h @@ -101,6 +101,6 @@ namespace smt { m_on_binding = on_binding; } }; -}; +} diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 525f6b3db3..f16ae6b55f 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -105,5 +105,5 @@ namespace smt { }; -}; +} diff --git a/src/smt/seq_offset_eq.h b/src/smt/seq_offset_eq.h index 669d63b7fd..ee308d5161 100644 --- a/src/smt/seq_offset_eq.h +++ b/src/smt/seq_offset_eq.h @@ -53,5 +53,5 @@ namespace smt { void pop_scope_eh(unsigned num_scopes); }; -}; +} diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index dd1c474b31..bba4d30eaa 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -214,4 +214,4 @@ namespace smt { }; -}; +} diff --git a/src/smt/smt_almost_cg_table.cpp b/src/smt/smt_almost_cg_table.cpp index f50f34dd6f..e97aa32d08 100644 --- a/src/smt/smt_almost_cg_table.cpp +++ b/src/smt/smt_almost_cg_table.cpp @@ -124,4 +124,4 @@ namespace smt { return result; } -}; +} diff --git a/src/smt/smt_almost_cg_table.h b/src/smt/smt_almost_cg_table.h index 6b0cc66526..f7b89af324 100644 --- a/src/smt/smt_almost_cg_table.h +++ b/src/smt/smt_almost_cg_table.h @@ -65,6 +65,6 @@ namespace smt { bool empty() const { return m_table.empty(); } }; -}; +} diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index 806598e76f..6c187b9482 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -169,4 +169,4 @@ namespace smt { return l_undef; return m_thr->check_lp_feasible(ineqs, lit_core, eq_core); } -}; +} diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index 7e351e43d5..3c2339887d 100644 --- a/src/smt/smt_arith_value.h +++ b/src/smt/smt_arith_value.h @@ -51,4 +51,4 @@ namespace smt { lbool check_lp_feasible(vector> &ineqs, literal_vector &lit_core, enode_pair_vector &eq_core); }; -}; +} diff --git a/src/smt/smt_b_justification.h b/src/smt/smt_b_justification.h index ae01a389d9..cbf399ef79 100644 --- a/src/smt/smt_b_justification.h +++ b/src/smt/smt_b_justification.h @@ -99,6 +99,6 @@ namespace smt { } typedef std::pair justified_literal; -}; +} diff --git a/src/smt/smt_bool_var_data.h b/src/smt/smt_bool_var_data.h index 68d7a8d45f..129a864897 100644 --- a/src/smt/smt_bool_var_data.h +++ b/src/smt/smt_bool_var_data.h @@ -131,6 +131,6 @@ namespace smt { m_atom = false; } }; -}; +} diff --git a/src/smt/smt_case_split_queue.h b/src/smt/smt_case_split_queue.h index 5c1b8c8ee3..1e503afdb9 100644 --- a/src/smt/smt_case_split_queue.h +++ b/src/smt/smt_case_split_queue.h @@ -52,6 +52,6 @@ namespace smt { }; case_split_queue * mk_case_split_queue(context & ctx, smt_params & p); -}; +} diff --git a/src/smt/smt_cg_table.cpp b/src/smt/smt_cg_table.cpp index 018a543c0b..a25b38aee9 100644 --- a/src/smt/smt_cg_table.cpp +++ b/src/smt/smt_cg_table.cpp @@ -258,5 +258,5 @@ namespace smt { return true; } -}; +} diff --git a/src/smt/smt_cg_table.h b/src/smt/smt_cg_table.h index 9c2baed11e..3b24ceccf1 100644 --- a/src/smt/smt_cg_table.h +++ b/src/smt/smt_cg_table.h @@ -216,6 +216,6 @@ namespace smt { bool check_invariant() const; }; -}; +} diff --git a/src/smt/smt_checker.cpp b/src/smt/smt_checker.cpp index d2c1758d35..ab25923111 100644 --- a/src/smt/smt_checker.cpp +++ b/src/smt/smt_checker.cpp @@ -182,7 +182,7 @@ namespace smt { m_bindings(nullptr) { } -}; +} diff --git a/src/smt/smt_checker.h b/src/smt/smt_checker.h index 3cd83a106d..7a69a12316 100644 --- a/src/smt/smt_checker.h +++ b/src/smt/smt_checker.h @@ -50,6 +50,6 @@ namespace smt { bool is_unsat(expr * n, unsigned num_bindings = 0, enode * const * bindings = nullptr); }; -}; +} diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 061e1dd230..0c2e8617eb 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -126,4 +126,4 @@ namespace smt { return out << mk_pp(disj, m, 3); } -}; +} diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index 89d8f2d66b..eeb9375ef5 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -279,6 +279,6 @@ namespace smt { typedef ptr_vector clause_vector; typedef obj_hashtable clause_set; -}; +} diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp index 324674a998..96e4a6d57c 100644 --- a/src/smt/smt_clause_proof.cpp +++ b/src/smt/smt_clause_proof.cpp @@ -291,6 +291,6 @@ namespace smt { } } -}; +} diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h index 28191cfa25..7fa86671e0 100644 --- a/src/smt/smt_clause_proof.h +++ b/src/smt/smt_clause_proof.h @@ -94,6 +94,6 @@ namespace smt { }; std::ostream& operator<<(std::ostream& out, clause_proof::status st); -}; +} diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 6cb22e5058..c1bed6fdb8 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1485,5 +1485,5 @@ namespace smt { return alloc(conflict_resolution, m, ctx, dack_manager, params, assigned_literals, watches); } -}; +} diff --git a/src/smt/smt_conflict_resolution.h b/src/smt/smt_conflict_resolution.h index 39f7c68d50..54e91ba941 100644 --- a/src/smt/smt_conflict_resolution.h +++ b/src/smt/smt_conflict_resolution.h @@ -276,6 +276,6 @@ namespace smt { ); -}; +} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0e8062e880..4fafb42980 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4884,7 +4884,7 @@ namespace smt { m_model->add_rec_funs(); } -}; +} #ifdef Z3DEBUG diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f11b54aeb1..8786e73bae 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1924,4 +1924,4 @@ namespace smt { std::ostream& operator<<(std::ostream& out, enode_pp const& p); -}; +} diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index e8f590e1a3..05b60ee625 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -420,5 +420,5 @@ namespace smt { } } -}; +} diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 8041099e59..10d6f624b8 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -786,5 +786,5 @@ namespace smt { IF_VERBOSE(2, verbose_stream() << str); } -}; +} diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp index e1ff89c544..c01091e2b2 100644 --- a/src/smt/smt_context_stat.cpp +++ b/src/smt/smt_context_stat.cpp @@ -145,4 +145,4 @@ namespace smt { if (m_fparams.m_profile_res_sub) display_profile_res_sub(out); } -}; +} diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 05b174e5e0..c4af96369b 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -374,5 +374,5 @@ namespace smt { get_enode()->m_func_decl_id = UINT_MAX; } -}; +} diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index e9dc4c4e13..30a2b512af 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -480,6 +480,6 @@ namespace smt { }; inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); } -}; +} diff --git a/src/smt/smt_eq_justification.h b/src/smt/smt_eq_justification.h index cc8b3ceb61..a8a3226c36 100644 --- a/src/smt/smt_eq_justification.h +++ b/src/smt/smt_eq_justification.h @@ -78,6 +78,6 @@ namespace smt { }; const eq_justification null_eq_justification(static_cast(nullptr)); -}; +} diff --git a/src/smt/smt_failure.h b/src/smt/smt_failure.h index 15890dd5bd..5ebc1fff61 100644 --- a/src/smt/smt_failure.h +++ b/src/smt/smt_failure.h @@ -35,5 +35,5 @@ namespace smt { QUANTIFIERS //!< Logical context contains universal quantifiers. }; -}; +} diff --git a/src/smt/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp index e71a848a2b..5aac74b349 100644 --- a/src/smt/smt_for_each_relevant_expr.cpp +++ b/src/smt/smt_for_each_relevant_expr.cpp @@ -295,4 +295,4 @@ namespace smt { m_manager.is_label(n, pos, m_buffer); // copy symbols to buffer } -}; +} diff --git a/src/smt/smt_for_each_relevant_expr.h b/src/smt/smt_for_each_relevant_expr.h index 20be165c67..5fdb151736 100644 --- a/src/smt/smt_for_each_relevant_expr.h +++ b/src/smt/smt_for_each_relevant_expr.h @@ -35,7 +35,7 @@ namespace smt { unsigned count_at_labels_lit(expr* n, bool polarity); public: - check_at_labels(ast_manager& m) : m_manager(m) {}; + check_at_labels(ast_manager& m) : m_manager(m) {} /** \brief Check that 'n' as a formula contains at most one @ label within each and-or path. @@ -105,6 +105,6 @@ namespace smt { void operator()(expr * n) override; }; -}; +} diff --git a/src/smt/smt_implied_equalities.h b/src/smt/smt_implied_equalities.h index 8a063a5d85..6357cc952f 100644 --- a/src/smt/smt_implied_equalities.h +++ b/src/smt/smt_implied_equalities.h @@ -36,6 +36,6 @@ namespace smt { unsigned* class_ids); -}; +} diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 3bb498882a..77fc5c0d84 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1867,4 +1867,4 @@ namespace smt { } SASSERT(th->is_attached_to_var(n)); } -}; +} diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 1ae6732173..03843f0a83 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -440,5 +440,5 @@ namespace smt { return m.mk_th_lemma(m_th_id, m.mk_or(lits), 0, nullptr, m_params.size(), m_params.data()); } -}; +} diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index 161ffe839f..14c1ce7483 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -423,6 +423,6 @@ namespace smt { char const * get_name() const override { return "theory-lemma"; } }; -}; +} diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 1e49a8d3ce..3453633f87 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -352,4 +352,4 @@ namespace smt { m_imp->m_kernel.user_propagate_initialize_value(var, value); } -}; +} diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 0a6faaa091..a5ddce96c3 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -346,4 +346,4 @@ namespace smt { context & get_context(); context const& get_context() const; }; -}; +} diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index 94ac5e5677..8ec28693dc 100644 --- a/src/smt/smt_literal.cpp +++ b/src/smt/smt_literal.cpp @@ -116,5 +116,5 @@ namespace smt { } -}; +} diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h index 17ed9c6c47..cf773353d1 100644 --- a/src/smt/smt_literal.h +++ b/src/smt/smt_literal.h @@ -54,6 +54,6 @@ namespace smt { bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2); -}; +} diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index c6c914fe03..64dc77eb59 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -582,4 +582,4 @@ namespace smt { } } -}; +} diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 3a8e816399..c0945689c7 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -104,5 +104,5 @@ namespace smt { void operator()(expr* e); }; -}; +} diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index 3b34e0192f..a8c1210492 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -64,7 +64,7 @@ namespace smt { class hint_solver; class non_auf_macro_solver; class instantiation_set; - }; + } class model_finder : public quantifier2macro_infos { typedef mf::quantifier_analyzer quantifier_analyzer; @@ -123,5 +123,5 @@ namespace smt { quantifier_macro_info* operator()(quantifier* q) override; }; -}; +} diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 8cf9508d6f..7ecbaca6c7 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -533,4 +533,4 @@ namespace smt { return m_model.get(); } -}; +} diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h index fd99dc6d84..ffd1a1f963 100644 --- a/src/smt/smt_model_generator.h +++ b/src/smt/smt_model_generator.h @@ -240,7 +240,7 @@ namespace smt { } } }; -}; +} diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 19953be75d..672246beae 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -962,4 +962,4 @@ namespace smt { return alloc(default_qm_plugin); } -}; +} diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 6d9a448222..ad3fee18e4 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -187,4 +187,4 @@ namespace smt { vector>& used_enodes) { return false; } }; -}; +} diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index f267cb481a..ad54d185b0 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/src/smt/smt_quick_checker.cpp @@ -404,5 +404,5 @@ namespace smt { return new_expr; } -}; +} diff --git a/src/smt/smt_quick_checker.h b/src/smt/smt_quick_checker.h index 8c8fd6c81f..b152ecd6d5 100644 --- a/src/smt/smt_quick_checker.h +++ b/src/smt/smt_quick_checker.h @@ -98,6 +98,6 @@ namespace smt { bool instantiate_not_sat(quantifier * q); bool instantiate_not_sat(quantifier * q, unsigned num_candidates, expr * const * candidates); }; -}; +} diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 720eac6c22..3f24a4e11c 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -720,6 +720,6 @@ namespace smt { } relevancy_propagator * mk_relevancy_propagator(context & ctx) { return alloc(relevancy_propagator_imp, ctx); } -}; +} diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h index 4827fffcb8..8bd7f7b95b 100644 --- a/src/smt/smt_relevancy.h +++ b/src/smt/smt_relevancy.h @@ -196,6 +196,6 @@ namespace smt { relevancy_propagator * mk_relevancy_propagator(context & ctx); -}; +} diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 69dec1348c..f13eed6fbc 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -941,6 +941,6 @@ namespace smt { setup_unknown(); } -}; +} diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 897755ef71..ce00baf679 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -124,6 +124,6 @@ namespace smt { symbol const & get_logic() const { return m_logic; } void operator()(config_mode cm); }; -}; +} diff --git a/src/smt/smt_statistics.cpp b/src/smt/smt_statistics.cpp index 95acd48191..10c65401ac 100644 --- a/src/smt/smt_statistics.cpp +++ b/src/smt/smt_statistics.cpp @@ -25,5 +25,5 @@ namespace smt { memset(this, 0, sizeof(statistics)); } -}; +} diff --git a/src/smt/smt_statistics.h b/src/smt/smt_statistics.h index 11f7612e6f..831cf67b04 100644 --- a/src/smt/smt_statistics.h +++ b/src/smt/smt_statistics.h @@ -52,7 +52,7 @@ namespace smt { void reset(); }; -}; +} diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index be32edacb9..b762e757e5 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -261,5 +261,5 @@ namespace smt { return get_th_var(ctx.get_enode(e)); } -}; +} diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 70b5556d68..79d8629e51 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -655,6 +655,6 @@ namespace smt { virtual bool is_fixed_propagated(theory_var v, expr_ref& val, literal_vector & explain) { return false; } }; -}; +} diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h index 4b7fc4cc76..f8cff938f4 100644 --- a/src/smt/smt_types.h +++ b/src/smt/smt_types.h @@ -72,6 +72,6 @@ namespace smt { // if defined, then clauses have an extra mask field used to optimize backward subsumption, and backward/forward subsumption resolution. #define APPROX_LIT_SET -}; +} diff --git a/src/smt/smt_value_sort.h b/src/smt/smt_value_sort.h index 979afebf2d..e477a0b723 100644 --- a/src/smt/smt_value_sort.h +++ b/src/smt/smt_value_sort.h @@ -30,6 +30,6 @@ namespace smt { bool is_value_sort(ast_manager& m, expr* e); -}; +} diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp index 6aee87408c..b97615c3e1 100644 --- a/src/smt/theory_arith.cpp +++ b/src/smt/theory_arith.cpp @@ -27,4 +27,4 @@ namespace smt { // template class theory_arith; template class smt::theory_arith; -}; +} diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index c5dc9df663..6b9a7dc75d 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1277,6 +1277,6 @@ namespace smt { // typedef theory_arith theory_smi_arith; -}; +} diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index c8fd25dbae..553e945967 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -147,7 +147,7 @@ namespace smt { result_map[it->m_var] = -1; } } - }; + } #ifdef Z3DEBUG /** @@ -2295,6 +2295,6 @@ namespace smt { } #endif -}; +} diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 6ba5eef741..2c352a6a25 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3570,5 +3570,5 @@ namespace smt { } -}; +} diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index b983475778..45dab16bfc 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -346,6 +346,6 @@ namespace smt { tout << enode_pp(_x, ctx) << " = " << enode_pp(_y, ctx) << "\n";); ctx.assign_eq(_x, _y, eq_justification(js)); } -}; +} diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index fe02fe8842..e1ea198e17 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1110,6 +1110,6 @@ namespace smt { return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE; } -}; +} diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index f69d69d2f7..0b52ef7f17 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -229,6 +229,6 @@ namespace smt { #endif -}; +} diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 749ac82512..30cc8cbac2 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2410,7 +2410,7 @@ final_check_status theory_arith::process_non_linear() { } -}; +} diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 81ed037623..be642f5b87 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -528,6 +528,6 @@ namespace smt { id++; } -}; +} diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index d35da46796..eadaf69c5d 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -505,4 +505,4 @@ namespace smt { st.update("array splits", m_stats.m_num_eq_splits); } -}; +} diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 88f5678aea..135255ab78 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -114,5 +114,5 @@ namespace smt { ptr_vector const& parent_selects(enode* n) { return m_var_data[find(n->get_root()->get_th_var(get_id()))]->m_parent_selects; } }; -}; +} diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 19e89bd656..9f6841760d 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -1053,4 +1053,4 @@ namespace smt { return result; } -}; +} diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 629faec98c..34da46f93f 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -213,5 +213,5 @@ namespace smt { ~theory_array_base() override { restore_sorts(0); } }; -}; +} diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 9dae2dcb96..8ea160507f 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -118,5 +118,5 @@ namespace smt { void propagate() override; }; -}; +} diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index b535838438..f09be95069 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -2071,4 +2071,4 @@ namespace smt { #endif -}; +} diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 247424e18c..6d64b7a14d 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -296,4 +296,4 @@ namespace smt { bool check_invariant(); bool check_zero_one_bits(theory_var v); }; -}; +} diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 3782f54d12..6d58f0c2f4 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -1414,4 +1414,4 @@ namespace smt { } -}; +} diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index be6b3d61ab..d76740aed9 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -215,6 +215,6 @@ namespace smt { bool include_func_interp(func_decl* f) override; }; -}; +} diff --git a/src/smt/theory_dense_diff_logic.cpp b/src/smt/theory_dense_diff_logic.cpp index 3d352ee845..7057a47f24 100644 --- a/src/smt/theory_dense_diff_logic.cpp +++ b/src/smt/theory_dense_diff_logic.cpp @@ -23,4 +23,4 @@ namespace smt { template class theory_dense_diff_logic; template class theory_dense_diff_logic; template class theory_dense_diff_logic; -}; +} diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index 8c2d62aa9a..d60d9edaff 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -292,6 +292,6 @@ namespace smt { typedef theory_dense_diff_logic theory_dense_i; typedef theory_dense_diff_logic theory_dense_smi; typedef theory_dense_diff_logic theory_dense_si; -}; +} diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 243629db79..eba0e0ab83 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -1123,6 +1123,6 @@ namespace smt { return f; } -}; +} diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp index 1664dbfe2f..96593cdc00 100644 --- a/src/smt/theory_diff_logic.cpp +++ b/src/smt/theory_diff_logic.cpp @@ -31,9 +31,9 @@ template class theory_diff_logic; template class theory_diff_logic; -}; +} namespace simplex { template class simplex; template class sparse_matrix; -}; +} diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index ac73ca820f..3781042ef5 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -407,7 +407,7 @@ namespace smt { typedef theory_diff_logic theory_fidl; typedef theory_diff_logic theory_rdl; typedef theory_diff_logic theory_frdl; -}; +} diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index a3cd84853a..2783d7def4 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -291,4 +291,4 @@ namespace smt { theory* mk_theory_dl(context& ctx) { return alloc(theory_dl, ctx); } -}; +} diff --git a/src/smt/theory_dl.h b/src/smt/theory_dl.h index 4bcd94e83f..fb87c9f302 100644 --- a/src/smt/theory_dl.h +++ b/src/smt/theory_dl.h @@ -23,6 +23,6 @@ namespace smt { theory* mk_theory_dl(context& ctx); -}; +} diff --git a/src/smt/theory_dummy.cpp b/src/smt/theory_dummy.cpp index 7f8af5a9d0..58bdeaab6c 100644 --- a/src/smt/theory_dummy.cpp +++ b/src/smt/theory_dummy.cpp @@ -70,4 +70,4 @@ namespace smt { return m_name; } -}; +} diff --git a/src/smt/theory_dummy.h b/src/smt/theory_dummy.h index de77f292d6..bf4ace8db5 100644 --- a/src/smt/theory_dummy.h +++ b/src/smt/theory_dummy.h @@ -51,6 +51,6 @@ namespace smt { char const * get_name() const override; }; -}; +} diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 492595f609..b9fb4bf69d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -721,4 +721,4 @@ namespace smt { out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n"; } } -}; +} diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 14797f62a4..50493a30c6 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -126,5 +126,5 @@ namespace smt { app* get_ite_value(expr* e); }; -}; +} diff --git a/src/smt/theory_opt.cpp b/src/smt/theory_opt.cpp index 365315bf2e..f1917a3a86 100644 --- a/src/smt/theory_opt.cpp +++ b/src/smt/theory_opt.cpp @@ -74,4 +74,4 @@ namespace smt { return a.is_numeral(term); } -}; +} diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 73c9d5cba5..5fdcfbdcc3 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -424,4 +424,4 @@ namespace smt { void propagate() override; static literal assert_ge(context& ctx, unsigned k, unsigned n, literal const* xs); }; -}; +} diff --git a/src/smt/theory_polymorphism.h b/src/smt/theory_polymorphism.h index 8fd88c69b3..a10f9aa84e 100644 --- a/src/smt/theory_polymorphism.h +++ b/src/smt/theory_polymorphism.h @@ -100,6 +100,6 @@ namespace smt { void init_model(model_generator & mg) override { } }; -}; +} diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index ee2ae002ae..50a267d653 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -642,6 +642,6 @@ namespace smt { expr* expr2rep(expr* e) override; bool get_length(expr* e, rational& r) override; }; -}; +} diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 9571f46b76..26ad3573d8 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -43,6 +43,6 @@ namespace smt { }; -}; +} diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 439ffdb7ea..6f382dca07 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -167,4 +167,4 @@ namespace smt { void propagate() override; void display(std::ostream& out) const override {} }; -}; +} diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index e94df49ebc..eeb19da847 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -358,7 +358,7 @@ namespace smt { typedef theory_utvpi theory_rutvpi; typedef theory_utvpi theory_iutvpi; -}; +} diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 9d011299dc..6c96bb92fa 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -965,6 +965,6 @@ namespace smt { } -}; +} diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index d3b190010f..53b5c0b5fa 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -362,4 +362,4 @@ namespace smt { m_normalize = false; } -}; +} diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 65461eb708..42cfbb3fd6 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -134,5 +134,5 @@ namespace smt { }; -}; +} diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 973e586faa..08c8f117b5 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -128,4 +128,4 @@ namespace smt { begin_lits_core() += sizeof(literal); } -}; +} diff --git a/src/smt/watch_list.h b/src/smt/watch_list.h index e974ea51c3..f866adf094 100644 --- a/src/smt/watch_list.h +++ b/src/smt/watch_list.h @@ -193,6 +193,6 @@ namespace smt { }; -}; +} diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index ba0b1f8406..14f9c93968 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -190,7 +190,7 @@ class asserted_formulas { } \ void post_op() override { if (REDUCE) af.reduce_and_solve(); } \ bool should_apply() const override { return APP; } \ - }; + } #define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE) diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index 4835eacd9c..e5c20462de 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -26,7 +26,7 @@ struct bv_bound_chk_stats { unsigned m_unsats; unsigned m_singletons; unsigned m_reduces; - bv_bound_chk_stats() : m_unsats(0), m_singletons(0), m_reduces(0) {}; + bv_bound_chk_stats() : m_unsats(0), m_singletons(0), m_reduces(0) {} }; struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg { diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 213f01f623..476e97eb1d 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -57,7 +57,7 @@ public: virtual simplifier * translate(ast_manager & m) = 0; virtual unsigned scope_level() const = 0; virtual void updt_params(params_ref const & p) {} - void set_occs(goal_num_occurs& occs) { m_occs = &occs; }; + void set_occs(goal_num_occurs& occs) { m_occs = &occs; } bool shared(expr* t) const; }; diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index c05116c0a1..194388bde8 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -341,7 +341,7 @@ private: } typedef hashtable uint_set; - typedef obj_map app_siblings;; + typedef obj_map app_siblings; class siblings { app_map const& m_colors; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 22e0f498be..d91ae3192a 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -1012,7 +1012,7 @@ public: result.reset(); // assumes in is not strenthened to one of the branches throw tactic_exception("failed-if-branching tactical"); } - }; + } tactic * translate(ast_manager & m) override { tactic * new_t = m_t->translate(m); diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h index fb22ce5e17..95209fef24 100644 --- a/src/util/sat_literal.h +++ b/src/util/sat_literal.h @@ -190,7 +190,7 @@ namespace sat { return out << mk_lits_pp(ls.size(), ls.data()); } -}; +} namespace std { @@ -198,4 +198,4 @@ namespace std { if (l.sign()) return "-" + to_string(l.var()); return to_string(l.var()); } -}; +} diff --git a/src/util/sat_sls.h b/src/util/sat_sls.h index 82b84bd03d..3289d8a29e 100644 --- a/src/util/sat_sls.h +++ b/src/util/sat_sls.h @@ -36,6 +36,6 @@ namespace sat { inline std::ostream& operator<<(std::ostream& out, clause_info const& ci) { return out << ci.m_clause << " w: " << ci.m_weight << " nt: " << ci.m_num_trues; } -}; +} diff --git a/src/util/sign.h b/src/util/sign.h index 5221b3f684..8c21716495 100644 --- a/src/util/sign.h +++ b/src/util/sign.h @@ -18,7 +18,7 @@ Author: #pragma once typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign; -static inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } }; +static inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } } static inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); } static inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); } static inline bool is_zero(sign s) { return s == sign_zero; } diff --git a/src/util/util.h b/src/util/util.h index d580209e94..34eec199bd 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -270,7 +270,7 @@ public: scoped_ptr& operator=(scoped_ptr&& other) noexcept { *this = other.detach(); return *this; - }; + } T * detach() { T* tmp = m_ptr;