Python Z3绑定中拼接两个正则表达式的方法是什么？

SMTLIB 中的re.++正则拼接函数，在Python Z3绑定中的等价实现为Concat函数，直接传入待拼接的正则表达式对象即可，无需额外用Re()包裹。

你提供的示例修改后正确写法如下：

from z3 import *
r1 = Star(Re('ab'))
r2 = Re('a')
r_concatenated = Concat(r1, r2)

以上代码生成的r_concatenated就等价于正则(ab)*a，和SMTLIB中re.++的语义完全一致。如果需要拼接多个正则表达式，按顺序将所有正则对象作为参数传入Concat即可，比如拼接三个正则可以写为Concat(r1, r2, r3)。

注意：不要把正则拼接和字符串拼接混淆，Concat传入的参数必须是Z3的正则类型对象，不能直接传入普通字符串，普通字符串需要先用Re()转换为正则对象后再拼接。

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