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
}