Convert more uses of strings to words (#3921)

Towards theory of sequences.

Also adds documentation to strncmp/rstrncmp and adds them to the Word interface.

1 files changed, 28 insertions, 0 deletions

diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index a0ee0d224..dd573b68c 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -78,6 +78,34 @@ size_t Word::getLength(TNode x)
 
 bool Word::isEmpty(TNode x) { return getLength(x) == 0; }
 
+bool Word::strncmp(TNode x, TNode y, std::size_t n)
+{
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    Assert(y.getKind() == CONST_STRING);
+    String sx = x.getConst<String>();
+    String sy = y.getConst<String>();
+    return sx.strncmp(sy, n);
+  }
+  Unimplemented();
+  return false;
+}
+
+bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
+{
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    Assert(y.getKind() == CONST_STRING);
+    String sx = x.getConst<String>();
+    String sy = y.getConst<String>();
+    return sx.rstrncmp(sy, n);
+  }
+  Unimplemented();
+  return false;
+}
+
 std::size_t Word::find(TNode x, TNode y, std::size_t start)
 {
   Kind k = x.getKind();