Есть ли способ получить контекст по умолчанию в Z3?

Question

Я использую API z3py (4.3.0). Я могу легко перевести выражение expr из контекста по умолчанию в новый контекст target_ctx, используя expr.translate(target_ctx). Но как я могу перевести из заданного контекста ctx в контекст Z3 по умолчанию? Есть ли способ получить значение по умолчанию Context из API Python?

Answer 1

Доступ к нему осуществляется через main_ctx().

Вот API Python описания main_ctx: http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-main_ctx

Другой способ сделать это с object.ctx из любого объекта, созданного без ссылки на конкретный контекст (который использует глобальный контекст main_ctx() по умолчанию).

Вот Python API, описывающий Context в котором обсуждаются некоторые из этого: 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