From 12fe80eff81db3d7b13cbd785061429b1c49c522 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 18 Feb 2022 13:10:25 -0800 Subject: [PATCH] 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. --- src/theory/strings/array_core_solver.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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& 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( -- 2.30.2