有没有办法获得Z3中的默认上下文？
有没有办法获得Z3中的默认上下文？
提问于 2013-05-11 10:54:28
我使用的是z3py API (4.3.0)。我可以使用expr.translate(target_ctx)轻松地将表达式expr从默认上下文转换为新的上下文target_ctx。但是，如何将给定的上下文ctx转换为默认的Z3上下文呢？有没有办法从Python API中获取默认的Context？
回答 1
Stack Overflow用户
回答已采纳
发布于 2013-05-11 11:19:05
它可以通过main_ctx()访问。
下面是描述main_ctx的Python API：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页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/16493305
复制相关文章
相似问题
腾讯云开发者
