Commit d2d2b5c9 authored by Anastasiia's avatar Anastasiia

smtcomplete fixed

parent c457a123
......@@ -118,12 +118,11 @@ 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, preconditions)
case "taylor" => getRelErrorTaylorApprox(relErrorExpr, inputValMap, bodyReal, ctx)
case "naive" => getRelErrorNaive(relErrorExpr, inputValMap, bodyReal, ctx)
}
if (relError.isDefined) {
......@@ -170,9 +169,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
private def getRelErrorTaylorApprox(relErrorExpr: Expr,
inputValMap: Map[Identifier, Interval],
bodyReal: Expr,
ctx: Context,
precond: Expr
): (Option[Rational], Seq[Map[Identifier, Interval]]) = {
ctx: Context ): (Option[Rational], Seq[Map[Identifier, Interval]]) = {
var listFailInterval: Seq[Map[Identifier, Interval]] = Seq.empty
// get intervals subdivision for the complete divLimit
......@@ -202,7 +199,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, precond)
val tmp = evaluateOpt(tmpExpr, interval, rangeMethod)
reporter.debug("err on "+removeDeltasFromMap(interval)+s" is $tmp")
if (tmp.isEmpty)
if (!listFailInterval.contains(interval)) listFailInterval = listFailInterval :+ interval
......@@ -259,8 +256,7 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
private def evaluateOpt(relErrorExpr: Expr,
inputValMap: Map[Identifier, Interval],
rangeMethod: String,
precond: Expr = null ):Option[Rational] = {
rangeMethod: String):Option[Rational] = {
try {
rangeMethod match {
case ("interval") => Some(maxAbs(Evaluators.evalInterval(relErrorExpr, inputValMap)))
......@@ -270,7 +266,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("smtcomplete") => Some(maxAbs(evaluateSMTComplete(relErrorExpr, inputValMap).toInterval))
//case _ => reporter.error("Something went wrong. Unknown range method")
}
}
......@@ -304,12 +300,26 @@ object RelativeErrorPhase extends DaisyPhase with Subdivision with ErrorFunction
def evaluateSMTComplete(expr:Expr,
_intMap: Map[Identifier, Interval],
precond: Expr): SMTRange = {
_intMap: Map[Identifier, Interval]): SMTRange = {
val intMap = _intMap
val interval = Evaluators.evalInterval(expr, intMap)
SMTRange(expr, interval, precond)
// reporter.warning(s"interval is $interval")
//TODO build proper preconditions
var constrs: Set[Expr] = Set.empty
val deltas = deltasOf(expr)
val vars = variablesOf(expr)
intMap.foreach(x => {
val (id, interval) = x
if (deltas.contains(Delta(id)) || vars.contains(id)) {
constrs = constrs ++ SMTRange.toConstraints(Variable(id), interval)
}
})
// reporter.debug(s"preconditions $constrs")
val tmp = SMTRange(expr, interval, constrs)
// reporter.debug(s"AFTER $tmp")
tmp
}
/**
*This version records the already seen intervals (from identical, repeated subtrees)
*and does not recompute the range.
......
......@@ -80,7 +80,7 @@ class DRealInterpreter(executable: String, args: Array[String])
} (ExecutionContext.global)
try {
Await.result(f, 1.second) // TODO parameter?
Await.result(f, 5.second) // TODO parameter?
} catch {
case e: TimeoutException => CheckSatStatus(UnknownStatus)
} finally {
......
......@@ -43,7 +43,7 @@ class DRealSolver(context: Context) extends SMTLibSolver(context) {
override def targetName = "dReal"
// TODO make a parameter?
val precision = 0.0000000001
val precision = 0.000000000000000000001
val interpreterOpts = Seq("--in", "--precision "+precision)
......
......@@ -23,6 +23,7 @@ import lang.Trees._
import lang.Identifiers._
import utils.Bijection
import lang.TreeOps.variablesOf
import lang.TreeOps.deltasOf
import utils.Rational
import Rational._
import lang.Constructors._
......@@ -154,6 +155,9 @@ abstract class SMTLibSolver(val context: Context) {
def assertConstraint(expr: Expr): Unit = {
try {
variablesOf(expr).foreach(declareVariable)
deltasOf(expr).foreach {
case Delta(id) => declareVariable(id)
}
val term = toSMT(expr)(Map())
emit(SMTAssert(term))
} catch {
......@@ -199,8 +203,10 @@ abstract class SMTLibSolver(val context: Context) {
res match {
case CheckSatStatus(SatStatus) => Some(true)
case CheckSatStatus(UnsatStatus) => Some(false)
case CheckSatStatus(UnknownStatus) => None
case e => None
case CheckSatStatus(UnknownStatus) => reporter.warning(s"solver says $res")
None
case e => reporter.warning(s"solver CRIES $res")
None
}
}
......@@ -268,6 +274,7 @@ abstract class SMTLibSolver(val context: Context) {
*/
protected val variables = new Bijection[Identifier, SSymbol]()
protected val deltas = new Bijection[Identifier, SSymbol]()
// in Leon, this is FunDef -> SSymbol
// we may have to do extra work, when mapping back to get the full fnc
protected val functions = new Bijection[Identifier, SSymbol]()
......@@ -331,8 +338,9 @@ abstract class SMTLibSolver(val context: Context) {
case Delta(id) =>
toSMT(e.getType)
// either bindings has the mapping, or else we look in variables.
// reporter.warning(s"delta $id")
bindings.getOrElse(id, SSymbol(id.name)) //variables.toB(id))
val name = id.uniqueNameDelimited("!")
// reporter.debug(s"delta $name")
bindings.getOrElse(id, SSymbol(name))
case Variable(id) =>
toSMT(e.getType)
......
......@@ -19,6 +19,8 @@ object SMTRange {
val lowPrecision = Rational.fromReal(0.01)
val lowLoopThreshold = 20
val highPrecision = Rational.fromReal(0.00000000000000000001)
val highLoopThreshold = 100
def toConstraints(v: Variable, i: Interval): Set[Expr] = {
Set(
......@@ -53,24 +55,14 @@ 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]()
}
def apply(v: Expr, i: Interval, precondition: Set[Expr]): SMTRange = {
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)
val allConstraints = precondition ++ extra
val tightRange = tightenBounds(i, v, allConstraints, highPrecision, highLoopThreshold)
SMTRange(tightRange, v, allConstraints)
}
......@@ -112,18 +104,17 @@ object SMTRange {
//print(lang.TreeOps.size(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
def findLowerBound(lo: Rational, hi: Rational, loopCount: Int): Rational = {
// if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
// reporter.warning(s"not doing anything low $lo, hi $hi")
// lo
// } else
if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
lo
} else
{
val mid = lo + (hi - lo) / two
val solverQuery = And(condition, LessThan(t, RealLiteral(mid)))
......@@ -133,7 +124,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")
res match {
case Some(false) => findLowerBound(mid, hi, loopCount + 1) //UNSAT
case Some(true) => findLowerBound(lo, mid, loopCount + 1) //SAT
......@@ -151,7 +142,7 @@ object SMTRange {
if (hi - lo <= precisionThreshold || loopCount >= loopThreshold) {
hi
} else {
// 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))
......
......@@ -7,9 +7,9 @@ import Real._
object Summation {
def summ(u: Real, v: Real): Real = { //
require(-2.0 <= u && u <= 10 && -1 <= v && v <= 10)//
require(2.0 <= u && u <= 10 && 1 <= v && v <= 10)//
u + v
u + u * u
}
......
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