Reimplement support for relational triggers (#7063)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 16:14:50 +0000 (11:14 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 16:14:50 +0000 (16:14 +0000)
commitb038b34584f37c40a6dc4a476e8f486cf6977b81
tree35ae34b5d91f2f4f9790a0237734b77a1c055f89
parent3e9e1c54ef54627e4f38094910effb32f6ad7cd2
Reimplement support for relational triggers (#7063)

This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.

This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.

This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.
src/CMakeLists.txt
src/theory/quantifiers/ematching/inst_match_generator.cpp
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
src/theory/quantifiers/ematching/relational_match_generator.cpp [new file with mode: 0644]
src/theory/quantifiers/ematching/relational_match_generator.h [new file with mode: 0644]
src/theory/quantifiers/ematching/trigger_term_info.cpp
src/theory/quantifiers/ematching/trigger_term_info.h
test/regress/CMakeLists.txt
test/regress/regress0/quantifiers/veqt-delta.smt2 [new file with mode: 0644]
test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 [new file with mode: 0644]