Skip to content

Commit

Permalink
lower bound formula updates
Browse files Browse the repository at this point in the history
  • Loading branch information
@AYadrov
AYadrov committed Oct 22, 2024
1 parent 373dcb5 commit 2db247e
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 62 deletions.
2 changes: 1 addition & 1 deletion eval/adjust.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@
(for ([x (in-list tail-registers)]
[bound (in-list ampl-bounds)]
#:when (>= x varc)) ; when tail register is not a variable
(match-define (list up-bound lo-bound) bound)
(match-define (cons up-bound lo-bound) bound)

; Upper precision bound propogation
(vector-set! vprecs-max
Expand Down
127 changes: 66 additions & 61 deletions eval/tricks.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@
[4 4096]
[5 8192]))

(define (prev-iter)
(- (*sampling-iteration*) 1))

(define (crosses-zero? x)
(not (equal? (mpfr-sign (ival-lo x)) (mpfr-sign (ival-hi x)))))

Expand Down Expand Up @@ -93,32 +96,32 @@
; k = 2: logspan(x)
(define x (first srcs))
(define y (second srcs))
(list (list (logspan y) 0) ; bounds per x
(list (logspan x) 0))] ; bounds per y
(list (cons (logspan y) 0) ; bounds per x
(cons (logspan x) 0))] ; bounds per y

[(ival-div)
; k = 1: logspan(y)
; k = 2: logspan(x) + 2 * logspan(y)
(define x (first srcs))
(define y (second srcs))
(list (list (logspan y) 0) ; bounds per x
(list (+ (logspan x) (* 2 (logspan y))) 0))] ; bounds per y
(list (cons (logspan y) 0) ; bounds per x
(cons (+ (logspan x) (* 2 (logspan y))) 0))] ; bounds per y

[(ival-sqrt ival-cbrt)
; sqrt: logspan(x)/2 - 1
; cbrt: logspan(x)*2/3 - 1
(define x (first srcs))
(list (list (quotient (logspan x) 2) 0))]
(list (cons (quotient (logspan x) 2) 0))]

