如何在 Python api 中使用 Z3 上下文？

如何解决如何在 Python api 中使用 Z3 上下文？

在 C++ 中，z3::context context 生成一个新的上下文。通过这个带有新上下文的 Z3 表达式可以创建为 context.bv_const(variable_name,16)。

如何使用 z3 python api 完成相同的行为？

解决方法

在 z3py 中，一般使用模型是通过一个 Solver 对象，该对象由一个全局上下文支持。这简化了编程，因为最终用户无需担心上下文创建的细节。来自文档：

  Z3Py uses a default global context. For most applications this is sufficient.
    An application may use multiple Z3 contexts. Objects created in one context
    cannot be used in another one. However,several objects may be "translated" from
    one context to another. It is not safe to access Z3 objects from multiple threads.
    The only exception is the method `interrupt()` that can be used to interrupt() a long
    computation.

因此，确实可以在 z3py 中创建一个新的 Context，如果您选择这样做的话；虽然这不是通用模型。

API 的设计使得大多数（如果不是全部）方法都将可选的上下文参数作为它们的最后一个参数。关于您提到的 bv_const，z3py 版本是：

def z3py.BitVecSort(sz,ctx = None)

（见https://z3prover.github.io/api/html/namespacez3py.html#afbff817f0f2dbfb6b9bebd9d50598683）

如您所见，最后一个参数是可选的 ctx 参数。如果不提供（这是一般的 z3py 编程模型），将使用全局的。然而，你可以通过你自己的，只要你注意我上面引用的警告。（也就是说，始终将来自不同上下文的对象分开。）

您可以在此处阅读 Context 课程详情：https://z3prover.github.io/api/html/classz3py_1_1_context.html