regex - Z3 RegEx for Int*

Question

我正在尝试编写一个断言，即某个整数序列至少包含 2 次出现的某个整数(比如 8)。这是我写的:

(declare-const s (Seq Int))
(assert (seq.in.re s
    (re.++
        re.all
        (re.++
            (seq.to.re (seq.unit 8))
            (re.++
                re.all
                (re.++
                    (seq.to.re (seq.unit 8))
                    re.all))))))

当我尝试运行它时，出现以下错误:

(error "line 11 column 11: Sort of function 're.++' does not match the declared type. Given domain: (RegEx (Seq Int)) (RegEx String) ")

所以我猜 re.all 只是为字符串定义的？有没有办法为所有整数创建一个正则表达式？

Answer 1

SMTLib 类型系统相当薄弱，当它看到 re.all 时会感到困惑，因为它无法区分字符串正则表达式和其他序列的正则表达式。因此你会遇到类型错误。

这实际上是在 SMTLib 标准中预期的，请参阅 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 3.6.4 节

解决方案(如标准中所述)是使用 as 子句来提供显式类型，如下所示:

(define-fun allInt () (RegEx (Seq Int)) (as re.all (RegEx (Seq Int))))

(declare-const s (Seq Int))
(assert (seq.in.re s
    (re.++
        allInt
        (re.++
            (seq.to.re (seq.unit 8))
            (re.++
                allInt
                (re.++
                    (seq.to.re (seq.unit 8))
                    allInt))))))

对于希望系统从上下文中找出实际类型应该是什么的人来说，这是一个常见的问题。但是为了保持系统简单，设计者选择了一个非常简单的类型系统:每个术语都应该可以独立输入，没有任何上下文信息。在极少数情况下这是不可能的(例如您的用例)，他们提供了 as 语法作为明确输入的一种方式。