Incorporate sequences into the word interface (#4543)

Also renames a function mkWord -> mkWordFlatten.

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 55d58b860f731a090e9225595f6c5ac20803dfc6..4f74d7c156c9fa4f96d129399c42176ab9c98d6f 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -264,7 +264,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
           // Add a constant string to the side with more `cn`s to restore
           // the difference in number of `cn`s
           std::vector<Node> vec(diff, cn);
-          trimmed[j].push_back(Word::mkWord(vec));
+          trimmed[j].push_back(Word::mkWordFlatten(vec));
         }
       }
 
@@ -602,7 +602,7 @@ Node SequencesRewriter::rewriteConcat(Node node)
           std::vector<Node> wvec;
           wvec.push_back(preNode);
           wvec.push_back(tmpNode[0]);
-          preNode = Word::mkWord(wvec);
+          preNode = Word::mkWordFlatten(wvec);
           node_vec.push_back(preNode);
         }
         else
@@ -644,7 +644,7 @@ Node SequencesRewriter::rewriteConcat(Node node)
         std::vector<Node> vec;
         vec.push_back(preNode);
         vec.push_back(tmpNode);
-        preNode = Word::mkWord(vec);
+        preNode = Word::mkWordFlatten(vec);
       }
     }
   }

diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index e9ab2652e7006f6e9bf780fb84bc83aef7199f26..3f6a9de32295b03cc87678d543c4463e377b1ddc 100644 (file)
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/word.h"
 
+#include "expr/sequence.h"
 #include "util/string.h"
 
 using namespace CVC4::kind;
@@ -28,23 +29,28 @@ Node Word::mkEmptyWord(TypeNode tn)
   {
     return mkEmptyWord(CONST_STRING);
   }
+  else if (tn.isSequence())
+  {
+    std::vector<Expr> seq;
+    return NodeManager::currentNM()->mkConst(
+        ExprSequence(tn.getSequenceElementType().toType(), seq));
+  }
   Unimplemented();
   return Node::null();
 }
 
 Node Word::mkEmptyWord(Kind k)
 {
-  NodeManager* nm = NodeManager::currentNM();
   if (k == CONST_STRING)
   {
     std::vector<unsigned> vec;
-    return nm->mkConst(String(vec));
+    return NodeManager::currentNM()->mkConst(String(vec));
   }
   Unimplemented();
   return Node::null();
 }
 
-Node Word::mkWord(const std::vector<Node>& xs)
+Node Word::mkWordFlatten(const std::vector<Node>& xs)
 {
   Assert(!xs.empty());
   NodeManager* nm = NodeManager::currentNM();
@@ -61,6 +67,22 @@ Node Word::mkWord(const std::vector<Node>& xs)
     }
     return nm->mkConst(String(vec));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    std::vector<Expr> seq;
+    TypeNode tn = xs[0].getType();
+    for (TNode x : xs)
+    {
+      Assert(x.getType() == tn);
+      const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+      const std::vector<Node>& vecc = sx.getVec();
+      for (const Node& c : vecc)
+      {
+        seq.push_back(c.toExpr());
+      }
+    }
+    return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq));
+  }
   Unimplemented();
   return Node::null();
 }
@@ -72,6 +94,10 @@ size_t Word::getLength(TNode x)
   {
     return x.getConst<String>().size();
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    return x.getConst<ExprSequence>().getSequence().size();
+  }
   Unimplemented();
   return 0;
 }
@@ -111,6 +137,13 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n)
     String sy = y.getConst<String>();
     return sx.strncmp(sy, n);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.strncmp(sy, n);
+  }
   Unimplemented();
   return false;
 }
@@ -125,6 +158,13 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
     String sy = y.getConst<String>();
     return sx.rstrncmp(sy, n);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.rstrncmp(sy, n);
+  }
   Unimplemented();
   return false;
 }
@@ -139,6 +179,13 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start)
     String sy = y.getConst<String>();
     return sx.find(sy, start);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.find(sy, start);
+  }
   Unimplemented();
   return 0;
 }
@@ -153,6 +200,13 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
     String sy = y.getConst<String>();
     return sx.rfind(sy, start);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.rfind(sy, start);
+  }
   Unimplemented();
   return 0;
 }
@@ -167,6 +221,13 @@ bool Word::hasPrefix(TNode x, TNode y)
     String sy = y.getConst<String>();
     return sx.hasPrefix(sy);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.hasPrefix(sy);
+  }
   Unimplemented();
   return false;
 }
@@ -181,6 +242,13 @@ bool Word::hasSuffix(TNode x, TNode y)
     String sy = y.getConst<String>();
     return sx.hasSuffix(sy);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.hasSuffix(sy);
