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

author	Morgan Deters <mdeters@gmail.com>
	Sat, 7 Jul 2012 21:01:33 +0000 (21:01 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Sat, 7 Jul 2012 21:01:33 +0000 (21:01 +0000)
commit	8b01efc32d61391d8d3cd2aaac0de49cd8e88ecc
tree	9e61b253a66fc91ca86b11bc1cabae9e1a7394da	tree
parent	8166b6cef258b198d0ffc97d125da3c85acf9708	commit \| diff

Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.

I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0

98 files changed:

contrib/extract-strings-and-comments	[new file with mode: 0755]	blob
contrib/spellcheck	[new file with mode: 0755]	blob
contrib/theoryskel/theory_DIR.h		diff \| blob \| history
src/context/cdhashmap_forward.h		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdhashset_forward.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/cdmaybe.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/decision/justification_heuristic.h		diff \| blob \| history
src/decision/relevancy.cpp		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/pickler.h		diff \| blob \| history
src/main/driver.cpp		diff \| blob \| history
src/main/driver_portfolio.cpp		diff \| blob \| history
src/proof/sat_proof.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_registry.cpp		diff \| blob \| history
src/prop/sat_solver_registry.h		diff \| blob \| history
src/prop/sat_solver_types.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/theory/arith/arith_priority_queue.h		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/arithvar.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/constraint.cpp		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/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/simplex.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_instantiator.cpp		diff \| blob \| history
src/theory/arith/theory_arith_instantiator.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/bv/bitblast_strategies.cpp		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/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/datatypes/theory_datatypes_instantiator.h		diff \| blob \| history
src/theory/inst_match.h		diff \| blob \| history
src/theory/inst_match_impl.h		diff \| blob \| history
src/theory/instantiator_default.h		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.h		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.cpp		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_params.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_preprocess.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rewriter.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.cpp		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_type_rules.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/term_registration_visitor.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_registrar.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/theoryof_mode.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/equality_engine_types.h		diff \| blob \| history
src/theory/uf/theory_uf_candidate_generator.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.h		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
src/util/backtrackable.h		diff \| blob \| history
src/util/bool.h		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/index.h		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/lemma_input_channel.h		diff \| blob \| history
src/util/node_visitor.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history
src/util/stats.cpp		diff \| blob \| history
test/system/cvc3_george.cpp		diff \| blob \| history
test/system/cvc3_george.h		diff \| blob \| history
test/unit/context/context_mm_black.h		diff \| blob \| history

RSS Atom