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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 25 Nov 2017 01:08:41 +0000 (19:08 -0600)
committer	GitHub <noreply@github.com>
	Sat, 25 Nov 2017 01:08:41 +0000 (19:08 -0600)
commit	3ab0db55341e7e752411bb003fb203fcd9ec9120
tree	df79841a5e8244ea159ccc4a5e32c9e9d5fee2dc	tree
parent	bb095659fb12e3733a73f1be31769ff5b5eb6055	commit \| diff

(Refactor) Instantiate utility (#1387)

33 files changed:

src/Makefile.am		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.h		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/ho_trigger.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/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_match_trie.h	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_propagator.cpp		diff \| blob \| history
src/theory/quantifiers/inst_propagator.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/instantiate.h	[new file with mode: 0644]	blob
src/theory/quantifiers/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.h		diff \| blob \| history
src/theory/quantifiers/rewrite_engine.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.h		diff \| blob \| history
src/theory/quantifiers/trigger.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom