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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Thu, 5 Dec 2013 20:04:30 +0000 (15:04 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Thu, 5 Dec 2013 20:41:28 +0000 (15:41 -0500)
commit	d692211d62a5d5a58c4bbe11b495554671c43847
tree	5097a72499b72d54630d7dc7f890831eb1996b00	tree
parent	2fab0a67761f8b63a3c3f5abdbe7f382f722a04f	commit \| diff

Update copyrights, add missing file-level documentation; fix perms.

195 files changed:

examples/hashsmt/sha1.hpp		diff \| blob \| history
examples/hashsmt/sha1smt.cpp		diff \| blob \| history
examples/hashsmt/word.h		diff \| blob \| history
examples/nra-translate/normalize.cpp		diff \| blob \| history
examples/nra-translate/smt2info.cpp		diff \| blob \| history
examples/nra-translate/smt2todreal.cpp		diff \| blob \| history
src/compat/cvc3_compat.cpp		diff \| blob \| history
src/context/cdvector.h		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/decision_mode.h		diff \| blob \| history
src/decision/options_handlers.h		diff \| blob \| history
src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/attribute_unique_id.h		diff \| blob \| history
src/expr/command.cpp		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/pickle_data.h		diff \| blob \| history
src/expr/type_checker.h		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/options_handlers.h		diff \| blob \| history
src/parser/bounded_token_factory.cpp		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt1/smt1.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/parser/tptp/tptp_input.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/proof/proof_manager.h		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/proof/theory_proof.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_types.h		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/model_postprocessor.cpp		diff \| blob \| history
src/smt/options_handlers.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/arith_heuristic_pivot_rule.cpp		diff \| blob \| history
src/theory/arith/arith_heuristic_pivot_rule.h		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/arithvar.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.h		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/options_handlers.h		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/simplex_update.cpp		diff \| blob \| history
src/theory/arith/simplex_update.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.h		diff \| blob \| history
src/theory/arith/tableau.cpp		diff \| blob \| history
src/theory/arith/tableau.h		diff \| blob \| history
src/theory/arith/tableau_sizes.cpp		diff \| blob \| history
src/theory/arith/tableau_sizes.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.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/arith/theory_arith_private_forward.h		diff \| blob \| history
src/theory/arith/theory_arith_type_rules.h		diff \| blob \| history
src/theory/atom_requests.cpp		diff \| blob \| history
src/theory/atom_requests.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/bv/bitblast_strategies.cpp		diff \| blob \| history
src/theory/bv/bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblaster.h		diff \| blob \| history
src/theory/bv/bv_inequality_graph.cpp		diff \| blob \| history
src/theory/bv/bv_inequality_graph.h		diff \| blob \| history
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.h		diff \| blob \| history
src/theory/bv/bv_to_bool.cpp		diff \| blob \| history
src/theory/bv/bv_to_bool.h		diff \| blob \| history
src/theory/bv/slicer.cpp		diff \| blob \| history
src/theory/bv/slicer.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/decision_attributes.h		diff \| blob \| history
src/theory/idl/idl_assertion.cpp		diff \| blob \| history
src/theory/idl/idl_assertion.h		diff \| blob \| history
src/theory/idl/idl_assertion_db.cpp		diff \| blob \| history
src/theory/idl/idl_assertion_db.h		diff \| blob \| history
src/theory/idl/idl_model.cpp		diff \| blob \| history
src/theory/idl/idl_model.h		diff \| blob \| history
src/theory/idl/theory_idl.cpp		diff \| blob \| history
src/theory/idl/theory_idl.h		diff \| blob \| history
src/theory/ite_utilities.cpp		diff \| blob \| history
src/theory/ite_utilities.h		diff \| blob \| history
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_reasoning.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_reasoning.h		diff \| blob \| history
src/theory/quantifiers/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/relevant_domain.h	[changed mode: 0755->0644]	blob \| history
src/theory/quantifiers/rewrite_engine.cpp	[changed mode: 0755->0644]	diff \| blob \| history
src/theory/quantifiers/rewrite_engine.h	[changed mode: 0755->0644]	diff \| blob \| history
src/theory/quantifiers/symmetry_breaking.cpp	[changed mode: 0755->0644]	diff \| blob \| history
src/theory/quantifiers/symmetry_breaking.h	[changed mode: 0755->0644]	diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp	[changed mode: 0755->0644]	blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriter_tables_template.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rewriter.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/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.h		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.h		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.h		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.h		diff \| blob \| history
src/theory/theory_registrar.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
src/theory/unconstrained_simplifier.h		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/configuration.cpp		diff \| blob \| history
src/util/configuration.h		diff \| blob \| history
src/util/configuration_private.h		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/gmp_util.h		diff \| blob \| history
src/util/hash.h		diff \| blob \| history
src/util/index.h		diff \| blob \| history
src/util/ite_removal.cpp		diff \| blob \| history
src/util/ite_removal.h		diff \| blob \| history
src/util/maybe.h		diff \| blob \| history
src/util/model.cpp		diff \| blob \| history
src/util/model.h		diff \| blob \| history
src/util/nary_builder.cpp		diff \| blob \| history
src/util/nary_builder.h		diff \| blob \| history
src/util/regexp.h		diff \| blob \| history
test/unit/context/cdvector_black.h		diff \| blob \| history
test/unit/expr/attribute_white.h		diff \| blob \| history
test/unit/expr/expr_manager_public.h		diff \| blob \| history
test/unit/theory/logic_info_white.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history

RSS Atom