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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 23 Mar 2021 20:41:13 +0000 (15:41 -0500)
committer	GitHub <noreply@github.com>
	Tue, 23 Mar 2021 20:41:13 +0000 (20:41 +0000)
commit	d5d526730d11d08c65aa17ea53d0dffb0a72e692
tree	13ce2001785e168ea82cbd0bce0c1750f987a338	tree
parent	8fc8793f4337663f7250846dd6acae167a7f27ec	commit \| diff

Passing term registry to ematching utilities (#6190)

Model is now nested into term registry.

This PR also resolves some complications due to namespaces within quantifiers.

53 files changed:

src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.h		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/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_term_info.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_term_info.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_trie.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_trie.h		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.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_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_registry.cpp		diff \| blob \| history
src/theory/quantifiers/term_registry.h		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom