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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 3 Dec 2020 03:55:00 +0000 (19:55 -0800)
committer	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 3 Dec 2020 03:55:00 +0000 (19:55 -0800)
commit	92e9feab5f417fbbd3ac07d47fe9b6b49f5c4168
tree	c7c533d12e91b68d350d5dcc5e77441a831f69a9	tree
parent	3a8e2f4e52f4debfb8eb6fb9c49934a66d742ec9	commit \| diff

Update copyright headers.

296 files changed:

examples/api/combination.cpp		diff \| blob \| history
examples/api/linear_arith.cpp		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/linear_arith.py		diff \| blob \| history
examples/api/python/sequences.py		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/api/python/strings.py		diff \| blob \| history
examples/api/python/sygus-fun.py		diff \| blob \| history
examples/api/python/sygus-grammar.py		diff \| blob \| history
examples/api/python/sygus-inv.py		diff \| blob \| history
examples/api/sets.cpp		diff \| blob \| history
examples/api/strings.cpp		diff \| blob \| history
examples/api/sygus-fun.cpp		diff \| blob \| history
examples/api/sygus-grammar.cpp		diff \| blob \| history
examples/api/sygus-inv.cpp		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
examples/simple_vc_quant_cxx.cpp		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/ascription_type.cpp		diff \| blob \| history
src/expr/ascription_type.h		diff \| blob \| history
src/expr/buffered_proof_generator.cpp		diff \| blob \| history
src/expr/buffered_proof_generator.h		diff \| blob \| history
src/expr/emptybag.cpp		diff \| blob \| history
src/expr/emptybag.h		diff \| blob \| history
src/expr/expr_iomanip.cpp		diff \| blob \| history
src/expr/lazy_proof_chain.cpp		diff \| blob \| history
src/expr/lazy_proof_chain.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_value.cpp		diff \| blob \| history
src/expr/proof_node.h		diff \| blob \| history
src/expr/proof_node_algorithm.cpp		diff \| blob \| history
src/expr/proof_node_algorithm.h		diff \| blob \| history
src/expr/proof_node_manager.cpp		diff \| blob \| history
src/expr/proof_node_manager.h		diff \| blob \| history
src/expr/proof_node_updater.cpp		diff \| blob \| history
src/expr/proof_node_updater.h		diff \| blob \| history
src/expr/proof_set.h		diff \| blob \| history
src/expr/record.cpp		diff \| blob \| history
src/expr/record.h		diff \| blob \| history
src/expr/symbol_table.h		diff \| blob \| history
src/expr/tconv_seq_proof_generator.cpp		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/parser/antlr_tracing.h		diff \| blob \| history
src/parser/parser_builder.cpp		diff \| blob \| history
src/parser/parser_builder.h		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.cpp		diff \| blob \| history
src/preprocessing/passes/global_negate.h		diff \| blob \| history
src/preprocessing/passes/ho_elim.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.h		diff \| blob \| history
src/preprocessing/passes/ite_simp.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/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.h		diff \| blob \| history
src/printer/let_binding.cpp		diff \| blob \| history
src/printer/let_binding.h		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.h		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/proof/unsat_core.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/proof_cnf_stream.h		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/check_models.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/dump_manager.cpp		diff \| blob \| history
src/smt/dump_manager.h		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/expand_definitions.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/interpolation_solver.h		diff \| blob \| history
src/smt/listeners.h		diff \| blob \| history
src/smt/managed_ostreams.cpp		diff \| blob \| history
src/smt/model.cpp		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/node_command.cpp		diff \| blob \| history
src/smt/options_manager.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/process_assertions.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_engine_state.cpp		diff \| blob \| history
src/smt/smt_engine_state.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.h		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/arith_utilities.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/bound_inference.cpp		diff \| blob \| history
src/theory/arith/bound_inference.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/inference_id.cpp		diff \| blob \| history
src/theory/arith/inference_id.h		diff \| blob \| history
src/theory/arith/nl/ext/constraint.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.h		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.h		diff \| blob \| history
src/theory/arith/nl/iand_table.cpp		diff \| blob \| history
src/theory/arith/nl/iand_table.h		diff \| blob \| history
src/theory/arith/nl/icp/candidate.cpp		diff \| blob \| history
src/theory/arith/nl/icp/candidate.h		diff \| blob \| history
src/theory/arith/nl/icp/contraction_origins.cpp		diff \| blob \| history
src/theory/arith/nl/icp/contraction_origins.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/intersection.cpp		diff \| blob \| history
src/theory/arith/nl/icp/intersection.h		diff \| blob \| history
src/theory/arith/nl/icp/interval.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/strategy.cpp		diff \| blob \| history
src/theory/arith/nl/strategy.h		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		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/inference_manager.cpp		diff \| blob \| history
src/theory/arrays/inference_manager.h		diff \| blob \| history
src/theory/arrays/proof_checker.cpp		diff \| blob \| history
src/theory/arrays/proof_checker.h		diff \| blob \| history
src/theory/arrays/skolem_cache.cpp		diff \| blob \| history
src/theory/arrays/skolem_cache.h		diff \| blob \| history
src/theory/bags/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/inference_manager.cpp		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/make_bag_op.h		diff \| blob \| history
src/theory/bags/normal_form.cpp		diff \| blob \| history
src/theory/bags/normal_form.h		diff \| blob \| history
src/theory/bags/solver_state.cpp		diff \| blob \| history
src/theory/bags/solver_state.h		diff \| blob \| history
src/theory/bags/term_registry.cpp		diff \| blob \| history
src/theory/bags/term_registry.h		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags.h		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.h		diff \| blob \| history
src/theory/bags/theory_bags_type_rules.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.cpp		diff \| blob \| history
src/theory/bv/bv_solver_simple.cpp		diff \| blob \| history
src/theory/bv/bv_solver_simple.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/inference.cpp		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/datatypes/proof_checker.cpp		diff \| blob \| history
src/theory/datatypes/proof_checker.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.h		diff \| blob \| history
src/theory/fp/type_enumerator.h		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/skolemize.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_qe_preproc.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/solver_state.cpp		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.h		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/shared_solver.cpp		diff \| blob \| history
src/theory/shared_solver.h		diff \| blob \| history
src/theory/shared_solver_distributed.cpp		diff \| blob \| history
src/theory/shared_solver_distributed.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.h		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory_eq_notify.h		diff \| blob \| history
src/theory/theory_id.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/theory_proof_step_buffer.cpp		diff \| blob \| history
src/theory/theory_proof_step_buffer.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/trust_substitutions.cpp		diff \| blob \| history
src/theory/trust_substitutions.h		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/floatingpoint.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.cpp		diff \| blob \| history
src/util/gmp_util.h		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
test/api/CMakeLists.txt		diff \| blob \| history
test/api/ouroborous.cpp		diff \| blob \| history
test/api/python/test_grammar.py		diff \| blob \| history
test/api/python/test_sort.py		diff \| blob \| history
test/api/python/test_to_python_obj.py		diff \| blob \| history
test/api/reset_assertions.cpp		diff \| blob \| history
test/api/sep_log_api.cpp		diff \| blob \| history
test/regress/run_regression.py	[changed mode: 0755->0644]	blob \| history
test/unit/api/CMakeLists.txt		diff \| blob \| history
test/unit/api/grammar_black.cpp		diff \| blob \| history
test/unit/api/result_black.cpp		diff \| blob \| history
test/unit/api/sort_black.h		diff \| blob \| history
test/unit/api/term_black.cpp		diff \| blob \| history
test/unit/expr/CMakeLists.txt		diff \| blob \| history
test/unit/expr/symbol_table_black.h		diff \| blob \| history
test/unit/expr/type_node_white.h		diff \| blob \| history
test/unit/main/interactive_shell_black.h		diff \| blob \| history
test/unit/parser/parser_black.h		diff \| blob \| history
test/unit/parser/parser_builder_black.h		diff \| blob \| history
test/unit/preprocessing/CMakeLists.txt		diff \| blob \| history
test/unit/printer/CMakeLists.txt		diff \| blob \| history
test/unit/theory/CMakeLists.txt		diff \| blob \| history
test/unit/theory/theory_bags_normal_form_white.h		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.h		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_white.h		diff \| blob \| history
test/unit/theory/theory_sets_type_enumerator_white.h		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.h		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history
test/unit/util/bitvector_black.h		diff \| blob \| history
test/unit/util/output_black.h		diff \| blob \| history

RSS Atom