z3 - 如何在 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 连接多个正则表达式？

标签： z3z3py

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"))))