Split pattern term selector from trigger (#5811)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Jan 2021 19:04:46 +0000 (13:04 -0600)
committerGitHub <noreply@github.com>
Wed, 27 Jan 2021 19:04:46 +0000 (13:04 -0600)
commit2c4025e44771707ba548b6d8aa5a8a13ec3cd8f1
tree89b4a2a0eefe117dc1fb714af6c82bab34f339c3
parent8795787c2ef337e73b46778b99f5bfa6c2a19f93
Split pattern term selector from trigger (#5811)

This separates the utilities for selecting pattern terms from the Trigger class itself. This includes a PatternTermSelector, which implements the techniques for selecting the pool of pattern terms, and TriggerTermInfo which contains basic information about pattern terms.

It makes minor refactoring to make the PatternTermSelector class more than just static methods, e.g. it is now a configurable object that selects pattern terms. This makes some of the methods take fewer arguments.

More refactoring is possible, to be addressed on future PRs.
15 files changed:
src/CMakeLists.txt
src/preprocessing/passes/quantifier_macros.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/ematching/inst_match_generator.cpp
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
src/theory/quantifiers/ematching/pattern_term_selector.cpp [new file with mode: 0644]
src/theory/quantifiers/ematching/pattern_term_selector.h [new file with mode: 0644]
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/ematching/trigger.h
src/theory/quantifiers/ematching/trigger_term_info.cpp [new file with mode: 0644]
src/theory/quantifiers/ematching/trigger_term_info.h [new file with mode: 0644]
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/term_database.cpp