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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 23 Oct 2012 23:40:29 +0000 (23:40 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 23 Oct 2012 23:40:29 +0000 (23:40 +0000)
commit	304404e3709ff7e95156c87f65a3e2647d9f3441
tree	10fd1c4cc42567c3fac5fd91ad76aef3d49975b5	tree
parent	697dd317af39a896865c99b922e80baac2bb4b23	commit \| diff

more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code

23 files changed:

src/theory/quantifiers/Makefile.am		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.cpp	[new file with mode: 0755]	blob
src/theory/quantifiers/inst_match_generator.h	[new file with mode: 0755]	blob
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.cpp		diff \| blob \| history
src/theory/rewriterules/rr_inst_match.h		diff \| blob \| history
src/theory/rewriterules/rr_inst_match_impl.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.cpp		diff \| blob \| history
src/theory/uf/theory_uf_instantiator.h		diff \| blob \| history