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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 25 Mar 2021 18:17:30 +0000 (13:17 -0500)
committer	GitHub <noreply@github.com>
	Thu, 25 Mar 2021 18:17:30 +0000 (18:17 +0000)
commit	8a3876f74f377817345af405aebfceebc7896059
tree	82474f0df4b65274e6fbbb8a2d3f56ec42815a40	tree
parent	f9e3d2dccd5018e07df1c2cd323c5e192b020819	commit \| diff

Refactor construction of triggers (#6209)

This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.

27 files changed:

src/CMakeLists.txt		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_simple.cpp		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/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_database.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/ematching/trigger_database.h	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/quantifiers_statistics.h	[new file with mode: 0644]	blob
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom