Fix off by one error in strings flat form explanation (#3273)

Fixes #3272.

This was caused by not explaining the last equal component in a flat form inference.  For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error.

Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`.  #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0f9a78516b3b394be6c979fc0060817d00166166..fafff1412f723de9993a5ec56d292281693a04c2 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2380,6 +2380,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
     inelig.push_back(eqc[start]);
   }
   Node a = eqc[start];
+  Trace("strings-ff-debug")
+      << "Check flat form for a = " << a << ", whose flat form is "
+      << d_flat_form[a] << ")" << std::endl;
   Node b;
   do
   {
@@ -2398,6 +2401,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
           unsigned bsize = d_flat_form[b].size();
           if (count < bsize)
           {
+            Trace("strings-ff-debug")
+                << "Found endpoint (in a) with non-empty b = " << b
+                << ", whose flat form is " << d_flat_form[b] << std::endl;
             // endpoint
             std::vector<Node> conc_c;
             for (unsigned j = count; j < bsize; j++)
@@ -2412,7 +2418,6 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
             // swap, will enforce is empty past current
             a = eqc[i];
             b = eqc[start];
-            count--;
             break;
           }
           inelig.push_back(eqc[i]);
@@ -2434,6 +2439,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
           if (count == d_flat_form[b].size())
           {
             inelig.push_back(b);
+            Trace("strings-ff-debug")
+                << "Found endpoint in b = " << b << ", whose flat form is "
+                << d_flat_form[b] << std::endl;
             // endpoint
             std::vector<Node> conc_c;
             for (unsigned j = count; j < asize; j++)
@@ -2445,7 +2453,6 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
             conc = utils::mkAnd(conc_c);
             inf_type = 2;
             Assert(count > 0);
-            count--;
             break;
           }
           else
@@ -2558,10 +2565,11 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc,
           }
         }
       }
-      // notice that F_EndpointEmp is not typically applied, since
+      // Notice that F_EndpointEmp is not typically applied, since
       // strict prefix equality ( a.b = a ) where a,b non-empty
-      //  is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
-      //  when len(b)!=0.
+      // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a)
+      // when len(b)!=0. Although if we do not infer this conflict eagerly,
+      // it may be applied (see #3272).
       d_im.sendInference(
           exp,
           conc,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bcae83b0a29b16652a36569d4d597cf79fb1c6d0..a1be9ad6242c59cfb470904c0a17d1d014e50838 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1571,6 +1571,7 @@ set(regress_1_tests
   regress1/strings/issue2982.smt2
   regress1/strings/issue3090.smt2
   regress1/strings/issue3217.smt2
+  regress1/strings/issue3272.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2
new file mode 100644 (file)
index 0000000..47759ef
--- /dev/null
+++ b/test/regress/regress1/strings/issue3272.smt2
@@ -0,0 +1,23 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun a () String) 
+(declare-fun b () String) 
+(declare-fun c () String) 
+(assert 
+    (and              
+        (and                                      
+            (and                          
+                (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\t") 1 0) 0))   
+                   
+                (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "\n") 1 0) 0)
+            )     
+                            
+            (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) " ") 1 0) 0)                   
+            (not (= (ite (= (str.at (str.substr (str.replace a b "") 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "\v") 1 0) 0))
+        )       
+        (= (ite (= (str.at (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0) " ") 1 0) 0)
+    )
+)
+; may trigger F_EndpointEmp inference
+(check-sat)