0

Eclipse IDE 内でZ3 ( http://z3.codeplex.com/ ) を使用しようとしています。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 は未​​定義の変数です。このコードを実行すると、次のエラー メッセージが表示されました。

「ImportError: ...\bin\z3.pyc の不正なマジック ナンバー」

これは、インタープリターとは異なるバージョンの python (通常はそれ以降) の問題のようです (参照: What's the bad magic number error? )。

何か助けはありますか？コンパイル済みの Windows バイナリを使用するのではなく、Z3Py をコンパイルしてインストールする必要がありますか?

ありがとう。

4

1 に答える 1

0

私は Eclipse から Python を使用することにあまり慣れていませんが、これは実際には Python のバージョンの不一致が原因である可能性が非常に高いです。おそらく最も安全な方法は、Python 2.7.x の 32 ビット バージョンをインストールし、Eclipse でもこのバージョンが使用されるようにすることです。あるいは、Python バインディング用にお気に入りのバージョンの Python を使用して、Z3 を自分でコンパイルすることもできます。不安定なブランチを使用することをお勧めします。これには、まだマスター ブランチに統合されていない多くの修正が含まれているためです (コンパイル手順については、READMEを参照してください)。Codeplex の「計画済み」セクション (こちらを参照) には、この問題を解決する可能性がある不安定版ブランチ用のプリコンパイル済み Windows バイナリもあることに注意してください。

于 2014-01-16T16:33:28.730 に答える