Z3 Solver Python字符串函数编码：如何省略公式中的concat变量？

原公式里的concat变量只是Concat(fs1, fs2)的临时别名，直接将所有concat的引用替换为Concat(fs1, fs2)即可省略该变量，且逻辑完全等价。

修改后的公式如下：

formula = ForAll([fs1, fs2],
                Implies(
                    And(Length(fs1) == l1, Length(fs2) == l2),
                    Length(Concat(fs1, fs2)) == l1 + l2
                ))

改动说明： #

• 移除了原条件中的concat == Concat(fs1, fs2)判断，因为不再需要这个中间变量来承接拼接结果
• 将结论里的Length(concat)直接替换为Length(Concat(fs1, fs2))，直接对拼接操作的结果做长度约束
• 最终公式逻辑和原公式一致：对任意两个字符串fs1、fs2，若它们的长度分别为l1和l2，则二者拼接后的字符串长度必为l1 + l2

内容的提问来源于stack exchange，提问作者Poojal Katiyar