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)).

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 1e1c9a01889f7929f7c7fcc07c77f45574869cd1..ca092c4fa4c01227d47d75964068ff792ae7c01d 100644 (file)
--- 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 0c830d8efff918fc3efe96660270dd644fcc766e..36d91e4cd91edaa30e378598e553c7084c90714e 100644 (file)
--- 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 a1cef29b2a59a6fb9dbd6a4a4b1d824c821daf13..bf7a4eb0529080f044b2848e55f8a4e3edd827cd 100644 (file)
--- 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 f52bfc8ef967f722e113b154ad9a825b12ebc646..7fa845d35246ba1a814108a38cbadb57c32960bb 100644 (file)
--- 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.