Commit 559421dd authored by Anastasiia's avatar Anastasiia

if there are more than 30 sub-intervals, do not report relErr

parent 5b85fcc8
......@@ -136,23 +136,25 @@ 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) {
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)
......
......@@ -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
}
......
......@@ -50,6 +50,7 @@ trait Subdivision extends Taylor{
reporter.debug(model)
model match {
case Some(tmp) =>
reporter.warning(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,15 +75,18 @@ 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
// sort the list of input vars by width of intervals
val inputSeq = inputValMap.toSeq.sortWith(_._2 > _._2)
var subdivided = 0
var left = removeDeltasFromMap(inputValMap).keys.size
var counter = split + left - 1
var left = removeDeltasFromMap(inputValMap).keys.size - 1
var counter = 0
reporter.warning(s"amount of vars is "+(left+1))
// set of vectors. each vector contains the maps for one var
for (inputVal <- inputSeq) {
counter = Math.pow(split, subdivided + 1).toInt + left
// reporter.warning(s"counter $counter")
if (inputVal._1.isDeltaId || inputVal._1.isEpsilonId || counter > subdivFirst) {
srcCartesian += (inputVal._1 -> Seq(inputVal._2))
left = left - 1
......@@ -93,12 +97,10 @@ trait Subdivision extends Taylor{
srcCartesian += (id -> oneVar)
subdivided = subdivided + 1
left = left - 1
counter = Math.pow(split, subdivided).toInt + left
// reporter.warning(s"counter $counter")
}
}
val result = cartesianProduct(srcCartesian)
//reporter.warning(s"size cartesian " + result.size)
reporter.warning(s"size cartesian " + result.size)
result
}
}
......
......@@ -973,7 +973,7 @@ trait Taylor{
* @return map for variables
*/
def removeDeltasFromMap(in: Map[Identifier, Interval]): Map[Identifier, Interval] ={
in.filterKeys(x => !(x.isDeltaId||x.isEpsilonId))
in.filterKeys(x => !x.isDeltaId && !x.isEpsilonId)
}
/**
......
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