Commit 7fbe5cbb by Anastasiia

new input intervals to avoid divbyzero for some benchmarks

parent 336f0df4
 import daisy.lang._ import Real._ object Bsplines { def bspline0(u: Real): Real = { require(0 <= u && u <= 0.875) (1 - u) * (1 - u) * (1 - u) / 6.0 } ensuring (res => 0 <= res && res <= 0.17 && res +/- 1e-15) // proven in paper: [-0.05, 0.17] def bspline1(u: Real): Real = { require(0.875 <= u && u <= 1) (3 * u*u*u - 6 * u*u + 4) / 6.0 } ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15) // in paper [-0.05, 0.98] def bspline2(u: Real): Real = { require(0.5 <= u && u <= 1) (-3 * u*u*u + 3*u*u + 3*u + 1) / 6.0 } ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15) // in paper [-0.02, 0.89] def bspline3(u: Real): Real = { require(0.125 <= u && u <= 1) -u*u*u / 6.0 } ensuring (res => -0.17 <= res && res <= 0.0 && res +/- 1e-15) // in paper [-0.17, 0.05] }
 import daisy.lang._ import Real._ object Doppler { def doppler(u: Real, v: Real, T: Real): Real = { require(-100.0 <= u && u <= 100 && 20 <= v && v <= 20000 && -30 <= T && T <= 50) // val t1 = 331.4 + 0.6 * T (- (331.4 + 0.6 * T) *v) / ((331.4 + 0.6 * T + u)*(331.4 + 0.6 * T + u)) } } \ No newline at end of file
 import daisy.lang._ import Real._ object JetEngine { def jetEngine(x1: Real, x2: Real): Real = { require(4 <= x1 && x1 <= 4.65 && 1 <= x2 && x2 <= 5) x1 + ((2*x1*((3*x1*x1 + 2*x2 - x1)/(x1*x1 + 1))* ((3*x1*x1 + 2*x2 - x1)/(x1*x1 + 1) - 3) + x1*x1*(4*((3*x1*x1 + 2*x2 - x1)/(x1*x1 + 1))-6))* (x1*x1 + 1) + 3*x1*x1*((3*x1*x1 + 2*x2 - x1)/(x1*x1 + 1)) + x1*x1*x1 + x1 + 3*((3*x1*x1 + 2*x2 -x1)/(x1*x1 + 1))) } } \ No newline at end of file
 import daisy.lang._ import Real._ object RigidBody { def rigidBody1(x1: Real, x2: Real, x3: Real): Real = { require(-15.0 <= x1 && x1 <= -0.1 && 0.1 <= x2 && x2 <= 15.0 && -15.0 <= x3 && x3 <= -0.1) -x1*x2 - 2*x2*x3 - x1 - x3 } def rigidBody2(x1: Real, x2: Real, x3: Real): Real = { require(-15.0 <= x1 && x1 <= -11.25 && -15.0 <= x2 && x2 <= -11.25 && -15.0 <= x3 && x3 <= -11.25) 2*(x1*x2*x3) + (3*x3*x3) - x2*(x1*x2*x3) + (3*x3*x3) - x2 } } \ No newline at end of file
 import daisy.lang._ import Real._ object Sine { def sine(x: Real): Real = { require(x > 0.875 && x < 1.57079632679) x - (x*x*x)/6.0 + (x*x*x*x*x)/120.0 - (x*x*x*x*x*x*x)/5040.0 } def sineOrder3(x: Real): Real = { require(-2.0 < x && x < -1.125) 0.954929658551372 * x - 0.12900613773279798*(x*x*x) } } \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment