[Strings] Fix extended equality rewriter (#5092)

Fixes #5090. Our extended equality rewriter was performing the following
unsound rewrite:

(= (str.++ Str13 Str5 Str16 Str13) (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")) ---> (and (= (str.++ Str13 Str5) Str5) (= (str.++ Str16 Str13) (str.++ Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")))
The rule being applied was SPLIT_EQ_STRIP_R. The rewrite was applied
due to the following circumstances:

The rewriter found that (str.++ Str13 Str5) is strictly shorter than (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")
The rewriter stripped the symbolic length of the former from the
latter
stripSymbolicLength() was only able to strip the first component, so
there was a remaining length of (str.len Str13)
The rule SPLIT_EQ_STRIP_R, however, was implicitly assuming that the
symbolic length can either be stripped completly or not at all and was
not considering the case where only a part of the length can be
stripped.

The commit adds a flag to stripSymbolicLength() that makes the
function only return true if the whole length can be stripped from the
input. The commit also refactors the code in stripSymbolicLength()
slightly.

Note: It is not necessary to try to do something smart in the case where
only a partial prefix can be stripped because the rewriter tries to
apply the rule to all the different prefix combinations anyway.

1 files changed, 32 insertions, 0 deletions

diff --git a/test/regress/regress0/strings/issue5090.smt2 b/test/regress/regress0/strings/issue5090.smt2
new file mode 100644
index 000000000..44a57d4d2
--- /dev/null
+++ b/test/regress/regress0/strings/issue5090.smt2
@@ -0,0 +1,32 @@
+; COMMAND-LINE: --strings-exp --incremental
+(set-logic QF_S)
+(declare-const Str0 String)
+(declare-const Str1 String)
+(declare-const Str2 String)
+(declare-const Str3 String)
+(declare-const Str4 String)
+(declare-const Str5 String)
+(declare-const Str6 String)
+(declare-const Str7 String)
+(declare-const Str8 String)
+(declare-const Str9 String)
+(declare-const Str10 String)
+(declare-const Str11 String)
+(declare-const Str12 String)
+(declare-const Str13 String)
+(declare-const Str14 String)
+(declare-const Str15 String)
+(declare-const Str16 String)
+(declare-const Str17 String)
+(declare-const Str18 String)
+(declare-const Str19 String)
+(assert (str.in_re Str19(re.opt (str.to_re Str10))))
+(assert (str.in_re Str9(re.opt (str.to_re Str18))))
+(assert (str.in_re (str.replace Str12 "jkngjj" Str14)(re.opt (str.to_re (str.++ Str13 "spifluyxzmbznnejkmfajdisgnyfeogvtwxuclzmrlmjmmwhly" Str5 Str19 "rsjusudbyjoyfpwbpasemhhxoayzouhoaekszsvhbsmnysbcih")))))
+(assert (str.in_re Str13(re.opt (str.to_re Str3))))
+(push 1)
+(assert (str.in_re (str.++ Str12 (str.++ Str5 Str16 Str13) (str.++ Str5 "tqckdn" "hvhftx" (str.replace Str12 "jkngjj" Str14)) "trcuij" "ovnscketrkugxyqewkvuvondgahkfzwczexnyiziwhyqlomqie")(re.opt (str.to_re Str8))))
+(push 1)
+(assert (str.in_re (str.++ Str13 (str.++ Str5 Str16 Str13))(re.++ (str.to_re (str.++ Str5 Str16 Str13)) (str.to_re "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs" ))))
+(set-info :status sat)
+(check-sat)