如何将bool与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表达式。请注意False作为Python布尔（b > 7）与Z3布尔（simplify(And(a > 7, b > 7))）之间的区别。

from z3 import Int, simplify, And, ExprRef

a = Int('a')
b = 3
expr = [a + 3,
        a < 7,
        And(a < 7, a > 2),
        And(a < 7, b > 7),
        simplify(And(a > 7, b > 7)),
        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)}')

输出：

[a + 3, a < 7, And(a < 7, a > 2), And(a < 7, False), False, False, True]
Is "a + 3" a Z3 expression? True
Is "a < 7" a Z3 expression? True
Is "And(a < 7, a > 2)" a Z3 expression? True
Is "And(a < 7, False)" a Z3 expression? True
Is "False" a Z3 expression? True
Is "False" a Z3 expression? False
Is "True" a Z3 expression? False