From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 18 Feb 2022 21:10:25 +0000 (-0800)
Subject: Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)
X-Git-Tag: cvc5-1.0.0~414
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=12fe80eff81db3d7b13cbd785061429b1c49c522;p=cvc5.git

Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)

This changes the `STRINGS_ARRAY_UPDATE_BOUND` inference to explicitly
include the disequality between the term before and after the update if
the update has an effect. This is an optimization that prevents us from
splitting on that (dis-)equality later on.
---

diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp
index e31a5e5a4..4be5ec04d 100644
--- a/src/theory/strings/array_core_solver.cpp
+++ b/src/theory/strings/array_core_solver.cpp
@@ -145,14 +145,15 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& updateTerms)
                          false,
                          true);
 
-      // update(s, n, t)
+      // x = update(s, n, t)
       // ------------------------
-      // 0 <= n < len(t) and nth(s, n) != nth(update(s, n, t)) ||
-      // s = update(s, n, t)
+      // 0 <= n < len(t) and nth(s, n) != nth(update(s, n, t))  and x != s ||
+      // x = s
       lem = nm->mkNode(
           OR,
           nm->mkNode(AND,
                      left.eqNode(nm->mkNode(SEQ_NTH, n[0], n[1])).notNode(),
+                     n.eqNode(n[0]).negate(),
                      cond),
           n.eqNode(n[0]));
       d_im.sendInference(