4

z3pyをアプリケーションに統合しようとしています。次のような小さな実数を含むアサーションがあります

solver.add(x <= 1e-6)

次に、次のエラーが発生しました。

File "~/src/solver/z3.py", line 2001, in __le__
  a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
  b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
  return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
  raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'

アサーション中

solver.add(x <= 1e-4)

大丈夫そうです。

したがって、z3にはある種の精度制限があると思います。もしそうなら、最初のアサーションを通過させるオプションはありますか？

ありがとう。

4

1 に答える 1

5

Z3には精度の制限はありません。任意精度の有理数と代数的数を表すことができます。次に例を示します。

print RealVal('1/10000000000000000000000000000')
print simplify((RealVal('1/10') ** RealVal('10')) ** RealVal('10'))

あなたはそれをオンラインで試すことができます：http：//rise4fun.com/Z3Py/ahJQ

この関数RealVal(a)は、Pythonの値をZ3の実際の値に変換します。これを実現するためにZ3CAPIを使用しますZ3_mk_numeral。このコードはz3.py、Z3ディストリビューションに含まれているファイルで入手できます。APIZ3_mk_numeralは、有理数を10進形式（例：「1.3」）または小数形式（例：「1/3」）でエンコードする文字列を想定しています。科学的記数法はサポートされていないことに注意してください。RealVal(a)Pythonユーザーにとって便利なように、このメソッドを使用して、を呼び出す前に文字列にstr(a)変換します。したがって、ユーザーは、、などを書くこともできます。aZ3_mk_numeralRealVal(1)RealVal(1.2)

情報の2番目のビットは、ステートメントsolver.add(x <= 1e-4)が本質的に。の省略形であるということですsolver.add(x <= RealVal(1e-4))。

さて、なぜこの例は機能する1e-4のに、機能しないのかを尋ねることができます1e-6。問題はstrPythonでの実装です。Z3でサポートされている10進表記str(1e-4)の文字列を返しますが、でサポートされていない科学的記数法の文字列を返します。"0.0001"Z3_mk_numeralstr(1e-6)"1e-6"Z3_mk_numeral

print str(1e-4)
print str(1e-6)

上記の例へのリンクは次のとおりです。http：//rise4fun.com/Z3Py/C02q

この問題を回避するには、Z3式を作成するときに科学的記数法の数値を避ける必要があります。Z3_mk_numeral次のバージョンのZ3で、科学的記数法のサポートを追加する時間があるかどうかを確認します。

于 2012-09-07T18:55:05.403 に答える