Remove spurious assertion from core solver (cvc5#10019)

Fixes cvc5#9988. The assertion does not hold in general if we break words of size > 1 into single characters. Setting the index to size-1 was a way of terminating previously, now this is made explicit via the return value of the method.
mpreiner · Sep 12, 2023 · 1a2b2d7 · 1a2b2d7
1 parent af4b8a9
commit 1a2b2d7
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 8 deletions.
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
@@ -1139,7 +1139,10 @@ void CoreSolver::processNEqc(Node eqc,
       unsigned rindex = 0;
       nfi.reverse();
       nfj.reverse();
-      processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
+      if (processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype))
+      {
+        break;
+      }
       nfi.reverse();
       nfj.reverse();
       if (d_im.hasProcessed())
@@ -1150,7 +1153,10 @@ void CoreSolver::processNEqc(Node eqc,
       // rindex = 0;
 
       unsigned index = 0;
-      processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
+      if (processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype))
+      {
+        break;
+      }
       if (d_im.hasProcessed())
       {
         break;
@@ -1198,7 +1204,7 @@ void CoreSolver::processNEqc(Node eqc,
   }
 }
 
-void CoreSolver::processSimpleNEq(NormalForm& nfi,
+bool CoreSolver::processSimpleNEq(NormalForm& nfi,
                                   NormalForm& nfj,
                                   unsigned& index,
                                   bool isRev,
@@ -1219,7 +1225,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     if (lhsDone && rhsDone)
     {
       // We are done with both normal forms
-      break;
+      return true;
     }
     else if (lhsDone || rhsDone)
     {
@@ -1280,7 +1286,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       {
         // if both are constant, it's just a constant conflict
         d_im.sendInference(ant, d_false, InferenceId::STRINGS_N_CONST, isRev, true);
-        return;
+        return false;
       }
       // `x` and `y` have the same length. We infer that the two components
       // have to be the same.
@@ -1339,8 +1345,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       }
       else
       {
-        Assert(nfiv.size() == nfjv.size());
-        index = nfiv.size() - rproc;
+        // endpoints are equal, we have verified normal forms are equal
+        return true;
       }
       break;
     }
@@ -1688,6 +1694,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     pinfer.push_back(info);
     break;
   }
+  return false;
 }
 
 bool CoreSolver::detectLoop(NormalForm& nfi,

diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
@@ -409,8 +409,10 @@ class CoreSolver : protected EnvObj
    * pinfer: the set of possible inferences we add to.
    *
    * stype is the string-like type of the equivalence class we are processing.
+   *
+   * @return true if the normal forms are equal
    */
-  void processSimpleNEq(NormalForm& nfi,
+  bool processSimpleNEq(NormalForm& nfi,
                         NormalForm& nfj,
                         unsigned& index,
                         bool isRev,

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -2915,6 +2915,7 @@ set(regress_1_tests
   regress1/strings/issue9269-rei-nconst.smt2
   regress1/strings/issue9287-trivial-deq-disl.smt2
   regress1/strings/issue9543-re-inc.smt2
+  regress1/strings/issue9988-3.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/cli/regress1/strings/issue9988-3.smt2 b/test/regress/cli/regress1/strings/issue9988-3.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --no-strings-lazy-pp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re (str.++ b "z" a) (re.++ (re.* (re.++ (str.to_re "z") (re.* (str.to_re "b")))) (str.to_re "b"))))
+(assert (not (str.in_re (str.++ b "a") (re.* (re.++ (re.* (str.to_re "b")) (re.diff (str.to_re (str.from_int (str.len b))) (str.to_re (str.replace a b ""))))))))
+(check-sat)