Примеры z3py не работают на macOS

Я не могу заставить работать ни один из примеров z3py. Мне удалось успешно установить его, следуя инструкциям из README на github. Я успешно обновил свой путь Python, чтобы он указывал на соответствующий каталог. Кроме того, мне удалось успешно импортировать z3, но каждый раз, когда я объявляю переменную, я получаю сообщение об ошибке. Компилятор не распознает Int, Ints, Real, RealVal.

Я включил пример для иллюстрации.

Код:

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

Ошибка: трассировка (последний вызов последний): файл "test.py", строка 3, в x = Int ('x') NameError: имя 'Int' не определено

Буду очень признателен за любую помощь. Большое спасибо.


python z3 z3py
person Akanksha Vyas    schedule 17.06.2016    source источник
comment
Что dir() показывает вам после from z3 import *? Вы вместо этого пробовали import z3; x = z3.Int('x')?   -  person nekomatic    schedule 17.06.2016
comment
@nekantic: Спасибо за ответ. Вот ответы: from z3 import * dir() >>>['__builtins__', '__doc__', '__name__', '__package__'] >>> x = Int('x') Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'Int' is not defined >>> import z3 >>> x = Int('x') Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'Int' is not defined   -  person Akanksha Vyas    schedule 18.06.2016
comment
После того, как вы import модуль, он должен появиться в результате dir(), поэтому я бы проверил, правильно ли вы установили z3.   -  person nekomatic    schedule 19.06.2016
comment
@nekantic Я исправил это, и та же проблема сохраняется, хотя кажется, что импорт выполняется правильно. Вот результат. Еще раз спасибо: >>> import z3 >>> dir() ['__builtins__', '__doc__', '__name__', '__package__', '__warningregistry__', 'z3'] >>> x = Int('x') Traceback (most recent call last): File "<stdin>", line 1, in <module> NameError: name 'Int' is not defined   -  person Akanksha Vyas    schedule 20.06.2016
comment
Внимательно прочтите мое предложение: если вы сделали import z3, попробуйте x = z3.Int('x') и так далее.   -  person nekomatic    schedule 20.06.2016
comment
У вас есть z3.py в вашем рабочем каталоге? Он затеняет установленный пакет.   -  person Łukasz Rogalski    schedule 23.06.2016
comment
Наконец-то он заработал после чистой установки. Спасибо за твою помощь.   -  person Akanksha Vyas    schedule 25.06.2016

Ответы (1)


arrow_upward
0
arrow_downward

Что-то не так с вашей локальной установкой Python или Z3.

Я только что скомпилировал Z3 на своем Mac и без проблем запустил предоставленный вами пример test.py. Я использую OS X 10.9.5 с Python 2.7.11 и текущую основную версию Z3 (фиксация 41edf5f). Я использовал следующие точные инструкции:

git clone https://github.com/Z3Prover/z3.git
cd z3
./configure
cd build
make -j4
emacs test.py
# Write in the example you gave.
python ./test.py

Я получил результат [y = 0, x = 7], то есть тот же результат, который я получил от вашего скрипта на моем компьютере с Linux. Таким образом, проблема связана с вашей машиной OS X или процедурой сборки.

person Douglas B. Staple    schedule 23.06.2016