[consolidated] issues in FP

[zhendongsu]

Refutation unsoundness:

[532] % z3release small.smt2
unsat
[533] % z3-4.8.17 small.smt2 
unsat
[534] % cvc5 -q small.smt2
sat
[535] % cat small.smt2
(declare-fun a () Float64)
(declare-fun b () Float64)
(assert (= a (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(assert (= b (fp #b0 #b11111110111 #b1111101100111000010100011011001111010101111001101010)))
(assert (= (fp.fma RTP b a a) a))
(check-sat)

[zhendongsu]

Invalid model:

[526] % z3release model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(
  (define-fun b () Float64
    (fp #b1 #b11110111010 #xc3d3b4877cae8))
  (define-fun c () Float64
    (fp #b1 #b11100001101 #x575a9f8927da0))
  (define-fun d () Float64
    (fp #b1 #b11111111110 #xfffffffffffff))
  (define-fun a () Float64
    (fp #b0 #b11101000110 #x7808bd015c801))
)
[527] % cat small.smt2
(declare-fun a () Float64)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert (= b (fp #b1 #b11110111010 #b1100001111010011101101001000011101111100101011101000)))
(assert (= c (fp #b1 #b11100001101 #b0101011101011010100111111000100100100111110110100000)))
(assert (= d (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(assert (= (fp.fma RTZ a b c) d))
(check-sat)
(get-model)

[zhendongsu]

Another likely related invalid model issue:

[521] % z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
[522] % cat small.smt2
(declare-fun x () Float64)
(declare-fun y () Float64)
(declare-fun z () Float64)
(declare-fun r () Float64)
(assert (distinct x (fp #b0 #b11111001010 #b0111110000010101111110101011010100011000011010010011)))
(assert (distinct z (fp #b0 #b01001110111 #b0010111000000100111110110011001101010101110110011000)))
(assert (= r (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111) (fp.fma RTP x y z) r))
(check-sat)

[zhendongsu]

Refutation unsoundness (very similar to the one from #6117 (comment)):

[548] % z3release small.smt2
unsat
[549] % z3-4.8.17 small.smt2
sat
[550] % cvc5 -q small.smt2
sat
[551] % cat small.smt2
(declare-fun a () Float64)
(declare-fun b () Float64)
(assert (= a (fp #b0 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(assert (= b (fp #b0 #b11111100001 #b0111011111011101010111011000011011101111111110010010)))
(assert (= (fp.fma RTN b b a) a))
(check-sat)

[zhendongsu]

Solution unsoundness:

[518] % z3release model_validate=true small.smt2
sat
[519] % z3-4.8.17 model_validate=true small.smt2
unsat
[520] % cvc5 -q small.smt2
unsat
[521] % cat small.smt2
(assert (distinct (fp (_ bv0 1) #b11111111110 #b1111111111111111111111111111111111111111111111111111)
         (fp.fma RTN (fp (_ bv1 1) #b11101011010 (_ bv0 52))
          (fp (_ bv1 1) #b11101011010 (_ bv0 52))
          (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)))))
(check-sat)

[zhendongsu]

Refutation unsoundness:

[527] % z3release small.smt2
unsat
[528] % z3-4.8.17 small.smt2
sat
[529] % cvc5 -q small.smt2
sat
[530] % cat small.smt2
(declare-fun a () Float64)
(declare-fun b () Float64)
(assert (= b (fp #b0 #b10111101110 #b0000000000101010111000101110000010010100111011011000)))
(assert (= a (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(assert (= (fp.fma RTP b a a) a))
(check-sat)

[zhendongsu]

[539] % z3release model_validate=true small.smt2
sat
sat
sat
sat
[540] % z3release rewriter.bv_sort_ac=true rewriter.bv_extract_prop=true rewriter.bv_le_extra=true rewriter.bv_ite2id=true model_validate=true small.smt2
sat
sat
sat
sat
(error "line 12 column 10: an invalid model was generated")
[541] % cat small.smt2
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(declare-fun r () Float64)
(check-sat)
(assert (= b (fp #b1 #b11111111100 #b1011001010010001100100010101001101011100101111010100)))
(check-sat)
(assert (distinct c (fp #b0 #b00011000100 #b1100010001001000011111001110010110001101101011010001)))
(check-sat)
(assert (= d (fp #b0 #b00111111110 #b0111111111100010000010001100011000011111001001011101)))
(assert (= (fp.fma RTN b c d) r))
(check-sat)

[NikolajBjorner]

See also QF_FP/wintersteiger/fma/fma-has-no-other-solution-10232.smt2

[NikolajBjorner]

It is claimed that returning unsat here is unsound.

[527] % z3release small.smt2
unsat
[528] % z3-4.8.17 small.smt2
sat
[529] % cvc5 -q small.smt2
sat
[530] % cat small.smt2
(declare-fun a () Float64)
(declare-fun b () Float64)
(assert (= b (fp #b0 #b10111101110 #b0000000000101010111000101110000010010100111011011000)))
(assert (= a (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
(assert (= (fp.fma RTP b a a) a))
(check-sat)

Is the verdict on unsoundness based on relative testing or is there a semantics-based argument?
I am asking because I am not sure what hypothesis to work from here.

fma b a a is (b * a) + a
Then b * a overflows with exponent 1518. The maximal exponent should be 1023 from what I am aware of.
b and a have opposite signs so the result is minus infinity.

[zhendongsu]

Is the verdict on unsoundness based on relative testing or is there a semantics-based argument?

Nikolaj, yes, it was based on differential testing. So, I'm unsure either.

To me, your analysis seems correct.

[NikolajBjorner]

@wintersteiger has a tool to evaluate against hardware semantics. It says this is a bug.

[zhendongsu]

Solution unsoundness:

[542] % z3release model_validate=true small.smt2
sat
[543] % z3-4.8.17 model_validate=true small.smt2
unsat
[544] % cvc5 -q small.smt2
unsat
[545] % cat small.smt2
(assert (= (fp (_ bv1 1) (_ bv2047 11) (_ bv0 52)) (fp.fma RTP (fp (_ bv0 1) #b11100001000 (_ bv0 52)) (fp (_ bv1 1) #b11101101011 (_ bv0 52)) (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)))))
(check-sat)

[wintersteiger]

There is a known (to me) bug in fp.fma and these are likely all different instances thereof. I'll try to make some time to fix this soon.