Commit 29c81f50 authored by Anastasiia's avatar Anastasiia

Merge branch 'relative' into 'relative'

subdivide for remainder

See merge request !99
parents 432f1702 3e1e85b3
#!/bin/bash --posix
## declare an array variable
# declare -a arr=("element1" "element2" "element3")
# ## now loop through the above array
# for i in "${arr[@]}"
# do
# echo "$i"
# # or do whatever with individual element of the array
# done
# figure out how to write a list
declare -a uni=("testcases/relative/changedinputs/Bsplines.scala" \
"testcases/relative/changedinputs/Sine.scala" \
"testcases/relative/changedinputs/Sqrt.scala")
declare -a multi=("testcases/relative/changedinputs/Doppler.scala" \
"testcases/relative/changedinputs/Himmilbeau.scala" \
"testcases/relative/changedinputs/InvertedPendulum.scala" \
"testcases/relative/changedinputs/JetEngine.scala" \
"testcases/relative/changedinputs/Kepler.scala" \
"testcases/relative/changedinputs/RigidBody.scala" \
"testcases/relative/changedinputs/Traincar4.scala" \
"testcases/relative/changedinputs/Turbine.scala")
for file in "${uni[@]}"
do
echo $file
# ./daisy --solver=dreal --relative --rel-rangeMethod=smtcomplete $file >> paper_results/relerr_dreal_uni.txt
done
for file in "${multi[@]}"
do
echo $file
# ./daisy --solver=dreal --relative --rel-rangeMethod=smtcomplete $file >> paper_results/relerr_dreal_multi_nozero.txt
done
echo "testcases/relative/changedinputs/Kepler.scala"
./daisy --solver=dreal --relative --rel-rangeMethod=smtcomplete "testcases/relative/changedinputs/Kepler.scala" >> paper_results/relerr_dreal_multi_nozero.txt
echo "testcases/relative/changedinputs/JetEngine.scala"
./daisy --solver=dreal --relative --rel-rangeMethod=smtcomplete "testcases/relative/changedinputs/JetEngine.scala" >> paper_results/relerr_dreal_multi_nozero.txt
......@@ -199,7 +199,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
reporter.info("Computing the error ...")
// fixme for div-by-zero benchmarks subdivision parameter should be greater than 0
val remainderMap = getEqualSubintervals(inputValMap, divLimit, 0)
val remainderMap = getEqualSubintervals(inputValMap, divLimit, 4)
val taylorRemainder = getTaylorRemainder(relErrorExpr, remainderMap)
reporter.info(s"The taylor remainder value is $taylorRemainder")
......@@ -257,7 +257,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
reporter.debug("The set we got")
// output subintervals without deltas
for (entry <- newSet){
for (mapEntry <- entry if !mapEntry._1.isDeltaId)
for (mapEntry <- entry if !(mapEntry._1.isDeltaId|| mapEntry._1.isEpsilonId))
reporter.debug(mapEntry._1 + " -> " + mapEntry._2)
}
......@@ -322,10 +322,11 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
val interval = Evaluators.evalInterval(expr, intMap)
var constrs: Set[Expr] = Set.empty
val deltas = deltasOf(expr)
val eps = epsilonsOf(expr)
val vars = variablesOf(expr)
intMap.foreach(x => {
val (id, interval) = x
if (deltas.contains(Delta(id)) || vars.contains(id)) {
if (deltas.contains(Delta(id)) || vars.contains(id) || eps.contains(Epsilon(id))) {
constrs = constrs ++ SMTRange.toConstraints(Variable(id), interval)
}
})
......
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