Make datatype selector expansion to its own accessible method (#7069)

This eliminates another call to currentSmtEngine.

After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index e0e2f7ac8962975086d7f23161131c852b537cda..e41bef01507cf57133d7b43bcba238bafb69c689 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -824,6 +824,45 @@ Node DatatypesRewriter::replaceDebruijn(Node n,
   return n;
 }
 
+Node DatatypesRewriter::expandApplySelector(Node n)
+{
+  Assert(n.getKind() == APPLY_SELECTOR);
+  Node selector = n.getOperator();
+  // APPLY_SELECTOR always applies to an external selector, cindexOf is
+  // legal here
+  size_t cindex = utils::cindexOf(selector);
+  const DType& dt = utils::datatypeOf(selector);
+  const DTypeConstructor& c = dt[cindex];
+  Node selector_use;
+  TypeNode ndt = n[0].getType();
+  if (options::dtSharedSelectors())
+  {
+    size_t selectorIndex = utils::indexOf(selector);
+    Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
+    Assert(selectorIndex < c.getNumArgs());
+    selector_use = c.getSelectorInternal(ndt, selectorIndex);
+  }
+  else
+  {
+    selector_use = selector;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
+  if (options::dtRewriteErrorSel())
+  {
+    return sel;
+  }
+  Node tester = c.getTester();
+  Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
+  SkolemManager* sm = nm->getSkolemManager();
+  TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
+  Node f = sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
+  Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
+  Node ret = nm->mkNode(kind::ITE, tst, sel, sk);
+  Trace("dt-expand") << "Expand def : " << n << " to " << ret << std::endl;
+  return ret;
+}
+
 TrustNode DatatypesRewriter::expandDefinition(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -833,44 +872,7 @@ TrustNode DatatypesRewriter::expandDefinition(Node n)
   {
     case kind::APPLY_SELECTOR:
     {
-      Node selector = n.getOperator();
-      // APPLY_SELECTOR always applies to an external selector, cindexOf is
-      // legal here
-      size_t cindex = utils::cindexOf(selector);
-      const DType& dt = utils::datatypeOf(selector);
-      const DTypeConstructor& c = dt[cindex];
-      Node selector_use;
-      TypeNode ndt = n[0].getType();
-      if (options::dtSharedSelectors())
-      {
-        size_t selectorIndex = utils::indexOf(selector);
-        Trace("dt-expand") << "...selector index = " << selectorIndex
-                           << std::endl;
-        Assert(selectorIndex < c.getNumArgs());
-        selector_use = c.getSelectorInternal(ndt, selectorIndex);
-      }
-      else
-      {
-        selector_use = selector;
-      }
-      Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
-      if (options::dtRewriteErrorSel())
-      {
-        ret = sel;
-      }
-      else
-      {
-        Node tester = c.getTester();
-        Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
-        SkolemManager* sm = nm->getSkolemManager();
-        TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
-        Node f =
-            sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
-        Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
-        ret = nm->mkNode(kind::ITE, tst, sel, sk);
-        Trace("dt-expand") << "Expand def : " << n << " to " << ret
-                           << std::endl;
-      }
+      ret = expandApplySelector(n);
     }
     break;
     case APPLY_UPDATER:

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 89e1901fa41bb7af2d1cf75bbc9706b91825677c..7ba3c97589b9c96d67272278991b3254a686ffcb 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -48,6 +48,17 @@ class DatatypesRewriter : public TheoryRewriter
    * on all top-level codatatype subterms of n.
    */
   static Node normalizeConstant(Node n);
+  /**
+   * Expand an APPLY_SELECTOR term n, return its expanded form. If n is
+   *   (APPLY_SELECTOR selC x)
+   * its expanded form is
+   *   (ITE (APPLY_TESTER is-C x)
+   *     (APPLY_SELECTOR_TOTAL selC' x)
+   *     (f x))
+   * where f is a skolem function with id SELECTOR_WRONG, and selC' is the
+   * internal selector function for selC (possibly a shared selector).
+   */
+  static Node expandApplySelector(Node n);
   /** expand defintions */
   TrustNode expandDefinition(Node n) override;
 

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 5295302c4b6feaea3b76c6a9394e4588c6ed7ed5..0fd5c21d5e605b8678699980005d346b882a50d1 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -14,11 +14,13 @@
  */
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
+
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
@@ -292,7 +294,7 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
   // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
   // expand definitions is eliminated, however, this also requires avoiding
   // term formula removal.
-  Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
+  Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat);
   Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
   if (mpatExp.getKind() == ITE)
   {