Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2cfc262c211453c7e49deed1f09f67e89a45fd6f..0dd86f8142ee211197129f353047fb425001f342 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -571,7 +571,6 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         /* Datatypes ------------------------------------------------------- */
         {cvc5::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
         {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
-        {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND},
         {cvc5::Kind::APPLY_TESTER, APPLY_TESTER},
         {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER},
         {cvc5::Kind::DT_SIZE, DT_SIZE},

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 535b96d5fd24554e006714575b019856cc06534b..1ca7893c02b601332f984c32bdc2b1e66b09ffe4 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -843,7 +843,6 @@ void Smt2Printer::toStream(std::ostream& out,
     }
   }
   break;
-  case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE: break;
 
   // separation logic

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index ca120c2414c085d114d6c5b24e0c5d794f028493..cbb94558457a3e373cf62452987b12f943e13d96 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -181,7 +181,7 @@ Node LfscNodeConverter::postConvert(Node n)
     return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
   }
   else if (k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_TESTER
-           || k == APPLY_SELECTOR_TOTAL || k == APPLY_UPDATER)
+           || k == APPLY_UPDATER)
   {
     // must convert other kinds of apply to functions, since we convert to
     // HO_APPLY
@@ -1089,12 +1089,9 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
       // get its variable name
       opName << getNameForUserNameOf(dt[index].getConstructor());
     }
-    else if (k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL)
+    else if (k == APPLY_SELECTOR)
     {
-      if (k == APPLY_SELECTOR_TOTAL)
-      {
-        ret = maybeMkSkolemFun(op, macroApply);
-      }
+      ret = maybeMkSkolemFun(op, macroApply);
       if (ret.isNull())
       {
         unsigned index = DType::indexOf(op);

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index a88421c7a8d48d8fcea63994053bc703c3cfefc2..57e2b7fcc3e1248c1d42281f5d0bc561cae0cd15 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -50,7 +50,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   {
     return rewriteConstructor(in);
   }
-  else if (kind == kind::APPLY_SELECTOR_TOTAL || kind == kind::APPLY_SELECTOR)
+  else if (kind == kind::APPLY_SELECTOR)
   {
     return rewriteSelector(in);
   }
@@ -375,7 +375,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in)
 
 RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
 {
-  Kind k = in.getKind();
+  Assert (in.getKind()==kind::APPLY_SELECTOR);
   if (in[0].getKind() == kind::APPLY_CONSTRUCTOR)
   {
     // Have to be careful not to rewrite well-typed expressions
@@ -423,25 +423,6 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       }
     }
-    else if (k == kind::APPLY_SELECTOR_TOTAL)
-    {
-      // evaluates to the first ground value of type tn.
-      NodeManager* nm = NodeManager::currentNM();
-      Node gt = nm->mkGroundValue(tn);
-      Assert(!gt.isNull());
-      if (tn.isDatatype() && !tn.isInstantiatedDatatype())
-      {
-        gt = NodeManager::currentNM()->mkNode(
-            kind::APPLY_TYPE_ASCRIPTION,
-            NodeManager::currentNM()->mkConst(AscriptionType(tn)),
-            gt);
-      }
-      Trace("datatypes-rewrite")
-          << "DatatypesRewriter::postRewrite: "
-          << "Rewrite trivial selector " << in
-          << " to distinguished ground term " << gt << std::endl;
-      return RewriteResponse(REWRITE_DONE, gt);
-    }
   }
   return RewriteResponse(REWRITE_DONE, in);
 }

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index ee42add6b2500bce314c984ce44239db4dcbeea7..45553a00f8a9b4f1cb71ade22f7d0bee241813be 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -41,7 +41,6 @@ cardinality UPDATER_TYPE \
 parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor"
 
 parameterized APPLY_SELECTOR SELECTOR_TYPE 1 "selector application; parameter is a datatype term (undefined if mis-applied)"
-parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; parameter is a datatype term (defined rigidly if mis-applied)"
 
 parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term"
 
@@ -89,7 +88,6 @@ constant ASCRIPTION_TYPE \
 
 typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule
-typerule APPLY_SELECTOR_TOTAL ::cvc5::theory::datatypes::DatatypeSelectorTypeRule
 typerule APPLY_TESTER ::cvc5::theory::datatypes::DatatypeTesterTypeRule
 typerule APPLY_UPDATER ::cvc5::theory::datatypes::DatatypeUpdateTypeRule
 typerule APPLY_TYPE_ASCRIPTION ::cvc5::theory::datatypes::DatatypeAscriptionTypeRule

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 74228167ae5fa59cd6e6841042281bf42fca3431..1461889b1f68d22e9d2b1c938edb1bbe498dc35e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -445,8 +445,6 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 {
   Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
-  // should not use APPLY_SELECTOR_TOTAL
-  Assert(n.getKind() != APPLY_SELECTOR_TOTAL);
   // must ensure the type is well founded and has no nested recursion if
   // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 7ce5c0df60a5a94e47cae02aac9ff4b47a14cbab..4d907b25947a5a5a6243bc492c923d5bfe433d4b 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -118,8 +118,7 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager,
                                                TNode n,
                                                bool check)
 {
-  Assert(n.getKind() == kind::APPLY_SELECTOR
-         || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
+  Assert(n.getKind() == kind::APPLY_SELECTOR);
   TypeNode selType = n.getOperator().getType(check);
   TypeNode t = selType[0];
   Assert(t.isDatatype());