z3pyの例はmacOSでは動作しません

z3pyの例は動作しません。私はgithub上のREADMEからの指示を使ってうまくインストールできました。私は正常に私のpythonのパスを適切なディレクトリを指すように更新しました。さらに、z3を正常にインポートすることができましたが、変数を宣言するたびにエラーが発生します。コンパイラはInt、Ints、Real、RealValを認識しません。z3pyの例はmacOSでは動作しません

説明する例を示しました。

コード：

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

Error: Traceback (most recent call last): File "test.py", line 3, in x = Int('x') NameError: name 'Int' is not defined

私は本当に任意の助けをいただければ幸いです。どうもありがとうございます。

出典

2016-06-17 Akanksha Vyas

'from z3 import *'の後に 'dir（）'が表示されますか？代わりに 'import z3;を試しましたか？ x = z3.Int（ 'x'） '？ – nekomatic

@nekomantic：お返事ありがとうございます。ここでの答えは以下のとおりです。 'Z3のインポート* DIRから（） >>> [ '__ builtins__'、 '__doc__'、 '__name__'、 '__PACKAGE__'] >>> X = INT（ 'X'）トレースバック（最新の呼び出しの最後）： NameErrorでファイル ""、行1、：名 'INTが' '>>>インポートZ3を >>> X = INT（ 'X'）defined'されていませんトレースバック（最新のコール最後）：ファイル ""、行1、 NameError：名前 'Int'が定義されていません。 –

モジュールをインポートした後、 'dir（）'なので、z3を正しくインストールしたかどうかを確認します。 – nekomatic

PythonまたはZ3のいずれかのローカルインストールに問題があります。

私はちょうど私のMacでZ3をコンパイルして、問題なく提供した例test.pyを実行しました。私はPython 2.7.11と現在のマスターバージョンZ3（コミット41edf5f）でOS X 10.9.5を使用しています。私が使用される正確な命令があった。私が得た

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

出力は、私は私のLinuxボックスのスクリプトからもらった同じ出力され、[y = 0, x = 7]ました。したがって、問題はお使いのOS Xのマシンまたはビルド手順に固有です。

出典

2016-06-23 17:24:09

z3pyの例はmacOSでは動作しません

答えて

関連する問題