new rewritecav2019strings_exp

2 files changed, 49 insertions, 1 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 94e43be36..98a2183ad 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1537,6 +1537,16 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
       }
     }
+    else if (nk0 == STRING_SUBSTR)
+    {
+      Node len = nm->mkNode(STRING_LENGTH, node[0][0]);
+      Node end = nm->mkNode(PLUS, node[0][1], node[0][2]);
+      if (checkEntailArith(node[0][1]) && checkEntailArith(node[0][2]) && checkEntailArith(len, end))
+      {
+        //std::cout << len << " > " << end << std::endl;
+        retNode = node[0][2];
+      }
+    }
   }
   else if (nk == kind::STRING_CHARAT)
   {
@@ -4783,7 +4793,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption,
   }
 
   Node solution = ArithMSum::solveEqualityFor(assumption, v);
-  if (solution.isNull())
+  if (solution.isNull())// || hasExtOp(solution))
   {
     // Could not solve for v
     return false;
@@ -5349,3 +5359,39 @@ Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c)
   }
   return ret;
 }
+
+bool TheoryStringsRewriter::hasExtOp(TNode n)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+
+      Kind k = cur.getKind();
+      if (k == kind::STRING_STRCTN || k == kind::STRING_STRREPL
+          || k == kind::STRING_STRIDOF || k == kind::STRING_ITOS
+          || k == kind::STRING_STOI || k == kind::STRING_IN_REGEXP
+          || k == kind::STRING_SUBSTR || k == kind::STRING_CHARAT
+          || k == kind::STRING_PREFIX || k == kind::STRING_SUFFIX)
+      {
+        return true;
+      }
+
+      for (unsigned i = 0; i < cur.getNumChildren(); i++)
+      {
+        visit.push_back(cur[i]);
+      }
+    }
+  } while (!visit.empty());
+
+  return false;
+}
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 61031ea87..a0edb3e0e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -745,6 +745,8 @@ class TheoryStringsRewriter {
    * and the list of nodes that are compared to the empty string
    */
   static std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x);
+
+  static bool hasExtOp(TNode n);
 };/* class TheoryStringsRewriter */
 
 }/* CVC4::theory::strings namespace */