z3 - 有没有办法在 Z3 中获取默认上下文？

Question

我正在使用 z3py API (4.3.0)。我可以轻松地将表达式expr从默认上下文转换为新上下文target_ctx，使用expr.translate(target_ctx). 但是如何从给定的上下文ctx转换为默认的 Z3 上下文？有没有办法Context从 Python API 获取默认值？

Answer 1

可以通过main_ctx().

这是 Python API 描述main_ctx：http ://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-main_ctx

另一种方法是object.ctx从没有引用特定上下文（main_ctx()默认使用全局上下文）创建的任何对象。

Context这是描述其中一些内容的 Python API ： http ://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#Context

这是显示这些方法的示例（z3py 链接：http ://rise4fun.com/Z3Py/1sN ）：

x, y = Reals('x y')

print x.ctx == y.ctx # True
ctx_default = x.ctx
print x.ctx == main_ctx() # True

ctx1 = Context()
x1, y1 = Reals('x1 y1', ctx1)
print ctx_default == x1.ctx # False