国际贸易组织的Z3 RegEx *

Question

我试图写一个断言，即某个整数的序列至少包含两个整数(例如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不能区分字符串regexp和regexp时，它会感到困惑。因此你得到了一个类型错误。

实际上，这在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语法作为显式输入的一种方式。