z3 - 处理空模型的量化公式的正确方法是什么？

Question

我在玩未解释的排序和函数，不能完全理解量化公式如何与空模型交互。这里（也在这里http://rise4fun.com/Z3Py/6ets）是一些让我有些困惑的简单例子：

1. [∀v : False]是不饱和的，而“直观地”它适用于空模型。
2. 检查[∃v : v = v]会产生一个空模型，而该模型没有令人满意的分配。
3. 一些看似等同于 的公式以[∃v : v = v]某种方式阻止 z3 生成空模型。[∃v, v1 : v = v1]就是这样一个例子。例如，如果我们将这样的公式添加到求解器，然后尝试创建类似于 allsat 程序的东西（添加越来越多的约束以排除越来越多的模型），我们会在得到一个空模型之前遇到 unsat。

那么，您能否请我参考任何描述 z3 如何处理量词和空模型的文档/论文？另外，如果我选择只关注非空模型，那么询问 z3 的正确方法是什么？诸如此类的事情[∃v, v1 : v = v1]似乎可以解决问题，但是有更好的方法吗？

Answer 1

Z3 不考虑空模型。这是一阶逻辑中的标准假设。有关更多详细信息，请搜索“一阶逻辑空模型”，您将获得许多解释此约定动机的链接。一阶逻辑的维基百科页面有一个简短的描述（“空域”部分）。

此外，我们不应该[]与空模型混淆。只是说为了满足输入公式，Z3不需要为输入公式中任何未解释的符号分配解释。Z3 仅显示满足公式所需的符号解释。例如，公式[∃v : v = v]不包含任何未解释的符号，则 Z3 仅显示空赋值 []。