Split sequences rewriter (#4194)

This is in preparation for making the strings rewriter configurable for stats.

This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas.

No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.

1 files changed, 26 insertions, 1 deletions

diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index b42cf3160..085078dea 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -99,7 +99,7 @@ std::vector<Node> Word::getChars(TNode x)
   return ret;
 }
 
-bool Word::isEmpty(TNode x) { return getLength(x) == 0; }
+bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
 
 bool Word::strncmp(TNode x, TNode y, std::size_t n)
 {
@@ -283,6 +283,31 @@ std::size_t Word::roverlap(TNode x, TNode y)
   return 0;
 }
 
+Node Word::splitConstant(Node x, Node y, size_t& index, bool isRev)
+{
+  Assert(x.isConst() && y.isConst());
+  size_t lenA = getLength(x);
+  size_t lenB = getLength(y);
+  index = lenA <= lenB ? 1 : 0;
+  size_t lenShort = index == 1 ? lenA : lenB;
+  bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
+  if (cmp)
+  {
+    Node l = index == 0 ? x : y;
+    if (isRev)
+    {
+      size_t new_len = getLength(l) - lenShort;
+      return substr(l, 0, new_len);
+    }
+    else
+    {
+      return substr(l, lenShort);
+    }
+  }
+  // not the same prefix/suffix
+  return Node::null();
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4