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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Wed, 3 Jul 2013 21:13:31 +0000 (17:13 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Wed, 27 Nov 2013 22:55:53 +0000 (17:55 -0500)
commit	a97891f9cc892fdc261cd4e3d3229ec68f05b45e
tree	a05c30ddbe81d9dd084a2e024875f829d6f1f3a7	tree
parent	b28a42c3a4fd8c9b079b157ad8ff36e581b60d29	commit \| diff

General pre-release cleanup commit

* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing

45 files changed:

contrib/theoryskel/README.WHATS-NEXT		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/expr/command.cpp		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		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_type_rules.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		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/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/bv/bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/decision_attributes.h		diff \| blob \| history
src/theory/model.cpp	[deleted file]	blob \| history
src/theory/model.h	[deleted file]	blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_model.cpp	[new file with mode: 0644]	blob
src/theory/theory_model.h	[new file with mode: 0644]	blob
src/theory/theory_traits_template.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/model.cpp	[new file with mode: 0644]	blob
src/util/model.h	[new file with mode: 0644]	blob
src/util/util_model.cpp	[deleted file]	blob \| history
src/util/util_model.h	[deleted file]	blob \| history

RSS Atom