如何从 z3 Python API 中的求解器获得的模型创建附加约束？

Question

一旦遇到约束问题，我想看看它是否可满足。基于返回的模型（当它被坐下时）我想添加断言然后再次运行求解器。但是，我似乎误解了返回模型中包含的某些 types/values 。考虑以下示例：

solv = z3.Solver()
n = z3.Int("n")
solv.add(n >= 42)
solv.check()  # This is satisfiable
model = solv.model()
for var in model:
    # do something
    solv.add(var == model[var])
solv.check() # This is unsat

我希望在循环之后我基本上有两个约束 n >= 42 和 n == 42，当然假设 z3 在第一次调用中生成模型 n=42。尽管如此，在第二次调用中 check() returns 不满意。我错过了什么？

旁注：当用 solv.add(var >= model[var]) 替换 solv.add(var == model[var]) 时，我得到 z3.z3types.Z3Exception: Python value cannot be used as a Z3 integer。这是为什么？

Answer 1

循环模型时，您不会获得可以直接查询的变量。你得到的是一个内部表示，它可以对应一个常量，也可以对应更复杂的东西，比如函数或数组。通常，您应该使用您拥有的变量查询模型，即使用 n。（如 model[n]。）

您可以像这样解决眼前的问题：

for var in model:
  solve.add(var() == model[var()])

但这只适用于假设模型中有简单变量，即没有 uninterpreted-functions、数组或其他对象。有关详细讨论，请参阅此问题：

同样，您的第二个表达式抛出异常，因为虽然 == 是在任意对象上定义的（尽管这里做错了事），但 >= 不是。因此，从某种意义上说，在这里抛出异常是“正确”的做法。（也就是说，== 也应该抛出异常。）唉，Python 绑定是松散类型的，这意味着它会尝试理解你写的东西，而不一定总是做你一路上的打算。

如何从 z3 Python API 中的求解器获得的模型创建附加约束？

How do I create additional constraints from a model obtained by a solver in z3 Python API?

smt

z3

z3py

smt-lib