diff --git a/src/main/scala/leon/invariant/engine/RefinementEngine.scala b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
index 3d849ac4684aee0efca93f75b43b17b8d64ff0d7..0c5189072dba45957c9c8a3d8a7ea7c9e0cdbe61 100644
--- a/src/main/scala/leon/invariant/engine/RefinementEngine.scala
+++ b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
@@ -152,7 +152,7 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
reporter.info("Creating VC for " + recFun.id)
// instantiate the body with new types
val tparamMap = (recFun.tparams zip recFunTyped.tps).toMap
- val paramMap = recFun.params.map{pdef =>
+ val paramMap = recFun.params.map { pdef =>
pdef.id -> FreshIdentifier(pdef.id.name, instantiateType(pdef.id.getType, tparamMap))
}.toMap
val freshBody = instantiateType(freshenLocals(recFun.body.get), tparamMap, paramMap)
@@ -186,14 +186,12 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
//here inline the body and conjoin it with the guard
//Important: make sure we use a fresh body expression here, and freshenlocals
val tparamMap = (callee.tparams zip tfd.tps).toMap
- val freshBody = instantiateType(freshenLocals(callee.body.get), tparamMap, Map())
- val calleeSummary = Equals(getFunctionReturnVariable(callee), freshBody)
- val argmap1 = formalToActual(call)
- val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
-
+ val freshBody = instantiateType(replace(formalToActual(call),
+ Equals(getFunctionReturnVariable(callee), freshenLocals(callee.body.get))),
+ tparamMap, Map())
+ val inlinedSummary = ExpressionTransformer.normalizeExpr(freshBody, ctx.multOp)
if (this.dumpInlinedSummary)
- println(s"Inlined Summary of ${callee.id}: " + inlinedSummary)
-
+ println(s"Call: ${call} \n FunDef: $callee \n Inlined Summary of ${callee.id}: $inlinedSummary")
//conjoin the summary with the disjunct corresponding to the 'guard'
//note: the parents of the summary are the parents of the call plus the callee function
formula.conjoinWithDisjunct(calldata.guard, inlinedSummary, (callee +: calldata.parents), calldata.inSpec)
diff --git a/src/main/scala/leon/invariant/engine/SpecInstantiator.scala b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
index dfd5292f4c8d7be528d72e652dd929e9b0a221d5..4e6de1675701345d31b0b9d85829f50250678641 100644
--- a/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
+++ b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
@@ -112,26 +112,25 @@ class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: Cons
}
def specForCall(call: Call): Option[Expr] = {
- val argmap = formalToActual(call)
val tfd = call.fi.tfd
val callee = tfd.fd
if (callee.hasPostcondition) {
+ //get the postcondition without templates
+ val rawpost = freshenLocals(callee.getPostWoTemplate)
+ val rawspec =
+ if (callee.hasPrecondition) {
+ val pre = freshenLocals(callee.precondition.get)
+ if (ctx.assumepre)
+ And(pre, rawpost)
+ else
+ Implies(pre, rawpost)
+ } else {
+ rawpost
+ }
// instantiate the post
val tparamMap = (callee.tparams zip tfd.tps).toMap
- val trans = freshenLocals _ andThen (e => instantiateType(e, tparamMap, Map()))
- //get the postcondition without templates
- val rawpost = trans(callee.getPostWoTemplate)
- val rawspec = if (callee.hasPrecondition) {
- val pre = trans(callee.precondition.get)
- if (ctx.assumepre)
- And(pre, rawpost)
- else
- Implies(pre, rawpost)
- } else {
- rawpost
- }
- val spec = replace(argmap, rawspec)
- val inlinedSpec = ExpressionTransformer.normalizeExpr(spec, ctx.multOp)
+ val instSpec = instantiateType(replace(formalToActual(call), rawspec), tparamMap, Map())
+ val inlinedSpec = ExpressionTransformer.normalizeExpr(instSpec, ctx.multOp)
Some(inlinedSpec)
} else {
None
@@ -144,14 +143,13 @@ class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: Cons
if (callee.hasTemplate) {
val argmap = formalToActual(call)
val tparamMap = (callee.tparams zip tfd.tps).toMap
- val tempExpr = replace(argmap, instantiateType(callee.getTemplate, tparamMap, Map()))
+ val tempExpr = instantiateType(replace(argmap, freshenLocals(callee.getTemplate)), tparamMap, Map())
val template = if (callee.hasPrecondition) {
- val pre = replace(argmap, instantiateType(callee.precondition.get, tparamMap, Map()))
- val freshPre = freshenLocals(pre)
+ val pre = instantiateType(replace(argmap, freshenLocals(callee.precondition.get)), tparamMap, Map())
if (ctx.assumepre)
- And(freshPre, tempExpr)
+ And(pre, tempExpr)
else
- Implies(freshPre, tempExpr)
+ Implies(pre, tempExpr)
} else {
tempExpr
}
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 79448c7c505b53ffbf7ee57f8b2f8bbd26409ee0..7a5dd39a921944d067697dc7eef721a172ba56c7 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -33,7 +33,7 @@ import PredicateUtil._
import SolverUtil._
object NLTemplateSolver {
- val verbose = false
+ val verbose = true
}
class NLTemplateSolver(ctx: InferenceContext, program: Program,
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index 90064561d1da3382384e9835482faa80c0786d17..858b1fec28e5aff3d307ca485006c7673dae3dc7 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -33,12 +33,19 @@ object LazinessUtil {
val outputFile = s"$outputFolder${File.separator}${u.id.toString}$suffix.scala"
try {
val out = new BufferedWriter(new FileWriter(outputFile))
+ val plainText = ScalaPrinter.apply(u, purescala.PrinterOptions(printUniqueIds = uniqueIds))
+ //println("Plain text: "+plainText)
// remove '@' from the end of the identifier names
val pat = new Regex("""(\w+)(@)(\w*)(\*?)(\S*)""", "base", "at", "mid", "star", "rest")
- val pgmText = pat.replaceAllIn(ScalaPrinter.apply(u, purescala.PrinterOptions(printUniqueIds = uniqueIds)),
- m => m.group("base") + m.group("mid") + (
- if (!m.group("star").isEmpty()) "S" else "") + m.group("rest"))
- //val pgmText = ScalaPrinter.apply(p)
+
+ val pgmText = try{ pat.replaceAllIn(plainText,
+ m => {
+ m.group("base") + m.group("mid") + (
+ if (!m.group("star").isEmpty()) "S" else "") + m.group("rest")
+ })
+ } catch {
+ case _: IndexOutOfBoundsException => plainText
+ }
out.write(pgmText)
out.close()
} catch {
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index 864f3ff285df43a9d49452c183b40b3874980f30..00007decdb1927a298a584d7c0dc775284bcfc79 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -18,7 +18,7 @@ import invariant.engine._
object LazyVerificationPhase {
val debugInstVCs = false
- val debugInferProgram = false
+ val debugInferProgram = true
class LazyVerificationReport(val stateVerification: Option[VerificationReport],
val resourceVeri: Option[VerificationReport]) {
diff --git a/src/main/scala/leon/verification/TraceInductionTactic.scala b/src/main/scala/leon/verification/TraceInductionTactic.scala
index 3177f70e8c2e1545b251acb7497cf3ad8d94cd26..f1c7b455d359e61708a9c5e6e773031bd3756b86 100644
--- a/src/main/scala/leon/verification/TraceInductionTactic.scala
+++ b/src/main/scala/leon/verification/TraceInductionTactic.scala
@@ -145,8 +145,7 @@ class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) {
}
val argsMap = callee.params.map(_.id).zip(finv.args).toMap
val tparamMap = callee.tparams.zip(finv.tfd.tps).toMap
- val inlinedBody = replaceFromIDs(argsMap,
- instantiateType(callee.body.get, tparamMap, Map()))
+ val inlinedBody = instantiateType(replaceFromIDs(argsMap, callee.body.get), tparamMap, Map())
val inductScheme = inductPattern(inlinedBody)
// add body, pre and post for the tactFun
tactFun.body = Some(createAnd(Seq(inductScheme, prop)))
diff --git a/src/test/resources/regression/verification/purescala/valid/TraceInductTacticTest.scala b/src/test/resources/regression/verification/purescala/valid/TraceInductTacticTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..46a2bdecae4dbfc0f3446dfe5335ed1055b4f6dd
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/TraceInductTacticTest.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+
+object TraceInductTacticTest {
+
+ def contains(l: List[BigInt], set: Set[BigInt]): Boolean = {
+ l match {
+ case Cons(x, xs) => set.contains(x) && contains(xs, set)
+ case Nil() => true
+ }
+ }
+
+ @traceInduct
+ def monotonicity(l: List[BigInt], set1: Set[BigInt], set2: Set[BigInt]): Boolean = {
+ (contains(l, set1) && set1.subsetOf(set2)) ==> contains(l, set2)
+ } holds
+}