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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 1 Aug 2019 14:26:26 +0000 (09:26 -0500)
committer	GitHub <noreply@github.com>
	Thu, 1 Aug 2019 14:26:26 +0000 (09:26 -0500)
commit	c1d9bed7f73db9567f635f59cde134795e65c9ba
tree	cec6839b42cc6c691bbb888bd356f627d973e968	tree
parent	79881c196e29ef341166e7a31c1183e8b537d069	commit \| diff

Move some generic utilities out of quantifiers (#3139)

18 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/match_trie.cpp	[new file with mode: 0644]	blob
src/expr/match_trie.h	[new file with mode: 0644]	blob
src/expr/term_canonize.cpp	[new file with mode: 0644]	blob
src/expr/term_canonize.h	[new file with mode: 0644]	blob
src/preprocessing/passes/symmetry_detect.h		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
src/theory/quantifiers/anti_skolem.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/term_canonize.cpp	[deleted file]	blob \| history
src/theory/quantifiers/term_canonize.h	[deleted file]	blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history