在 Z3-Python 中使用求解器的基本错误：它返回 [] 作为模型
Basic error using solver in Z3-Python: it is returning [] as a model
也许我今天睡得不好，但我真的在为 Z3-Python:
这个简单的查询而苦苦挣扎
from z3 import *
a = Bool('a')
b = Bool('b')
sss = Solver()
sss.add(Exists([a,b], True))
print(sss.check())
print(sss.model())
支票打印出来sat，但是型号是[]。但是，它应该打印一些（任何人）具体的分配，例如 a=True, b=True.
如果我将公式更改为：sss.add(Exists([a,b], Not(And(a,b))))，也会发生同样的情况。还测试了sss.add(True)。因此，我遗漏了一些非常基本的东西，很抱歉这个问题的基本性质。
其他代码运行正常（即使使用优化器而不是求解器），所以这不是我环境的问题（Collab）
有什么帮助吗？
请注意，两者之间存在很大差异：
a = Bool('a')
b = Bool('b')
sss.add(Exists([a, b], True))
和
a = Bool('a')
b = Bool('b')
sss.add(True) # redundant, but to illustrate
在第一种情况下，您要检查语句 Exists a. Exists b. True 是否可满足；这很简单；但是没有模型可以显示：变量a和b是inside quantification；而且它们在模型构建中没有任何作用。
在第二种情况下，a 和 b 是模型的一部分，因此会显示出来。
令人困惑的是为什么你需要在第一种情况下声明a和b。也就是说，为什么我们不能直接说：
sss.add(Exists([a, b], True))
环境中没有任何 a 或 b？毕竟，就问题而言，它们是无关紧要的。这只是 Python API 的一个特点；除了它的实现方式之外，真的没有什么好的理由。
您可以通过添加以下形式的语句来查看生成的 SMTLib：
print(sss.sexpr())
如果您对上述部分执行此操作，您会发现第一个部分甚至根本没有声明变量。
所以，长话短说，公式 exists a, b. True 没有“模型”变量，因此没有可显示的内容。你在 z3py 中声明它们的唯一原因是因为它们使用了一个实现技巧（因此它们可以找出变量的类型），仅此而已。
以下是针对您的问题的一些具体评论：
SMT 求解器只会为 top-level 声明的变量构造 model-values。如果您通过 exists/forall 创建“本地”变量，它们将不会显示在构建的模型中。请注意，您可能有两个完全独立的断言来讨论“相同的”存在量化变量：它甚至没有办法引用该项目。 Rule-of-thumb：如果要查看模型中的值，必须在 top-level 处声明。
对，就是这个原因。所以他们可以弄清楚这些变量是什么类型。 （和其他簿记。）z3py 没有提供语法来让你说 Exists([Int(a), Int(b)], True) 之类的东西。请注意，这并不意味着这样的事情无法实施。他们只是没有。 （而且可能不值得。）
不，你没看错。你得到 [] 的原因是因为对那些 a 和 b 绝对没有约束，并且 z3 的模型构造函数不会分配任何值，因为它们是不相关的。您可以通过 model_completion 参数恢复它们的值。但是最好的试验方法是在顶层添加一些额外的约束。 （如果你做 a 和 b 整数可能更容易玩。在顶层，断言 a = 5, b = 12。在“存在”层面断言其他东西。你会看到你的模型将只满足 top-level 约束。有趣的是，如果你断言在你的存在查询中不能满足的东西，整个事情将变成 unsat；这是他们如何被对待的另一个标志。
我说的很对，因为你的公式是Exists a. Exists b. True。没有约束，所以对 a 和 b 的任何赋值都满足它。从这个意义上说，这是微不足道的。 （所有 SMTLib 逻辑都在 non-empty 域上工作，因此您始终可以自由分配值。）
量化变量总是可以alpha-renamed而不改变语义。因此，每当量化名称和 top-level 名称之间存在冲突时，想象将它们重命名为唯一的。如果你这样想，我想你就能回答你自己的问题了。
对评论进行长时间的讨论确实没有效果。如果有任何不清楚的地方，请随时提出新问题。
也许我今天睡得不好，但我真的在为 Z3-Python:
这个简单的查询而苦苦挣扎from z3 import *
a = Bool('a')
b = Bool('b')
sss = Solver()
sss.add(Exists([a,b], True))
print(sss.check())
print(sss.model())
支票打印出来sat，但是型号是[]。但是，它应该打印一些（任何人）具体的分配，例如 a=True, b=True.
如果我将公式更改为：sss.add(Exists([a,b], Not(And(a,b))))，也会发生同样的情况。还测试了sss.add(True)。因此，我遗漏了一些非常基本的东西，很抱歉这个问题的基本性质。
其他代码运行正常（即使使用优化器而不是求解器），所以这不是我环境的问题（Collab）
有什么帮助吗？
请注意，两者之间存在很大差异：
a = Bool('a')
b = Bool('b')
sss.add(Exists([a, b], True))
和
a = Bool('a')
b = Bool('b')
sss.add(True) # redundant, but to illustrate
在第一种情况下，您要检查语句 Exists a. Exists b. True 是否可满足；这很简单；但是没有模型可以显示：变量a和b是inside quantification；而且它们在模型构建中没有任何作用。
在第二种情况下，a 和 b 是模型的一部分，因此会显示出来。
令人困惑的是为什么你需要在第一种情况下声明a和b。也就是说，为什么我们不能直接说：
sss.add(Exists([a, b], True))
环境中没有任何 a 或 b？毕竟，就问题而言，它们是无关紧要的。这只是 Python API 的一个特点；除了它的实现方式之外，真的没有什么好的理由。
您可以通过添加以下形式的语句来查看生成的 SMTLib：
print(sss.sexpr())
如果您对上述部分执行此操作，您会发现第一个部分甚至根本没有声明变量。
所以，长话短说，公式 exists a, b. True 没有“模型”变量，因此没有可显示的内容。你在 z3py 中声明它们的唯一原因是因为它们使用了一个实现技巧（因此它们可以找出变量的类型），仅此而已。
以下是针对您的问题的一些具体评论：
SMT 求解器只会为 top-level 声明的变量构造 model-values。如果您通过 exists/forall 创建“本地”变量，它们将不会显示在构建的模型中。请注意，您可能有两个完全独立的断言来讨论“相同的”存在量化变量：它甚至没有办法引用该项目。 Rule-of-thumb：如果要查看模型中的值，必须在 top-level 处声明。
对，就是这个原因。所以他们可以弄清楚这些变量是什么类型。 （和其他簿记。）z3py 没有提供语法来让你说
Exists([Int(a), Int(b)], True)之类的东西。请注意，这并不意味着这样的事情无法实施。他们只是没有。 （而且可能不值得。）不，你没看错。你得到
[]的原因是因为对那些a和b绝对没有约束，并且 z3 的模型构造函数不会分配任何值，因为它们是不相关的。您可以通过model_completion参数恢复它们的值。但是最好的试验方法是在顶层添加一些额外的约束。 （如果你做a和b整数可能更容易玩。在顶层，断言a = 5, b = 12。在“存在”层面断言其他东西。你会看到你的模型将只满足 top-level 约束。有趣的是，如果你断言在你的存在查询中不能满足的东西，整个事情将变成unsat；这是他们如何被对待的另一个标志。我说的很对，因为你的公式是
Exists a. Exists b. True。没有约束，所以对a和b的任何赋值都满足它。从这个意义上说，这是微不足道的。 （所有 SMTLib 逻辑都在 non-empty 域上工作，因此您始终可以自由分配值。）量化变量总是可以alpha-renamed而不改变语义。因此，每当量化名称和 top-level 名称之间存在冲突时，想象将它们重命名为唯一的。如果你这样想，我想你就能回答你自己的问题了。
对评论进行长时间的讨论确实没有效果。如果有任何不清楚的地方，请随时提出新问题。