Skip to content

Commit b131a8e

Browse files
authored
Merge pull request #143 from herbie-fp/fix-copysign
Fix bug with copysign movability flags
2 parents c7884d1 + 3560e43 commit b131a8e

File tree

3 files changed

+55
-11
lines changed

3 files changed

+55
-11
lines changed

ops/core.rkt

Lines changed: 45 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@
105105
ival-==
106106
ival-!=
107107
ival-if
108+
ival-mobilize
108109
ival-and
109110
ival-or
110111
ival-not
@@ -661,27 +662,62 @@
661662
(ival (endpoint lo #f) (endpoint hi #f) err? err))
662663

663664
(define (ival-fmin x y)
664-
(ival (endpoint-min2 (ival-lo x) (ival-lo y) 'down)
665-
(endpoint-min2 (ival-hi x) (ival-hi y) 'up)
666-
(or (ival-err? x) (ival-err? y))
667-
(or (ival-err x) (ival-err y))))
665+
(match-define (ival (endpoint xlo xlo!) (endpoint xhi xhi!) xerr? xerr) x)
666+
(match-define (ival (endpoint ylo ylo!) (endpoint yhi yhi!) yerr? yerr) y)
667+
(define lo (bf 0))
668+
(define hi (bf 0))
669+
(define lo-exact? (= 0 (mpfr-min! lo xlo ylo 'down)))
670+
(define hi-exact? (= 0 (mpfr-min! hi xhi yhi 'up)))
671+
;; For lower endpoints (which can only move upward under refinement),
672+
;; a fixed minimum is stable if one fixed endpoint is <= the other.
673+
(define lo-stable?
674+
(cond
675+
[(and xlo! ylo!) #t]
676+
[xlo! (bflte? xlo ylo)]
677+
[ylo! (bflte? ylo xlo)]
678+
[else #f]))
679+
(define lo! (and lo-exact? lo-stable?))
680+
;; For upper endpoints (which can only move downward), a fixed minimum is
681+
;; only guaranteed when both endpoints are fixed.
682+
(define hi! (and hi-exact? xhi! yhi!))
683+
(ival (endpoint lo lo!) (endpoint hi hi!) (or xerr? yerr?) (or xerr yerr)))
668684

669685
(define (ival-fmax x y)
670-
(ival (endpoint-max2 (ival-lo x) (ival-lo y) 'down)
671-
(endpoint-max2 (ival-hi x) (ival-hi y) 'up)
672-
(or (ival-err? x) (ival-err? y))
673-
(or (ival-err x) (ival-err y))))
686+
(match-define (ival (endpoint xlo xlo!) (endpoint xhi xhi!) xerr? xerr) x)
687+
(match-define (ival (endpoint ylo ylo!) (endpoint yhi yhi!) yerr? yerr) y)
688+
(define lo (bf 0))
689+
(define hi (bf 0))
690+
(define lo-exact? (= 0 (mpfr-max! lo xlo ylo 'down)))
691+
(define hi-exact? (= 0 (mpfr-max! hi xhi yhi 'up)))
692+
;; For lower endpoints (which can only move upward), a fixed maximum is
693+
;; only guaranteed when both endpoints are fixed.
694+
(define lo! (and lo-exact? xlo! ylo!))
695+
;; For upper endpoints (which can only move downward), a fixed maximum is
696+
;; stable if one fixed endpoint is >= the other.
697+
(define hi-stable?
698+
(cond
699+
[(and xhi! yhi!) #t]
700+
[xhi! (bfgte? xhi yhi)]
701+
[yhi! (bfgte? yhi xhi)]
702+
[else #f]))
703+
(define hi! (and hi-exact? hi-stable?))
704+
(ival (endpoint lo lo!) (endpoint hi hi!) (or xerr? yerr?) (or xerr yerr)))
674705

675706
(define (ival-copysign x y)
676707
(match-define (ival xlo xhi xerr? xerr) (ival-fabs x))
677708
(define can-zero (or (bfzero? (ival-lo-val y)) (bfzero? (ival-hi-val y))))
678709
;; 0 is both positive and negative because we don't handle signed zero well
679710
(define can-neg (or (= (mpfr-sign (ival-lo-val y)) -1) can-zero))
680711
(define can-pos (or (= (mpfr-sign (ival-hi-val y)) 1) can-zero))
712+
(define sign-immovable? (and can-neg can-pos (ival-lo-fixed? y) (ival-hi-fixed? y)))
681713
(define err? (or (ival-err? y) xerr?))
682714
(define err (or (ival-err y) xerr))
683715
(match* (can-neg can-pos)
684-
[(#t #t) (ival (rnd 'down epunary bfneg xhi) (rnd 'up epunary bfcopy xhi) err? err)]
716+
[(#t #t)
717+
(define out (ival (rnd 'down epunary bfneg xhi) (rnd 'up epunary bfcopy xhi) err? err))
718+
(if sign-immovable?
719+
out
720+
(ival-mobilize out))]
685721
[(#t #f) (ival (rnd 'down epunary bfneg xhi) (rnd 'up epunary bfneg xlo) err? err)]
686722
[(#f #t) (ival xlo xhi err? err)]
687723
[(#f #f)

ops/pow.rkt

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,4 +161,9 @@
161161
[(or (= (mpfr-sign (ival-lo-val x)) 1) (bfzero? (ival-lo-val x))) (ival-pow-pos x y)]
162162
[else
163163
(define-values (neg pos) (split-ival x 0.bf))
164-
(ival-union (ival-pow-neg neg y) (ival-pow-pos pos y))]))
164+
(define out (ival-union (ival-pow-neg neg y) (ival-pow-pos pos y)))
165+
;; If x straddles 0 with movable endpoints, a refinement can drop one
166+
;; branch entirely, so branch-derived endpoint fixedness is not stable.
167+
(if (and (ival-lo-fixed? x) (ival-hi-fixed? x))
168+
out
169+
(ival-mobilize out))]))

test.rkt

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,10 @@
315315
(with-check-info (['split-argument k] ['ilo ilo] ['ihi ihi] ['iylo iylo] ['iyhi iyhi])
316316
(check-ival-equals? iy
317317
(parameterize ([bf-precision out-prec])
318-
(ival-union iylo iyhi))))))
318+
(ival-union iylo iyhi)))
319+
;; Refining an input argument should refine the output.
320+
(check ival-refines? iy iylo)
321+
(check ival-refines? iy iyhi))))
319322
(when (or (ival-lo-fixed? iy) (ival-hi-fixed? iy))
320323
(define iy*
321324
(parameterize ([bf-precision 128])

0 commit comments

Comments
 (0)