Revert change and clean datatypes cons candidate generator (#7645)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 17 Nov 2021 12:29:14 +0000 (06:29 -0600)
committerGitHub <noreply@github.com>
Wed, 17 Nov 2021 12:29:14 +0000 (12:29 +0000)
commitb203bed15b9b907ea23422417fb0aa4773830483
treed88e18b4c4ba531205e2dc8d9b032cc51ffca9c4
parent09e934c84777ef4dbc74b19e22ec24a1c643c71b
Revert change and clean datatypes cons candidate generator (#7645)

PR #7600 refactored and optimized candidate generator. This PR actually corrected an issue where the datatypes constructor expansion candidate generator did not generate instances for triggers whose top symbol is a constructor. However, fixing it to generate instances led to a performance regression on Facebook benchmarks.

This PR reverts the behavior change from that PR, and moreover makes it explicit that we do not generate instances in this case.
src/options/quantifiers_options.toml
src/theory/quantifiers/ematching/candidate_generator.cpp
src/theory/quantifiers/ematching/candidate_generator.h