与z3表达式区分开来

Question

我从Python的输入文件中读取z3表达式。然后，稍后在我的代码中，我对它们调用__deepcopy__()。

问题是，有时输入的z3表达式是True或False，然后Python感到困惑，并认为它们是布尔型的，因此拒绝调用__deepcopy__()。错误消息是

AttributeError: 'bool' object has no attribute '__deepcopy__'

在这种情况下，如何区分bool和z3表达式？

Answer 1

您可以使用isinstance(e, ExprRef)添加显式测试您的表达式是否为Z3表达式：

from z3 import *

a = Int('a')
b = 3
expr = [a + 3,
        a < 7,
        And(a < 7, a > 2),
        b < 7,
        True]

expr_copy = [e.__deepcopy__() if isinstance(e, ExprRef) else e for e in expr]
print(expr_copy)
for e in expr:
    print(f'Is "{e}" a Z3 expression? {isinstance(e, ExprRef)}')