-
Notifications
You must be signed in to change notification settings - Fork 33
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #234 from uwplse/develop
Release Herbie 1.3
- Loading branch information
Showing
160 changed files
with
7,851 additions
and
7,634 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,19 +1,9 @@ | ||
*~ | ||
graphs | ||
compile/*.o | ||
compile/*.bin | ||
compile/tc*.c | ||
compile/tc*.out | ||
compile/tc.json | ||
compile/nr*.c | ||
compile/nr*.out | ||
compile/nr.json | ||
compile/cost | ||
compiled/ | ||
ml-toy | ||
papers | ||
www/demo | ||
demo.log | ||
*.class | ||
cost | ||
infra/cost | ||
previous | ||
*.swp |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
FROM jackfirth/racket:6.12 | ||
FROM jackfirth/racket:7.3 | ||
MAINTAINER Pavel Panchekha <[email protected]> | ||
RUN apt-get update \ | ||
&& apt-get install -y libcairo2-dev libjpeg62 libpango1.0-dev \ | ||
|
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
(FPCore (x0 x1) | ||
:name "(- (/ x0 (- 1 x1)) x0)" | ||
:pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186))) | ||
:herbie-target (/ (* x0 x1) (- 1 x1)) | ||
(- (/ x0 (- 1 x1)) x0)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
(FPCore (y) | ||
:name "Kahan's Monster" | ||
:pre (<= 1 y 9999) ; Integers only in Kahan's example but this is not essential | ||
(let ([Qx (- (fabs (- y (sqrt (+ (* y y) 1)))) | ||
(/ 1 (+ y (sqrt (+ (* y y) 1)))))]) | ||
(let ([z (* Qx Qx)]) | ||
(if (== z 0) 1 (/ (- (exp z) 1) z))))) | ||
|
||
(FPCore (y) | ||
:name "Kahan's Unum-Targeted Monster" | ||
:pre (<= 1 y 9999) ; Integers only in Kahan's example but this is not essential | ||
(let ([Qx (- (fabs (- y (sqrt (+ (* y y) 1)))) (/ 1 (+ y (sqrt (+ (* y y) 1)))))]) | ||
(let ([z (+ (* Qx Qx) (pow (pow 10 -300) (* 10000 (+ y 1))))]) | ||
(if (== z 0) 1 (/ (- (exp z) 1) z))))) | ||
|
||
(FPCore (x y) | ||
:name "Kahan p9 Example" | ||
:pre (and (< 0 x 1) (< y 1)) | ||
:herbie-target | ||
(if (< 0.5 (fabs (/ x y)) 2) | ||
(/ (* (- x y) (+ x y)) (+ (* x x) (* y y))) | ||
(- 1 (/ 2 (+ 1 (* (/ x y) (/ x y)))))) | ||
|
||
(/ (* (- x y) (+ x y)) (+ (* x x) (* y y)))) | ||
|
||
(FPCore (t) | ||
:name "Kahan p13 Example 1" | ||
(let ([u (/ (* 2 t) (+ 1 t))]) | ||
(/ (+ 1 (* u u)) (+ 2 (* u u))))) | ||
|
||
(FPCore (t) | ||
:name "Kahan p13 Example 2" | ||
(let ([v (- 2 (/ (/ 2 t) (+ 1 (/ 1 t))))]) | ||
(/ (+ 1 (* v v)) (+ 2 (* v v))))) | ||
|
||
(FPCore (t) | ||
:name "Kahan p13 Example 3" | ||
(let ([v (- 2 (/ (/ 2 t) (+ 1 (/ 1 t))))]) | ||
(- 1 (/ 1 (+ 2 (* v v)))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
(FPCore (x y) | ||
:name "Rump's expression from Stadtherr's award speech" | ||
:pre (and (== x 77617) (== y 33096)) | ||
:spec -54767/66192 | ||
(+ (* 333.75 (pow y 6)) | ||
(* (* x x) | ||
(- (* 11 x x y y) | ||
(pow y 6) | ||
(* 121 (pow y 4)) | ||
2)) | ||
(* 5.5 (pow y 8)) | ||
(/ x (* 2 y)))) | ||
|
||
;; From | ||
;; How Reliable are the Results of Computers | ||
;; Jahrbuch Uberblicke Mathematik (1983) | ||
|
||
(FPCore (x y) | ||
:name "From Rump in a 1983 paper" | ||
:pre (and (== x 10864) (== y 18817)) | ||
;:pre (and (< 10500 x 11000) (< 18500 y 19000)) | ||
(+ (- (* 9 (pow x 4)) (pow y 4)) (* 2 (* y y)))) | ||
|
||
(FPCore (x y) | ||
:name "From Rump in a 1983 paper, rewritten" | ||
:pre (and (== x 10864) (== y 18817)) | ||
;:pre (and (< 10500 x 11000) (< 18500 y 19000)) | ||
(- (* 9 (pow x 4)) (* (* y y) (- (* y y) 2)))) |
Oops, something went wrong.