Kepler.scala 1.49 KB
 Joachim Bard committed Feb 25, 2019 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 `````` import daisy.lang._ import Real._ /* These benchmarks were used by the Real2Float tool, and come from the proof of the Kepler conjecture Introduction to the flyspec project, T.C. Hales, Dagstuhl 2006 */ object Kepler { //15 operations def kepler0(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = { require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 && 4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36) val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6) x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * t } // 1.15e-15 //24 operations def kepler1(x1: Real, x2: Real, x3: Real, x4: Real): Real = { require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 && 4 <= x4 && x4 <= 6.36) val t = ((-1 * x1) + x2 + x3 - x4) x1 * x4 * t + x2 * (x1 - x2 + x3 + x4) + x3 * (x1 + x2 - x3 + x4) - x2 * x3 * x4 - x1 * x3 - x1 * x2 - x4 } // 4.50e–13 //36 operations def kepler2(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = { require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 && 4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36) val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6) val t2 = (x1 - x2 + x3 + x4 - x5 + x6) x1 * x4 * t + x2 * x5 * t2 + x3* x6 * (x1 + x2 - x3 + x4 + x5 - x6) - x2 * x3 * x4 - x1* x3* x5 - x1 * x2 * x6 - x4 * x5 * x6 } //2.08e–12 }``````