1+ ; -*- mode: scheme -*-
2+
3+ ; Herbie cannot properly sample points for this FPCore
4+ ;
5+ ; (FPCore (a b c)
6+ ; :pre (and (< 0 a) (< 0 b) (< 0 c))
7+ ; :name "Area of a triangle"
8+ ; :precision posit16
9+ ; :herbie-expected 16
10+ ; (let ([s (/ (+ (+ a b) c) 2)])
11+ ; (sqrt (* s (- s a) (- s b) (- s c)))))
12+
13+ (FPCore (a b c)
14+ :name " quadp (p42, positive)"
15+ :precision posit16
16+ :herbie-expected 16
17+ (let ([d (sqrt (- (* b b) (* 4 (* a c))))])
18+ (/ (+ (- b) d) (* 2 a))))
19+
20+ (FPCore (a b c)
21+ :name " quadm (p42, negative)"
22+ :precision posit16
23+ :herbie-expected 16
24+ (let ([d (sqrt (- (* b b) (* 4 (* a c))))])
25+ (/ (- (- b) d) (* 2 a))))
26+
27+ (FPCore (a b_2 c)
28+ :name " quad2m (problem 3.2.1, negative)"
29+ :precision posit16
30+ :herbie-expected 16
31+ (let ([d (sqrt (- (* b_2 b_2) (* a c)))])
32+ (/ (- (- b_2) d) a)))
33+
34+ (FPCore (a b_2 c)
35+ :name " quad2p (problem 3.2.1, positive)"
36+ :precision posit16
37+ :herbie-expected 16
38+ (let ([d (sqrt (- (* b_2 b_2) (* a c)))])
39+ (/ (+ (- b_2) d) a)))
40+
41+ (FPCore (x)
42+ :name " 2sqrt (example 3.1)"
43+ :precision posit16
44+ :herbie-expected 16
45+ (- (sqrt (+ x 1 )) (sqrt x)))
46+
47+ (FPCore (x)
48+ :name " 2isqrt (example 3.6)"
49+ :precision posit16
50+ :herbie-expected 16
51+ (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1 )))))
52+
53+ (FPCore (x)
54+ :name " 2frac (problem 3.3.1)"
55+ :precision posit16
56+ :herbie-expected 16
57+ (- (/ 1 (+ x 1 )) (/ 1 x)))
58+
59+ (FPCore (x)
60+ :name " 3frac (problem 3.3.3)"
61+ :precision posit16
62+ :herbie-expected 16
63+ (+ (- (/ 1 (+ x 1 )) (/ 2 x)) (/ 1 (- x 1 ))))
64+
65+ (FPCore (re im)
66+ :name " math.abs on complex"
67+ :precision posit16
68+ :herbie-expected 16
69+ (sqrt (+ (* re re) (* im im))))
70+
71+ (FPCore (x.re x.im)
72+ :name " math.cube on complex, real part"
73+ :precision posit16
74+ :herbie-expected 16
75+ (-
76+ (* (- (* x.re x.re) (* x.im x.im)) x.re)
77+ (* (+ (* x.re x.im) (* x.im x.re)) x.im)))
78+
79+ (FPCore (x.re x.im)
80+ :name " math.cube on complex, imaginary part"
81+ :precision posit16
82+ :herbie-expected 16
83+ (+
84+ (* (- (* x.re x.re) (* x.im x.im)) x.im)
85+ (* (+ (* x.re x.im) (* x.im x.re)) x.re)))
86+
87+ (FPCore (x.re x.im y.re y.im)
88+ :name " _divideComplex, real part"
89+ :precision posit16
90+ :herbie-expected 16
91+ (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))))
92+
93+ (FPCore (x.re x.im y.re y.im)
94+ :name " _divideComplex, imaginary part"
95+ :precision posit16
96+ :herbie-expected 16
97+ (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))
98+
99+ (FPCore (x.re x.im y.re y.im)
100+ :name " _multiplyComplex, real part"
101+ :precision posit16
102+ :herbie-expected 16
103+ (- (* x.re y.re) (* x.im y.im)))
104+
105+ (FPCore (x.re x.im y.re y.im)
106+ :name " _multiplyComplex, imaginary part"
107+ :precision posit16
108+ :herbie-expected 16
109+ (+ (* x.re y.im) (* x.im y.re)))
110+
111+ (FPCore (re im)
112+ :name " math.sqrt on complex, real part"
113+ :precision posit16
114+ :herbie-expected 16
115+ (* 0.5 (sqrt (* 2.0 (+ (sqrt (+ (* re re) (* im im))) re)))))
116+
117+ (FPCore (re im)
118+ :name " math.sqrt on complex, imaginary part, im greater than 0 branch"
119+ :precision posit16
120+ :herbie-expected 16
121+ (* 0.5 (sqrt (* 2.0 (- (sqrt (+ (* re re) (* im im))) re)))))
122+
123+ (FPCore (re im)
124+ :name " math.square on complex, real part"
125+ :precision posit16
126+ :herbie-expected 16
127+ (- (* re re) (* im im)))
128+
129+ (FPCore (re im)
130+ :name " math.square on complex, imaginary part"
131+ :precision posit16
132+ :herbie-expected 16
133+ (+ (* re im) (* im re)))
134+
135+ (FPCore (alpha beta)
136+ :pre (and (> alpha -1) (> beta -1))
137+ :name " Octave 3.8, jcobi/1"
138+ :precision posit16
139+ :herbie-expected 16
140+ (let ((ab (+ alpha beta)) (ad (- beta alpha)) (ap (* beta alpha)))
141+ (/ (+ (/ ad (+ ab 2.0 )) 1.0 ) 2.0 )))
142+
143+ (FPCore (alpha beta i)
144+ :pre (and (> alpha -1) (> beta -1) (> i 0 ))
145+ :name " Octave 3.8, jcobi/2"
146+ :precision posit16
147+ :herbie-expected 16
148+ (let ((ab (+ alpha beta)) (ad (- beta alpha)) (ap (* beta alpha)))
149+ (let ((z (+ ab (* 2 i))))
150+ (/ (+ (/ (* ab ad) z (+ z 2.0 )) 1.0 ) 2.0 ))))
151+
152+ (FPCore (alpha beta)
153+ :pre (and (> alpha -1) (> beta -1))
154+ :name " Octave 3.8, jcobi/3"
155+ :precision posit16
156+ :herbie-expected 16
157+ (let ((i 1 ) (ab (+ alpha beta)) (ad (- beta alpha)) (ap (* beta alpha)))
158+ (let ((z1 i))
159+ (let ((z (+ ab (* 2 z1))))
160+ (/ (+ ab ap 1.0 ) z z (+ z 1.0 ))))))
161+
162+ (FPCore (alpha beta i) ; TODO: i should be an integer
163+ :pre (and (> alpha -1) (> beta -1) (> i 1 ))
164+ :name " Octave 3.8, jcobi/4"
165+ :precision posit16
166+ :herbie-expected 16
167+ (let ((ab (+ alpha beta)) (ad (- beta alpha)) (ap (* beta alpha)))
168+ (let ((z (+ ab (* 2 i))))
169+ (let ((z* (* z z)) (y (* i (+ ab i))))
170+ (let ((y* (* y (+ ap y))))
171+ (/ y* z* (- z* 1.0 )))))))
172+
173+ (FPCore (i)
174+ :pre (and (> i 0 ))
175+ :name " Octave 3.8, jcobi/4, as called"
176+ :precision posit16
177+ :herbie-expected 16
178+ (let ((z (* 2 i)))
179+ (let ((z* (* z z)) (y (* i i)))
180+ (let ((y* (* y y))) (/ y* z* (- z* 1.0 ))))))
181+
182+ (FPCore (a rand)
183+ :name " Octave 3.8, oct_fill_randg"
184+ :precision posit16
185+ :herbie-expected 16
186+ (let ((d (- a (/ 1.0 3.0 ))))
187+ (let ((c (/ 1 (sqrt (* 9 d)))) (x rand))
188+ (let ((v (+ 1 (* c x))))
189+ (let ((v* (* v (* v v))) (xsq (* x x)))
190+ (* d v))))))
191+
192+ (FPCore (d1 d2 d3)
193+ :name " FastMath dist"
194+ :precision posit16
195+ :herbie-expected 16
196+ (+ (* d1 d2) (* d1 d3)))
197+
198+ (FPCore (d)
199+ :name " FastMath test1"
200+ :precision posit16
201+ :herbie-expected 16
202+ (+ (* d 10 ) (* d 20 )))
203+
204+ (FPCore (d1 d2)
205+ :name " FastMath test2"
206+ :precision posit16
207+ :herbie-expected 16
208+ (+ (* d1 10 ) (* d1 d2) (* d1 20 )))
209+
210+ (FPCore (d1 d2 d3)
211+ :name " FastMath dist3"
212+ :precision posit16
213+ :herbie-expected 16
214+ (+ (* d1 d2) (* (+ d3 5 ) d1) (* d1 32 )))
215+
216+ (FPCore (d1 d2 d3 d4)
217+ :name " FastMath dist4"
218+ :precision posit16
219+ :herbie-expected 16
220+ (- (+ (- (* d1 d2) (* d1 d3)) (* d4 d1)) (* d1 d1)))
221+
222+ (FPCore (d1 d2 d3)
223+ :name " FastMath test3"
224+ :precision posit16
225+ :herbie-expected 16
226+ (+ (* d1 3 ) (* d1 d2) (* d1 d3)))
227+
228+ (FPCore (d1)
229+ :name " FastMath repmul"
230+ :precision posit16
231+ :herbie-expected 16
232+ (* d1 d1 d1 d1))
233+
234+ (FPCore (x)
235+ :name " Jmat.Real.dawson"
236+ :precision posit16
237+ :herbie-expected 16
238+ (let ((p1 0.1049934947 ) (p2 0.0424060604 ) (p3 0.0072644182 )
239+ (p4 0.0005064034 ) (p5 0.0001789971 ) (q1 0.7715471019 )
240+ (q2 0.2909738639 ) (q3 0.0694555761 ) (q4 0.0140005442 )
241+ (q5 0.0008327945 ))
242+ (let ((x2 (* x x)))
243+ (let ((x4 (* x2 x2)))
244+ (let ((x6 (* x4 x2)))
245+ (let ((x8 (* x6 x2)))
246+ (let ((x10 (* x8 x2)))
247+ (let ((x12 (* x10 x2)))
248+ (*
249+ (/ (+ 1 (* p1 x2) (* p2 x4) (* p3 x6) (* p4 x8) (* p5 x10))
250+ (+ 1 (* q1 x2) (* q2 x4) (* q3 x6) (* q4 x8) (* q5 x10) (* 2 p5 x12)))
251+ x)))))))))
0 commit comments