From b203bed15b9b907ea23422417fb0aa4773830483 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Nov 2021 06:29:14 -0600
Subject: 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               |  8 ++++++
 .../quantifiers/ematching/candidate_generator.cpp  | 29 ++++++++++++++--------
 .../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
@@ -258,6 +258,14 @@ name   = "Quantifiers"
   default    = "false"
   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"
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
-- 
cgit v1.2.3