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

'dir（）'在'from z3 import *'之後顯示給你什麼？你有沒有嘗試過'import z3; x = z3.Int（'x'）'？ – nekomatic

@nekomantic：感謝您的回覆。下面是正確答案： '從Z3進口* DIR（） >>> [ '__ builtins__'， '__doc__'， '__name__'， '__PACKAGE__'] >>> X = INT（ 'X'）回溯（最後最近一次調用）：文件「」，1號線，在 NameError：名字 '詮釋' 不是defined' '>>>進口Z3 >>> X = INT（ 'X'）回溯（最近通話最後一個）：文件「」，1號線，在 NameError：名字「詮釋」不是defined' –

後你'import'它應該出現在結果的模塊'dir（）'，所以我會檢查你是否已經正確安裝了z3。 – nekomatic

您的本地安裝有問題，無論是Python還是Z3。

我剛剛在我的Mac上編譯了Z3，並運行了您提供的沒有問題的示例test.py。我使用Python 2.7.11的OS X 10.9.5和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機器或構建過程。

來源

2016-06-23 17:24:09

z3py示例不能在macOS上工作

回答

相關問題