Int 排序(SMT-LIB 2.0 Ints 理论)和 z3 中定义的动态声明排序如何? [英] How are Int sort (of SMT-LIB 2.0 Ints theory) and dynamically declared sorts defined in z3?

问题描述

这是我用 z3 执行的 SMT-LIB 2.0 基准测试:

Here is an SMT-LIB 2.0 benchmark which I executed with z3 :

(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)

(assert (forall ((x Int)) (exists ((X PZ)) 
            (and (MS x X) 
                 (forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)

我希望结果是 sat，至少有一个模型，其中 PZ 是 Z(整数)和 MS 是一个谓词，用于测试一个整数是否属于 Z(PZ 类型的元素)的子集.

I expected the result to be sat, with at least a model where PZ is the powerset of Z (integers) and MS is a predicate which tests the membership of an integer into a subset of Z (an element of the sort PZ).

但是 z3 回答了unsat.

你能帮我理解这个结果吗?具体来说，z3 如何解释排序 Int ?它真的被认为是无限的吗?动态声明的排序(这里是排序 PZ)怎么样?

Could you help me understanding this result please ? Specifically, how does z3 interprets the sort Int ? Is it really considered infinite ? What about dynamically declared sort (here the sort PZ) ?

推荐答案

在 Z3 中，Int 是无限的.你是对的，结果必须是 sat.unsat 结果是由于 Z3 模块之一中的错误造成的.我已经修复了这个错误.实现中的一个临时缓存没有被重置.该修复程序将在下一个版本中提供.同时，您可以通过在脚本开头使用以下命令来禁用错误模块.

In Z3, Int is infinite. You are correct, the result must be sat. The unsat result is due to a bug in one of the Z3 modules. I've already fixed the bug. One temporary cache in the implementation was not being reset. The fix will be available in the next release. In the meantime, you can disable the buggy module by using the following command in the beginning of your script.

(set-option :mbqi false)

顺便说一句，该错误仅影响包含 (= xy) 形式的文字的示例，其中 x 和 y 是通用变量.

BTW, the bug only affects examples that contain literals of the form (= x y) where x and y are universal variables.

顺便说一句，尽管您的示例是令人满意的，但 Z3 无法为其构建模型(即使在错误修复之后).实际上，在错误修复之后，Z3 产生了答案unknown.模型查找器(在 Z3 中使用)只能查找未解释类型(例如 PZ)的解释是有限的模型.此限制将来可能会更改.

BTW, although your example is satisfiable, Z3 can't build a model for it (even after the bug fix). Actually, after the bug fix, Z3 produces the answer unknown. The model finder (used in Z3) is only capable of finding models where the interpretation of uninterpreted sorts (such as PZ) is finite. This limitation may change in the future.

这篇关于Int 排序(SMT-LIB 2.0 Ints 理论)和 z3 中定义的动态声明排序如何?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！