QF_FPA？ Z3はIEEE-754の算術演算をサポートしていますか？

Question

Z3のソースコードを参照すると、QF_FPAを参照しているファイルがたくさん出てきました。QF_FPAは、量子のない浮動小数点演算のように見えます。しかし、私はその状態に関するドキュメントや、さまざまなフロントエンド（特にSMT-Lib2）でどのように使用できるかを見つけることができないようです。これはIEEE-754 FPのエンコーディングですか？もしそうなら、どの精度/演算がサポートされていますか？すべてのドキュメントが最も役に立ちます。

Answer 1

はい、Z3は最近のSMTワークショップpaperのRuemmerとWahlが提案した浮動小数点演算をサポートしています。現在の段階では、公式のFPA理論はなく、Z3のサポートは非​​常に基本的です（ビットブラスターのみ）。私たちはこれをまだ積極的に宣伝していませんが、Ruemmer/Wahlの論文（QF_FPAとQF_FPABVの設定ロジック）で提案されているように正確に使用できます。現時点では、FPAの新しい決定手続きに取り組んでいますが、それが利用可能になるまでには時間がかかるでしょう。

(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

浮動小数点ロジックは、v4.4.2でQF_FPとQF_FPBV名前が付けられます。

はここFPA SMT2式は次のようになり何の簡単な例です。 RELEASE_NOTESの理論の説明へのリンクは壊れています。正しいページはhttp://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtmlです。上記の提案例は、

(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)