Я пытаюсь использовать Z3 (http://z3.codeplex.com/) в Eclipse IDE. Я установил PyDev и загрузил предварительно скомпилированные двоичные файлы Windows для Z3. Я также добавил подкаталог «bin» в переменные окружения PYTHONPATH и PATH.
В этом очень простом примере
from z3 import *
x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()
Eclipse говорит, что Real e Solver - это неопределенные переменные. Запустив этот код, я получил сообщение об ошибке:
"ImportError: неверное магическое число в ...\bin\z3.pyc"
Кажется, это проблема другой версии Python (обычно более поздней), чем интерпретатор (см.: Что за ошибка неправильного магического числа?).
Любая помощь? Нужно ли компилировать и устанавливать Z3Py, а не использовать предварительно скомпилированные двоичные файлы Windows?
Спасибо.
