Fix component contains for splicing due to substring. (#4705)

Fixes #4701. That benchmark now times out.

diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 9284145231293ee5f3880c7cb65b4deac4fdfaa1..b2c2c3cd3e3e9fb4d8e8d6117acb42dae9878565 100644 (file)
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -225,6 +225,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
 {
   Assert(nb.empty());
   Assert(ne.empty());
+  Trace("strings-entail") << "Component contains: " << std::endl;
+  Trace("strings-entail") << "n1 = " << n1 << std::endl;
+  Trace("strings-entail") << "n2 = " << n2 << std::endl;
   // if n2 is a singleton, we can do optimized version here
   if (n2.size() == 1)
   {
@@ -301,6 +304,10 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
                                       -1,
                                       computeRemainder && remainderDir != -1))
             {
+              Trace("strings-entail-debug")
+                  << "Last remainder begin is " << n1rb_last << std::endl;
+              Trace("strings-entail-debug")
+                  << "Last remainder end is " << n1re_last << std::endl;
               Assert(n1rb_last.isNull());
               if (computeRemainder)
               {
@@ -325,6 +332,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
                   }
                 }
               }
+              Trace("strings-entail-debug") << "ne = " << ne << std::endl;
+              Trace("strings-entail-debug") << "nb = " << nb << std::endl;
+              Trace("strings-entail-debug") << "...return " << i << std::endl;
               return i;
             }
             else
@@ -444,12 +454,12 @@ bool StringsEntail::componentContainsBase(
               {
                 return false;
               }
-              if (dir != 1)
+              if (dir != -1)
               {
                 n1rb = nm->mkNode(
                     STRING_SUBSTR, n2[0], nm->mkConst(Rational(0)), start_pos);
               }
-              if (dir != -1)
+              if (dir != 1)
               {
                 n1re = nm->mkNode(STRING_SUBSTR, n2[0], end_pos, len_n2s);
               }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 95c272a3e8f76baa706204a116b9568d978c9137..a0fee218562084c52eb0dd82a42f872f0161e21e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1808,6 +1808,7 @@ set(regress_1_tests
   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/issue4379.smt2
   regress1/strings/issue4608-re-derive.smt2
+  regress1/strings/issue4701_substr_splice.smt2
   regress1/strings/issue4735.smt2
   regress1/strings/issue4735_2.smt2
   regress1/strings/issue4759-comp-delta.smt2

diff --git a/test/regress/regress1/strings/issue4701_substr_splice.smt2 b/test/regress/regress1/strings/issue4701_substr_splice.smt2
new file mode 100644 (file)
index 0000000..28e8958
--- /dev/null
+++ b/test/regress/regress1/strings/issue4701_substr_splice.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(declare-fun e () String)
+(assert (= e (str.++ b (str.substr a 0 1))))
+(assert (= a (str.substr c 0 (str.len e))))
+(assert (= "a" b))
+(assert (= (str.++ b a) (str.replace c e a)))
+(check-sat)