From cdec9ce9b5ea190344f63423ebed93bea5f95571 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Apr 2022 14:41:34 -0500
Subject: [PATCH] Minor simplifications for datatype selector triggers (#8636)

This is leftover simplification from the fact that (s x) is no longer expanded to (ite (is-C x) (s_total x) (uf x)).
---
 .../ematching/candidate_generator.cpp         | 42 +++----------------
 .../ematching/candidate_generator.h           |  2 -
 .../ematching/instantiation_engine.cpp        |  2 +-
 src/theory/quantifiers/instantiate.cpp        |  1 +
 4 files changed, 7 insertions(+), 40 deletions(-)

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 1e1c9a018..ca092c4fa 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -309,37 +309,19 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
 {
   Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
   Assert(mpat.getKind() == APPLY_SELECTOR);
-  // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
-  // expand definitions is eliminated, however, this also requires avoiding
-  // term formula removal.
+  // Get the expanded form of the selector, meaning that we will match on
+  // the shared selector if shared selectors are enabled.
   Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat);
   Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
-  if (mpatExp.getKind() == ITE)
-  {
-    Assert(mpatExp[1].getKind() == APPLY_SELECTOR);
-    Assert(mpatExp[2].getKind() == APPLY_UF);
-    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
-    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
-  }
-  else if (mpatExp.getKind() == APPLY_SELECTOR)
-  {
-    // corner case of datatype with one constructor
-    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
-  }
-  else
-  {
-    // corner case of a wrongly applied selector as a trigger
-    Assert(mpatExp.getKind() == APPLY_UF);
-    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
-  }
-  Assert(d_selOp != d_ufOp);
+  Assert (mpatExp.getKind() == APPLY_SELECTOR);
+  d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
 }
 
 void CandidateGeneratorSelector::reset(Node eqc)
 {
   Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
   // start with d_selOp, if it exists
-  resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
+  resetForOperator(eqc, d_selOp);
 }
 
 Node CandidateGeneratorSelector::getNextCandidate()
@@ -350,20 +332,6 @@ Node CandidateGeneratorSelector::getNextCandidate()
     Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
     return nextc;
   }
-  else if (d_op == d_selOp)
-  {
-    if (d_ufOp.isNull())
-    {
-      // corner case: selector cannot be wrongly applied (1-cons case)
-      d_op = Node::null();
-    }
-    else
-    {
-      // finished correctly applied selectors, now try incorrectly applied ones
-      resetForOperator(d_eqc, d_ufOp);
-      return getNextCandidate();
-    }
-  }
   Trace("sel-trigger-debug") << "...finished" << std::endl;
   // no more candidates
   return Node::null();
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 0c830d8ef..36d91e4cd 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -255,8 +255,6 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE
  protected:
   /** the selector operator */
   Node d_selOp;
-  /** the UF operator */
-  Node d_ufOp;
 };
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index a1cef29b2..bf7a4eb05 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -83,7 +83,7 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   bool finished = false;
   //while unfinished, try effort level=0,1,2....
   while( !finished && e<=eLimit ){
-    Trace("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
+    Trace("inst-engine-debug") << "IE: Prepare instantiation (" << e << ")." << std::endl;
     finished = true;
     //instantiate each quantifier
     for( unsigned i=0; i<d_quants.size(); i++ ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f52bfc8ef..7fa845d35 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -183,6 +183,7 @@ bool Instantiate::addInstantiation(Node q,
     }
 #endif
   }
+  Trace("inst-add-debug") << "id is " << id << std::endl;
 
   EntailmentCheck* ec = d_treg.getEntailmentCheck();
   // Note we check for entailment before checking for term vector duplication.
-- 
2.30.2