モデルでブール式を評価しても、式に具体的な値が明確に含まれている場合でも、具体的なブール値が返されないことがあります。これを、このテスト ケースのような配列式を含むケースに減らすことができました。
from z3 import *
x = K(IntSort(), 0)
s = Solver()
s.check()
m = s.model()
print m.evaluate(x == Store(x, 0, 1), model_completion=True)
これが印刷されることを期待しますFalseが、代わりに印刷されK(Int, 0) == Store(K(Int, 0), 0, 1)ます。他の例でも同様の結果が得られます。最初の行を に置き換えてx = Array('x', IntSort(), IntSort())も、同じ結果が得られます (ただし、それはデフォルトの解釈次第です)。興味深いことに、最初の行を に置き換えるx = Store(K(IntSort(), 0), 0, 1)と、例が出力されますTrue。
Z3にそのような式を具体的な値に評価させる方法はありますか?