如何在z3py中连接正则表达式？ [英] How to concatenate regular expressions in z3py?

问题描述

我想构造一个正则表达式，比如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连接多个正则表达式？

推荐答案

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

这篇关于如何在z3py中连接正则表达式？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！