1

我写了以下断言：

(assert (!
    (forall ((A Set) (B Set))
        (= 
            (= A B) 
            (and (subset A B)(subset B A)))
:no-pattern)))

为什么它会给出错误“ invalid expression, unexpected input”？为了检查语法错误，我复制了指南中的示例并将其替换为. 这也会产生错误。:pattern (…):no-pattern

4

1 回答 1

2

注释:no-pattern需要一个表达式作为参数。如果一个普遍量化的公式F没有用模式注释，那么 Z3 将启发式地为F. 注释指示 Z3 中出现:no-pattern的哪些子表达式F不应用作模式。这是您的示例（也可在http://rise4fun.com/Z3/KfO5获得）：

(declare-sort Set)
(declare-fun mysubset (Set Set) Bool)

(assert 
    (forall ((A Set) (B Set))
        (! (= 
            (= A B) 
            (and (mysubset A B) (mysubset B A)))
           :no-pattern (mysubset A B))))

(check-sat)

备注：方程（例如，(= A B)）从未被 Z3 选为模式。

这是另一个示例http://rise4fun.com/Z3/njVu的链接。

顺便说一句，注释:pattern接受两种参数：表达式；或表达式列表。在 Z3 指南中，我们有注释：:pattern ((f (g x))，其中((f (g x))是一个长度为 1 的列表，其中包含表达式(f (g x))。如果我们用 替换:pattern，:no-pattern我们会得到一个错误，因为((f (g x))它不是一个表达式。另一方面，:no-pattern (f (g x)是一个有效的:no-pattern注解。

最后，:pattern接受表达式列表，因为 Z3 支持多模式（指南）。

于 2012-11-23T19:27:54.430 回答