Commit 48b445f5 authored by Anastasiia's avatar Anastasiia

moved interval subdivision to separate trait

parent cb25a81e
......@@ -34,7 +34,7 @@ import scala.util.control.Breaks._
*Prerequisites:
*- SpecsProcessingPhase
*/
object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunctions{
// default parameters for the complete run
var divLimit = 3
......@@ -160,89 +160,6 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
(ctx, prg)
}
private def cartesianProduct(a: Map[Identifier, Seq[Interval]]) = {
def product(a: List[(Identifier, Seq[Interval])]): Seq[Map[Identifier, Interval]] =
a match {
case (name, values) :: tail =>
for {
result <- product(tail)
value <- values
} yield Map(name -> value).++(result)
case Nil => Seq(Map.empty)
}
product(a.toList)
}
private def getSubintervals(inputValMap: Map[Identifier, Interval],
bodyReal: Expr,
// TODO get rid of the context in here
ctx: Context
): Seq[Map[Identifier, Interval]] = {
subdiv match {
case "simple" => getEqualSubintervals(inputValMap)
case "model" => val result = getModelSubintervals(bodyReal, inputValMap, ctx)
result match {
case Some(x) => x
case None => getEqualSubintervals(inputValMap)
}
}
}
def getModelSubintervals(bodyReal: Expr,
inputValMap: Map[Identifier, Interval],
ctx: Context): Option[Seq[Map[Identifier, Interval]]] = {
val constrs = removeDeltasFromMap(inputValMap).flatMap(x => {
val (id, interval) = x
SMTRange.toConstraints(Variable(id), interval)
})
val condition = and(constrs.toSeq :_*)
val solverQuery = And(condition, Equals(zero, bodyReal))
val model = Solver.getModel(solverQuery)
reporter.debug(model)
model match {
case Some(tmp) =>
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 =>
{expr._1 ->
Evaluators.evalInterval(expr._2, Map.empty).extendBy(Rational.fromReal(0.1))})
reporter.warning(s"Model values are $values")
val newInts = excludeInterval(values, inputValMap)
Some(newInts)
case None => reporter.debug(s"No true zeros in function")
None
}
}
private def getEqualSubintervals(inputValMap: Map[Identifier, Interval],
divParameter: Int = 0):
Seq[Map[Identifier, Interval]] = {
val split = if (divParameter!=0)
divParameter
else
Math.pow(2, divLimit).toInt
var srcCartesian: Map[Identifier, Seq[Interval]] = Map.empty
// set of vectors. each vector contains the maps for one var
for (inputVal <- inputValMap ){
if (inputVal._1.isDeltaId){
srcCartesian += (inputVal._1 -> Seq(inputVal._2))
}
else {
val (id, interval) = inputVal
val oneVar = interval.divide(split)
srcCartesian += (id -> oneVar)
}
}
val result = cartesianProduct(srcCartesian)
result
}
/**
* Evaluates the relative error for the taylor approximation for relErrorExpr on the set of subintervals
* @param relErrorExpr - expression to evaluate, i.e. |f(x) - f~(x)|/f(x)
......@@ -256,7 +173,7 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
var listFailInterval: Seq[Map[Identifier, Interval]] = Seq.empty
// get intervals subdivision for the complete divLimit
val newSet = getSubintervals(inputValMap, bodyReal, ctx)
val newSet = getSubintervals(inputValMap, bodyReal, ctx, subdiv, divLimit)
reporter.debug(s"EXPRESSION is $relErrorExpr")
reporter.debug("The set we got")
......@@ -273,7 +190,7 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
// taylorFirst.foreach(x=>{reporter.debug(s"term is $x")})
reporter.info("Computing the error ...")
val remainderMap = getEqualSubintervals(inputValMap, 3)
val remainderMap = getEqualSubintervals(inputValMap, divLimit, 3)
val taylorRemainder = getTaylorRemainder(relErrorExpr, remainderMap)
reporter.info(s"The taylor remainder value is $taylorRemainder")
......@@ -318,7 +235,7 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
var listFailInterval: Seq[Map[Identifier, Interval]] = Seq.empty
// get intervals subdivision for the complete divLimit
val newSet = getSubintervals(inputValMap, bodyReal, ctx).par
val newSet = getSubintervals(inputValMap, bodyReal, ctx, subdiv, divLimit).par
reporter.debug("The set we got")
// output subintervals without deltas
......@@ -553,48 +470,6 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
else Seq()
}
def excludeInterval(toExclude: Map[Identifier, Interval],
original: Map[Identifier, Interval]
): Seq[Map[Identifier, Interval]] = {
var result: Seq[Map[Identifier, Interval]] = Seq.empty
for ((id, interval) <- toExclude) {
var copy = original
val origInterval = original(id)
if (interval.xlo.<(origInterval.xlo))
if (interval.xhi.>(origInterval.xhi))
// interval to exclude is greater than original
// fixme find a better way
throw new IllegalArgumentException("The resulting interval is empty")
else
// lower bound of interval toExclude is smaller than lower bound of originalInterval
// e.g. exclude [-0.1 ; 0.1] from [0; 10]
{
val tmp = Interval(interval.xhi, origInterval.xhi)
copy = copy + (id -> tmp)
result = result ++ Set(copy)
}
else if (interval.xhi.>(origInterval.xhi))
// upper bound of interval toExclude is greater than upper bound of originalInterval
// e.g. exclude [-0.1 ; 0.1] from [-10; 0]
{
val tmp = Interval(origInterval.xlo, interval.xlo)
copy = copy + (id -> tmp)
result = result ++ Set(copy)
}
else
// general case
{
val tmplo = Interval(origInterval.xlo, interval.xlo)
copy = copy + (id -> tmplo)
result = result ++ Set(copy)
val tmphi = Interval(interval.xhi, origInterval.xhi)
copy = copy + (id -> tmphi)
result = result ++ Set(copy)
}
}
result
}
def mergeSortedMaps(in: Seq[Map[Identifier,Interval]]): Seq[Map[Identifier,Interval]] = in match {
case x:: y::tail =>
val merged = mergeMaps(x, y)
......
package daisy.utils
import daisy.lang.Identifiers.Identifier
import daisy._
import daisy.lang.Constructors.and
import daisy.lang.TreeOps._
import daisy.lang.Trees.{RealLiteral, _}
import daisy.solvers.Solver
import scala.collection.immutable.Map
/**
* Trait with collections of methods to perform
* interval subdivision
*/
trait Subdivision extends Taylor{
def getSubintervals(inputValMap: Map[Identifier, Interval],
bodyReal: Expr,
// TODO get rid of the context in here
ctx: Context,
subdiv: String,
divLimit: Int
): Seq[Map[Identifier, Interval]] = {
subdiv match {
case "simple" => getEqualSubintervals(inputValMap ,divLimit)
case "model" => val result = getModelSubintervals(bodyReal, inputValMap, ctx)
result match {
case Some(x) => x
case None => getEqualSubintervals(inputValMap, divLimit)
}
}
}
def getModelSubintervals(bodyReal: Expr,
inputValMap: Map[Identifier, Interval],
ctx: Context): Option[Seq[Map[Identifier, Interval]]] = {
val constrs = removeDeltasFromMap(inputValMap).flatMap(x => {
val (id, interval) = x
SMTRange.toConstraints(Variable(id), interval)
})
val condition = and(constrs.toSeq :_*)
val solverQuery = And(condition, Equals(zero, bodyReal))
val model = Solver.getModel(solverQuery)
reporter.debug(model)
model match {
case Some(tmp) =>
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 =>
{expr._1 ->
Evaluators.evalInterval(expr._2, Map.empty).extendBy(Rational.fromReal(0.1))})
reporter.warning(s"Model values are $values")
val newInts = excludeInterval(values, inputValMap)
Some(newInts)
case None => reporter.debug(s"No true zeros in function")
None
}
}
def getEqualSubintervals(inputValMap: Map[Identifier, Interval], divLimit: Int,
divParameter: Int = 0):
Seq[Map[Identifier, Interval]] = {
val split = if (divParameter!=0)
divParameter
else
Math.pow(2, divLimit).toInt
var srcCartesian: Map[Identifier, Seq[Interval]] = Map.empty
// set of vectors. each vector contains the maps for one var
for (inputVal <- inputValMap ){
if (inputVal._1.isDeltaId){
srcCartesian += (inputVal._1 -> Seq(inputVal._2))
}
else {
val (id, interval) = inputVal
val oneVar = interval.divide(split)
srcCartesian += (id -> oneVar)
}
}
val result = cartesianProduct(srcCartesian)
result
}
def cartesianProduct(a: Map[Identifier, Seq[Interval]]) = {
def product(a: List[(Identifier, Seq[Interval])]): Seq[Map[Identifier, Interval]] =
a match {
case (name, values) :: tail =>
for {
result <- product(tail)
value <- values
} yield Map(name -> value).++(result)
case Nil => Seq(Map.empty)
}
product(a.toList)
}
def excludeInterval(toExclude: Map[Identifier, Interval],
original: Map[Identifier, Interval]
): Seq[Map[Identifier, Interval]] = {
var result: Seq[Map[Identifier, Interval]] = Seq.empty
for ((id, interval) <- toExclude) {
var copy = original
val origInterval = original(id)
if (interval.xlo.<(origInterval.xlo))
if (interval.xhi.>(origInterval.xhi))
// interval to exclude is greater than original
// fixme find a better way
throw new IllegalArgumentException("The resulting interval is empty")
else
// lower bound of interval toExclude is smaller than lower bound of originalInterval
// e.g. exclude [-0.1 ; 0.1] from [0; 10]
{
val tmp = Interval(interval.xhi, origInterval.xhi)
copy = copy + (id -> tmp)
result = result ++ Set(copy)
}
else if (interval.xhi.>(origInterval.xhi))
// upper bound of interval toExclude is greater than upper bound of originalInterval
// e.g. exclude [-0.1 ; 0.1] from [-10; 0]
{
val tmp = Interval(origInterval.xlo, interval.xlo)
copy = copy + (id -> tmp)
result = result ++ Set(copy)
}
else
// general case
{
val tmplo = Interval(origInterval.xlo, interval.xlo)
copy = copy + (id -> tmplo)
result = result ++ Set(copy)
val tmphi = Interval(interval.xhi, origInterval.xhi)
copy = copy + (id -> tmphi)
result = result ++ Set(copy)
}
}
result
}
}
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