Z3 и Eclipse IDE

Question

Я пытаюсь использовать Z3 ( http://z3.codeplex.com/) в Eclipse IDE. Я установил PyDev и скачал предварительно скомпилированные двоичные файлы Z3 для Windows. Я также добавил подкаталог 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 - неопределенные переменные. Запустив этот код, я получил эту ошибку MSG:

"ImportError: неверное магическое число в...\bin\z3.pyc"

Кажется, что это проблема другой версии Python (обычно позже), чем интерпретатор (см.: Что такое ошибка с магическим числом?).

Любая помощь? Нужно ли мне компилировать и устанавливать Z3Py, а не использовать предварительно скомпилированные двоичные файлы Windows?

Благодарю.

Answer 1

Я не очень знаком с использованием Python из Eclipse, но очень вероятно, что это действительно из-за несоответствия версий Python. Возможно, самый безопасный способ - установить 32-битную версию Python 2.7.x и убедиться, что Eclipse также использует эту версию. Кроме того, вы можете скомпилировать Z3 самостоятельно, используя вашу любимую версию Python для привязок Python. Я бы посоветовал использовать нестабильную ветку, так как она содержит много исправлений, которые еще не интегрированы в основную ветку (инструкции по компиляции см. В README). Обратите внимание, что в нестандартной ветке в разделе "запланировано" на Codeplex есть также предварительно скомпилированные двоичные файлы Windows (см. Здесь), которые могут решить эту проблему.