z3 - 列表理论是可判定的吗？

Question

我想知道列表的z3理论是否可判定？似乎我们只能用该理论证明不饱和但不饱和的事实，所以我很好奇它是否真的可以判定。谢谢你的帮助。

Answer 1

在 Z3 中，当我们说一个理论是可判定的时，我们通常谈论的是无量词问题。Z3中实现的列表理论是可判定的。但是，一旦我们使用量词和未解释的函数，例如z3 中的问题叉积，问题就变得无法确定。Z3可以决定一些分片，但是在z3的叉积中描述的问题不在Z3支持的任何分片中。实际上，Z3 将无法为任何与此类似的问题构建模型。因此，它将永远运行尝试构建模型，或者将放弃返回unknown。结果unknown可能仍然有用。在某些情况下，Z3 可能会产生一个“候选模型”。也就是说，一种解释不满足您问题中的所有通用公式，但满足所有量词自由公式以及通用公式的许多实例。为此，我们必须禁用模块 MBQI。启用 MBQI 后，Z3 将继续尝试找到满足所有量词的解释。以下是我们为您做的示例：

http://rise4fun.com/Z3/kGtk

诀窍是我在脚本开头包含的以下两个命令：

(set-option :auto-config false)
(set-option :mbqi false) 

我用这个get-value命令来证明 Z3 产生的解释满足(assert (= (first (head l)) a)). 另一方面， 的解释append并不真正满足这个例子中的通用公式。