5 files changed, 79 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index aa1e2627a..cd8550905 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -31,6 +31,9 @@ operator STRING_CODE 1 "string to code, returns the code of the first character
 operator STRING_TOLOWER 1 "string to lowercase conversion"
 operator STRING_TOUPPER 1 "string to uppercase conversion"
 operator STRING_REV 1 "string reverse"
+operator STRING_SK_PREFIX 2 "string prefix"
+operator STRING_SK_SUFFIX 2 "string suffix"
+operator STRING_SK_FIRST_CTN_PRE 2 "string suffix"
 
 sort STRING_TYPE \
     Cardinality::INTEGERS \
@@ -106,6 +109,9 @@ typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
 typerule STRING_REV "SimpleTypeRule<RString, AString>"
+typerule STRING_SK_PREFIX "SimpleTypeRule<RString, AString, AInteger>"
+typerule STRING_SK_SUFFIX "SimpleTypeRule<RString, AString, AInteger>"
+typerule STRING_SK_FIRST_CTN_PRE "SimpleTypeRule<RString, AString, AString>"
 
 typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
 
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index b4e1c74ea..327ae19e1 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -52,6 +52,17 @@ Node SkolemCache::mkTypedSkolemCached(
     std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
   }
 
+  NodeManager* nm = NodeManager::currentNM();
+  switch (id)
+  {
+    case SK_PREFIX: return nm->mkNode(STRING_SK_PREFIX, a, b); break;
+    case SK_SUFFIX_REM: return nm->mkNode(STRING_SK_SUFFIX, a, b); break;
+    case SK_FIRST_CTN_PRE:
+      return nm->mkNode(STRING_SK_FIRST_CTN_PRE, a, b);
+      break;
+    default: break;
+  }
+
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1bc104096..2f658550f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -130,6 +130,9 @@ TheoryStrings::TheoryStrings(context::Context* c,
   getExtTheory()->addFunctionKind(kind::STRING_TOLOWER);
   getExtTheory()->addFunctionKind(kind::STRING_TOUPPER);
   getExtTheory()->addFunctionKind(kind::STRING_REV);
+  getExtTheory()->addFunctionKind(kind::STRING_SK_PREFIX);
+  getExtTheory()->addFunctionKind(kind::STRING_SK_SUFFIX);
+  getExtTheory()->addFunctionKind(kind::STRING_SK_FIRST_CTN_PRE);
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
@@ -149,6 +152,9 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_equalityEngine.addFunctionKind(kind::STRING_TOLOWER);
   d_equalityEngine.addFunctionKind(kind::STRING_TOUPPER);
   d_equalityEngine.addFunctionKind(kind::STRING_REV);
+  d_equalityEngine.addFunctionKind(kind::STRING_SK_PREFIX);
+  d_equalityEngine.addFunctionKind(kind::STRING_SK_SUFFIX);
+  d_equalityEngine.addFunctionKind(kind::STRING_SK_FIRST_CTN_PRE);
 
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -164,6 +170,15 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+void TheoryStrings::finishInit()
+{
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  tm->setSemiEvaluatedKind(STRING_SK_FIRST_CTN_PRE);
+  tm->setSemiEvaluatedKind(STRING_SK_SUFFIX);
+  tm->setSemiEvaluatedKind(STRING_SK_PREFIX);
+}
+
 bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   Assert(d_equalityEngine.hasTerm(x));
   Assert(d_equalityEngine.hasTerm(y));
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8e2af8434..4ce83704e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -102,6 +102,8 @@ class TheoryStrings : public Theory {
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
 
+  void finishInit() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   std::string identify() const override { return std::string("TheoryStrings"); }
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f17944027..0f6ec03d2 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1563,6 +1563,51 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   {
     retNode = rewriteConcat(node);
   }
+  else if (nk == STRING_SK_PREFIX)
+  {
+    if (node[0].isConst() && node[1].isConst())
+    {
+      String s = node[0].getConst<String>();
+      size_t n = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+      if (s.size() >= n)
+      {
+        retNode = nm->mkConst(s.prefix(n));
+      }
+    }
+    else if (node[1].getKind() == STRING_LENGTH && node[0] == node[1][0])
+    {
+      retNode = node[0];
+    }
+  }
+  else if (nk == STRING_SK_SUFFIX)
+  {
+    if (node[0].isConst() && node[1].isConst())
+    {
+      String s = node[0].getConst<String>();
+      size_t n = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+      if (s.size() >= n)
+      {
+        retNode = nm->mkConst(s.suffix(s.size() - n));
+      }
+    }
+    else if (node[1].getKind() == STRING_LENGTH && node[0] == node[1][0])
+    {
+      retNode = nm->mkConst(String());
+    }
+  }
+  else if (nk == STRING_SK_FIRST_CTN_PRE)
+  {
+    if (node[0].isConst() && node[1].isConst())
+    {
+      String s1 = node[0].getConst<String>();
+      String s2 = node[1].getConst<String>();
+      size_t pos = s1.find(s2);
+      if (pos != std::string::npos)
+      {
+        retNode = nm->mkConst(s1.prefix(pos));
+      }
+    }
+  }
   else if (nk == kind::EQUAL)
   {
     retNode = rewriteEquality(node);