Commit 11e34702 authored by Anastasiia's avatar Anastasiia

dreal evaluate complete expression. draft 1

parent 87f4787e
......@@ -47,7 +47,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
override val description = "computes relative errors directly"
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
ChoiceOptionDef("rel-rangeMethod", "Method to use for range analysis",
Set("affine", "interval", "smtreuse", "smtredo"), "interval"),
Set("affine", "interval", "smtreuse", "smtredo", "smtcomplete"), "interval"),
ParamOptionDef("divLimit", "Max amount of interval divisions", divLimit.toString),
ChoiceOptionDef("subdiv", "Method to subdivide intervals", Set("simple", "model"), "simple"),
ChoiceOptionDef("approach", "Approach for expressions", Set("taylor", "naive"), "taylor"),
......@@ -71,7 +71,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
for (opt <- ctx.options) opt match {
case ParamOption("divLimit", value) => divLimit = value.toInt
case ChoiceOption("rel-rangeMethod", s) => s match {
case "interval" | "affine" | "smtreuse" | "smtredo" =>
case "interval" | "affine" | "smtreuse" | "smtredo" | "smtcomplete" =>
rangeMethod = s
reporter.info(s"using $s")
case _ =>
......@@ -118,11 +118,12 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
// no initial errors
val allIDs = fnc.params.map(_.id)
val inputErrorMap: Map[Identifier, Rational] = allIDs.map( id => (id -> Rational.zero)).toMap
val preconditions = fnc.precondition.get
try {
reporter.info("Evaluating " + fnc.id + "...")
val (relError, tmpList) = approach match {
case "taylor" => getRelErrorTaylorApprox(relErrorExpr, inputValMap, bodyReal, ctx)
case "taylor" => getRelErrorTaylorApprox(relErrorExpr, inputValMap, bodyReal, ctx, preconditions)
case "naive" => getRelErrorNaive(relErrorExpr, inputValMap, bodyReal, ctx)
}
if (relError.isDefined) {
......@@ -169,7 +170,9 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
private def getRelErrorTaylorApprox(relErrorExpr: Expr,
inputValMap: Map[Identifier, Interval],
bodyReal: Expr,
ctx: Context): (Option[Rational], Seq[Map[Identifier, Interval]]) = {
ctx: Context,
precond: Expr
): (Option[Rational], Seq[Map[Identifier, Interval]]) = {
var listFailInterval: Seq[Map[Identifier, Interval]] = Seq.empty
// get intervals subdivision for the complete divLimit
......@@ -199,7 +202,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
val tmpExpr = simplify(Times(replaceDeltasWithZeros(expr), Delta(wrt)))
reporter.debug(s"Evaluate the term $tmpExpr")
val tmpForMax = newSet.par.map(interval => {
val tmp = evaluateOpt(tmpExpr, interval, rangeMethod)
val tmp = evaluateOpt(tmpExpr, interval, rangeMethod, precond)
reporter.debug("err on "+removeDeltasFromMap(interval)+s" is $tmp")
if (tmp.isEmpty)
if (!listFailInterval.contains(interval)) listFailInterval = listFailInterval :+ interval
......@@ -254,7 +257,10 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
(errors.max, listFailInterval)
}
private def evaluateOpt(relErrorExpr: Expr, inputValMap: Map[Identifier, Interval], rangeMethod: String ):Option[Rational] = {
private def evaluateOpt(relErrorExpr: Expr,
inputValMap: Map[Identifier, Interval],
rangeMethod: String,
precond: Expr = null ):Option[Rational] = {
try {
rangeMethod match {
case ("interval") => Some(maxAbs(Evaluators.evalInterval(relErrorExpr, inputValMap)))
......@@ -264,6 +270,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) })).toInterval))
case ("smtredo") => Some(maxAbs(Evaluators.evalSMT(relErrorExpr,
inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) })).toInterval))
case("smtcomplete") => Some(maxAbs(evaluateSMTComplete(relErrorExpr, inputValMap, precond).toInterval))
//case _ => reporter.error("Something went wrong. Unknown range method")
}
}
......@@ -282,9 +289,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
case "affine" =>
errorAffineAffine(bodyReal, inputValMap, inputErrorMap, uniformPrecision)
case "smtreuse" =>
errorSMTAffine(bodyReal, inputValMap, inputErrorMap, uniformPrecision)
case "smtredo" =>
case "smtreuse" | "smtredo" | "smtcomplete" =>
errorSMTAffine(bodyReal, inputValMap, inputErrorMap, uniformPrecision)
case _ =>
......@@ -297,6 +302,14 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
val loopDefault = 100
val loopLower = 75
def evaluateSMTComplete(expr:Expr,
_intMap: Map[Identifier, Interval],
precond: Expr): SMTRange = {
val intMap = _intMap
val interval = Evaluators.evalInterval(expr, intMap)
SMTRange(expr, interval, precond)
}
/**
*This version records the already seen intervals (from identical, repeated subtrees)
*and does not recompute the range.
......
......@@ -27,6 +27,7 @@ object DRealSolver {
solver.emit(SetLogic(QF_NRA))
// solver.emit(SetOption(timeoutOption))
solver.assertConstraint(query)
// context.reporter.warning(s"check sat for $query")
val res = solver.checkSat
solver.free()
res
......@@ -37,7 +38,7 @@ object DRealSolver {
class DRealSolver(context: Context) extends SMTLibSolver(context) {
override def targetName = "dReal"
// TODO make a parameter?
val precision = 0.0000000001
val precision = 0.000000000000000001
val interpreterOpts = Seq("--in", "--precision "+precision)
override protected def emit(cmd: SExpr, rawOut: Boolean = false): SExpr = {
debugOut foreach { o =>
......
......@@ -41,7 +41,8 @@ object Solver {
def setContext(ctx: Context) = {
context = ctx
solver = context.findOption(Main.optionSolver) match {
case Some("dreal") | Some("dReal") => "dreal"
case Some("dreal") | Some("dReal") => context.reporter.info("Using dReal")
"dreal"
case Some("z3") => "z3"
case None => defaultVal
case Some(s) =>
......@@ -330,7 +331,8 @@ abstract class SMTLibSolver(val context: Context) {
case Delta(id) =>
toSMT(e.getType)
// either bindings has the mapping, or else we look in variables.
bindings.getOrElse(id, variables.toB(id))
// reporter.warning(s"delta $id")
bindings.getOrElse(id, SSymbol(id.name)) //variables.toB(id))
case Variable(id) =>
toSMT(e.getType)
......
......@@ -53,6 +53,27 @@ object SMTRange {
SMTRange(tightRange, v, allConstraints)
}
def apply(v: Expr, i: Interval, precondition: Expr): SMTRange = {
val constrs: Set[Expr] = precondition match {
case And(exprs) => exprs.toSet
case x if isBooleanTerm(x) => Set(x)
case _ =>
System.err.println("Calling SMTRange with a non-term constraint." +
"It will be ignored.")
Set[Expr]()
}
val extra = Set(
LessEquals(RealLiteral(i.xlo), v), LessEquals(v, RealLiteral(i.xhi))
)
reporter.debug("evaluate complete expression")
val allConstraints = constrs ++ extra
val tightRange = tightenBounds(i, v, allConstraints, lowPrecision, lowLoopThreshold)
SMTRange(tightRange, v, allConstraints)
}
// This needs to be populated before we can use SMTRange
// It is needed for the reporter inside the solver.
// This is not an ideal solution, but I don't want every SMTRange
......@@ -82,7 +103,7 @@ object SMTRange {
*/
def tightenBounds(i: Interval, t: Expr, constrs: Set[Expr], precisionThreshold: Rational,
loopThreshold: Int): Interval = {
// reporter.warning(s"Tighten the bounds on $t")
// TODO: massage arithmetic
if (lang.TreeOps.size(t) == 1) {
......@@ -97,9 +118,11 @@ object SMTRange {
def findLowerBound(lo: Rational, hi: Rational, loopCount: Int): Rational = {
if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
lo
} else {
// if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
// reporter.warning(s"not doing anything low $lo, hi $hi")
// lo
// } else
{
val mid = lo + (hi - lo) / two
......
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