如何将两个正则表达式与 Python Z3 绑定连接起来？ [复制]

【问题标题】：How do I concatenate two regexes with the Python Z3 bindings? [duplicate]如何将两个正则表达式与 Python Z3 绑定连接起来？ [复制]
【发布时间】：2021-11-03 20:08:46
【问题描述】：

我从this question 看到，SMTLIB 绑定中有一个re.++ 函数似乎可以满足我的要求。它在 Python 绑定中的等价物是什么？例如：

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

相当于正则表达式ab*a。我如何获得r_concatenated？

【问题讨论】：

标签： python regex z3

【解决方案1】：

我在发布此问题大约一分钟后找到了答案。如果您使用 Concat 方法，它可以工作，尽管文档只提到了位向量。所以代码是：

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

【讨论】：

重复stackoverflow.com/questions/64408788/…