Remove unused `SEQ_NTH_TOTAL` kind (#8048)

Originally, the idea was to expand the definition of `SEQ_NTH` to use
`SEQ_NTH_TOTAL` (i.e., a total version of that operator), but we have
since then decided to just use `SEQ_NTH`.

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 750ec1d7d7fa96c8b661d301d51b9dac71baa0f4..47bb7d7d68cab164cc925da3a4a6ad63c4d9c3d9 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -25,7 +25,6 @@
 
 #include "api/cpp/cvc5.h"
 #include "cvc5_export.h"
-#include "expr/kind.h"
 #include "expr/symbol_manager.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index bec5fd363b67aa30a80ed2af5f8823c412366fa6..5f14efce74e41d5dee2916a5439e8240c10b23e3 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -97,7 +97,6 @@ parameterized SEQ_UNIT SEQ_UNIT_OP 1  \
 "a sequence of length one. First parameter is a SeqUnitOp. Second is a term"
 
 operator SEQ_NTH 2 "The nth element of a sequence"
-operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)"
 
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
@@ -196,6 +195,5 @@ typerule CONST_SEQUENCE ::cvc5::internal::theory::strings::ConstSequenceTypeRule
 typerule SEQ_UNIT_OP   "SimpleTypeRule<RBuiltinOperator>"
 typerule SEQ_UNIT ::cvc5::internal::theory::strings::SeqUnitTypeRule
 typerule SEQ_NTH ::cvc5::internal::theory::strings::SeqNthTypeRule
-typerule SEQ_NTH_TOTAL ::cvc5::internal::theory::strings::SeqNthTypeRule
 
 endtheory

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index bc651cb70a186549cbbc09f874b94ad085c96052..e4d702905d3ab3b219e54fecbabee9d90b454b52 100644 (file)
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -228,7 +228,6 @@ const char* toString(Rewrite r)
     case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
     case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
     case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL";
-    case Rewrite::SEQ_NTH_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB";
     case Rewrite::SEQ_NTH_EVAL_SYM: return "SEQ_NTH_EVAL_SYM";
     default: return "?";
   }

diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index ff58989c9fe01c27b4813c1f8ee4cc3f6061b388..98a3bc86660b1faa057f7328dfe23e8b327b4bd4 100644 (file)
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -229,7 +229,6 @@ enum class Rewrite : uint32_t
   CHARAT_ELIM,
   SEQ_UNIT_EVAL,
   SEQ_NTH_EVAL,
-  SEQ_NTH_TOTAL_OOB,
   SEQ_NTH_EVAL_SYM
 };
 

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 83288b55f24b3382427459212e6a3694eea9e786..3b3290b2649d2968250b915e8fe41c6fd36dc144 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1717,7 +1717,7 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
   {
     retNode = rewriteSeqUnit(node);
   }
-  else if (nk == SEQ_NTH || nk == SEQ_NTH_TOTAL)
+  else if (nk == SEQ_NTH)
   {
     retNode = rewriteSeqNth(node);
   }
@@ -1743,33 +1743,9 @@ RewriteResponse SequencesRewriter::preRewrite(TNode node)
   return RewriteResponse(REWRITE_DONE, node);
 }
 
-TrustNode SequencesRewriter::expandDefinition(Node node)
-{
-  Trace("strings-exp-def") << "SequencesRewriter::expandDefinition : " << node
-                           << std::endl;
-
-  if (node.getKind() == kind::SEQ_NTH)
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    Node s = node[0];
-    Node n = node[1];
-    // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
-    Node cond = nm->mkNode(AND,
-                           nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n),
-                           nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
-    Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
-    Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
-    Node u = nm->mkNode(APPLY_UF, uf, s, n);
-    Node ret = nm->mkNode(ITE, cond, ss, u);
-    Trace("strings-exp-def") << "...return " << ret << std::endl;
-    return TrustNode::mkTrustRewrite(node, ret, nullptr);
-  }
-  return TrustNode::null();
-}
-
 Node SequencesRewriter::rewriteSeqNth(Node node)
 {
-  Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL);
+  Assert(node.getKind() == SEQ_NTH);
   Node s = node[0];
   Node i = node[1];
   if (s.isConst() && i.isConst())
@@ -1786,13 +1762,6 @@ Node SequencesRewriter::rewriteSeqNth(Node node)
         return returnRewrite(node, ret, Rewrite::SEQ_NTH_EVAL);
       }
     }
-    if (node.getKind() == SEQ_NTH_TOTAL)
-    {
-      // return arbitrary term
-      NodeManager* nm = NodeManager::currentNM();
-      Node ret = nm->mkGroundValue(s.getType().getSequenceElementType());
-      return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB);
-    }
   }
 
   std::vector<Node> prefix, suffix;

diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 451a27e4f26a90327a3bc6171ee4f0d922ab28f1..e7b1831f1f924a7080ac0b998ced2d4de048b917 100644 (file)
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -132,8 +132,6 @@ class SequencesRewriter : public TheoryRewriter
  public:
   RewriteResponse postRewrite(TNode node) override;
   RewriteResponse preRewrite(TNode node) override;
-  /** Expand definition */
-  TrustNode expandDefinition(Node n) override;
 
   /** rewrite equality
    *

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6549944b6d025338485b5cfd92e477cc29398e20..52ff945100f16473579e5159e272bfedf5e3dee3 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -62,7 +62,6 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
   d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH);
-  d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL);
   // do not interpret APPLY_UF if we are not assigning function values
   if (!d_enableFuncModels)
   {

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 50210380a9497c529812899638647324e8278aad..7720cdcc95dc4626570db7137c3587c551120aa1 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -131,7 +131,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR
-      || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH)
+      || n.getKind() == kind::SEQ_NTH)
   {
     // selectors are always assignable (where we guarantee that they are not
     // evaluatable here)

diff --git a/test/regress/cli/regress0/seq/seq-expand-defs.smt2 b/test/regress/cli/regress0/seq/seq-expand-defs.smt2
index 065dd6bd57e0c98911b2ce4064662915c7fbda06..cafb516baece83ab9aaf8f2a62d7a79cf85bf6b4 100644 (file)
--- a/test/regress/cli/regress0/seq/seq-expand-defs.smt2
+++ b/test/regress/cli/regress0/seq/seq-expand-defs.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --strings-exp -q
 ; EXPECT: sat
-; EXPECT: (((seq.nth y 7) 404))
+; EXPECT: (((seq.nth y 7) (seq.nth (as seq.empty (Seq Int)) 7)))
 ; EXPECT: (((str.from_code x) "?"))
 (set-logic ALL)
 (set-option :produce-models true)