Merge pull request #1333 from herbie-fp/QuantumWithConstants

New benchmark of Quantum approximation

Author: pavpanchekha

bench/demo.fpcore

@@ -73,3 +73,152 @@
   :precision binary64
   :pre (and (<= 0.0 x 1) (<= 1/3 a 3.0))
   (- 1.0 (pow (- 1.0 x) a)))
+
+(FPCore (x)
+ :name "Quantum aproximation with lots of constants"
+ :precision binary64
+ (let* (
+        (E (exp 1))
+        (sqrtE (sqrt E))
+        (invSqrtE (/ 1 sqrtE))
+        (logTerm (log (- 1 invSqrtE)))
+        (log2Term (* logTerm logTerm))
+        (log3Term (* log2Term logTerm))
+        (E3/2 (pow E 1.5))
+        (E5/2 (pow E 2.5))
+        (E7/2 (pow E 3.5))
+        (dx (- x 1/2))
+
+        ;; Common denominator
+        (D (+ (* sqrtE log2Term)
+              (* 16 sqrtE logTerm)
+              (* -64 sqrtE)
+              (* -8 (pow E 2) log2Term)
+              (* -4 (pow E 2) logTerm)
+              (* -8 E log2Term)
+              (* -84 E logTerm)
+              (* 16 E)
+              (* 2 E3/2 log2Term)
+              (* 16 E3/2 logTerm)
+              (* -4 E3/2)
+              (* E5/2 log2Term)
+              -24))
+
+        ;; Numerators
+        (n1 (+ (* sqrtE log3Term)
+               (* 20 sqrtE log2Term)
+               (* 210 sqrtE logTerm)
+               (* -1200 sqrtE)
+               (* -18 (pow E 3) log3Term)
+               (* -20 (pow E 3) log2Term)
+               (* -116 (pow E 2) log3Term)
+               (* -720 (pow E 2) log2Term)
+               (* 120 (pow E 2) logTerm)
+               (* -18 E log3Term)
+               (* -220 E log2Term)
+               (* -1280 E logTerm)
+               (* -300 E)
+               (* 3 E3/2 log3Term)
+               (* -20 E3/2 log2Term)
+               (* -930 E3/2 logTerm)
+               (* 3 E5/2 log3Term)
+               (* 120 E5/2 log2Term)
+               (* -20 E5/2 logTerm)
+               (* E7/2 log3Term)
+               -120))
+
+        (n2 (+ (* sqrtE log3Term)
+               (* 18 sqrtE log2Term)
+               (* -108 sqrtE logTerm)
+               (* -192 sqrtE)
+               (* (pow E 3) log3Term)
+               (* -16 (pow E 2) log3Term)
+               (* 6 (pow E 2) log2Term)
+               (* -18 (pow E 2) logTerm)
+               (* -9 E log3Term)
+               (* -94 E log2Term)
+               (* -378 E logTerm)
+               (* 48 E)
+               (* -16 E3/2 log3Term)
+               (* -174 E3/2 log2Term)
+               (* 72 E3/2 logTerm)
+               (* -12 E3/2)
+               (* -9 E5/2 log3Term)
+               (* -4 E5/2 log2Term)
+               (* -12 logTerm)
+               -72))
+
+        (n3 (+ (* sqrtE logTerm)
+               (* -216 sqrtE)
+               (* -8 (pow E 3) logTerm)
+               (* 2 (pow E 3))
+               (* -176 (pow E 2) logTerm)
+               (* 96 (pow E 2))
+               (* -8 E logTerm)
+               (* 266 E)
+               (* 83 E3/2 logTerm)
+               (* -232 E3/2)
+               (* 83 E5/2 logTerm)
+               (* -16 E5/2)
+               (* E7/2 logTerm)
+               12))
+
+        (n4 (+ (* -18 sqrtE logTerm)
+               (* -110 sqrtE)
+               (* (pow E 3) logTerm)
+               (* 53 (pow E 2) logTerm)
+               (* 13 E logTerm)
+               (* 30 E)
+               (* -66 E3/2 logTerm)
+               (* 30 E3/2)
+               (* -8 E5/2 logTerm)
+               logTerm
+               10))
+
+        (n5 (+ (* -18 sqrtE log2Term)
+               (* -115 sqrtE logTerm)
+               (* -340 sqrtE)
+               (* (pow E 3) log2Term)
+               (* 3 (pow E 2) log2Term)
+               (* 90 (pow E 2) logTerm)
+               (* -10 (pow E 2))
+               (* 3 E log2Term)
+               (* 20 E logTerm)
+               (* -390 E)
+               (* -116 E3/2 log2Term)
+               (* -530 E3/2 logTerm)
+               (* 60 E3/2)
+               (* -18 E5/2 log2Term)
+               (* -15 E5/2 logTerm)
+               log2Term
+               (* 10 logTerm)
+               60))
+
+        (n6 (+ (* sqrtE log2Term)
+               (* 15 sqrtE logTerm)
+               (* -156 sqrtE)
+               (* (pow E 3) log2Term)
+               (* -16 (pow E 2) log2Term)
+               (* 30 (pow E 2) logTerm)
+               (* -6 (pow E 2))
+               (* -9 E log2Term)
+               (* -70 E logTerm)
+               (* -126 E)
+               (* -16 E3/2 log2Term)
+               (* -180 E3/2 logTerm)
+               (* 24 E3/2)
+               (* -9 E5/2 log2Term)
+               (* -7 E5/2 logTerm)
+               -12))
+       )
+   (+ 1
+      (/
+       (+
+         (/ (* n1 (* dx dx)) (* 30 (pow (- 1 sqrtE) 2) D))
+         (/ (* n2 dx) (* 3 (- 1 sqrtE) D))
+         (/ (* sqrtE n3 (pow dx 4)) (* 360 (pow (- 1 sqrtE) 4) D))
+         (/ (* sqrtE n4 (pow dx 3)) (* 30 (pow (- 1 sqrtE) 3) D))
+         (/ (* sqrtE n5 (pow dx 2)) (* 30 (pow (- 1 sqrtE) 2) D))
+         (/ (* n6 dx) (* 3 (- 1 sqrtE) D))
+         logTerm)
+       ))))