1

Mac で z3py に奇妙な問題が発生しています。

$ cat bug.py
from z3 import *       
x = Int('x')
s = Solver()
s.add(x > 5)
print(s.check())
print(s.model())
$ python bug.py
sat
[x = ]

x の値がモデルにありません。マスター ブランチと不安定ブランチの両方を試してみましたが、結果は同じでした。ただし、同様の .smt2 ファイルで実行すると、z3 自体は正しいモデルを提供します。私の構成は Mac OSX 10.6.8、Python 2.7.4 です。

4

2 に答える 2

3

この問題は私のセットアップに非常に固有のものですが、誰かがそれに遭遇するかもしれません: 根本的な原因は、間違ったバージョンの libgomp が動的ローダーによって取得されたことです。つまり、コンパイルと実行に使用されたバージョンが一致しません。 .

この問題のより深刻な症状を次に示します。

$ python
Python 2.7.4 (default, May  9 2013, 18:51:46)
[GCC 4.2.1 (Apple Inc. build 5664)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> IntVal(1)

>>>

数値は表示されません。つまり、正しい出力は次のとおりです。

>>> IntVal(1)
1
>>>

ライブラリの正しいバージョンを指すように DYLD_LIBRARY_PATH を設定すると、問題が修正されます。

于 2013-05-10T15:55:20.917 に答える
2

Mac OSX 10.8.3 で Z3 4.1 と Python 2.7.2 を使用しても問題はありません。なんらかの理由でキャラクターを食い尽くすのは、ある種の端末の問題なのだろうか。出力をファイルにリダイレクトするとどうなりますか? (つまり、"python bug.py > out" を試してください。ファイル "out" の内容は問題ないように見えますか?)

于 2013-05-09T07:28:32.677 に答える