z3 - 如何从可满足的公式中恢复估值，关于模型的问题

Question

我正在使用带有 ml 接口的 Z3。根据求解器 Solver.mk_simple_solver ctxr，我创建了一个可满足的公式 f(x_i)。

问题是：我可以得到一个模型，但他只为公式的一些变量找到我的值，而不是全部（我的一些Model.get_const_interp_er 以无类型结尾）

模型怎么可能只给我x_ir的一部分？据我了解，如果模型适用于其中一个值，则意味着该公式是可满足的（在我的情况下是可满足的），因此可以给出所有值...

我不明白的东西.. 感谢您阅读我！

标签： z3

Answer 1

您应该始终发布完整的示例，以便人们可以帮助解决实际的编码问题；如果没有看到您的实际代码，就不可能知道可能是什么实际原因。

话虽如此，这听起来很像以下问题：为什么 Z3Py 没有提供所有可能的解决方案所以，也许那里给出的答案会对您有所帮助。

长话短说：Z3 模型将只包含对模型很重要的变量的值。对于未明确分配的任何内容，任何值都可以。当然，有一些方法可以获得“完整”模型，如该答案中所述；我敢肯定，这也可以通过 ML 界面实现。