Commit 9338eb60 authored by Anastasiia's avatar Anastasiia

do not tighten the range for simple expressions

parent f41148cc
......@@ -98,13 +98,7 @@ object SMTRange {
// reporter.warning(s"Tighten the bounds on $t")
// TODO: massage arithmetic
if (lang.TreeOps.size(t) == 1) {
reporter.warning("Calling tightenRange on simple expression: " + t)
} else {
//print(lang.TreeOps.size(t) + " ")
}
// reporter.info(s"Calling tighten range with $constrs on $t ")
// reporter.info(s"Calling tighten range with $constrs on $t ")
val condition = and(constrs.toSeq :_*)
//val precisionThreshold = Rational.fromReal(0.01)
//val loopThreshold = 10
......@@ -124,7 +118,7 @@ object SMTRange {
// TODO: make this less inefficient, we are creating a new solver each time.
val res = Solver.checkSat(solverQuery)
// reporter.warning(s"Result for the query is $res")
// reporter.warning(s"Result for the query is $res")
res match {
case Some(false) => findLowerBound(mid, hi, loopCount + 1) //UNSAT
case Some(true) => findLowerBound(lo, mid, loopCount + 1) //SAT
......@@ -142,7 +136,7 @@ object SMTRange {
if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
hi
} else {
// reporter.warning(s"HI: ACTUALLY doing something low $lo, hi $hi")
// reporter.warning(s"HI: ACTUALLY doing something low $lo, hi $hi")
val mid = lo + (hi - lo) / two
val solverQuery = And(condition, LessThan(RealLiteral(mid), t))
......@@ -194,22 +188,32 @@ object SMTRange {
}
}
reporter.debug(s"Going to find lower bound starting from [${i.xlo}, ${i.xhi}].")
// it reduces the # of calls to Z3, but not the overall time
// TODO: it seems that these calls are expensive, figure out why
val lowerBound = if (checkTightness && lowerBoundIsTight) {
if (lang.TreeOps.size(t) == 1) {
reporter.warning("Calling tightenRange on simple expression: " + t)
//TODO what to do?
i
} else {
//print(lang.TreeOps.size(t) + " ")
reporter.debug(s"Going to find lower bound starting from [${i.xlo}, ${i.xhi}].")
// it reduces the # of calls to Z3, but not the overall time
// TODO: it seems that these calls are expensive, figure out why
val lowerBound = if (checkTightness && lowerBoundIsTight) {
reporter.info("lower bound is tight")
i.xlo
} else {
findLowerBound(i.xlo, i.xhi, 0)
}
//val lowerBound = findLowerBound(i.xlo, i.xhi, 0)
//val lowerBound = findLowerBound(i.xlo, i.xhi, 0)
reporter.debug(s"Going to find upper bound starting from [${i.xlo}, ${i.xhi}].")
reporter.debug(s"Going to find upper bound starting from [${i.xlo}, ${i.xhi}].")
val upperBound = if (checkTightness && upperBoundIsTight) {
val upperBound = if (checkTightness && upperBoundIsTight) {
reporter.info("upper bound is tight")
i.xhi
} else {
......@@ -217,10 +221,12 @@ object SMTRange {
}
//val upperBound = findUpperBound(i.xlo, i.xhi, 0)
//val upperBound = findUpperBound(i.xlo, i.xhi, 0)
Interval(lowerBound, upperBound)
Interval(lowerBound, upperBound)
}
}
}
......@@ -261,6 +267,8 @@ case class SMTRange private(interval: Interval, tree: Expr, constraints: Set[Exp
def -(y: SMTRange): SMTRange = this.-(y, lowPrecision, lowLoopThreshold)
def *(y: SMTRange): SMTRange = this.*(y, lowPrecision, lowLoopThreshold)
def /(y: SMTRange): SMTRange = this./(y, lowPrecision, lowLoopThreshold)
//todo fix Pow
def ^(n: SMTRange): SMTRange = this.^(n, lowPrecision, lowLoopThreshold)
def squareRoot: SMTRange = this.squareRoot(lowPrecision, lowLoopThreshold)
def +(y: SMTRange, precision: Rational = lowPrecision, maxLoops: Int = lowLoopThreshold): SMTRange = {
......
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