如何在 z3py 中连接正则表达式？

Question

我想构造一个正则表达式，例如a* b* c*，z3中有一个函数re.++可以将3个正则表达式连接在一起，所以我可以构造a* b* c*如下

(assert (str.in.re "aabbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")) (re.* (str.to.re "c")))))
(check-sat)

但是，我在 z3py API 中找不到这样的连接函数 网站：https://z3prover.github.io/api/html/namespacez3py.html

所以我的问题是如何使用 z3py 连接多个正则表达式？

Answer 1

使用Concat:

>>> from z3 import *
>>> print(Concat(Star(Re("a")), Star(Re("b")), Star(Re("c"))))
re.++(Star(Re("a")), re.++(Star(Re("b")), Star(Re("c"))))