diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-17 06:29:14 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-17 12:29:14 +0000 |
commit | b203bed15b9b907ea23422417fb0aa4773830483 (patch) | |
tree | d88e18b4c4ba531205e2dc8d9b032cc51ffca9c4 | |
parent | 09e934c84777ef4dbc74b19e22ec24a1c643c71b (diff) |
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.
-rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/candidate_generator.h | 2 |
3 files changed, 28 insertions, 11 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index e53d3f5ba..80692055f 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -259,6 +259,14 @@ name = "Quantifiers" help = "use triggers that do not contain all free variables" [[option]] + name = "consExpandTriggers" + category = "regular" + long = "cons-exp-triggers" + type = "bool" + default = "false" + help = "use constructor expansion for single constructor datatypes triggers" + +[[option]] name = "multiTriggerWhenSingle" category = "regular" long = "multi-trigger-when-single" diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 513a3965b..57752d375 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -64,11 +64,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) d_eqc = eqc; d_op = op; d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op); - if (d_termIterList == nullptr) - { - d_mode = cand_term_none; - } - else if (eqc.isNull()) + if (eqc.isNull()) { d_mode = cand_term_db; }else{ @@ -109,11 +105,15 @@ Node CandidateGeneratorQE::getNextCandidate(){ Node CandidateGeneratorQE::getNextCandidateInternal() { if( d_mode==cand_term_db ){ - Assert(d_termIterList != nullptr); + if (d_termIterList == nullptr) + { + d_mode = cand_term_none; + return Node::null(); + } Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; //get next candidate term in the uf term database - size_t tlSize = d_termIterList->d_list.size(); - while (d_termIter < tlSize) + size_t tlLimit = d_termIterList->d_list.size(); + while (d_termIter < tlLimit) { Node n = d_termIterList->d_list[d_termIter]; d_termIter++; @@ -254,8 +254,17 @@ void CandidateGeneratorConsExpand::reset(Node eqc) d_termIter = 0; if (eqc.isNull()) { - d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op); - d_mode = d_termIterList == nullptr ? cand_term_none : cand_term_db; + // generates too many instantiations at top-level when eqc is null, thus + // set mode to none unless option is set. + if (options::consExpandTriggers()) + { + d_termIterList = d_treg.getTermDatabase()->getGroundTermList(d_op); + d_mode = cand_term_db; + } + else + { + d_mode = cand_term_none; + } } else { diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 5c85d118f..3b4017e99 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -206,7 +206,7 @@ class CandidateGeneratorQEAll : public CandidateGenerator * This modifies the candidates t1, ..., tn generated by CandidateGeneratorQE * so that they are "expansions" of a fixed datatype constructor C. Assuming * C has arity m, we instead return the stream: - * C(sel_1( t1 ), ..., sel_m( tn )) ... C(sel_1( t1 ), ..., C( sel_m( tn )) + * C(sel_1( t1 ), ..., sel_m( t1 )) ... C(sel_1( tn ), ..., C( sel_m( tn )) * where sel_1 ... sel_m are the selectors of C. */ class CandidateGeneratorConsExpand : public CandidateGeneratorQE |