Как отличить guish bool от выражения z3? - PullRequest
Новая
       9

Как отличить guish bool от выражения z3?

2 голосов
/ 23 января 2020

Я читаю выражения z3 из входного файла в Python. Затем в моем коде я вызываю __deepcopy__() для них.

Проблема в том, что иногда выражение ввода z3 имеет значение True или False, тогда Python сбивается с толку и думает, что это бул и отказывается позвонить __deepcopy__(). Сообщение об ошибке:

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

Как в этом случае можно различить guish между выражениями bool и z3?

1 Ответ

3 голосов
/ 26 января 2020

Вы можете добавить явный тест, является ли ваше выражение выражением Z3, используя isinstance(e, ExprRef). Обратите внимание на разницу между 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
...