Commit a4643d84 authored by Anastasiia's avatar Anastasiia

Merge branch 'relative' into 'relative'

update for the public version

See merge request !104
parents 15735196 eae0afdb
#!/bin/bash --posix
declare -a uni=("testcases/relative/changedinputs/Bsplines.scala" "testcases/relative/changedinputs/Sine.scala" "testcases/relative/changedinputs/Sqrt.scala")
for file in "${uni[@]}"
do
echo "$file"
bash daisy --relative --denormals --rel-rangeMethod=smtreuse --divLimit=0 --approach=naive $file >> nozero_z3_naive_bUp_univar.txt
done
declare -a multi=("testcases/relative/changedinputs/Doppler.scala" "testcases/relative/changedinputs/RigidBody.scala" "testcases/relative/changedinputs/Turbine.scala" "testcases/relative/changedinputs/JetEngine.scala" "testcases/relative/changedinputs/Himmilbeau.scala" "testcases/relative/changedinputs/InvertedPendulum.scala" "testcases/relative/changedinputs/Kepler.scala" "testcases/relative/changedinputs/Traincar4.scala")
for file in "${multi[@]}"
do
echo "$file"
bash daisy --relative --denormals --rel-rangeMethod=smtreuse --divLimit=0 --approach=naive $file >> nozero_z3_naive_bUp_multivar.txt
done
......@@ -52,20 +52,22 @@ object RelThroughAbsPhase extends DaisyPhase with Subdivision with ErrorFunction
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
ChoiceOptionDef("rel-rangeMethod", "Method to use for range analysis",
Set("affine", "interval", "smtreuse", "smtredo"), "interval"),
ParamOptionDef("divLimit", "Max amount of interval divisions", divLimit.toString),
ParamOptionDef("divLimit", "Max amount of interval divisions", divLimit.toString),
ParamOptionDef("totalOpt", "Max total amount of analysis runs", totalOpt.toString),
ChoiceOptionDef("subdiv", "Method to subdivide intervals", Set("simple", "model"), "simple"),
ChoiceOptionDef("approach", "Approach for expressions", Set("taylor", "naive"), "taylor"),
// fixme change name to not overlap with RangeErrorPhase or put into Main
FlagOptionDef("noRoundoff", "No initial roundoff errors"),
FlagOptionDef("denormals","Include parameter for denormals in the FP abstraction"))
val deltaName = "delta"
val epsilonName = "eps"
var reporter: Reporter = null
override def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
reporter.info(s"\nStarting $name")
val timer = ctx.timers.analysis.start
val timer = ctx.timers.relAbs.start
// default range method: intervals
var rangeMethod = "interval"
......@@ -86,6 +88,8 @@ object RelThroughAbsPhase extends DaisyPhase with Subdivision with ErrorFunction
case _ =>
reporter.warning(s"Unknown range method: $s, choosing default (interval)!")
}
case ParamOption("divLimit", value) => divLimit = value.toInt
case ParamOption("totalOpt", value) => totalOpt = value.toInt
case FlagOption("noInitialErrors") => trackInitialErrs = false
case FlagOption("noRoundoff") => trackRoundoffErrs = false
case ChoiceOption("precision", s) => s match {
......
......@@ -51,6 +51,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
Set("affine", "interval", "smtreuse", "smtredo", "smtcomplete"), "interval"),
ParamOptionDef("divLimit", "Max amount of interval divisions", divLimit.toString),
ParamOptionDef("divRemainder", "Max amount of interval divisions for remainder term", divRemainder.toString),
ParamOptionDef("totalOpt", "Max total amount of analysis runs", totalOpt.toString),
ChoiceOptionDef("subdiv", "Method to subdivide intervals", Set("simple", "model"), "simple"),
ChoiceOptionDef("approach", "Approach for expressions", Set("taylor", "naive"), "taylor"),
// fixme change name to not overlap with RangeErrorPhase or put into Main
......@@ -74,6 +75,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
for (opt <- ctx.options) opt match {
case ParamOption("divLimit", value) => divLimit = value.toInt
case ParamOption("divRemainder", value) => divRemainder = value.toInt
case ParamOption("totalOpt", value) => totalOpt = value.toInt
case ChoiceOption("rel-rangeMethod", s) => s match {
case "interval" | "affine" | "smtreuse" | "smtredo" | "smtcomplete" =>
rangeMethod = s
......@@ -106,7 +108,11 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
val bodyReal = fnc.body.get
val deltaVarMap = mapDeltasToVars(bodyReal)
val bodyDeltaAbs = deltaAbstract(bodyReal, deltaVarMap)
val epsVarMap = mapEpsilonsToVars(bodyReal)
val bodyDeltaAbs = if (denormals)
deltaAbstract(bodyReal, deltaVarMap, epsVarMap)
else
deltaAbstract(bodyReal, deltaVarMap, Map.empty)
// reporter.warning(s"bodyDelta $bodyDeltaAbs")
// Step 1: disregard initial errors for now
// (f(x) - fl(x))/ f(x)
......@@ -122,7 +128,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
for (delta <- deltas){
deltaIntervalMap = deltaIntervalMap + (delta.id -> delta.interval)
}
val eps = epsilonsOf(relErrorExpr); //reporter.warning("epsilons: " + eps)
val eps = epsilonsOf(relErrorExpr)
for (e <- eps){
deltaIntervalMap = deltaIntervalMap + (e.id -> e.interval)
}
......@@ -136,23 +142,26 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
case "taylor" => getRelErrorTaylorApprox(relErrorExpr, inputValMap, bodyReal, ctx)
case "naive" => getRelErrorNaive(relErrorExpr, inputValMap, bodyReal, ctx)
}
if (relError.isDefined) {
reporter.warning("Failed on " + tmpList.distinct.size + " sub-domain(s)")
val list = mergeIntervals(tmpList, inputValMap)
// if returned None or too many subintervals where failed to compute relError,
// say it is not possible to compute
if (relError.isDefined && (list.size < 30)) {
val time = System.currentTimeMillis
reporter.info("relError: " + relError.get.toString + ", time: " + (time - startTime))
val list = mergeIntervals(tmpList, inputValMap)
if (list.nonEmpty) {
reporter.info(s"On several sub-intervals relative error cannot be computed.")
reporter.info("Computing absolute error on these sub-intervals.")
for (mapEntry <- list) {
// here we compute the abs error for intervals where rel error is not possible
//todo put abs error computation back
val absError = getAbsError(bodyReal, mapEntry, inputErrorMap, uniformPrecision)
reporter.info(s"For intervals $mapEntry, absError: $absError, time: " +
(System.currentTimeMillis - time))
}
}
} else {
reporter.info("Not possible to get relative error, compute the absolute instead")
reporter.info("Not possible to get relative error, compute the absolute instead, time:" +
(System.currentTimeMillis - startTime))
val time = System.currentTimeMillis
// fixme for JetEngine DivByZeroException is thrown
val absError = getAbsError(bodyReal, inputValMap, inputErrorMap, uniformPrecision)
......@@ -192,7 +201,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
// output subintervals without deltas
for (entry <- newSet){
reporter.debug("============================================")
for (mapEntry <- entry if !mapEntry._1.isDeltaId)
for (mapEntry <- entry if !(mapEntry._1.isDeltaId|| mapEntry._1.isEpsilonId))
reporter.debug(mapEntry._1 + " -> " + mapEntry._2)
}
reporter.debug(s"We need to evaluate expression on "+newSet.size+" intervals")
......@@ -202,11 +211,12 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
// taylorFirst.foreach(x=>{reporter.debug(s"term is $x")})
reporter.info("Computing the error ...")
// fixme for div-by-zero benchmarks subdivision parameter should be greater than 0
reporter.info(s"subdiv for remainder $divRemainder")
// separate timer for remainder
val remainderTime = System.currentTimeMillis
val remainderMap = getEqualSubintervals(inputValMap, divLimit, divRemainder)
val taylorRemainder = getTaylorRemainder(relErrorExpr, remainderMap)
reporter.info(s"The taylor remainder value is $taylorRemainder")
reporter.info(s"The taylor remainder value is $taylorRemainder, time: " + (System.currentTimeMillis - remainderTime))
if (taylorRemainder.isDefined) {
val errForSum = taylorFirst.map(x => {
val (expr, wrt) = x
......@@ -216,15 +226,15 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
// do not call evaluation function on all subintervals
// if simplified expression is delta or RealLiteral
val tmpForMax = tmpExpr match {
case x@Delta(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x@Epsilon(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x@Variable(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x@RealLiteral(r) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x @ Delta(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x @ Epsilon(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x @ Variable(id) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case x @ RealLiteral(r) => List(evaluateOpt(tmpExpr, inputValMap, rangeMethod))
case _ => newSet.map(interval => {
val tmp = evaluateOpt(tmpExpr, interval, rangeMethod)
reporter.debug("err on " + removeDeltasFromMap(interval) + s" is $tmp")
if (tmp.isEmpty)
if (!listFailInterval.contains(interval)) listFailInterval = listFailInterval :+ interval
if (!listFailInterval.contains(interval) && !listFailed.contains(interval)) listFailInterval = listFailInterval :+ interval
tmp
})
}
......@@ -243,6 +253,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
}
listFailInterval = (listFailInterval ++ listFailed).toSet.toList
reporter.debug("print what is ACTUALLY in ListFailed " + listFailed.map(removeDeltasFromMap).map(_.keySet.map(_.globalId)))
(finalErr, listFailInterval)
}
......@@ -500,9 +511,8 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
while (tmp == 0 && iterator.hasNext){
val (id, interval) = iterator.next()
if (!id.isDeltaId) {
if (!(id.isDeltaId|| id.isEpsilonId)) {
tmp = compareIntervals(interval, second(id))
}
}
tmp <= 0
......
......@@ -73,8 +73,9 @@ object TaylorErrorPhase extends DaisyPhase with Taylor with ErrorFunctions {
val bodyReal = fnc.body.get
val deltaVarMap = mapDeltasToVars(bodyReal)
val epsVarMap = mapEpsilonsToVars(bodyReal)
// derive f~(x)
val bodyDelta = deltaAbstract(bodyReal, deltaVarMap)
val bodyDelta = deltaAbstract(bodyReal, deltaVarMap, epsVarMap)
// get set of partial derivatives wrt deltas
val taylor = getDerivative(bodyDelta)
......
......@@ -87,6 +87,7 @@ class DRealInterpreter(executable: String, args: Array[String])
} finally {
// now kill the process
invalidated = true
this.free()
kill()
}
......
......@@ -181,6 +181,7 @@ abstract class SMTLibSolver(val context: Context) {
case Epsilon(id) => declareVariable(id)
}
val term = toSMT(expr)(Map())
//reporter.warning(s"solver query SMT:" + SMTAssert(term))
emit(SMTAssert(term))
} catch {
case _ : SMTLIBUnsupportedError =>
......@@ -244,10 +245,10 @@ abstract class SMTLibSolver(val context: Context) {
syms.head,
syms.tail.map(s => QualifiedIdentifier(SMTIdentifier(s)))
)
// reporter.warning(cmd)
emit(cmd) match {
case GetValueResponseSuccess(valuationPairs) =>
// System.out.println("Val Pairs: "+valuationPairs)
System.out.println("Val Pairs: "+valuationPairs)
new Model(valuationPairs.collect {
case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
val id = variables.toA(sym)
......@@ -333,6 +334,7 @@ abstract class SMTLibSolver(val context: Context) {
variables.getOrElseAddB(id) {
val s = id2sym(id)
val cmd = DeclareFun(s, List(), toSMTSort(id.getType))
// reporter.warning(cmd)
emit(cmd)
s
}
......
This diff is collapsed.
......@@ -16,8 +16,7 @@ import scala.collection.immutable.Map
trait Subdivision extends Taylor{
//TODO make a parameter
implicit val subdivFirst: Int = 32
var totalOpt: Int = 32
def getSubintervals(inputValMap: Map[Identifier, Interval],
bodyReal: Expr,
......@@ -50,6 +49,7 @@ trait Subdivision extends Taylor{
reporter.debug(model)
model match {
case Some(tmp) =>
reporter.debug(s"true zeros detected at $model")
val exprs: Map[Identifier, Expr] = variablesOf(bodyReal).map(id => {(id -> model.get(id))}).toMap
reporter.debug(s"Model expressions are $exprs")
val values: Map[Identifier, Interval] = exprs.map(expr =>
......@@ -74,27 +74,36 @@ trait Subdivision extends Taylor{
val split = if (divParameter != -1)
divParameter
else
Math.pow(2, divLimit).toInt
divLimit
var srcCartesian: Map[Identifier, Seq[Interval]] = Map.empty
var counter = split
// sort the list of input vars by width of intervals
val inputSeq = inputValMap.toSeq.sortWith(_._2 > _._2)
// reporter.warning(s"sorted map $inputSeq")
var subdivided = 0
var left = removeDeltasFromMap(inputValMap).keys.size - 1
var counter = 0
reporter.info(s"amount of vars is "+(left+1))
// set of vectors. each vector contains the maps for one var
for (inputVal <- inputSeq) {
if (inputVal._1.isDeltaId || inputVal._1.isEpsilonId || counter > subdivFirst) {
counter = Math.pow(split, subdivided + 1).toInt + left
// reporter.warning(s"counter $counter ;var $inputVal")
if (inputVal._1.isDeltaId || inputVal._1.isEpsilonId || counter > totalOpt) {
srcCartesian += (inputVal._1 -> Seq(inputVal._2))
if (!(inputVal._1.isDeltaId || inputVal._1.isEpsilonId)) left = left - 1
}
else {
// reporter.info(s"took the subdiv branch $inputVal")
val (id, interval) = inputVal
val oneVar = interval.divide(split)
val oneVar = if (interval.xlo.equals(interval.xhi))
List(interval)
else
interval.divide(split)
srcCartesian += (id -> oneVar)
counter = counter + split
subdivided = subdivided + 1
left = left - 1
}
}
// reporter.warning(s"src cartesian $srcCartesian")
val result = cartesianProduct(srcCartesian)
reporter.warning(s"size cartesian " + result.size)
result
}
}
......
......@@ -677,7 +677,6 @@ trait Taylor{
// val simple = simplify(e)
deltasOf(e).foreach(wrt => {
val tmp = getPartialDerivative(e, wrt.id) //recurseDerivative(e, wrt.id)
//todo leave simple simplifications
taylorSeries = taylorSeries :+ (easySimplify(tmp), wrt.id)
})
taylorSeries
......@@ -692,34 +691,52 @@ trait Taylor{
def getTaylorRemainder(e:Expr, intervals: Seq[Map[Identifier, Interval]]): Option[Rational] = {
val simple = easySimplify(e)
reporter.debug("WHAT is INITIALLY in the listFailed " + listFailed.map(removeDeltasFromMap).map(_.keySet.map(_.globalId)))
// both deltas and epsilons
val deltas:Set[Expr with Identifiable] = deltasOf(simple) ++ epsilonsOf(simple)
//todo fix fold or map
val firstTerm = deltas.par.map(wrt => {
reporter.warning("Amount of runs for the first remainder term "+ Math.pow(deltas.size, 2)*intervals.size)
val firstTerm = deltas.map(wrt => {
// val wrtSt = System.currentTimeMillis()
// first derivative
val tmp = easySimplify(
getPartialDerivative(simple, wrt.getId))
val tmpValOut = deltas.par.map(wrtIn => {
// val start = System.currentTimeMillis()
// second derivative
if (containsVariables(tmp, wrtIn.getId)) {
val tmpIn = Times(wrt, Times(wrtIn, moreSimplify(
getPartialDerivative(tmp, wrtIn.getId))))
val tmpIn = easySimplify(Times(wrt, Times(wrtIn, moreSimplify(
getPartialDerivative(tmp, wrtIn.getId)))))
// reporter.warning(s"=============WRT $wrt * $wrtIn===============")
// reporter.warning(s"Second derivative $tmpIn")
val tmpVal = intervals.par.map(x => {
val interval = evaluateInterval(tmpIn, x)
if (interval.isDefined)
Some(maxAbs(interval.get))
else {
listFailed = listFailed :+ x
None
val tmpVal = tmpIn match {
case x @ Delta(id) => Seq(Some(maxAbs(x.interval)))
case x @ Epsilon(id) => Seq(Some(maxAbs(x.interval)))
case _ =>
intervals.par.map(x => {
val interval = evaluateInterval (tmpIn, x)
if (interval.isDefined)
Some (maxAbs (interval.get) )
else {
if (! listFailed.contains (x) ) {
listFailed = listFailed :+ x
}
None
}
})
}
})
// reporter.warning(s"finished iteration for $wrt, $wrtIn; time:" + (System.currentTimeMillis() - start))
tmpVal.max(optionAbsOrdering)
}
else None
})
// remove a dummy entry from the list
reporter.debug(s"before "+ listFailed.map(removeDeltasFromMap))
listFailed = listFailed.filter(x => removeDeltasFromMap(x).keySet == removeDeltasFromMap(intervals.head).keySet)
reporter.debug(s"after "+ listFailed.map(removeDeltasFromMap))
// reporter.warning(s"done for $wrt in " + (System.currentTimeMillis()-wrtSt))
tmpValOut.fold(None)(sumOption)
})
......@@ -869,8 +886,28 @@ trait Taylor{
(Variable(x) -> getADelta)
}).toMap
}
def mapEpsilonsToVars(e: Expr):Map[Variable, Epsilon] = {
variablesOf(e).map(x =>{
(Variable(x) -> getAnEpsilon)
}).toMap
}
def deltaAbstract(e: Expr, deltaToVarMap: Map[Variable, Delta],
epsToVarMap: Map[Variable,Epsilon]): Expr = (e: @unchecked) match {
def deltaAbstract(e: Expr, deltaToVarMap: Map[Variable, Delta]): Expr = (e: @unchecked) match {
// x -> x * (1 + delta)
case x: Variable if trackRoundoffErrs && denormals =>
// initial error
if (deltaToVarMap.contains(x))
if (epsToVarMap.contains(x))
Plus(Times(x, Plus(one, deltaToVarMap(x))), epsToVarMap(x))
else
Plus(Times(x, Plus(one, deltaToVarMap(x))), getAnEpsilon)
else
if (epsToVarMap.contains(x))
Plus(Times(x, Plus(one, getADelta)), epsToVarMap(x))
else
Plus(Times(x, Plus(one, getADelta)), getAnEpsilon)
// x -> x * (1 + delta)
case x: Variable if trackRoundoffErrs =>
......@@ -892,29 +929,29 @@ trait Taylor{
// x - > x ## negation does not incur any error
case UMinus(x) =>
UMinus(deltaAbstract(x, deltaToVarMap))
UMinus(deltaAbstract(x, deltaToVarMap, epsToVarMap))
// (x + y) -> (x + y)(1 + delta)
case z @ Plus(x, y) =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Times(Plus(xDelta, yDelta),
Plus(one,
getADelta))
// (x - y) -> (x - y)(1 + delta)
case z @ Minus(x, y) =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Times(Minus(xDelta, yDelta),
Plus(one,
getADelta))
// (x * y) -> (x * y)(1 + delta) + eps
case z @ Times(x, y) if denormals =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Plus(
Times(Times(xDelta, yDelta),
Plus(one,
......@@ -922,16 +959,16 @@ trait Taylor{
// (x * y) -> (x * y)(1 + delta)
case z @ Times(x, y) =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Times(Times(xDelta, yDelta),
Plus(one,
getADelta))
// (x / y) -> ( x / y)(1 + delta) + eps
case z @ Division(x, y) if denormals =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Plus(
Times(Division(xDelta, yDelta),
Plus(one,
......@@ -939,8 +976,8 @@ trait Taylor{
// (x / y) -> ( x / y)(1 + delta)
case z @ Division(x, y) =>
val xDelta = deltaAbstract(x, deltaToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap)
val xDelta = deltaAbstract(x, deltaToVarMap, epsToVarMap)
val yDelta = deltaAbstract(y, deltaToVarMap, epsToVarMap)
Times(Division(xDelta, yDelta),
Plus(one,
getADelta))
......@@ -948,19 +985,20 @@ trait Taylor{
// sqrt(x) = sqrt(x)(1 + delta) + eps
case z @ Sqrt(x) if denormals =>
Plus(
Times(Sqrt(deltaAbstract(x, deltaToVarMap)),
Times(Sqrt(deltaAbstract(x, deltaToVarMap, epsToVarMap)),
Plus(one, getADelta))
,getAnEpsilon)
// sqrt(x) = sqrt(x)(1 + delta)
case z @ Sqrt(x) =>
Times(Sqrt(deltaAbstract(x, deltaToVarMap)),
Times(Sqrt(deltaAbstract(x, deltaToVarMap, epsToVarMap)),
Plus(one, getADelta))
//todo add Pow ?
case z @ Let(x, value, body) =>
Let(x, deltaAbstract(value, deltaToVarMap), deltaAbstract(body, deltaToVarMap))
Let(x, deltaAbstract(value, deltaToVarMap, epsToVarMap),
deltaAbstract(body, deltaToVarMap, epsToVarMap))
case z =>
throw new IllegalArgumentException(s"Unknown expression $z. Parsing failed")
......@@ -973,7 +1011,7 @@ trait Taylor{
* @return map for variables
*/
def removeDeltasFromMap(in: Map[Identifier, Interval]): Map[Identifier, Interval] ={
in.filterKeys(x => !x.isDeltaId)
in.filterKeys(x => !x.isDeltaId && !x.isEpsilonId)
}
/**
......
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._
/*
Real2Float
From a global optimization problem
A Numerical Evaluation of Several Stochastic Algorithms on
Selected Continuous Global Optimization problems,
Ali, Khompatraporn, Zabinsky, 2005
*/
object Himmilbeau {
def himmilbeau(x1: Real, x2: Real) = {
require(0.1 <= x1 && x1 <= 0.5 && -2<= x2 && x2 <= 2)
(x1*x1 + x2 - 11)*(x1 * x1 + x2 - 11) + (x1 + x2*x2 - 7)*(x1 + x2*x2 - 7)
} //1.43e–12
}
\ No newline at end of file
import daisy.lang._
import Real._
object InvertedPendulum {
// s1: <1, 16, 9> s2: <1, 16, 11> s3,s4: <1, 16, 15>
def invPendulum(s1: Real, s2: Real, s3: Real, s4: Real) = {
require(0.005 <= s1 && s1 <= 50 &&
0.005 <= s2 && s2 <= 10 &&
-0.785 <= s3 && s3 <= -0.005 &&
-0.785 <= s4 && s4 <= -0.005)
1.0000 * s1 + 1.6567 * s2 + (-18.6854) * s3 + (-3.4594) * s4
}
}
\ 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._
/*
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 {
def kepler0(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 0.0001 <= x2 && x2 <= 0.00011 && 40 <= x3 && x3 <= 63.6 &&
-6.36 <= x4 && x4 <= -4 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * (-x1 + x2 + x3 - x4 + x5 + x6)
} // 1.15e-15
def kepler1(x1: Real, x2: Real, x3: Real, x4: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 0.04 <= x2 && x2 <= 0.0636 && 40 <= x3 && x3 <= 63.6 &&
-6.36 <= x4 && x4 <= -4)
x1 * x4 * (-x1 + x2 + x3 - x4) + x2 * (x1 - x2 + x3 + x4) + x3 * (x1 + x2 - x3 + x4) -