smt - 如何将 Z3 中的排序域限制为单个值？

Question

我在Z3 程序中使用以下规则来s生成 sort 的唯一可能值S。

(assert (forall ((t S)) (= t s)))

但是，上面的公式让Z3报如下错误：

Z3: ERROR: WARNING: failed to find a pattern for quantifier (quantifier id: k!8)

确保特定类型的域只有一个值的正确方法是什么？

Answer 1

讯息

Z3：错误：警告：找不到量词的模式（量词 id：k！8）

具有误导性。这只是一个警告，“错误”一词是偶然出现的。这已修复，将在下一个版本中提供。警告只是告诉用户电子匹配模块将忽略量词。但是，Z3 使用许多引擎来处理量化公式。MBQI 模块可以处理这个量化的公式，并为以下问题建立令人满意的分配：

（声明排序 S）

(declare-fun s () S)

(断言 (forall ((t S)) (= ts)))

(declare-fun a () S)

(declare-fun b () S)

（断言（= ab））

（检查周六）

（模型）

话虽如此，上面的量化公式并不是使用单个元素指定排序的最佳方式。您可以使用数据类型对枚举类型进行编码。例如，以下命令定义了一个包含元素 e1 ... en 的排序 S。 (declare-datatypes ((S e1 e2 … en))) 可以使用以下方法指定只有一个元素的排序： (declare-datatypes ((S e))) 以下示例无法满足：

（声明数据类型（（S elem）））

（声明常量 a S）

（声明常量 b S）

（断言（非（= ab）））

（检查周六）