Z3py上下文使用

Question

我不明白如何在Z3/Z3py中使用上下文。下面的示例返回context mismatch，但是如果我将And更改为==或Implies，它会工作，如果从x声明中删除上下文，则会得到z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value。为什么？我知道在这个简单的例子中我不需要上下文，但是我需要并行化一个使用Z3py的更复杂的脚本。

from z3 import *

ctx=Context()
solver=Solver(ctx=ctx)
x=Bool('x',ctx=ctx)
solver.add(And(x,x))
print(solver.check())

Traceback (most recent call last):
  File "minimal_test.py", line 6, in <module>
    solver.add(And(x,x))
  File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 1727, in And
    _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch")
  File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 96, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: context mismatch

Answer 1

这个程序，正如你在你的问题中所提出的，对我来说运行的很好，产生了sat。所以，我不知道你为什么要看到你看到的东西，除非你有一个非常老的z3版本，它有一个bug或什么的。(Github主版为4.11.2；我使用的是4.9.2；您有什么版本？)

如果从x的声明中删除上下文，您将得到"z3.z3types.Z3Exception: Value不能转换为Z3布尔值“，因为x是在全局上下文中创建的，但是解决程序是在特定的上下文中创建的。通常，如果您有多个上下文，那么只需使用该上下文声明所有变量。(默认情况下，它们都将使用全局上下文；如果没有显式声明，则可以使用全局上下文。)像And/Or/Implies这样的函数只需使用其参数的上下文来确定要在哪个上下文中创建表达式。

所以，你在问题中给出的程序是正确使用上下文的方法。我不清楚为什么你会失败；也许你有很多版本的这个程序，不知怎么搞不懂哪一个是哪一个？