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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 16 Oct 2012 21:59:50 +0000 (21:59 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 16 Oct 2012 21:59:50 +0000 (21:59 +0000)
commit	d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7
tree	f730bb17eba9412258c47617f144510d722d6006	tree
parent	bbcfb5208c6c0f343d1a63b129c54914f66b2701	commit \| diff

more cleanup of quantifiers code

27 files changed:

src/theory/arith/theory_arith_instantiator.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/inst_gen.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp	[new file with mode: 0755]	blob
src/theory/quantifiers/quant_util.h	[new file with mode: 0755]	blob
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/uf/inst_strategy.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.cpp		diff \| blob \| history

RSS Atom