diff --git a/mytest/Abs.scala b/mytest/Abs.scala
index 5be0d8cf5fb77aba749440ca3901a4b989f8a2fd..bcec4f3737c912707121f071a4d581207a12854b 100644
--- a/mytest/Abs.scala
+++ b/mytest/Abs.scala
@@ -3,9 +3,8 @@ import leon.Utils._
object Abs {
- def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = ({
- require(size <= 5 && /*)
- require(*/isArray(tab, size) && j >= 0 && j < size)
+ def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size <= 5 && isArray(tab, size))
var k = 0
var tabres = Map.empty[Int, Int]
(while(k < size) {
@@ -14,9 +13,17 @@ object Abs {
else
tabres = tabres.updated(k, tab(k))
k = k + 1
- }) invariant(k >= 0 && k <= size && (if(j < k) tabres(j) >= 0 else true))
+ }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
tabres
- }) ensuring(res => res(j) >= 0)
+ }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(isArray(a, size))
+ def rec(i: Int): Boolean = if(i >= size) true else {
+ if(a(i) < 0) false else rec(i+1)
+ }
+ rec(0)
+ }
def isArray(a: Map[Int, Int], size: Int): Boolean = {
if(size < 0)
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index c69f74fa2765c7042985b4f8325a5a70335f85c5..340022195b26fa364d55ac123d0e2c37869ec96b 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -2,8 +2,8 @@ import leon.Utils._
object Bubble {
- def sort(a: Map[Int, Int], size: Int, k: Int, l1: Int, l2: Int): Map[Int, Int] = ({
- require(size <= 5 && size > 0 && k < size - 1 && k >= 0 && l1 < size && l1 >= 0 && l2 < size && l2 >= 0 && isArray(a, size))
+ def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size <= 5 && isArray(a, size))
var i = size - 1
var j = 0
var sortedArray = a
@@ -17,35 +17,49 @@ object Bubble {
}
j = j + 1
}) invariant(
- isArray(sortedArray, size) &&
- j >= 0 &&
j <= i &&
- (if(k >= i) sortedArray(k) <= sortedArray(k+1) else true) &&
- (if(l1 <= i && l2 > i) sortedArray(l1) <= sortedArray(l2) else true)
+ isArray(sortedArray, size) &&
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ partitioned(sortedArray, size, 0, j-1, j, j) &&
+ sorted(sortedArray, size, i, size-1)
)
i = i - 1
}) invariant(
+ i >= 0 &&
isArray(sortedArray, size) &&
- i >= 0 &&
- i < size &&
- (if(k >= i) sortedArray(k) <= sortedArray(k+1) else true) &&
- (if(l1 <= i && l2 > i) sortedArray(l1) <= sortedArray(l2) else true)
+ partitioned(sortedArray, size, 0, i, i+1, size-1) &&
+ sorted(sortedArray, size, i, size-1)
)
sortedArray
- }) ensuring(res => res(k) <= res(k+1))
- //ensuring(res => sorted(res, 0, size-1))
+ }) ensuring(res => sorted(res, size, 0, size-1))
- //def sorted(a: Map[Int, Int], l: Int, u: Int): Boolean = {
- // require(isArray(a, u+1))
- // var k = l
- // var isSorted = true
- // while(k < u) {
- // if(a(k) > a(k+1))
- // isSorted = false
- // k = k + 1
- // }
- // isSorted
- //}
+ def sorted(a: Map[Int, Int], size: Int, l: Int, u: Int): Boolean = {
+ require(isArray(a, size) && l >= 0 && u < size && l <= u)
+ var k = l
+ var isSorted = true
+ while(k <= u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }
+ isSorted
+ }
+
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && l1 <= u1 && u1 < l2 && l2 <= u2 && u2 < size && isArray(a, size))
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ while(i <= u1) {
+ while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j+1
+ }
+ i = i + 1
+ }
+ isPartitionned
+ }
def isArray(a: Map[Int, Int], size: Int): Boolean = {
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index a7438c9e31637e431b1ab14f9dc3db953c8defb9..ac635c2f41ca3f2e688b915557ac3829add21125 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -11,10 +11,16 @@ object FunctionClosure extends Pass {
private var enclosingPreconditions: List[Expr] = Nil
+ private var pathConstraints: List[Expr] = Nil
+ private var newFunDefs: Map[FunDef, FunDef] = Map()
+ //private var
+
def apply(program: Program): Program = {
+ newFunDefs = Map()
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
enclosingPreconditions = fd.precondition.toList
+ pathConstraints = fd.precondition.toList
fd.body = Some(functionClosure(fd.getBody, fd.args.map(_.id).toSet))
})
program
@@ -22,52 +28,64 @@ object FunctionClosure extends Pass {
private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
case l @ LetDef(fd, rest) => {
+
val id = fd.id
val rt = fd.returnType
val varDecl = fd.args
val funBody = fd.getBody
- val previousEnclosingPreconditions = enclosingPreconditions
- enclosingPreconditions = fd.precondition match {
- case Some(pre) => pre :: enclosingPreconditions
- case None => enclosingPreconditions
- }
- val bodyVars: Set[Identifier] = variablesOf(funBody)
- val preconditionVars: Set[Identifier] = enclosingPreconditions.foldLeft(Set[Identifier]())((s, pre) => s ++ variablesOf(pre))
- val vars = bodyVars ++ preconditionVars
- val capturedVars = vars.intersect(bindedVars).toSeq // this should be the variable used that are in the scope
- val freshVars: Map[Identifier, Identifier] = capturedVars.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
+ val precondition = fd.precondition
+ val postcondition = fd.postcondition
+
+ val bodyVars: Set[Identifier] = variablesOf(funBody) ++ variablesOf(precondition.getOrElse(BooleanLiteral(true)))
+ val capturedVars = bodyVars.intersect(bindedVars)// this should be the variable used that are in the scope
+ val (constraints, allCapturedVars) = filterConstraints(capturedVars) //all relevant path constraints
+ val capturedVarsWithConstraints = allCapturedVars.toSeq
+
+ val freshVars: Map[Identifier, Identifier] = capturedVarsWithConstraints.map(v => (v, FreshIdentifier(v.name).setType(v.getType))).toMap
val freshVarsExpr: Map[Expr, Expr] = freshVars.map(p => (p._1.toVariable, p._2.toVariable))
- val freshBody = replace(freshVarsExpr, funBody)
+
val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
val newVarDecls = varDecl ++ extraVarDecls
val newFunId = FreshIdentifier(id.name)
val newFunDef = new FunDef(newFunId, rt, newVarDecls)
- enclosingPreconditions = enclosingPreconditions.map(pre => replace(freshVarsExpr, pre)) //introduce the new variables name for the list of preconditions
- newFunDef.precondition = enclosingPreconditions match {
- case List() => None
- case precs => Some(And(precs))
+
+ val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
+ val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
+ newFunDef.precondition = freshConstraints match {
+ case List() => freshPrecondition
+ case precs => Some(And(freshPrecondition.getOrElse(BooleanLiteral(true)) +: precs))
}
- newFunDef.postcondition = fd.postcondition.map(expr => replace(freshVarsExpr, expr))
+ newFunDef.postcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
+
def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)))
case _ => None
}
+ val freshBody = replace(freshVarsExpr, funBody)
+ val oldPathConstraints = pathConstraints
+ pathConstraints = (precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints).map(e => replace(freshVarsExpr, e))
val recBody = functionClosure(freshBody, bindedVars ++ newVarDecls.map(_.id))
+ pathConstraints = oldPathConstraints
val recBody2 = searchAndReplaceDFS(substFunInvocInDef)(recBody)
newFunDef.body = Some(recBody2)
+
def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
- case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVars.map(_.toVariable)))
+ case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)))
case _ => None
}
- //need to remove the enclosing precondition before considering the rest
- enclosingPreconditions = previousEnclosingPreconditions
val recRest = functionClosure(rest, bindedVars)
val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
LetDef(newFunDef, recRest2).setType(l.getType)
}
+
+ //case fi @ FunctionInvocation(fd, args) => {
+
+ //}
case l @ Let(i,e,b) => {
val re = functionClosure(e, bindedVars)
+ pathConstraints ::= Equals(Variable(i), re)
val rb = functionClosure(b, bindedVars + i)
+ pathConstraints = pathConstraints.tail
Let(i, re, rb).setType(l.getType)
}
case n @ NAryOperator(args, recons) => {
@@ -84,44 +102,40 @@ object FunctionClosure extends Pass {
val r = functionClosure(t, bindedVars)
recons(r).setType(u.getType)
}
- case i @ IfExpr(t1,t2,t3) => {
- val r1 = functionClosure(t1, bindedVars)
- val r2 = functionClosure(t2, bindedVars)
- val r3 = functionClosure(t3, bindedVars)
- IfExpr(r1, r2, r3).setType(i.getType)
+ case i @ IfExpr(cond,then,elze) => {
+ val rCond = functionClosure(cond, bindedVars)
+ pathConstraints ::= rCond
+ val rThen = functionClosure(then, bindedVars)
+ pathConstraints = pathConstraints.tail
+ pathConstraints ::= Not(rCond)
+ val rElze = functionClosure(elze, bindedVars)
+ pathConstraints = pathConstraints.tail
+ IfExpr(rCond, rThen, rElze).setType(i.getType)
}
case m @ MatchExpr(scrut,cses) => sys.error("Will see")//MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPosInfo(m)
case t if t.isInstanceOf[Terminal] => t
case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
}
- //def collectWithPathCondition(matcher: Expr=>Boolean, expression: Expr) : Set[(Seq[Expr],Expr)] = {
- // var collected : Set[(Seq[Expr],Expr)] = Set.empty
-
- // def rec(expr: Expr, path: List[Expr]) : Unit = {
- // if(matcher(expr)) {
- // collected = collected + ((path.reverse, expr))
- // }
-
- // expr match {
- // case Let(i,e,b) => {
- // rec(e, path)
- // rec(b, Equals(Variable(i), e) :: path)
- // }
- // case IfExpr(cond, then, elze) => {
- // rec(cond, path)
- // rec(then, cond :: path)
- // rec(elze, Not(cond) :: path)
- // }
- // case NAryOperator(args, _) => args.foreach(rec(_, path))
- // case BinaryOperator(t1, t2, _) => rec(t1, path); rec(t2, path)
- // case UnaryOperator(t, _) => rec(t, path)
- // case t : Terminal => ;
- // case _ => scala.sys.error("Unhandled tree in collectWithPathCondition : " + expr)
- // }
- // }
-
- // rec(expression, Nil)
- // collected
- //}
+ //filter the list of constraints, only keeping those relevant to the set of variables
+ def filterConstraints(vars: Set[Identifier]): (List[Expr], Set[Identifier]) = {
+ var allVars = vars
+ var newVars: Set[Identifier] = Set()
+ var constraints = pathConstraints
+ var filteredConstraints: List[Expr] = Nil
+ do {
+ allVars ++= newVars
+ newVars = Set()
+ constraints = pathConstraints.filterNot(filteredConstraints.contains(_))
+ constraints.foreach(expr => {
+ val vs = variablesOf(expr)
+ if(!vs.intersect(allVars).isEmpty) {
+ filteredConstraints ::= expr
+ newVars ++= vs.diff(allVars)
+ }
+ })
+ } while(newVars != Set())
+ (filteredConstraints, allVars)
+ }
+
}