aggressive prefix deductionprefixes

4 files changed, 47 insertions, 1 deletions

diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index 31d7f8b01..62bd8560b 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -31,7 +31,8 @@ EqcInfo::EqcInfo(context::Context* c)
       d_cardinalityLemK(c),
       d_normalizedLength(c),
       d_prefixC(c),
-      d_suffixC(c)
+      d_suffixC(c),
+      d_prefixes(c)
 {
 }
 
diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h
index 108264969..a8d2b3d7f 100644
--- a/src/theory/strings/eqc_info.h
+++ b/src/theory/strings/eqc_info.h
@@ -21,6 +21,7 @@
 
 #include "context/cdo.h"
 #include "context/context.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -72,6 +73,8 @@ class EqcInfo
   context::CDO<Node> d_prefixC;
   /** same as above, for suffix. */
   context::CDO<Node> d_suffixC;
+
+  context::CDList<Node> d_prefixes;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 06a86935f..41c07f5cf 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -127,6 +127,14 @@ void SolverState::eqNotifyNewClass(TNode t)
   {
     addEndpointsToEqcInfo(t, t, t);
   }
+  else if (k == STRING_SUBSTR)
+  {
+    if (t[1].isConst() && t[1].getConst<Rational>().isZero() && t[2].isConst())
+    {
+      EqcInfo* ei = getOrMakeEqcInfo(t);
+      ei->d_prefixes.push_back(t);
+    }
+  }
 }
 
 void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
@@ -162,6 +170,30 @@ void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
     {
       e1->d_normalizedLength.set(e2->d_normalizedLength);
     }
+
+    if (t1.isConst())
+    {
+      for (const Node& prefix : e2->d_prefixes)
+      {
+        EqcInfo* e3 = getOrMakeEqcInfo(prefix[0]);
+        setPendingConflictWhen(e3->addEndpointConst(t1.eqNode(t2), Node::null(), false));
+      }
+    }
+    else if (t2.isConst())
+    {
+      for (const Node& prefix : e1->d_prefixes)
+      {
+        EqcInfo* e3 = getOrMakeEqcInfo(prefix[0]);
+        setPendingConflictWhen(e3->addEndpointConst(t1.eqNode(t2), Node::null(), false));
+      }
+    }
+    else
+    {
+      for (const Node& prefix : e2->d_prefixes)
+      {
+        e1->d_prefixes.push_back(prefix);
+      }
+    }
   }
 }
 
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 3cf14fead..8400342d7 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -184,6 +184,16 @@ Node getConstantComponent(Node t)
 Node getConstantEndpoint(Node e, bool isSuf)
 {
   Kind ek = e.getKind();
+  if (ek == EQUAL) {
+    for (size_t i = 0; i < 2; i++) {
+      if (e[i].isConst()) {
+        Node c = e[i];
+        Node nc = e[1 - i];
+        size_t len = std::min(Word::getLength(c), (size_t) nc[2].getConst<Rational>().getNumerator().toUnsignedInt());
+        return Word::substr(c, 0, len);
+      }
+    }
+  }
   if (ek == STRING_IN_REGEXP)
   {
     e = e[1];