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

【问题标题】：What is the correct way to handle quantified formulas with respect to empty models?处理空模型的量化公式的正确方法是什么？
【发布时间】：2013-03-01 01:05:31
【问题描述】：

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

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

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

【问题讨论】：

标签： z3 smt first-order-logic

【解决方案1】：

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

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

【讨论】：