2

私はz3pythonでpythonの数学ライブラリを使おうとしていましたが、私がしたことは

import z3
import math
a,b = z3.Reals('a b')
solve(b == math.factorial(a), b == 6)

返されるエラー メッセージは AttributeError: ArithRef インスタンスに属性 ' float ' がありません。

私の目的は実際には Z3 で階乗関数を使用することではなく、数学ライブラリの関数が一般的に Z3 で使用できるかどうかに興味があります。どんな提案でも大歓迎です。

4

1 に答える 1

2

一般的に、いいえ、これは不可能です。その理由は、Python 関数の論理制約への変換がないためです (理論的には、たとえば固定小数点エンジンを介して行うことができます) が、かなりの労力と本質的に (一般的に決定不可能な) モデルのエンコードが必要になります。問題をチェックしています。関連する質問に対するレオの優れた回答も参照してください。

この特定の例では、aはシンボリックであることに注意してください。つまり、任意の実数を表します。math.factorial実装は具体的な実数のみを処理するため、この情報をどうするかわかりません。

一部の特定の機能については、Z3 に正確なエンコードを提供することがもちろん可能です。たとえば、Z3 は累乗をサポートし、Python API は__pow__演算子を提供します。ただし、この演算子は、Python の__pow__実数の on (浮動小数点抽象化) とまったく同じセマンティクスを持たない可能性があり、Python の の実装から派生したものではないことに注意してください__pow__。

于 2014-03-31T12:24:16.853 に答える