python - 如何区分 bool 和 z3 表达式？

Question

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

问题在于，有时输入的 z3 表达式为 True 或 False，那么 Python 就会感到困惑，认为它们是 bool 并拒绝调用 __deepcopy__() 。错误信息是

AttributeError:“bool”对象没有属性“__deepcopy__”

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

Answer 1

您可以使用 isinstance(e, ExprRef) 添加显式测试您的表达式是否为 Z3 表达式。请注意 Python bool 值 (b > 7) 和 Z3 bool 值 (simplify(And(a > 7, b > 7))False 之间的区别)。

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