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

author	Morgan Deters <mdeters@gmail.com>
	Tue, 31 Jul 2012 21:24:31 +0000 (21:24 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Tue, 31 Jul 2012 21:24:31 +0000 (21:24 +0000)
commit	b88133bc679c541798c2063fec2bc441e744328a
tree	42097c3b9dabc5f4195e489158ea122e73155813	tree
parent	f73e17d5649f636eb88aafe05aaf32565a806bab	commit \| diff

Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.

The namespaces weren't changed, only the file locations.

50 files changed:

src/theory/Makefile.am		diff \| blob \| history
src/theory/arrays/theory_arrays_instantiator.cpp		diff \| blob \| history
src/theory/candidate_generator.cpp	[deleted file]	blob \| history
src/theory/candidate_generator.h	[deleted file]	blob \| history
src/theory/datatypes/theory_datatypes_instantiator.cpp		diff \| blob \| history
src/theory/inst_match.cpp	[deleted file]	blob \| history
src/theory/inst_match.h	[deleted file]	blob \| history
src/theory/instantiator_default.cpp	[deleted file]	blob \| history
src/theory/instantiator_default.h	[deleted file]	blob \| history
src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/candidate_generator.h	[new file with mode: 0644]	blob
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_match.h	[new file with mode: 0644]	blob
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/instantiator_default.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/instantiator_default.h	[new file with mode: 0644]	blob
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/model_engine.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
src/theory/quantifiers/rep_set_iterator.h		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_instantiator.h		diff \| blob \| history
src/theory/quantifiers/trigger.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/trigger.h	[new file with mode: 0644]	blob
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriterules/Makefile.am		diff \| blob \| history
src/theory/rewriterules/rr_candidate_generator.cpp	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_candidate_generator.h	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_inst_match.cpp	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_inst_match.h	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_inst_match_impl.h	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_trigger.cpp	[new file with mode: 0644]	blob
src/theory/rewriterules/rr_trigger.h	[new file with mode: 0644]	blob
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rr_candidate_generator.cpp	[deleted file]	blob \| history
src/theory/rr_candidate_generator.h	[deleted file]	blob \| history
src/theory/rr_inst_match.cpp	[deleted file]	blob \| history
src/theory/rr_inst_match.h	[deleted file]	blob \| history
src/theory/rr_inst_match_impl.h	[deleted file]	blob \| history
src/theory/rr_trigger.cpp	[deleted file]	blob \| history
src/theory/rr_trigger.h	[deleted file]	blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/trigger.cpp	[deleted file]	blob \| history
src/theory/trigger.h	[deleted file]	blob \| history
src/theory/uf/inst_strategy.h		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.h		diff \| blob \| history

RSS Atom