diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index a616a1a0b77f3a36f35e3ebba4624e5f9ccb35a8..33975a011737d50a45d1511b108d4a2025208eb7 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -183,7 +183,7 @@ trait CodeGeneration {
// An offset we introduce to the parameters:
// 1 if this is a method, so we need "this" in position 0 of the stack
// 1 if we are monitoring
- val idParams = (if (requireMonitor) Seq(monitorID) else Seq.empty) ++ funDef.params.map(_.id)
+ val idParams = (if (requireMonitor) Seq(monitorID) else Seq.empty) ++ funDef.paramIds
val newMapping = idParams.zipWithIndex.toMap.mapValues(_ + (if (!isStatic) 1 else 0))
val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name))
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 6467226a0a788866891cad6ec183a89569bc5a66..ba6b11bcf49398e4a9ff1456aa4d7bffc734d2a8 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -483,7 +483,7 @@ object Definitions {
def paramSubst(realArgs: Seq[Expr]) = {
require(realArgs.size == params.size)
- (params map { _.id } zip realArgs).toMap
+ (paramIds zip realArgs).toMap
}
def withParamSubst(realArgs: Seq[Expr], e: Expr) = {
@@ -522,6 +522,8 @@ object Definitions {
lazy val returnType: TypeTree = translated(fd.returnType)
+ lazy val paramIds = params map { _.id }
+
private var trCache = Map[Expr, Expr]()
private def cached(e: Expr): Expr = {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 30999a647dc613a959ce8a3d95f2cf491bae24df..2f703312a0f1e064ed9af3d1f6f094d5d6f96bbc 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -513,7 +513,7 @@ object ExprOps {
(expr, idSeqs) => idSeqs.foldLeft(expr match {
case Lambda(args, _) => args.map(_.id)
case Forall(args, _) => args.map(_.id)
- case LetDef(fd, _) => fd.params.map(_.id)
+ case LetDef(fd, _) => fd.paramIds
case Let(i, _, _) => Seq(i)
case MatchExpr(_, cses) => cses.flatMap(_.pattern.binders)
case Passes(_, _, cses) => cses.flatMap(_.pattern.binders)
@@ -1511,7 +1511,7 @@ object ExprOps {
(fd1.params.size == fd2.params.size) && {
val newMap = map +
(fd1.id -> fd2.id) ++
- (fd1.params zip fd2.params).map{ case (vd1, vd2) => (vd1.id, vd2.id) }
+ (fd1.paramIds zip fd2.paramIds)
isHomo(fd1.fullBody, fd2.fullBody)(newMap)
}
}
@@ -1777,14 +1777,14 @@ object ExprOps {
def flattenFunctions(fdOuter: FunDef, ctx: LeonContext, p: Program): FunDef = {
fdOuter.body match {
case Some(LetDef(fdInner, FunctionInvocation(tfdInner2, args))) if fdInner == tfdInner2.fd =>
- val argsDef = fdOuter.params.map(_.id)
+ val argsDef = fdOuter.paramIds
val argsCall = args.collect { case Variable(id) => id }
if (argsDef.toSet == argsCall.toSet) {
val defMap = argsDef.zipWithIndex.toMap
val rewriteMap = argsCall.map(defMap)
- val innerIdsToOuterIds = (fdInner.params.map(_.id) zip argsCall).toMap
+ val innerIdsToOuterIds = (fdInner.paramIds zip argsCall).toMap
def pre(e: Expr) = e match {
case FunctionInvocation(tfd, args) if tfd.fd == fdInner =>
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 1214af2aa9526abf1f7adb9b875d7829fd2720cf..38fa0ae9f81190096aa4f19cbd5a5a988dbfb249 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -108,7 +108,7 @@ object Quantification {
case _ => Set.empty
} (fd.fullBody)
- val free = fd.params.map(_.id).toSet ++ (fd.postcondition match {
+ val free = fd.paramIds.toSet ++ (fd.postcondition match {
case Some(Lambda(args, _)) => args.map(_.id)
case _ => Seq.empty
})
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 47dc7abac071490e5d9408512413c80d23050185..e5a1eaafe1a73c439a846d0c344e489924edf6eb 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -180,7 +180,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val vrs = report.vrs
vrs.collect { case (_, VCResult(VCStatus.Invalid(ex), _, _)) =>
- InExample(fd.params.map{vd => ex(vd.id)})
+ InExample(fd.paramIds map ex)
}
} finally {
solverf.shutdown()
@@ -203,7 +203,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
case None =>
_ => true
case Some(pre) =>
- val argIds = fd.params.map(_.id)
+ val argIds = fd.paramIds
evaluator.compile(pre, argIds) match {
case Some(evalFun) =>
val sat = EvaluationResults.Successful(BooleanLiteral(true));
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index ba0187239bbd71e75cc656928fa451fa308b809c..bfcb706689062da6659b882c3672bd0e9088d4cd 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -21,7 +21,7 @@ trait SMTLIBQuantifiedSolver {
// Normally, UnrollingSolver tracks the input variable, but this one
// is invoked alone so we have to filter them here
override def getModel: Model = {
- val filter = currentFunDef.map{ _.params.map{_.id}.toSet }.getOrElse( (_:Identifier) => true )
+ val filter = currentFunDef.map{ _.paramIds.toSet }.getOrElse( (_:Identifier) => true )
getModel(filter)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index b6d6fbfb313a15deb9030424da48ba56a65c4524..d49e3316716ae2277af5ea35c6115d076e7029bd 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -30,7 +30,7 @@ trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
val inductiveHyps = for {
fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
} yield {
- val formalToRealArgs = tfd.params.map{ _.id}.zip(args).toMap
+ val formalToRealArgs = tfd.paramIds.zip(args).toMap
val post = tfd.postcondition map { post =>
application(
replaceFromIDs(formalToRealArgs, post),
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 4c8eedce5fb981ff037349eba6b0f6e69d595e88..f3c7cb69e83490f25c6b8dec79d082cb6f8f2c75 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -37,7 +37,7 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarge
val tfd = functions.toA(sym)
val term = quantifiedTerm(
SMTForall,
- tfd.params map { _.id },
+ tfd.paramIds,
Equals(
FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
tfd.body.get
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 5c746db2f7377d2900afcba807febbeda0e85e62..f6484ff7be0152f316d8cf911c56a94320fade5a 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -44,7 +44,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
val newBody : Option[Expr] = tfd.body.map(b => matchToIfThenElse(b))
val lambdaBody : Option[Expr] = newBody.map(b => simplifyHOFunctions(b))
- val funDefArgs: Seq[Identifier] = tfd.params.map(_.id)
+ val funDefArgs: Seq[Identifier] = tfd.paramIds
val lambdaArguments: Seq[Identifier] = lambdaBody.map(lambdaArgs).toSeq.flatten
val invocation : Expr = FunctionInvocation(tfd, funDefArgs.map(_.toVariable))