有没有办法在 Z3 中获取默认上下文? [英] Is there a way to obtain the default context in Z3?

问题描述

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

I am using the z3py API (4.3.0). I can easily translate an expression expr from the default context to a new context target_ctx, using expr.translate(target_ctx). But how can I translate from a given context ctx into the default Z3 context? Is there a way to obtain the default Context from the Python API?

推荐答案

可以通过main_ctx()访问.

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

Here's the Python API describing main_ctx: http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-main_ctx

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

Another way to do this is with object.ctx from any object created without a reference to a specific context (which uses the global context main_ctx() by default).

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

Here's the Python API describing Context which discusses some of this: http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#Context

以下是展示这些方法的示例(z3py 链接:http://rise4fun.com/Z3Py/1sN ):

Here's an example showing these approaches (z3py link: 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

这篇关于有没有办法在 Z3 中获取默认上下文?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！