z3 - QF_FPA? Z3 は IEEE-754 演算をサポートしていますか?

Question

Z3 のソース コードをブラウズしていると、QF_FPA を参照する一連のファイルに出くわしました。ただし、その状態に関するドキュメントや、さまざまなフロントエンド (特に SMT-Lib2) を介してどのように使用できるかについてのドキュメントを見つけることができないようです。これは IEEE-754 FP のエンコーディングですか? サポートされている場合、どの精度/操作がサポートされていますか? どんなドキュメントも最も役に立ちます..

Answer 1

はい。Z3 は、Ruemmer と Wahl が最近の SMT-workshop paperで提案したように、浮動小数点演算をサポートしています。現段階では、公式の FPA 理論はなく、Z3 のサポートは非​​常に基本的なもの (ビットブラスターのみ) です。これについてはまだ積極的に宣伝していませんが、Ruemmer/Wahl の論文で提案されているとおりに使用できます (ロジック QF_FPA および QF_FPABV を設定します)。現在、FPA の新しい決定手順に取り組んでいますが、それが利用できるようになるまでにはしばらく時間がかかります。

以下は、FPA SMT2 式がどのように見えるかの簡単な例です。

(set-logic QF_FPA)    

(declare-const x (_ FP 11 53))
(declare-const y (_ FP 11 53))
(declare-const r (_ FP 11 53))

(assert (and 
    (= x ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= y ((_ asFloat 11 53) roundTowardZero 0.5 0))
    (= r (+ roundTowardZero x y))
))

(check-sat)

Answer 2

The floating point logics are named QF_FP and QF_FPBV in v4.4.2. The link to the description of the theory in RELEASE_NOTES is broken. The correct page is http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml. The proposed example above should be

(set-logic QF_FP)

(declare-const x (_ FloatingPoint 11 53))
(declare-const y (_ FloatingPoint 11 53))
(declare-const r (_ FloatingPoint 11 53))

(assert (and 
    (= x (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
    (= y (fp #b0 #b00000000010 #b0000000000000000000000000000000000000000000000000010))
    (= r (fp.add roundTowardZero x y))
))

(check-sat)