(set-logic QF_FP)
; Model-to-code map: FeatureField.java:450  weight * (1 - pivot / (f + pivot))   (Java float = IEEE binary32, RNE)
;                    IntervalScoreFunction.java:72  weight * (1.0f - pivot / (pivot + freq))  (same expression, + commutes)
(define-sort F () (_ FloatingPoint 8 24))
(define-sort D () (_ FloatingPoint 11 53))
(declare-const f F)   ; decoded feature value S (FeatureField: positive normal finite float)
(declare-const k F)   ; pivot: newSaturationQuery accepts any finite k > 0 (subnormal included)
(declare-const w F)   ; weight / boost in (0, 64]
(define-fun zero () F (_ +zero 8 24))
(define-fun one () F ((_ to_fp 8 24) RNE 1.0))
(assert (fp.isNormal f)) (assert (fp.isPositive f))
(assert (fp.isPositive k)) (assert (not (fp.isZero k))) (assert (not (fp.isInfinite k))) (assert (not (fp.isNaN k)))
(assert (fp.gt w zero)) (assert (fp.leq w ((_ to_fp 8 24) RNE 64.0)))
(define-fun s () F (fp.add RNE f k))
(define-fun q () F (fp.div RNE k s))
(define-fun score () F (fp.mul RNE w (fp.sub RNE one q)))
(define-fun fd () D ((_ to_fp 11 53) RNE f))
(define-fun kd () D ((_ to_fp 11 53) RNE k))

; Q2a: a zero needs S/k <= 2^-24: assert score == 0 and S > k*2^-24 (exact, in binary64): expect unsat.
(assert (fp.eq score zero))
(assert (fp.gt fd (fp.mul RNE kd ((_ to_fp 11 53) RNE 0.000000059604644775390625))))
(check-sat)
(get-model)