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

【问题标题】：How to use Z3 Context in Python api?如何在 Python api 中使用 Z3 上下文？
【发布时间】：2021-01-02 20:22:24
【问题描述】：

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

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

【问题讨论】：

【解决方案1】：

在 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

【讨论】：