+  }
   Unimplemented();
   return false;
 }
@@ -198,6 +266,16 @@ Node Word::replace(TNode x, TNode y, TNode t)
     String st = t.getConst<String>();
     return nm->mkConst(String(sx.replace(sy, st)));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    Assert(t.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    const Sequence& st = t.getConst<ExprSequence>().getSequence();
+    Sequence res = sx.replace(sy, st);
+    return nm->mkConst(res.toExprSequence());
+  }
   Unimplemented();
   return Node::null();
 }
@@ -210,6 +288,12 @@ Node Word::substr(TNode x, std::size_t i)
     String sx = x.getConst<String>();
     return nm->mkConst(String(sx.substr(i)));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    Sequence res = sx.substr(i);
+    return nm->mkConst(res.toExprSequence());
+  }
   Unimplemented();
   return Node::null();
 }
@@ -222,6 +306,12 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j)
     String sx = x.getConst<String>();
     return nm->mkConst(String(sx.substr(i, j)));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    Sequence res = sx.substr(i, j);
+    return nm->mkConst(res.toExprSequence());
+  }
   Unimplemented();
   return Node::null();
 }
@@ -237,6 +327,12 @@ Node Word::suffix(TNode x, std::size_t i)
     String sx = x.getConst<String>();
     return nm->mkConst(String(sx.suffix(i)));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    Sequence res = sx.suffix(i);
+    return nm->mkConst(res.toExprSequence());
+  }
   Unimplemented();
   return Node::null();
 }
@@ -251,6 +347,13 @@ bool Word::noOverlapWith(TNode x, TNode y)
     String sy = y.getConst<String>();
     return sx.noOverlapWith(sy);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.noOverlapWith(sy);
+  }
   Unimplemented();
   return false;
 }
@@ -265,6 +368,13 @@ std::size_t Word::overlap(TNode x, TNode y)
     String sy = y.getConst<String>();
     return sx.overlap(sy);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.overlap(sy);
+  }
   Unimplemented();
   return 0;
 }
@@ -279,10 +389,32 @@ std::size_t Word::roverlap(TNode x, TNode y)
     String sy = y.getConst<String>();
     return sx.roverlap(sy);
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(y.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+    return sx.roverlap(sy);
+  }
   Unimplemented();
   return 0;
 }
 
+bool Word::isRepeated(TNode x)
+{
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    return x.getConst<String>().isRepeated();
+  }
+  else if (k == CONST_SEQUENCE)
+  {
+    return x.getConst<ExprSequence>().getSequence().isRepeated();
+  }
+  Unimplemented();
+  return false;
+}
+
 Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
 {
   Assert(x.isConst() && y.isConst());

diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h
index b84ea6874434b0006fd64ed78e52336e31f87256..ad1d9bc74a46c240132c1efd87c99e79273d6bac 100644 (file)
--- a/src/theory/strings/word.h
+++ b/src/theory/strings/word.h
@@ -37,7 +37,7 @@ class Word
   static Node mkEmptyWord(Kind k);
 
   /** make word from constants in (non-empty) vector vec */
-  static Node mkWord(const std::vector<Node>& xs);
+  static Node mkWordFlatten(const std::vector<Node>& xs);
 
   /** Return the length of word x */
   static size_t getLength(TNode x);
@@ -139,6 +139,8 @@ class Word
    * Notice that x.overlap(y) = y.roverlap(x)
    */
   static std::size_t roverlap(TNode x, TNode y);
+  /** Return true if word x is a repetition of the same character */
+  static bool isRepeated(TNode x);
   /** Split constant
    *
    * This returns the suffix remainder (resp. prefix remainder when isRev is

diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h
index d84df7836e12d4b91424f1094df8abb84321eaa5..6b594d904f98f4f580e10b3a88945de8fc4b3c36 100644 (file)
--- a/test/unit/theory/theory_strings_word_white.h
+++ b/test/unit/theory/theory_strings_word_white.h
@@ -67,10 +67,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite
 
     std::vector<Node> vec;
     vec.push_back(abc);
-    Node abcMk = Word::mkWord(vec);
+    Node abcMk = Word::mkWordFlatten(vec);
     TS_ASSERT_EQUALS(abc, abcMk);
     vec.push_back(a);
-    Node abcaMk = Word::mkWord(vec);
+    Node abcaMk = Word::mkWordFlatten(vec);
     TS_ASSERT_EQUALS(abca, abcaMk);
 
     TS_ASSERT(Word::getLength(empty) == 0);