Properly implement datatype selector triggers (#5624)

This ensures that datatype selectors are properly handled as triggers in E-matching.

This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.

It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).

This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.

Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.

FYI @barrettcw

2 files changed, 8 insertions, 6 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b1f56ea37..3bb49b703 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1152,15 +1152,14 @@ Node SmtEngine::simplify(const Node& ex)
   return d_pp->simplify(ex);
 }
 
-Node SmtEngine::expandDefinitions(const Node& ex)
+Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
 {
   d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
 
   SmtScope smts(this);
   finishInit();
   d_state->doPendingPops();
-  // set expandOnly flag to true
-  return d_pp->expandDefinitions(ex, true);
+  return d_pp->expandDefinitions(ex, expandOnly);
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f8a74597b..6f08359b5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -510,12 +510,15 @@ class CVC4_PUBLIC SmtEngine
   Node simplify(const Node& e);
 
   /**
-   * Expand the definitions in a term or formula.  No other
-   * simplification or normalization is done.
+   * Expand the definitions in a term or formula.
+   *
+   * @param n The node to expand
+   * @param expandOnly if true, then the expandDefinitions function of
+   * TheoryEngine is not called on subterms of n.
    *
    * @throw TypeCheckingException, LogicException, UnsafeInterruptException
    */
-  Node expandDefinitions(const Node& e);
+  Node expandDefinitions(const Node& n, bool expandOnly = true);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded by a SAT