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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 28 Jan 2014 15:51:33 +0000 (09:51 -0600)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 28 Jan 2014 15:51:44 +0000 (09:51 -0600)
commit	d3822db24e15e255766866a47e6ffa0d8d91911b
tree	221298973f410f4305f74cd6041b6a017aaa3075	tree
parent	587bc5c82e2921a72cec58dc2ec69e3e0ed71866	commit \| diff

More optimizations of quantifier instantiation data structures.

24 files changed:

src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_gen.cpp		diff \| blob \| history
src/theory/quantifiers/inst_gen.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		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.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/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/trigger.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/rewriterules/efficient_e_matching.cpp		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/theory_rewriterules.cpp		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules_rules.cpp		diff \| blob \| history