Константы Z3 и оператор python 'in' - PullRequest
Новая
       26

Константы Z3 и оператор python 'in'

0 голосов
/ 02 апреля 2020

Мне было интересно, безопасно ли использовать тестирование членства с python встроенным типом набора и константами z3.

Предположим, есть следующий пример: 

a = Int('a')
a2 = Int('a')

s = set()
s.add(a)

print(a2 in s)

последняя строка возвращает True, что является моим желаемым поведением (когда name то же самое). Однако оператор __eq__() в ExpRef переопределен, чтобы вернуть ограничение 'self == other', и поэтому я не понимаю, откуда взялся этот True. Может ли случиться так, что оператор in может вернуть True при наличии двух констант с другим name?

Ответы [ 2 ]

1 голос
/ 03 апреля 2020

__eq__ действительно просто возвращает ограничение, но __bool__ для этого ограничения возвращает логическое значение, которое сравнивает, являются ли два аргумента синтаксически равными. Таким образом, в основном __eq__ перегружен таким образом, что a == a2 сам по себе просто создает ограничение равенства, но использование его в логическом контексте фактически позволяет сравнивать, являются ли a и a2 синтаксически одинаковыми. Таким образом, две константы с одним и тем же именем будут сравниваться одинаково, а константы с разными именами - нет.

__hash__ также определяется с использованием того же понятия равенства. Поэтому его можно использовать в наборах (или в качестве ключей в словах).

1 голос
/ 03 апреля 2020

Да, это безопасно. Это работает, потому что вы буквально сравниваете базовое представление этих объектов (как AST), и они никогда не будут равны в этом смысле, если у вас разные имена.

Но я должен сказать, что это довольно неортодоксально. Чтобы проиллюстрировать это, рассмотрим следующее: 

from z3 import *

a = Int('a')
b = Int('b')
solver = Solver()
solver.add(a == b)

s = set()
s.add(a)
s.add(b)

print(s)

, это напечатает {b, a}, хотя мы явно утверждали, что a и b абсолютно одинаковы для решателя. Это может привести к путанице в будущем.

Конечно, это вполне может быть именно то, что вы пытаетесь сделать. То есть разделить переменные синтаксически, независимо от их значения. Я могу видеть некоторые варианты использования для этого, если вы выполняете программирование на «мета» уровне z3, то есть создаете библиотеки поверх него, но в целом вам следует избегать любых действий, которые проверяют идентичность таких объектов в z3py. Это может привести к путанице, если вы начнете смешивать идентичность объекта и идентичность значения. Обычно в программировании Symboli c требуется значение-тождество, но опять же, это зависит от вашего варианта использования.

...