From 559710702e4df3ddaac4905705cf93c08502984b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 11 Oct 2012 17:06:16 +0000 Subject: [PATCH] Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.) --- AUTHORS | 4 ++-- COPYING | 5 ++-- README | 6 ++--- contrib/update-copyright.pl | 10 +++----- src/bindings/swig.h | 4 +--- src/compat/cvc3_compat.cpp | 6 ++--- src/compat/cvc3_compat.h | 6 ++--- src/context/cdchunk_list.h | 6 ++--- src/context/cddense_set.h | 6 ++--- src/context/cdhashmap.h | 6 ++--- src/context/cdhashmap_forward.h | 4 +--- src/context/cdhashset.h | 6 ++--- src/context/cdhashset_forward.h | 4 +--- src/context/cdlist.h | 8 +++---- src/context/cdlist_forward.h | 6 ++--- src/context/cdmaybe.h | 6 ++--- src/context/cdo.h | 6 ++--- src/context/cdqueue.h | 8 +++---- src/context/cdtrail_queue.h | 4 +--- src/context/cdvector.h | 4 +--- src/context/context.cpp | 6 ++--- src/context/context.h | 6 ++--- src/context/context_mm.cpp | 4 +--- src/context/context_mm.h | 4 +--- src/context/stacking_map.h | 6 ++--- src/context/stacking_vector.h | 6 ++--- src/decision/decision_engine.cpp | 6 ++--- src/decision/decision_engine.h | 6 ++--- src/decision/decision_mode.cpp | 4 +--- src/decision/decision_mode.h | 6 ++--- src/decision/decision_strategy.h | 6 ++--- src/decision/justification_heuristic.cpp | 6 ++--- src/decision/justification_heuristic.h | 6 ++--- src/decision/options_handlers.h | 4 +--- src/decision/relevancy.cpp | 6 ++--- src/decision/relevancy.h | 6 ++--- src/expr/attribute.cpp | 4 +--- src/expr/attribute.h | 4 +--- src/expr/attribute_internals.h | 4 +--- src/expr/command.cpp | 8 +++---- src/expr/command.h | 6 ++--- src/expr/convenience_node_builders.h | 4 +--- src/expr/expr_manager_scope.h | 4 +--- src/expr/expr_manager_template.cpp | 8 +++---- src/expr/expr_manager_template.h | 6 ++--- src/expr/expr_stream.h | 4 +--- src/expr/expr_template.cpp | 8 +++---- src/expr/expr_template.h | 8 +++---- src/expr/kind_map.h | 6 ++--- src/expr/kind_template.h | 6 ++--- src/expr/metakind_template.h | 6 ++--- src/expr/node.cpp | 4 +--- src/expr/node.h | 6 ++--- src/expr/node_builder.h | 4 +--- src/expr/node_manager.cpp | 8 +++---- src/expr/node_manager.h | 4 +--- src/expr/node_self_iterator.h | 4 +--- src/expr/node_value.cpp | 4 +--- src/expr/node_value.h | 4 +--- src/expr/options_handlers.h | 4 +--- src/expr/pickle_data.cpp | 4 +--- src/expr/pickle_data.h | 6 ++--- src/expr/pickler.cpp | 10 ++++---- src/expr/pickler.h | 6 ++--- src/expr/symbol_table.cpp | 8 +++---- src/expr/symbol_table.h | 4 +--- src/expr/type.cpp | 4 +--- src/expr/type.h | 4 +--- src/expr/type_checker.h | 8 +++---- src/expr/type_checker_template.cpp | 8 +++---- src/expr/type_node.cpp | 8 +++---- src/expr/type_node.h | 6 ++--- src/expr/type_properties_template.h | 6 ++--- src/expr/variable_type_map.h | 6 ++--- src/include/cvc4.h | 4 +--- src/include/cvc4_private.h | 4 +--- src/include/cvc4_private_library.h | 4 +--- src/include/cvc4_public.h | 4 +--- src/include/cvc4parser_private.h | 4 +--- src/include/cvc4parser_public.h | 4 +--- src/lib/clock_gettime.c | 4 +--- src/lib/clock_gettime.h | 4 +--- src/lib/replacements.h | 4 +--- src/main/command_executor.cpp | 6 ++--- src/main/command_executor.h | 6 ++--- src/main/command_executor_portfolio.cpp | 6 ++--- src/main/command_executor_portfolio.h | 6 ++--- src/main/driver_unified.cpp | 10 ++++---- src/main/interactive_shell.cpp | 6 ++--- src/main/interactive_shell.h | 4 +--- src/main/main.cpp | 6 ++--- src/main/main.h | 6 ++--- src/main/options_handlers.h | 4 +--- src/main/portfolio.cpp | 6 ++--- src/main/portfolio.h | 6 ++--- src/main/portfolio_util.cpp | 8 +++---- src/main/portfolio_util.h | 8 +++---- src/main/util.cpp | 6 ++--- src/options/base_options_handlers.h | 4 +--- src/options/base_options_template.cpp | 6 ++--- src/options/base_options_template.h | 6 ++--- src/options/option_exception.h | 8 +++---- src/options/options.h | 8 +++---- src/options/options_holder_template.h | 6 ++--- src/options/options_template.cpp | 8 +++---- src/parser/antlr_input.cpp | 8 +++---- src/parser/antlr_input.h | 8 +++---- src/parser/antlr_line_buffered_input.cpp | 4 +--- src/parser/antlr_line_buffered_input.h | 4 +--- src/parser/antlr_tracing.h | 4 +--- src/parser/bounded_token_buffer.cpp | 4 +--- src/parser/bounded_token_buffer.h | 4 +--- src/parser/bounded_token_factory.cpp | 4 +--- src/parser/bounded_token_factory.h | 4 +--- src/parser/cvc/Cvc.g | 6 ++--- src/parser/cvc/cvc_input.cpp | 4 +--- src/parser/cvc/cvc_input.h | 6 ++--- src/parser/input.cpp | 4 +--- src/parser/input.h | 6 ++--- src/parser/memory_mapped_input_buffer.cpp | 4 +--- src/parser/memory_mapped_input_buffer.h | 4 +--- src/parser/parser.cpp | 6 ++--- src/parser/parser.h | 6 ++--- src/parser/parser_builder.cpp | 6 ++--- src/parser/parser_builder.h | 4 +--- src/parser/parser_exception.h | 4 +--- src/parser/smt1/Smt1.g | 6 ++--- src/parser/smt1/smt1.cpp | 6 ++--- src/parser/smt1/smt1.h | 6 ++--- src/parser/smt1/smt1_input.cpp | 4 +--- src/parser/smt1/smt1_input.h | 6 ++--- src/parser/smt2/Smt2.g | 6 ++--- src/parser/smt2/smt2.cpp | 6 ++--- src/parser/smt2/smt2.h | 4 +--- src/parser/smt2/smt2_input.cpp | 4 +--- src/parser/smt2/smt2_input.h | 4 +--- src/parser/tptp/Tptp.g | 8 +++---- src/parser/tptp/tptp.cpp | 10 ++++---- src/parser/tptp/tptp.h | 10 ++++---- src/parser/tptp/tptp_input.cpp | 10 ++++---- src/parser/tptp/tptp_input.h | 10 ++++---- src/printer/ast/ast_printer.cpp | 6 ++--- src/printer/ast/ast_printer.h | 4 +--- src/printer/cvc/cvc_printer.cpp | 8 +++---- src/printer/cvc/cvc_printer.h | 6 ++--- src/printer/dagification_visitor.cpp | 6 ++--- src/printer/dagification_visitor.h | 4 +--- src/printer/model_format_mode.cpp | 8 +++---- src/printer/model_format_mode.h | 8 +++---- src/printer/options_handlers.h | 4 +--- src/printer/printer.cpp | 6 ++--- src/printer/printer.h | 6 ++--- src/printer/smt1/smt1_printer.cpp | 6 ++--- src/printer/smt1/smt1_printer.h | 4 +--- src/printer/smt2/smt2_printer.cpp | 6 ++--- src/printer/smt2/smt2_printer.h | 4 +--- src/proof/cnf_proof.cpp | 6 ++--- src/proof/cnf_proof.h | 6 ++--- src/proof/proof.h | 6 ++--- src/proof/proof_manager.cpp | 6 ++--- src/proof/proof_manager.h | 6 ++--- src/proof/sat_proof.cpp | 6 ++--- src/proof/sat_proof.h | 6 ++--- src/prop/cnf_stream.cpp | 6 ++--- src/prop/cnf_stream.h | 6 ++--- src/prop/options_handlers.h | 4 +--- src/prop/prop_engine.cpp | 6 ++--- src/prop/prop_engine.h | 8 +++---- src/prop/registrar.h | 8 +++---- src/prop/sat_solver.h | 8 +++---- src/prop/sat_solver_factory.cpp | 6 ++--- src/prop/sat_solver_factory.h | 8 +++---- src/prop/sat_solver_registry.cpp | 6 ++--- src/prop/sat_solver_registry.h | 10 ++++---- src/prop/sat_solver_types.h | 6 ++--- src/prop/theory_proxy.cpp | 8 +++---- src/prop/theory_proxy.h | 8 +++---- src/smt/command_list.cpp | 4 +--- src/smt/command_list.h | 4 +--- src/smt/modal_exception.h | 4 +--- src/smt/options_handlers.h | 4 +--- src/smt/simplification_mode.cpp | 4 +--- src/smt/simplification_mode.h | 4 +--- src/smt/smt_engine.cpp | 8 +++---- src/smt/smt_engine.h | 8 +++---- src/smt/smt_engine_scope.cpp | 4 +--- src/smt/smt_engine_scope.h | 4 +--- src/smt/smt_options_template.cpp | 6 ++--- .../arith/arith_heuristic_pivot_rule.cpp | 4 +--- src/theory/arith/arith_heuristic_pivot_rule.h | 4 +--- src/theory/arith/arith_priority_queue.cpp | 8 +++---- src/theory/arith/arith_priority_queue.h | 4 +--- src/theory/arith/arith_propagation_mode.cpp | 4 +--- src/theory/arith/arith_propagation_mode.h | 4 +--- src/theory/arith/arith_rewriter.cpp | 8 +++---- src/theory/arith/arith_rewriter.h | 4 +--- src/theory/arith/arith_static_learner.cpp | 8 +++---- src/theory/arith/arith_static_learner.h | 4 +--- src/theory/arith/arith_unate_lemma_mode.cpp | 4 +--- src/theory/arith/arith_unate_lemma_mode.h | 4 +--- src/theory/arith/arith_utilities.h | 4 +--- src/theory/arith/arithvar.h | 6 ++--- src/theory/arith/arithvar_node_map.h | 8 +++---- src/theory/arith/congruence_manager.cpp | 6 ++--- src/theory/arith/congruence_manager.h | 6 ++--- src/theory/arith/constraint.cpp | 6 ++--- src/theory/arith/constraint.h | 6 ++--- src/theory/arith/constraint_forward.h | 4 +--- src/theory/arith/delta_rational.cpp | 4 +--- src/theory/arith/delta_rational.h | 6 ++--- src/theory/arith/dio_solver.cpp | 8 +++---- src/theory/arith/dio_solver.h | 6 ++--- src/theory/arith/linear_equality.cpp | 6 ++--- src/theory/arith/linear_equality.h | 6 ++--- src/theory/arith/matrix.cpp | 4 +--- src/theory/arith/matrix.h | 4 +--- src/theory/arith/normal_form.cpp | 8 +++---- src/theory/arith/normal_form.h | 8 +++---- src/theory/arith/options_handlers.h | 4 +--- src/theory/arith/partial_model.cpp | 4 +--- src/theory/arith/partial_model.h | 8 +++---- src/theory/arith/simplex.cpp | 6 ++--- src/theory/arith/simplex.h | 6 ++--- src/theory/arith/theory_arith.cpp | 8 +++---- src/theory/arith/theory_arith.h | 6 ++--- .../arith/theory_arith_instantiator.cpp | 6 ++--- src/theory/arith/theory_arith_instantiator.h | 6 ++--- src/theory/arith/theory_arith_type_rules.h | 6 ++--- src/theory/arith/type_enumerator.h | 4 +--- src/theory/arrays/array_info.cpp | 8 +++---- src/theory/arrays/array_info.h | 4 +--- src/theory/arrays/static_fact_manager.cpp | 6 ++--- src/theory/arrays/static_fact_manager.h | 4 +--- src/theory/arrays/theory_arrays.cpp | 6 ++--- src/theory/arrays/theory_arrays.h | 8 +++---- .../arrays/theory_arrays_instantiator.cpp | 8 +++---- .../arrays/theory_arrays_instantiator.h | 6 ++--- src/theory/arrays/theory_arrays_model.cpp | 6 ++--- src/theory/arrays/theory_arrays_model.h | 24 +++++++++---------- src/theory/arrays/theory_arrays_rewriter.h | 6 ++--- src/theory/arrays/theory_arrays_type_rules.h | 8 +++---- src/theory/arrays/type_enumerator.h | 6 ++--- src/theory/arrays/union_find.cpp | 6 ++--- src/theory/arrays/union_find.h | 6 ++--- src/theory/booleans/circuit_propagator.cpp | 4 +--- src/theory/booleans/circuit_propagator.h | 6 ++--- src/theory/booleans/theory_bool.cpp | 4 +--- src/theory/booleans/theory_bool.h | 6 ++--- src/theory/booleans/theory_bool_rewriter.cpp | 4 +--- src/theory/booleans/theory_bool_rewriter.h | 4 +--- src/theory/booleans/theory_bool_type_rules.h | 8 +++---- src/theory/booleans/type_enumerator.h | 4 +--- src/theory/builtin/theory_builtin.cpp | 6 ++--- src/theory/builtin/theory_builtin.h | 4 +--- .../builtin/theory_builtin_rewriter.cpp | 4 +--- src/theory/builtin/theory_builtin_rewriter.h | 4 +--- .../builtin/theory_builtin_type_rules.h | 8 +++---- src/theory/builtin/type_enumerator.h | 4 +--- src/theory/bv/bitblast_strategies.cpp | 6 ++--- src/theory/bv/bitblast_strategies.h | 6 ++--- src/theory/bv/bitblaster.cpp | 8 +++---- src/theory/bv/bitblaster.h | 6 ++--- src/theory/bv/bv_subtheory.h | 4 +--- src/theory/bv/bv_subtheory_bitblast.cpp | 6 ++--- src/theory/bv/bv_subtheory_bitblast.h | 8 +++---- src/theory/bv/bv_subtheory_eq.cpp | 10 ++++---- src/theory/bv/bv_subtheory_eq.h | 10 ++++---- src/theory/bv/cd_set_collection.h | 4 +--- src/theory/bv/theory_bv.cpp | 8 +++---- src/theory/bv/theory_bv.h | 8 +++---- src/theory/bv/theory_bv_rewrite_rules.h | 6 ++--- ...ory_bv_rewrite_rules_constant_evaluation.h | 6 ++--- src/theory/bv/theory_bv_rewrite_rules_core.h | 6 ++--- .../theory_bv_rewrite_rules_normalization.h | 8 +++---- ...ry_bv_rewrite_rules_operator_elimination.h | 6 ++--- .../theory_bv_rewrite_rules_simplification.h | 8 +++---- src/theory/bv/theory_bv_rewriter.cpp | 8 +++---- src/theory/bv/theory_bv_rewriter.h | 8 +++---- src/theory/bv/theory_bv_type_rules.h | 6 ++--- src/theory/bv/theory_bv_utils.h | 8 +++---- src/theory/bv/type_enumerator.h | 4 +--- src/theory/datatypes/datatypes_rewriter.h | 4 +--- src/theory/datatypes/theory_datatypes.cpp | 4 +--- src/theory/datatypes/theory_datatypes.h | 6 ++--- .../theory_datatypes_instantiator.cpp | 6 ++--- .../datatypes/theory_datatypes_instantiator.h | 6 ++--- .../datatypes/theory_datatypes_type_rules.h | 6 ++--- src/theory/datatypes/type_enumerator.h | 4 +--- src/theory/example/ecdata.cpp | 4 +--- src/theory/example/ecdata.h | 4 +--- src/theory/example/theory_uf_tim.cpp | 4 +--- src/theory/example/theory_uf_tim.h | 6 ++--- src/theory/instantiator_tables_template.cpp | 10 ++++---- src/theory/interrupted.h | 4 +--- src/theory/ite_simplifier.cpp | 6 ++--- src/theory/ite_simplifier.h | 8 +++---- src/theory/logic_info.cpp | 4 +--- src/theory/logic_info.h | 4 +--- src/theory/model.cpp | 8 +++---- src/theory/model.h | 8 +++---- src/theory/options_handlers.h | 4 +--- src/theory/output_channel.h | 6 ++--- .../quantifiers/candidate_generator.cpp | 4 +--- src/theory/quantifiers/candidate_generator.h | 8 +++---- src/theory/quantifiers/first_order_model.cpp | 6 ++--- src/theory/quantifiers/first_order_model.h | 6 ++--- src/theory/quantifiers/inst_match.cpp | 8 +++---- src/theory/quantifiers/inst_match.h | 8 +++---- .../quantifiers/instantiation_engine.cpp | 6 ++--- src/theory/quantifiers/instantiation_engine.h | 6 ++--- .../quantifiers/instantiator_default.cpp | 6 ++--- src/theory/quantifiers/instantiator_default.h | 6 ++--- src/theory/quantifiers/model_builder.cpp | 6 ++--- src/theory/quantifiers/model_builder.h | 4 +--- src/theory/quantifiers/model_engine.cpp | 8 +++---- src/theory/quantifiers/model_engine.h | 4 +--- src/theory/quantifiers/modes.cpp | 10 ++++---- src/theory/quantifiers/modes.h | 10 ++++---- src/theory/quantifiers/options_handlers.h | 6 ++--- .../quantifiers/quantifiers_attributes.cpp | 24 +++++++++---------- .../quantifiers/quantifiers_attributes.h | 24 +++++++++---------- .../quantifiers/quantifiers_rewriter.cpp | 4 +--- src/theory/quantifiers/quantifiers_rewriter.h | 4 +--- src/theory/quantifiers/relevant_domain.cpp | 6 ++--- src/theory/quantifiers/relevant_domain.h | 6 ++--- src/theory/quantifiers/term_database.cpp | 8 +++---- src/theory/quantifiers/term_database.h | 8 +++---- src/theory/quantifiers/theory_quantifiers.cpp | 6 ++--- src/theory/quantifiers/theory_quantifiers.h | 6 ++--- .../theory_quantifiers_instantiator.cpp | 6 ++--- .../theory_quantifiers_instantiator.h | 6 ++--- .../theory_quantifiers_type_rules.h | 6 ++--- src/theory/quantifiers/trigger.cpp | 8 +++---- src/theory/quantifiers/trigger.h | 6 ++--- src/theory/quantifiers_engine.cpp | 6 ++--- src/theory/quantifiers_engine.h | 6 ++--- src/theory/rep_set.cpp | 24 +++++++++---------- src/theory/rep_set.h | 24 +++++++++---------- src/theory/rewriter.cpp | 6 ++--- src/theory/rewriter.h | 4 +--- src/theory/rewriter_attributes.h | 4 +--- src/theory/rewriter_tables_template.h | 6 ++--- .../rewriterules/rr_candidate_generator.cpp | 8 +++---- .../rewriterules/rr_candidate_generator.h | 6 ++--- src/theory/rewriterules/rr_inst_match.cpp | 4 +--- src/theory/rewriterules/rr_inst_match.h | 4 +--- src/theory/rewriterules/rr_inst_match_impl.h | 6 ++--- src/theory/rewriterules/rr_trigger.cpp | 4 +--- src/theory/rewriterules/rr_trigger.h | 6 ++--- .../rewriterules/theory_rewriterules.cpp | 4 +--- src/theory/rewriterules/theory_rewriterules.h | 4 +--- .../rewriterules/theory_rewriterules_params.h | 6 ++--- .../theory_rewriterules_preprocess.h | 6 ++--- .../theory_rewriterules_rewriter.h | 6 ++--- .../theory_rewriterules_rules.cpp | 6 ++--- .../rewriterules/theory_rewriterules_rules.h | 6 ++--- .../theory_rewriterules_type_rules.h | 6 ++--- src/theory/shared_terms_database.cpp | 8 +++---- src/theory/shared_terms_database.h | 6 ++--- src/theory/substitutions.cpp | 8 +++---- src/theory/substitutions.h | 6 ++--- src/theory/term_registration_visitor.cpp | 6 ++--- src/theory/term_registration_visitor.h | 4 +--- src/theory/theory.cpp | 8 +++---- src/theory/theory.h | 6 ++--- src/theory/theory_engine.cpp | 8 +++---- src/theory/theory_engine.h | 6 ++--- src/theory/theory_registrar.h | 6 ++--- src/theory/theory_test_utils.h | 6 ++--- src/theory/theory_traits_template.h | 6 ++--- src/theory/theoryof_mode.h | 10 ++++---- src/theory/type_enumerator.h | 4 +--- src/theory/type_enumerator_template.cpp | 6 ++--- src/theory/uf/equality_engine.cpp | 6 ++--- src/theory/uf/equality_engine.h | 8 +++---- src/theory/uf/equality_engine_types.h | 6 ++--- src/theory/uf/inst_strategy.cpp | 8 +++---- src/theory/uf/inst_strategy.h | 6 ++--- src/theory/uf/options_handlers.h | 4 +--- src/theory/uf/symmetry_breaker.cpp | 4 +--- src/theory/uf/symmetry_breaker.h | 4 +--- src/theory/uf/theory_uf.cpp | 6 ++--- src/theory/uf/theory_uf.h | 6 ++--- src/theory/uf/theory_uf_instantiator.cpp | 8 +++---- src/theory/uf/theory_uf_instantiator.h | 8 +++---- src/theory/uf/theory_uf_model.cpp | 8 +++---- src/theory/uf/theory_uf_model.h | 6 ++--- src/theory/uf/theory_uf_rewriter.h | 4 +--- src/theory/uf/theory_uf_strong_solver.cpp | 6 ++--- src/theory/uf/theory_uf_strong_solver.h | 6 ++--- src/theory/uf/theory_uf_type_rules.h | 6 ++--- src/theory/unconstrained_simplifier.cpp | 6 ++--- src/theory/unconstrained_simplifier.h | 8 +++---- src/theory/valuation.cpp | 8 +++---- src/theory/valuation.h | 8 +++---- src/util/abstract_value.cpp | 4 +--- src/util/abstract_value.h | 4 +--- src/util/array.h | 4 +--- src/util/array_store_all.cpp | 4 +--- src/util/array_store_all.h | 4 +--- src/util/ascription_type.h | 4 +--- src/util/backtrackable.h | 4 +--- src/util/bitvector.h | 8 +++---- src/util/bool.h | 4 +--- src/util/boolean_simplification.cpp | 4 +--- src/util/boolean_simplification.h | 4 +--- src/util/cache.h | 4 +--- src/util/cardinality.cpp | 4 +--- src/util/cardinality.h | 4 +--- src/util/channel.h | 6 ++--- src/util/configuration.cpp | 4 +--- src/util/configuration.h | 4 +--- src/util/configuration_private.h | 9 ++----- src/util/cvc4_assert.cpp | 8 +++---- src/util/cvc4_assert.h | 6 ++--- src/util/datatype.cpp | 4 +--- src/util/datatype.h | 4 +--- src/util/debug.h | 4 +--- src/util/dense_map.h | 6 ++--- src/util/dump.cpp | 4 +--- src/util/dump.h | 4 +--- src/util/dynamic_array.h | 4 +--- src/util/exception.cpp | 4 +--- src/util/exception.h | 6 ++--- src/util/gmp_util.h | 4 +--- src/util/hash.h | 4 +--- src/util/index.h | 6 ++--- src/util/integer_cln_imp.h | 6 ++--- src/util/integer_gmp_imp.h | 6 ++--- src/util/ite_removal.cpp | 6 ++--- src/util/ite_removal.h | 8 +++---- src/util/language.cpp | 6 ++--- src/util/language.h | 6 ++--- src/util/lemma_input_channel.h | 6 ++--- src/util/lemma_output_channel.h | 4 +--- src/util/matcher.h | 4 +--- src/util/node_visitor.h | 10 ++++---- src/util/ntuple.h | 4 +--- src/util/output.cpp | 4 +--- src/util/output.h | 4 +--- src/util/predicate.cpp | 4 +--- src/util/predicate.h | 4 +--- src/util/proof.h | 4 +--- src/util/propositional_query.cpp | 4 +--- src/util/propositional_query.h | 4 +--- src/util/rational_cln_imp.cpp | 4 +--- src/util/rational_cln_imp.h | 8 +++---- src/util/rational_gmp_imp.cpp | 4 +--- src/util/rational_gmp_imp.h | 8 +++---- src/util/recursion_breaker.h | 4 +--- src/util/result.cpp | 4 +--- src/util/result.h | 4 +--- src/util/sexpr.cpp | 6 ++--- src/util/sexpr.h | 6 ++--- src/util/statistics.cpp | 4 +--- src/util/statistics.h | 4 +--- src/util/statistics_registry.cpp | 4 +--- src/util/statistics_registry.h | 4 +--- src/util/subrange_bound.h | 6 ++--- src/util/trans_closure.cpp | 6 ++--- src/util/trans_closure.h | 6 ++--- src/util/uninterpreted_constant.cpp | 4 +--- src/util/uninterpreted_constant.h | 4 +--- src/util/util_model.cpp | 6 ++--- src/util/util_model.h | 8 +++---- src/util/utility.h | 4 +--- test/system/CVC4JavaTest.java | 17 +++++++++++++ test/system/boilerplate.cpp | 4 +--- test/system/cvc3_george.cpp | 4 +--- test/system/cvc3_george.h | 4 +--- test/system/cvc3_main.cpp | 4 +--- test/system/ouroborous.cpp | 4 +--- test/system/smt2_compliance.cpp | 4 +--- test/system/statistics.cpp | 4 +--- test/system/two_smt_engines.cpp | 4 +--- test/unit/context/cdlist_black.h | 6 ++--- .../context/cdlist_context_memory_black.h | 6 ++--- test/unit/context/cdmap_black.h | 6 ++--- test/unit/context/cdmap_white.h | 6 ++--- test/unit/context/cdo_black.h | 4 +--- test/unit/context/cdvector_black.h | 4 +--- test/unit/context/context_black.h | 4 +--- test/unit/context/context_mm_black.h | 4 +--- test/unit/context/context_white.h | 4 +--- test/unit/context/stacking_map_black.h | 4 +--- test/unit/context/stacking_vector_black.h | 4 +--- test/unit/expr/attribute_black.h | 8 +++---- test/unit/expr/attribute_white.h | 4 +--- test/unit/expr/expr_manager_public.h | 4 +--- test/unit/expr/expr_public.h | 6 ++--- test/unit/expr/kind_black.h | 4 +--- test/unit/expr/kind_map_black.h | 4 +--- test/unit/expr/node_black.h | 4 +--- test/unit/expr/node_builder_black.h | 4 +--- test/unit/expr/node_manager_black.h | 8 +++---- test/unit/expr/node_manager_white.h | 4 +--- test/unit/expr/node_self_iterator_black.h | 4 +--- test/unit/expr/node_white.h | 4 +--- test/unit/expr/symbol_table_black.h | 8 +++---- test/unit/expr/type_cardinality_public.h | 4 +--- test/unit/expr/type_node_white.h | 4 +--- test/unit/main/interactive_shell_black.h | 6 ++--- test/unit/memory.h | 4 +--- test/unit/parser/parser_black.h | 4 +--- test/unit/parser/parser_builder_black.h | 4 +--- test/unit/prop/cnf_stream_white.h | 8 +++---- test/unit/theory/logic_info_white.h | 4 +--- test/unit/theory/stacking_map_black.h | 4 +--- test/unit/theory/theory_arith_white.h | 8 +++---- test/unit/theory/theory_black.h | 8 +++---- test/unit/theory/theory_bv_white.h | 6 ++--- test/unit/theory/theory_engine_white.h | 6 ++--- test/unit/theory/theory_white.h | 8 +++---- test/unit/theory/type_enumerator_white.h | 4 +--- test/unit/util/array_store_all_black.h | 4 +--- test/unit/util/assert_white.h | 4 +--- test/unit/util/bitvector_black.h | 4 +--- test/unit/util/boolean_simplification_black.h | 4 +--- test/unit/util/cardinality_public.h | 4 +--- test/unit/util/configuration_black.h | 4 +--- test/unit/util/datatype_black.h | 4 +--- test/unit/util/exception_black.h | 4 +--- test/unit/util/integer_black.h | 4 +--- test/unit/util/integer_white.h | 4 +--- test/unit/util/output_black.h | 4 +--- test/unit/util/rational_black.h | 4 +--- test/unit/util/rational_white.h | 4 +--- test/unit/util/recursion_breaker_black.h | 4 +--- test/unit/util/stats_black.h | 4 +--- test/unit/util/subrange_bound_white.h | 4 +--- test/unit/util/trans_closure_black.h | 6 ++--- 531 files changed, 1020 insertions(+), 2063 deletions(-) diff --git a/AUTHORS b/AUTHORS index 19eac8dce..133786ae1 100644 --- a/AUTHORS +++ b/AUTHORS @@ -8,8 +8,8 @@ The core authors and designers of CVC4 are: Liana Hadarean , New York University Dejan Jovanovic , New York University Tim King , New York University - Andrew Reynolds , University of Iowa - Cesare Tinelli , University of Iowa + Andrew Reynolds , The University of Iowa + Cesare Tinelli , The University of Iowa CVC4 is the fourth in the CVC series of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. Information about diff --git a/COPYING b/COPYING index df32895e7..648b42a02 100644 --- a/COPYING +++ b/COPYING @@ -1,6 +1,5 @@ -CVC4 is copyright (C) 2009, 2010, 2011, 2012 the ACSys research group at -the Courant Institute for Mathematical Sciences, New York University. -All rights reserved. +CVC4 is copyright (C) 2009, 2010, 2011, 2012 New York University and +The University of Iowa. All rights reserved. CVC4 is open-source; distribution is under the terms of the modified BSD license. However, certain builds of CVC4 link against GPLed libraries, diff --git a/README b/README index d70d4c221..4ae472659 100644 --- a/README +++ b/README @@ -2,10 +2,10 @@ This is CVC4 release version 1.0. For build and installation notes, please see the INSTALL file included with this distribution. This first official release of CVC4 is the result of more than three -years of efforts by researchers at New York University and the +years of efforts by researchers at New York University and The University of Iowa. The project leaders are Clark Barrett (New York -University) and Cesare Tinelli (University of Iowa). For a full list -of authors, please refer to the AUTHORS file in the source +University) and Cesare Tinelli (The University of Iowa). For a full +list of authors, please refer to the AUTHORS file in the source distribution. CVC4 is a tool for determining the satisfiability of a first order diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 94df7fe48..8ac920bbf 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -32,7 +32,7 @@ # the license.) # -my $excluded_directories = '^(minisat|CVS|generated)$'; +my $excluded_directories = '^(minisat|bvminisat|cryptominisat|CVS|generated)$'; my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$'; # Years of copyright for the template. E.g., the string @@ -41,18 +41,14 @@ my $years = '2009-2012'; my $standard_template = <