我正在玩未解释的排序和函数，不能完全理解量化公式如何与空模型相互作用。这里(也在这里http://rise4fun.com/Z3Py/6ets)是一些简单的例子，我有点困惑:
-
[∀v : False]是unsat，而"直观地"它适用于空模型。 - 检查
[∃v : v = v]会产生一个空模型，而该模型没有令人满意的分配。 - 一些看似等同于
[∃v : v = v]的公式，以某种方式阻止了z3产生空模型。[∃v, v1 : v = v1]就是这样一个例子。例如，如果我们将这样的公式添加到求解器中，然后尝试创建类似于allsat过程的东西(添加越来越多的约束来排除越来越多的模型)，我们将在获得空模型之前遇到unsat。
所以，你能给我参考一下描述z3如何处理量词和空模型的文件/论文吗?此外，如果我选择将注意力限制在非空模型上，那么问z3的正确方法是什么?像[∃v, v1 : v = v1]这样的东西似乎可以做到这一点，但有没有更好的方法?
Z3不考虑空模型。这是一阶逻辑的标准假设。要了解更多细节，请搜索"一阶逻辑空模型"，您将获得许多解释此约定动机的链接。一阶逻辑的维基百科页面有一个简短的描述(章节"空域")。
此外，我们不应该将[]与空模型混淆。它只是说，为了满足输入公式，Z3不需要为输入公式中任何未解释的符号分配解释。Z3只显示满足公式所需的符号的解释。例如，公式[∃v : v = v]不包含任何未解释的符号，那么Z3只显示空赋值 []。