Z3py Context使用报错：context mismatch原因及解决问询

问题原因 #

• context mismatch错误的核心是：And函数默认使用全局上下文，但你的变量x属于自定义创建的ctx上下文，两者上下文不匹配引发冲突。
• ==或Implies能正常运行，是因为它们通过Python操作符重载实现，会自动从传入的表达式（如x）中提取上下文信息，无需显式指定。而And是普通函数，默认绑定全局上下文，必须手动指定自定义上下文才能匹配。
• 移除x的ctx参数后报错，是因为x属于全局默认上下文，而solver属于自定义ctx上下文，Z3不允许将不同上下文的表达式添加到求解器中，因此抛出类型不兼容错误。

解决方法 #

有两种方式让And适配自定义上下文：

1. 给And显式传入ctx参数

from z3 import *

ctx = Context()
solver = Solver(ctx=ctx)
x = Bool('x', ctx=ctx)
solver.add(And(x, x, ctx=ctx))
print(solver.check())

2. 调用上下文对象的And方法
   每个Context实例都自带逻辑操作方法，直接调用即可自动使用该上下文：

from z3 import *

ctx = Context()
solver = Solver(ctx=ctx)
x = Bool('x', ctx=ctx)
solver.add(ctx.And(x, x))
print(solver.check())

并行化场景注意事项 #

并行脚本中使用Z3py时，必须保证同一线程内的所有Z3对象（变量、求解器、表达式等）归属同一个上下文，不同线程使用独立的上下文实例，完全隔离，避免跨上下文操作引发的各类错误。

内容的提问来源于stack exchange，提问作者65537