[(ival-add ival-sub)
; k = 1: maxlog(x) - minlog(z)
; k = 2: maxlog(y) - minlog(z)
(define x (first srcs))
(define y (second srcs))

(list (list (- (maxlog x) (minlog z))
(list (cons (- (maxlog x) (minlog z))
(- (minlog x #:no-slack #t) (maxlog z #:no-slack #t))) ; bounds per x
(list (- (maxlog y) (minlog z))
(cons (- (maxlog y) (minlog z))
(- (minlog y #:no-slack #t) (maxlog z #:no-slack #t))))] ; bounds per y

[(ival-pow)
Expand All @@ -140,79 +143,83 @@
(get-slack)
0))

(list (list (max (+ (maxlog y) (logspan x) (logspan z) x-slack) x-slack)
(list (cons (max (+ (maxlog y) (logspan x) (logspan z) x-slack) x-slack)
(minlog y #:no-slack #t)) ; bounds per x
(list (max (+ (maxlog y) (max (abs (maxlog x)) (abs (minlog x))) (logspan z) y-slack)
(cons (max (+ (maxlog y) (max (abs (maxlog x)) (abs (minlog x))) (logspan z) y-slack)
y-slack)
(minlog y #:no-slack #t)))] ; bounds per y

[(ival-exp ival-exp2)
; maxlog(x) + logspan(z)
(define x (car srcs))
(list (list (+ (maxlog x) (logspan z)) (minlog x #:no-slack #t)))]
(list (cons (+ (maxlog x) (logspan z)) (minlog x #:no-slack #t)))]

[(ival-tan)
; maxlog(x) + max(|minlog(z)|,|maxlog(z)|) + logspan(z) + 1
(define x (first srcs))
(list (list (+ (maxlog x) (max (abs (maxlog z)) (abs (minlog z))) (logspan z) 1)
(list (cons (+ (maxlog x) (max (abs (maxlog z)) (abs (minlog z))) (logspan z) 1)
(+ (minlog x #:no-slack #t)
(min (abs (maxlog z #:no-slack #t)) (abs (minlog z #:no-slack #t))))))]

[(ival-sin)
; maxlog(x) - minlog(z)
(define x (first srcs))
(list (list (- (maxlog x) (minlog z)) (- (maxlog z #:no-slack #t))))]
(list (cons (- (maxlog x) (minlog z)) (- (maxlog z #:no-slack #t))))]

[(ival-cos)
; maxlog(x) - minlog(z) + min(maxlog(x), 0)
(define x (first srcs))
(list (list (+ (- (maxlog x) (minlog z)) (min (maxlog x) 0)) (- (maxlog z #:no-slack #t))))]
(list (cons (+ (- (maxlog x) (minlog z)) (min (maxlog x) 0)) (- (maxlog z #:no-slack #t))))]

[(ival-sinh)
; maxlog(x) + logspan(z) - min(minlog(x), 0)
(define x (first srcs))
(list (list (- (+ (maxlog x) (logspan z)) (min (minlog x) 0)) (max 0 (minlog x #:no-slack #t))))]
(list (cons (- (+ (maxlog x) (logspan z)) (min (minlog x) 0)) (max 0 (minlog x #:no-slack #t))))]

[(ival-cosh)
; maxlog(x) + logspan(z) + min(maxlog(x), 0)
(define x (first srcs))
(list (list (+ (maxlog x) (logspan z) (min (maxlog x) 0)) (max 0 (minlog x #:no-slack #t))))]
(list (cons (+ (maxlog x) (logspan z) (min (maxlog x) 0)) (max 0 (minlog x #:no-slack #t))))]

[(ival-log ival-log2 ival-log10)
; log: logspan(x) - minlog(z)
; log2: logspan(x) - minlog(z) + 1
; log10: logspan(x) - minlog(z) - 1
(define x (first srcs))
(list (list (+ (- (logspan x) (minlog z)) 1) (- (maxlog z #:no-slack #t))))]
(list (cons (+ (- (logspan x) (minlog z)) 1) (- (maxlog z #:no-slack #t))))]

[(ival-asin)
; maxlog(x) - log[1-x^2]/2 - minlog(z)
; ^^^^^^^^^^^^
; condition of uncertainty
(define x (first srcs))
(define slack
(if (>= (maxlog z) 1) ; Condition of uncertainty
(get-slack) ; assumes that log[1-x^2]/2 is equal to slack
1))
; Γ[asin] = | x / (sqrt(1-x^2) * arcsin(x))|
; ampl[asin] = maxlog(x) - log[1-x^2]/2 - minlog(z)
; ^^^^^^^^^^^^
; unknown part

(list (list slack 0))]
(define x (first srcs))
(if (>= (maxlog z) 1)
(list (cons (get-slack)
(get-slack (prev-iter)))) ; assumes that log[1-x^2]/2 is equal to slack
(list (cons 1 0)))]

[(ival-acos)
; maxlog(x) - log[1-x^2]/2 - minlog(z)
; ^^^^^^^^^^^^
; condition of uncertainty
(define x (first srcs))
(define slack
(if (>= (maxlog x) 0) ; Condition of uncertainty
(get-slack) ; assumes that log[1-x^2]/2 is equal to slack
0))
; Γ[acos] = |- x / (sqrt(1-x^2) * arccos(x))|
; ampl[acos] = maxlog(x) - log[1-x^2]/2 - minlog(z)
; ^^^^^^^^^^^^
; unknown part

(list (list slack 0))]
(define x (first srcs))
(if (>= (maxlog x) 0)
(list (cons (get-slack)
(get-slack (prev-iter)))) ; assumes that log[1-x^2]/2 is equal to slack
(list (cons 0 0)))]

[(ival-atan)
; logspan(x) - min(|minlog(x)|, |maxlog(x)|) - minlog(z)
; Γ[atan] = | x / ((1+x^2) * arctan(x))|
; ampl[atan] = logspan(x) - min(|minlog(x)|, |maxlog(x)|) - minlog(z)
(define x (first srcs))
(list (list (- (logspan x) (min (abs (minlog x)) (abs (maxlog x))) (minlog z)) 0))]
(list (cons (- (logspan x) (min (abs (minlog x)) (abs (maxlog x))) (minlog z))
(- (- (max (abs (minlog x #:no-slack #t)) (abs (maxlog x #:no-slack #t))))
(maxlog z #:no-slack #t)
2)))]

[(ival-fmod ival-remainder)
; x mod y = x - y*q, where q is rnd_down(x/y)
Expand All @@ -228,8 +235,8 @@
(get-slack) ; y crosses zero
0))

(list (list (- (maxlog x) (minlog z)) 0) ; bounds per x
(list (max (+ (- (maxlog x) (minlog z)) slack) slack) 0))] ; bounds per y
(list (cons (- (maxlog x) (minlog z)) 0) ; bounds per x
(cons (max (+ (- (maxlog x) (minlog z)) slack) slack) 0))] ; bounds per y

; Currently log1p has a very poor approximation
[(ival-log1p)
Expand All @@ -240,60 +247,58 @@
(define xhi (ival-hi x))
(define xlo (ival-lo x))

(define slack
(if (or (equal? (mpfr-sign xlo) -1) (equal? (mpfr-sign xhi) -1))
(get-slack) ; if x in negative
0))

(list (list (max (+ (- (maxlog x) (minlog z)) slack) slack) 0))]
(list (if (or (equal? (mpfr-sign xlo) -1) (equal? (mpfr-sign xhi) -1))
(cons (max (+ (- (maxlog x) (minlog z)) (get-slack)) (get-slack)) 0) ; if x in negative
(cons (- (maxlog x) (minlog z)) 0)))]

; Currently expm1 has a very poor solution for negative values
[(ival-expm1)
; log[Гexpm1] = log[x * e^x / expm1] <= max(1 + maxlog(x), 1 + maxlog(x) - minlog(z))
(define x (first srcs))
(list (list (max (+ 1 (maxlog x)) (+ 1 (- (maxlog x) (minlog z)))) 0))]
(list (cons (max (+ 1 (maxlog x)) (+ 1 (- (maxlog x) (minlog z)))) 0))]

[(ival-atan2)
; maxlog(x) + maxlog(y) - 2*max(minlog(x), minlog(y)) - minlog(z)
(define x (first srcs))
(define y (second srcs))

(make-list 2
(list (- (+ (maxlog x) (maxlog y)) (* 2 (max (minlog x) (minlog y))) (minlog z)) 0))]
(cons (- (+ (maxlog x) (maxlog y)) (* 2 (max (minlog x) (minlog y))) (minlog z))
(- (+ (minlog x #:no-slack #t) (minlog y #:no-slack #t))
(* 2 (min (maxlog x #:no-slack #t) (maxlog y #:no-slack #t)))
(maxlog z #:no-slack #t))))]

[(ival-tanh)
; logspan(z) + logspan(x)
(define x (first srcs))
(list (list (+ (logspan z) (logspan x)) 0))]
(list (cons (+ (logspan z) (logspan x)) 0))]

[(ival-atanh)
; log[Гarctanh] = maxlog(x) - log[(1-x^2)] - minlog(z) = 1 if x < 0.5, otherwise slack
; ^^^^^^^
; a possible uncertainty
(define x (first srcs))
(list (list (if (>= (maxlog x) 1)
(get-slack)
1)
0))]
(list (if (>= (maxlog x) 1)
(cons (get-slack) (get-slack (prev-iter)))
(cons 1 0)))]

[(ival-acosh)
; log[Гacosh] = log[x / (sqrt(x-1) * sqrt(x+1) * acosh)] <= -minlog(z) + slack
(define z-exp (minlog z))
(define slack
(if (< z-exp 2) ; when acosh(x) < 1
(get-slack)
0))

(list (list (max (- slack z-exp) slack) 0))]
(list (if (< z-exp 2) ; when acosh(x) < 1
(cons (max (- (get-slack) z-exp) (get-slack)) 0)
(cons 0 0)))]

[(ival-pow2)
; same as multiplication
(define x (first srcs))
(list (list (+ (logspan x) 1) 0))]
(list (cons (+ (logspan x) 1) 0))]

; TODO
[(ival-erfc ival-erf ival-lgamma ival-tgamma ival-asinh ival-logb) (list (list (get-slack) 0))]
[(ival-erfc ival-erf ival-lgamma ival-tgamma ival-asinh ival-logb)
(list (cons (get-slack) (get-slack (prev-iter))))]
; TODO
[(ival-ceil ival-floor ival-rint ival-round ival-trunc) (list (list (get-slack) 0))]
[(ival-ceil ival-floor ival-rint ival-round ival-trunc)
(list (cons (get-slack) (get-slack (prev-iter))))]

[else (map (λ (_) (list 0 0)) srcs)])) ; exponents for arguments
[else (map (λ (_) (cons 0 0)) srcs)])) ; exponents for arguments

0 comments on commit 2db247e

Please sign in to comment.