Переменные Z3Py Bool преобразуются в Int в модели

Я использую API Python для Z3, чтобы создать инструмент для своих исследований. У меня возникла следующая проблема: я генерирую набор ограничений Z3 с помощью скрипта Python. Поскольку набор может быть непоследовательным, я отслеживаю каждую формулу с помощью assert_and_check. Например,

s.assert_and_track(occWrites_1== True, 'p16')

Конечно, occWrites объявляется логическим:

occWrites_1 = Bool('occWrites_1')

Однако в модели Z3 сообщает occWrites как целое число. Почему это происходит? Разве значение occWrites в модели не должно быть либо True, либо False?


boolean int z3 z3py
person Suvam Mukherjee    schedule 13.06.2013    source источник
comment
Пожалуйста, предоставьте ссылку на минимальный пример, размещенный на Rise4fun, который демонстрирует поведение.   -  person Malte Schwerhoff    schedule 14.06.2013

Ответы (1)


arrow_upward
0
arrow_downward

Не могу воспроизвести описанную вами проблему. В следующем примере значение occWrites_1 равно true в модели, созданной Z3. Он также доступен онлайн здесь. Обратите внимание, что значение является выражением Z3, а не значением Python True. Возможно, это и есть источник путаницы. Метод sexpr() красиво печатает значение, используя внутренний формат Z3.

from z3 import *

s = Solver()
occWrites_1 = Bool('occWrites_1')
s.assert_and_track(occWrites_1 == True, 'p16')
print s.check()
m = s.model()
print m[occWrites_1]
print m[occWrites_1].sexpr()

Производимый выход:

sat
True
true
person Leonardo de Moura    schedule 19.06.2013