git.libre-soc.org Git - cvc5.git/commit

author	Gereon Kremer <gkremer@cs.stanford.edu>
	Thu, 17 Mar 2022 18:00:56 +0000 (19:00 +0100)
committer	GitHub <noreply@github.com>
	Thu, 17 Mar 2022 18:00:56 +0000 (18:00 +0000)
commit	8f7952bc092d252a4d0c04c87636c443536833b3
tree	29fc5b0a7f8eb17f2b08f4fc4080711cb39e6892	tree
parent	169e32c8728a95128b4e78734f33d5ed53f32f1f	commit \| diff

Replace `Debug` by `Trace` (#7793)

This PR replaces all usages of Debug() by Trace(), the same for similar methods like Debug.isOn().
Given that Debug is no longer used then, it is removed.

251 files changed:

src/base/output.cpp		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/context/cdhashmap.h		diff \| blob \| history
src/context/cdinsert_hashmap.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/cdo.h		diff \| blob \| history
src/context/cdqueue.h		diff \| blob \| history
src/context/context.cpp		diff \| blob \| history
src/context/context.h		diff \| blob \| history
src/context/context_mm.cpp		diff \| blob \| history
src/decision/justify_stack.cpp		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/node_builder.cpp		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/expr/node_manager_template.h		diff \| blob \| history
src/expr/symbol_table.cpp		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/expr/type_matcher.cpp		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/options_template.cpp		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/antlr_input.h		diff \| blob \| history
src/parser/antlr_line_buffered_input.cpp		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/learned_rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/proof/conv_proof_generator.cpp		diff \| blob \| history
src/proof/conv_seq_proof_generator.cpp		diff \| blob \| history
src/proof/lazy_proof_chain.cpp		diff \| blob \| history
src/proof/proof_checker.cpp		diff \| blob \| history
src/proof/proof_ensure_closed.cpp		diff \| blob \| history
src/proof/proof_node_manager.cpp		diff \| blob \| history
src/proof/proof_node_updater.cpp		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/opt_clauses_manager.cpp		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/proof_post_processor.cpp		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/proof_final_callback.cpp		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/solver_engine_scope.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/unsat_core_manager.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/branch_and_bound.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/cut_log.cpp		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac_utils.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/lazard_evaluation.cpp		diff \| blob \| history
src/theory/arith/nl/coverings_solver.cpp		diff \| blob \| history
src/theory/arith/nl/equality_substitution.cpp		diff \| blob \| history
src/theory/arith/nl/ext/constraint.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/pow2_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/pp_rewrite_eq.cpp		diff \| blob \| history
src/theory/arith/proof_checker.cpp		diff \| blob \| history
src/theory/arith/rewriter/addition.cpp		diff \| blob \| history
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/tableau.cpp		diff \| blob \| history
src/theory/arith/tableau.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.cpp		diff \| blob \| history
src/theory/atom_requests.cpp		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_type_rules.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/combination_care_graph.cpp		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/model_manager.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/vts_term_cache.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/lazy_trie.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_registry.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/relevance_manager.cpp		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.cpp		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
test/unit/node/attribute_white.cpp		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/theory/theory_arith_rewriter_black.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history
test/unit/util/output_black.cpp		diff \| blob \| history

RSS Atom