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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 27 Nov 2018 21:39:13 +0000 (15:39 -0600)
committer	Andres Noetzli <andres.noetzli@gmail.com>
	Tue, 27 Nov 2018 21:39:13 +0000 (13:39 -0800)
commit	a2bba0806dab0e0d4728bbba8e4e6b4160335eeb
tree	76a9508f241908561176d2105a59195137944ec6	tree
parent	711234e01a17289d1fa4af3574ddf5d6de2405a1	commit \| diff

Make (T)NodeTrie a general utility (#2489)

This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.

25 files changed:

src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/node_trie.cpp	[new file with mode: 0644]	blob
src/expr/node_trie.h	[new file with mode: 0644]	blob
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_epr_instantiator.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/inst_propagator.h		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.cpp		diff \| blob \| history
src/theory/quantifiers/local_theory_ext.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history

RSS Atom