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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Thu, 13 May 2021 06:33:00 +0000 (23:33 -0700)
committer	GitHub <noreply@github.com>
	Thu, 13 May 2021 06:33:00 +0000 (06:33 +0000)
commit	31242de4b423d7225174dd1672edb2dacb68f5b8
tree	657a453475affc67628b1391909af92f3346b411	tree
parent	ffd7bb2069df08c31fd9d8a03d786f1e9fc7147c	commit \| diff

Add std::hash overloads for Node, TNode and TypeNode. (#6534)

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

323 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/decision/assertion_list.cpp		diff \| blob \| history
src/decision/assertion_list.h		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/expr/array_store_all.cpp		diff \| blob \| history
src/expr/ascription_type.cpp		diff \| blob \| history
src/expr/bound_var_manager.h		diff \| blob \| history
src/expr/buffered_proof_generator.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/emptybag.cpp		diff \| blob \| history
src/expr/emptyset.cpp		diff \| blob \| history
src/expr/lazy_proof.h		diff \| blob \| history
src/expr/lazy_proof_chain.cpp		diff \| blob \| history
src/expr/lazy_proof_chain.h		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/node_algorithm.h		diff \| blob \| history
src/expr/node_traversal.h		diff \| blob \| history
src/expr/proof.h		diff \| blob \| history
src/expr/proof_node_algorithm.cpp		diff \| blob \| history
src/expr/proof_node_manager.cpp		diff \| blob \| history
src/expr/sequence.cpp		diff \| blob \| history
src/expr/skolem_manager.cpp		diff \| blob \| history
src/expr/tconv_seq_proof_generator.h		diff \| blob \| history
src/expr/term_conversion_proof_generator.cpp		diff \| blob \| history
src/expr/term_conversion_proof_generator.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/expr/uninterpreted_constant.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.h		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.h		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.h		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.h		diff \| blob \| history
src/preprocessing/passes/bv_to_int.h		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.h		diff \| blob \| history
src/preprocessing/passes/global_negate.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.h		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.h		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.h		diff \| blob \| history
src/preprocessing/passes/real_to_int.h		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.cpp		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.h		diff \| blob \| history
src/printer/let_binding.cpp		diff \| blob \| history
src/printer/let_binding.h		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.h		diff \| blob \| history
src/prop/skolem_def_manager.cpp		diff \| blob \| history
src/prop/skolem_def_manager.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/abstract_values.h		diff \| blob \| history
src/smt/check_models.cpp		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/expand_definitions.h		diff \| blob \| history
src/smt/model_blocker.cpp		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.h		diff \| blob \| history
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/preprocessor.h		diff \| blob \| history
src/smt/process_assertions.h		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/smt/witness_form.cpp		diff \| blob \| history
src/smt/witness_form.h		diff \| blob \| history
src/smt_util/nary_builder.h		diff \| blob \| history
src/theory/arith/arith_ite_utils.h		diff \| blob \| history
src/theory/arith/arith_preprocess.cpp		diff \| blob \| history
src/theory/arith/arith_preprocess.h		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/inference_manager.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/iand_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arrays/array_info.h		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_rewriter.cpp		diff \| blob \| history
src/theory/arrays/union_find.cpp		diff \| blob \| history
src/theory/atom_requests.h		diff \| blob \| history
src/theory/bags/inference_manager.h		diff \| blob \| history
src/theory/bags/make_bag_op.cpp		diff \| blob \| history
src/theory/bags/term_registry.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/proof_checker.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.h		diff \| blob \| history
src/theory/bv/abstraction.h		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/simple_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.h		diff \| blob \| history
src/theory/bv/bv_inequality_graph.h		diff \| blob \| history
src/theory/bv/bv_quick_check.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/bv/bv_solver_lazy.h		diff \| blob \| history
src/theory/bv/bv_solver_simple.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.h		diff \| blob \| history
src/theory/bv/int_blaster.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.h		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		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/eager_proof_generator.h		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/evaluator.h		diff \| blob \| history
src/theory/ext_theory.h		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/fp/fp_expand_defs.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.h		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/equality_query.h		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/proof_checker.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.h		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_split.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_macros.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/query_generator.h		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.h		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.h		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.h		diff \| blob \| history
src/theory/quantifiers/sygus/example_min_eval.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_obligation_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_obligation_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_basic.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.h		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.h		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_database.h		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp		diff \| blob \| history
src/theory/quantifiers/term_enumeration.h		diff \| blob \| history
src/theory/quantifiers/term_pools.cpp		diff \| blob \| history
src/theory/quantifiers/term_registry.h		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/relevance_manager.cpp		diff \| blob \| history
src/theory/relevance_manager.h		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/cardinality_extension.h		diff \| blob \| history
src/theory/sets/inference_manager.h		diff \| blob \| history
src/theory/sets/singleton_op.cpp		diff \| blob \| history
src/theory/sets/skolem_cache.h		diff \| blob \| history
src/theory/sets/solver_state.h		diff \| blob \| history
src/theory/sets/term_registry.h		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/base_solver.h		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.h		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.h		diff \| blob \| history
src/theory/strings/infer_proof_cons.h		diff \| blob \| history
src/theory/strings/inference_manager.h		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.h		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.h		diff \| blob \| history
src/theory/strings/skolem_cache.h		diff \| blob \| history
src/theory/strings/strings_fmf.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
src/theory/subs_minimize.cpp		diff \| blob \| history
src/theory/substitutions.h		diff \| blob \| history
src/theory/term_registration_visitor.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_engine_proof_generator.h		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_model_builder.h		diff \| blob \| history
src/theory/theory_preprocessor.h		diff \| blob \| history
src/theory/theory_proof_step_buffer.cpp		diff \| blob \| history
src/theory/trust_substitutions.h		diff \| blob \| history
src/theory/type_set.cpp		diff \| blob \| history
src/theory/type_set.h		diff \| blob \| history
src/theory/uf/cardinality_extension.h		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/eq_proof.h		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/uf/ho_extension.h		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		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
test/unit/node/node_algorithm_black.cpp		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp		diff \| blob \| history
test/unit/theory/type_enumerator_white.cpp		diff \| blob \| history

RSS Atom