QF_FPA? Unterstützt Z3 IEEE-754-Arithmetik?

Beim Durchsuchen des Z3-Quellcodes bin ich auf eine Reihe von Dateien gestoßen, die sich auf QF_FPA beziehen und für quantifiziererfreie Fließkomma-Arithmetik stehen. Ich bin jedoch nicht in der Lage, eine Dokumentation über ihren Zustand zu finden oder wie sie über verschiedene Frontends (insbesondere SMT-Lib2) genutzt werden kann. Ist dies eine Codierung von IEEE-754 FP? Wenn ja, welche Präzisierungen/Operationen werden unterstützt? Jede Dokumentation wäre am hilfreichsten.QF_FPA? Unterstützt Z3 IEEE-754-Arithmetik?

Quelle

2013-03-03 Levent Erkok

Ja, Z3 unterstützt Fließkomma-Arithmetik wie von Ruemmer und Wahl in einer kürzlich erschienenen SMT-Workshop paper vorgeschlagen. Gegenwärtig gibt es keine offizielle FPA-Theorie und die Unterstützung von Z3 ist sehr einfach (nur ein Bit-Blaster). Wir werben nicht aktiv dafür, aber es kann genau so verwendet werden, wie es in dem Papier von Rümmer/Wahl vorgeschlagen wurde (Setzen der Logiken QF_FPA und QF_FPABV). Momentan arbeiten wir an einem neuen Entscheidungsverfahren für FPA, aber es wird noch einige Zeit dauern, bis es verfügbar ist.

Hier ist ein kurzes Beispiel, was eine FPA SMT2 Formel aussehen könnte:

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

Quelle

2013-03-04 11:11:45

Wurde diese Unterstützung für Fließkomma-Arithmetik in die neueste stabile Version 4.3.2 von z3 integriert? Wurde die Gleitkomma-Theorie-Unterstützung auch mit anderen Theorien kombiniert, z. B. mit linearer Ganzzahl-Arithmetik, entweder in stabiler oder instabiler Version? – user1779685

4.3.2 hatte nur teilweise Unterstützung, die aktuelle Version ist 4.4.0, die volle Unterstützung hat, einschließlich der Theorie Kombination. Beachten Sie, dass die Konvertierung von der Fließkommazahl in die reelle/rationale Zahl nichtlineare Bedingungen einführt, so dass die Kombination mit linearer Arithmetik ebenfalls nichtlinear wird. –

Danke für das Wissen über die Kombination von Konversion und Theorie. Ich habe auf Github gecheckt: Die April-End-Z3-Veröffentlichung mit breiterer Unterstützung ist eine gute Nachricht. Werde es bald versuchen. – user1779685

Die Gleitkomma-Logiken sind QF_FP und QF_FPBV in 4.4.2 genannt. Der Link zur Beschreibung der Theorie in RELEASE_NOTES ist unterbrochen. Die richtige Seite ist http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml. Das vorgeschlagene Beispiel sollte

sein

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

Quelle

2015-10-30 15:46:57

Danke Daniel für die Aktualisierung des Beispiels! Der SMT FP-Standard wurde seither aktualisiert und dies ist in der Tat die neue Syntax. Wir haben alle alten Symbole von Z3 entfernt und unterstützen nur den endgültigen Standard. –

QF_FPA? Unterstützt Z3 IEEE-754-Arithmetik?

Antwort

Verwandte Themen