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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 15 Feb 2013 16:19:08 +0000 (11:19 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Sat, 16 Feb 2013 20:23:00 +0000 (15:23 -0500)
commit	f06ae104dc3caf9b4ff01a0b2d49b09ace88faad
tree	488669992e6d375450e18a2c92659be3f93f7a88	tree
parent	5e29fdffd2f72212d699316f9b27e1bf9d6c715c	commit \| diff

Some cleanup and copyright updating

* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles

46 files changed:

COPYING		diff \| blob \| history
contrib/configure-in-place		diff \| blob \| history
contrib/mac-build		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
src/context/cdinsert_hashmap.h		diff \| blob \| history
src/context/cdtrail_hashmap.h		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/decision_strategy.h		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/expr/mkexpr		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/options/mkoptions		diff \| blob \| history
src/parser/bounded_token_buffer.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt1/Smt1.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2_input.h		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/proof/sat_proof.h		diff \| blob \| history
src/prop/bvminisat/Makefile	[new file with mode: 0644]	blob
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/delta_rational.h		diff \| blob \| history
src/theory/arith/options		diff \| blob \| history
src/theory/arith/options_handlers.h		diff \| blob \| history
src/theory/arrays/theory_arrays_model.cpp		diff \| blob \| history
src/theory/mkrewriter		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/model.h		diff \| blob \| history
src/theory/quantifiers/inst_gen.h		diff \| blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/rep_set.h		diff \| blob \| history
src/theory/rewriterules/rr_candidate_generator.h		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/configuration_private.h		diff \| blob \| history
src/util/integer.h.in		diff \| blob \| history
src/util/rational.h.in		diff \| blob \| history
src/util/sort_inference.cpp		diff \| blob \| history
src/util/tls.h.in		diff \| blob \| history
test/regress/regress1/arith/Makefile	[new file with mode: 0644]	blob

RSS Atom