diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index 0848ccbb487679dcaf07892b4d39c8ba4edf6942..3ffb5c532d19313b17747ff546609e9402739c7e 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -13,7 +13,6 @@ import BigInt._
import PredicateUtil._
import Stats._
-
class NotImplementedException(message: String) extends RuntimeException(message)
//a collections of utility methods that manipulate the templates
@@ -93,21 +92,21 @@ object LinearConstraintUtil {
//the top most operator should be a relation
val Operator(Seq(lhs, InfiniteIntegerLiteral(x)), op) = makeLinear(expr)
/*if (lhs.isInstanceOf[InfiniteIntegerLiteral])
- throw new IllegalStateException("relation on two integers, not in canonical form: " + linearExpr)*/
+ throw new IllegalStateException("relation on two integers, not in canonical form: " + linearExpr)*/
//handle each minterm
getMinTerms(lhs).foreach(minterm => minterm match {
- case _ if (isTemplateExpr(minterm)) => addConstant(minterm)
- case Times(e1, e2) =>
+ case _ if (isTemplateExpr(minterm)) => addConstant(minterm)
+ case Times(e1, e2) =>
e2 match {
- case Variable(_) | ResultVariable(_) | FunctionInvocation(_, _) =>
+ case Variable(_) | ResultVariable(_) | FunctionInvocation(_, _) =>
case _ => throw new IllegalStateException("Multiplicand not a constraint variable: " + e2)
}
- e1 match {
- case _ if (isTemplateExpr(e1)) => addCoefficient(e2, e1)
+ e1 match {
+ case _ if (isTemplateExpr(e1)) => addCoefficient(e2, e1)
case _ => throw new IllegalStateException("Coefficient not a constant or template expression: " + e1)
- }
- case Variable(_) => addCoefficient(minterm, one) //here the coefficient is 1
- case ResultVariable(_) => addCoefficient(minterm, one)
+ }
+ case Variable(_) => addCoefficient(minterm, one) //here the coefficient is 1
+ case ResultVariable(_) => addCoefficient(minterm, one)
case _ => throw new IllegalStateException("Unhandled min term: " + minterm)
})
@@ -142,14 +141,14 @@ object LinearConstraintUtil {
case RealMinus(e1, e2) => Plus(pushMinus(e1), e2)
case Plus(e1, e2) => Plus(pushMinus(e1), pushMinus(e2))
case RealPlus(e1, e2) => Plus(pushMinus(e1), pushMinus(e2))
- case Times(e1, e2) =>
+ case Times(e1, e2) =>
//here push the minus in to the coefficient which is the first argument
- Times(pushMinus(e1), e2)
+ Times(pushMinus(e1), e2)
case RealTimes(e1, e2) => Times(pushMinus(e1), e2)
case _ => throw new NotImplementedException("pushMinus -- Operators not yet handled: " + inExpr)
}
}
-
+
//we assume that ine is in linear form
def pushTimes(mul: Expr, ine: Expr): Expr = {
val isReal = ine.getType == RealType && mul.getType == RealType
@@ -165,9 +164,9 @@ object LinearConstraintUtil {
val r2 = pushTimes(mul, e2)
if (isReal) RealPlus(r1, r2)
else Plus(r1, r2)
- case Times(e1, e2) =>
+ case Times(e1, e2) =>
//here push the times into the coefficient which should be the first expression
- Times(pushTimes(mul, e1), e2)
+ Times(pushTimes(mul, e1), e2)
case RealTimes(e1, e2) =>
val r = pushTimes(mul, e1)
if (isReal) RealTimes(r, e2)
@@ -205,21 +204,21 @@ object LinearConstraintUtil {
|| e.isInstanceOf[GreaterEquals])) => {
//check if the expression has real valued sub-expressions
- val isReal = hasReals(e1) || hasReals(e2)
+ val isReal = hasReals(e1) || hasReals(e2)
val (newe, newop) = e match {
case t: Equals => (Minus(e1, e2), Equals)
case t: LessEquals => (Minus(e1, e2), LessEquals)
case t: GreaterEquals => (Minus(e2, e1), LessEquals)
- case t: LessThan =>
+ case t: LessThan =>
if (isReal)
(Minus(e1, e2), LessThan)
else
- (Plus(Minus(e1, e2), one), LessEquals)
- case t: GreaterThan =>
+ (Plus(Minus(e1, e2), one), LessEquals)
+ case t: GreaterThan =>
if (isReal)
(Minus(e2, e1), LessThan)
else
- (Plus(Minus(e2, e1), one), LessEquals)
+ (Plus(Minus(e2, e1), one), LessEquals)
}
val r = mkLinearRecur(newe)
//simplify the resulting constants
@@ -227,7 +226,7 @@ object LinearConstraintUtil {
val finale = if (r2.isDefined) {
if (const != 0) Plus(r2.get, InfiniteIntegerLiteral(const))
else r2.get
- } else InfiniteIntegerLiteral(const)
+ } else InfiniteIntegerLiteral(const)
newop(finale, zero)
}
case Minus(e1, e2) => Plus(mkLinearRecur(e1), pushMinus(mkLinearRecur(e2)))
@@ -237,15 +236,15 @@ object LinearConstraintUtil {
case Times(_, _) | RealTimes(_, _) => {
val Operator(Seq(e1, e2), op) = inExpr
val (r1, r2) = (mkLinearRecur(e1), mkLinearRecur(e2))
- if (isTemplateExpr(r1))
+ if (isTemplateExpr(r1))
pushTimes(r1, r2)
- else if (isTemplateExpr(r2))
+ else if (isTemplateExpr(r2))
pushTimes(r2, r1)
else
throw new IllegalStateException("Expression not linear: " + Times(r1, r2))
}
case Plus(e1, e2) => Plus(mkLinearRecur(e1), mkLinearRecur(e2))
- case rp @ RealPlus(e1, e2) =>
+ case rp @ RealPlus(e1, e2) =>
RealPlus(mkLinearRecur(e1), mkLinearRecur(e2))
case t: Terminal => t
case fi: FunctionInvocation => fi
@@ -316,7 +315,7 @@ object LinearConstraintUtil {
restctrs += lc
case _ => throw new IllegalStateException("LinearConstraint not in expeceted form : " + lc.toExpr)
}
- }
+ }
// sort 'eqctrs' by the size of the constraints so that we use smaller expressions in 'subst' map.
var currEqs = eqctrs.sortBy(eqc => eqc.coeffMap.keySet.size + (if (eqc.const.isDefined) 1 else 0))
// compute the subst map recursively
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index f5a10ad83e77b6acdb743b3804dfbec00687d59f..f1fedec33f8502ba17e6364c75941bded8fbd21a 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -46,14 +46,14 @@ _
object LazinessEliminationPhase extends TransformationPhase {
val debugLifting = false
val dumpInputProg = false
- val dumpLiftProg = true
- val dumpProgramWithClosures = true
+ val dumpLiftProg = false
+ val dumpProgramWithClosures = false
val dumpTypeCorrectProg = false
- val dumpProgWithPreAsserts = true
- val dumpProgWOInstSpecs = true
- val dumpInstrumentedProgram = true
+ val dumpProgWithPreAsserts = false
+ val dumpProgWOInstSpecs = false
+ val dumpInstrumentedProgram = false
val debugSolvers = false
- val skipStateVerification = true
+ val skipStateVerification = false
val skipResourceVerification = false
val name = "Laziness Elimination Phase"
diff --git a/testcases/lazy-datastructures/conc/ConcTrees.scala b/testcases/lazy-datastructures/conc/ConcTrees.scala
index 61dd75f8c9a549bda06d7b8eca8bbc40dc4a903a..c8b007f14b60787c5212728443a80627e932207b 100644
--- a/testcases/lazy-datastructures/conc/ConcTrees.scala
+++ b/testcases/lazy-datastructures/conc/ConcTrees.scala
@@ -14,7 +14,6 @@ object ConcTrees {
@inline
def max(x: BigInt, y: BigInt): BigInt = if (x >= y) x else y
- //@inline
def abs(x: BigInt): BigInt = if (x < 0) -x else x
sealed abstract class Conc[T] {
@@ -94,47 +93,6 @@ object ConcTrees {
override def toString = s"Chunk(${array.mkString("", ", ", "")}; $size; $k)"
}*/
- @invisibleBody
- def concatNonEmpty[T](xs: Conc[T], ys: Conc[T]): Conc[T] = {
- require(xs.valid && ys.valid && !xs.isEmpty && !ys.isEmpty)
- val diff = ys.level - xs.level
- if (diff >= -1 && diff <= 1) CC(xs, ys)
- else if (diff < -1) { // ys is smaller than xs
- xs match {
- case CC(l, r) if (l.level >= r.level) =>
- CC(l, concatNonEmpty(r, ys))
- case CC(l, r) =>
- r match {
- case CC(rl, rr) =>
- val nrr = concatNonEmpty(rr, ys)
- if (nrr.level == xs.level - 3)
- CC(l, CC(rl, nrr))
- else
- CC(CC(l, rl), nrr)
- }
- }
- } else ys match {
- case CC(l, r) if (r.level >= l.level) =>
- CC(concatNonEmpty(xs, l), r)
- case CC(l, r) =>
- l match {
- case CC(ll, lr) =>
- val nll = concatNonEmpty(xs, ll)
- if (nll.level == ys.level - 3)
- CC(CC(nll, lr), r)
- else
- CC(nll, CC(lr, r))
- }
- }
- } ensuring (res =>
- res.level <= max(xs.level, ys.level) + 1 && // height invariants
- res.level >= max(xs.level, ys.level) &&
- //res.balanced && res.concInv && // tree invariant is preserved
- res.valid &&
- appendAssocInst(xs, ys) && // instantiation of an axiom
- res.toList == xs.toList ++ ys.toList && // correctness
- time <= ? * abs(xs.level - ys.level) + ?) // time bounds
-
@invisibleBody
def lookup[T](xs: Conc[T], i: BigInt): T = {
require(xs.valid && !xs.isEmpty && i >= 0 && i < xs.size)
@@ -185,6 +143,55 @@ object ConcTrees {
}
}.holds
+ /**
+ * A generic concat that applies to general concTrees
+ */
+ // @invisibleBody
+ // def concat[T](xs: Conc[T], ys: Conc[T]): Conc[T] = {
+ // require(xs.valid && ys.valid)
+ // concatNormalized(normalize(xs), normalize(ys))
+ // }
+
+ @invisibleBody
+ def concatNonEmpty[T](xs: Conc[T], ys: Conc[T]): Conc[T] = {
+ require(xs.valid && ys.valid && !xs.isEmpty && !ys.isEmpty)
+ val diff = ys.level - xs.level
+ if (diff >= -1 && diff <= 1) CC(xs, ys)
+ else if (diff < -1) { // ys is smaller than xs
+ xs match {
+ case CC(l, r) if (l.level >= r.level) =>
+ CC(l, concatNonEmpty(r, ys))
+ case CC(l, r) =>
+ r match {
+ case CC(rl, rr) =>
+ val nrr = concatNonEmpty(rr, ys)
+ if (nrr.level == xs.level - 3)
+ CC(l, CC(rl, nrr))
+ else
+ CC(CC(l, rl), nrr)
+ }
+ }
+ } else ys match {
+ case CC(l, r) if (r.level >= l.level) =>
+ CC(concatNonEmpty(xs, l), r)
+ case CC(l, r) =>
+ l match {
+ case CC(ll, lr) =>
+ val nll = concatNonEmpty(xs, ll)
+ if (nll.level == ys.level - 3)
+ CC(CC(nll, lr), r)
+ else
+ CC(nll, CC(lr, r))
+ }
+ }
+ } ensuring (res =>
+ res.level <= max(xs.level, ys.level) + 1 && // height invariants
+ res.level >= max(xs.level, ys.level) &&
+ res.valid &&
+ appendAssocInst(xs, ys) && // instantiation of an axiom
+ concatCorrectness(res, xs, ys) && // correctness
+ time <= ? * abs(xs.level - ys.level) + ?) // time bounds
+
@invisibleBody
def appendAssocInst[T](xs: Conc[T], ys: Conc[T]): Boolean = {
(xs match {
@@ -211,15 +218,6 @@ object ConcTrees {
})
}.holds
- /**
- * A generic concat that applies to general concTrees
- */
- // @invisibleBody
- // def concat[T](xs: Conc[T], ys: Conc[T]): Conc[T] = {
- // require(xs.valid && ys.valid)
- // concatNormalized(normalize(xs), normalize(ys))
- // }
-
/**
* This concat applies only to normalized trees.
* This prevents concat from being recursive
@@ -235,28 +233,32 @@ object ConcTrees {
} ensuring (res => res.valid && // tree invariants
res.level <= max(xs.level, ys.level) + 1 && // height invariants
res.level >= max(xs.level, ys.level) &&
- (res.toList == xs.toList ++ ys.toList) && // correctness
- time <= ? * abs(xs.level - ys.level) + ?)
+ concatCorrectness(res, xs, ys) && // correctness
+ time <= ? * abs(xs.level - ys.level) + ?)
+
+ @invisibleBody
+ def concatCorrectness[T](res: Conc[T], xs: Conc[T], ys: Conc[T]): Boolean =
+ (res.toList == xs.toList ++ ys.toList)
@invisibleBody
- def insert[T](xs: Conc[T], i: BigInt, y: T): Conc[T] = {
+ def insert[T](xs: Conc[T], i: BigInt, y: T): Conc[T] = {
require(xs.valid && i >= 0 && i <= xs.size) //note the precondition
xs match {
case Empty() => Single(y)
case Single(x) =>
if (i == 0) CC(Single(y), xs)
else CC(xs, Single(y))
- case CC(l, r) if i < l.size =>
+ case CC(l, r) if i < l.size =>
concatNonEmpty(insert(l, i, y), r)
- case CC(l, r) =>
+ case CC(l, r) =>
concatNonEmpty(l, insert(r, i - l.size, y))
}
- } ensuring (res =>
+ } ensuring (res =>
res.valid && // tree invariants
res.level - xs.level <= 1 && res.level >= xs.level && // height of the output tree is at most 1 greater than that of the input tree
!res.isEmpty &&
insertAppendAxiomInst(xs, i, y) && // instantiation of an axiom
- res.toList == insertAtIndex(xs.toList, i, y) && // correctness
+ res.toList == insertAtIndex(xs.toList, i, y) && // correctness
time <= ? * xs.level + ? // time is linear in the height of the tree
)
@@ -301,33 +303,37 @@ object ConcTrees {
}
}.holds
- //TODO: why with instrumentation we are not able prove the running time here ? (performance bug ?)
@invisibleBody
def split[T](xs: Conc[T], n: BigInt): (Conc[T], Conc[T]) = {
require(xs.valid)
xs match {
case Empty() => (Empty[T](), Empty[T]())
case s @ Single(x) =>
- if (n <= 0) (Empty[T](), s) //a minor fix
- else (s, Empty[T]())
+ if (n <= 0) (Empty[T](), s) //a minor fix
+ else (s, Empty[T]())
case CC(l, r) =>
if (n < l.size) {
- val (ll, lr) = split(l, n)
+ val (ll, lr) = split(l, n)
(ll, concatNormalized(lr, r))
} else if (n > l.size) {
- val (rl, rr) = split(r, n - l.size)
+ val (rl, rr) = split(r, n - l.size)
(concatNormalized(l, rl), rr)
} else {
(l, r)
}
- }
+ }
} ensuring (res => res._1.valid && res._2.valid && // tree invariants are preserved
xs.level >= res._1.level && xs.level >= res._2.level && // height bounds of the resulting tree
instSplitAxiom(xs, n) && // instantiation of an axiom
- res._1.toList == xs.toList.take(n) && res._2.toList == xs.toList.drop(n) && // correctness
+ splitCorrectness(res, xs, n) &&
time <= ? * xs.level + ? * res._1.level + ? * res._2.level + ? // time is linear in height
)
+ @invisibleBody
+ def splitCorrectness[T](r: (Conc[T], Conc[T]), xs: Conc[T], n: BigInt): Boolean = {
+ r._1.toList == xs.toList.take(n) && r._2.toList == xs.toList.drop(n)
+ }
+
@invisibleBody
def instSplitAxiom[T](xs: Conc[T], n: BigInt): Boolean = {
xs match {