From 48f7ffc1eaae5f5af0f8e5baaaf26b30844c196b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 24 Feb 2015 15:52:44 +0100
Subject: [PATCH] Remove MutableTyped from Identifiers and eliminate it
completely
---
.../scala/leon/datagen/VanuatooDataGen.scala | 4 +--
.../frontends/scalac/CodeExtraction.scala | 26 +++++++-------
src/main/scala/leon/purescala/Common.scala | 14 +++++---
.../CompleteAbstractDefinitions.scala | 2 +-
.../scala/leon/purescala/Constructors.scala | 2 +-
.../scala/leon/purescala/Definitions.scala | 4 +--
.../leon/purescala/FunctionClosure.scala | 6 ++--
.../scala/leon/purescala/MethodLifting.scala | 4 +--
.../leon/purescala/ScopeSimplifier.scala | 2 +-
src/main/scala/leon/purescala/TreeOps.scala | 24 +++++++------
src/main/scala/leon/purescala/Trees.scala | 11 ++++--
.../scala/leon/purescala/TypeTreeOps.scala | 2 +-
src/main/scala/leon/repair/Repairman.scala | 4 +--
.../leon/repair/rules/GuidedDecomp.scala | 2 +-
.../solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 4 +--
.../solvers/templates/TemplateGenerator.scala | 20 +++++------
.../leon/solvers/templates/Templates.scala | 2 +-
.../solvers/templates/UnrollingBank.scala | 10 +++---
.../scala/leon/synthesis/ConvertHoles.scala | 8 ++---
.../leon/synthesis/LinearEquations.scala | 2 +-
src/main/scala/leon/synthesis/Solution.scala | 2 +-
.../scala/leon/synthesis/Synthesizer.scala | 4 +--
.../leon/synthesis/rules/ADTInduction.scala | 12 +++----
.../synthesis/rules/ADTLongInduction.scala | 12 +++----
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
.../leon/synthesis/rules/BottomUpTegis.scala | 2 +-
.../leon/synthesis/rules/CegisLike.scala | 10 +++---
.../leon/synthesis/rules/DetupleInput.scala | 4 +--
.../leon/synthesis/rules/DetupleOutput.scala | 2 +-
.../leon/synthesis/rules/InlineHoles.scala | 2 +-
.../leon/synthesis/rules/IntInduction.scala | 8 ++---
.../synthesis/rules/IntegerEquation.scala | 4 +--
.../synthesis/rules/IntegerInequalities.scala | 14 ++++----
.../synthesis/utils/ExpressionGrammar.scala | 4 +--
.../scala/leon/synthesis/utils/Helpers.scala | 2 +-
.../scala/leon/termination/ChainBuilder.scala | 2 +-
.../leon/termination/ChainProcessor.scala | 2 +-
.../leon/termination/LoopProcessor.scala | 2 +-
.../scala/leon/termination/Processor.scala | 4 +--
.../scala/leon/termination/Strengthener.scala | 2 +-
.../leon/termination/StructuralSize.scala | 8 ++---
src/main/scala/leon/utils/TypingPhase.scala | 2 +-
.../scala/leon/utils/UnitElimination.scala | 2 +-
.../leon/xlang/ArrayTransformation.scala | 6 ++--
.../scala/leon/xlang/EpsilonElimination.scala | 4 +--
.../xlang/ImperativeCodeElimination.scala | 24 ++++++-------
src/main/scala/leon/xlang/Trees.scala | 3 +-
.../evaluators/DefaultEvaluatorTests.scala | 10 +++---
.../scala/leon/test/purescala/DataGen.scala | 8 ++---
.../leon/test/purescala/LikelyEqSuite.scala | 6 ++--
.../purescala/TreeNormalizationsTests.scala | 8 ++---
.../leon/test/purescala/TreeOpsTests.scala | 8 ++---
.../scala/leon/test/purescala/TreeTests.scala | 2 +-
.../test/solvers/EnumerationSolverTests.scala | 4 +--
.../test/solvers/TimeoutSolverTests.scala | 4 +--
.../test/solvers/UnrollingSolverTests.scala | 6 ++--
.../test/solvers/z3/FairZ3SolverTests.scala | 10 +++---
.../solvers/z3/FairZ3SolverTestsNewAPI.scala | 10 +++---
.../z3/UninterpretedZ3SolverTests.scala | 6 ++--
.../test/synthesis/LinearEquationsSuite.scala | 10 +++---
src/test/scala/leon/test/utils/Streams.scala | 34 +++++++++----------
62 files changed, 218 insertions(+), 208 deletions(-)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 368b56808..9b12b5beb 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -109,7 +109,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val cs = for (size <- List(1, 2, 3, 5)) yield {
val subs = (1 to size).flatMap(_ => from :+ to).toList
Constructor[Expr, TypeTree](subs, ft, { s =>
- val args = from.map(tpe => FreshIdentifier("x", true).setType(tpe))
+ val args = from.map(tpe => FreshIdentifier("x", tpe, true))
val argsTuple = Tuple(args.map(_.toVariable))
val grouped = s.grouped(from.size + 1).toSeq
val body = grouped.init.foldRight(grouped.last.last) { case (t, elze) =>
@@ -227,7 +227,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
try {
val ttype = TupleType(argorder.map(_.getType))
- val tid = FreshIdentifier("tup").setType(ttype)
+ val tid = FreshIdentifier("tup", ttype)
val map = argorder.zipWithIndex.map{ case (id, i) => (id -> TupleSelect(Variable(tid), i+1)) }.toMap
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9a298342a..9a7255eb0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -496,7 +496,7 @@ trait CodeExtraction extends ASTExtractors {
val fields = args.map { case (symbol, t) =>
val tpt = t.tpt
val tpe = toPureScalaType(tpt.tpe)(defCtx, sym.pos)
- LeonValDef(FreshIdentifier(symbol.name.toString).setType(tpe).setPos(t.pos), tpe).setPos(t.pos)
+ LeonValDef(FreshIdentifier(symbol.name.toString, tpe).setPos(t.pos), tpe).setPos(t.pos)
}
ccd.setFields(fields)
@@ -585,7 +585,7 @@ trait CodeExtraction extends ASTExtractors {
val newParams = sym.info.paramss.flatten.map{ sym =>
val ptpe = toPureScalaType(sym.tpe)(nctx, sym.pos)
- val newID = FreshIdentifier(sym.name.toString).setType(ptpe).setPos(sym.pos)
+ val newID = FreshIdentifier(sym.name.toString, ptpe).setPos(sym.pos)
owners += (newID -> None)
LeonValDef(newID, ptpe).setPos(sym.pos)
}
@@ -867,12 +867,12 @@ trait CodeExtraction extends ASTExtractors {
private def extractPattern(p: Tree, binder: Option[Identifier] = None)(implicit dctx: DefContext): (Pattern, DefContext) = p match {
case b @ Bind(name, t @ Typed(pat, tpt)) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(tpt)).setPos(b.pos).setOwner(currentFunDef)
+ val newID = FreshIdentifier(name.toString, extractType(tpt)).setPos(b.pos).setOwner(currentFunDef)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(t, Some(newID))(pctx)
case b @ Bind(name, pat) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(b)).setPos(b.pos).setOwner(currentFunDef)
+ val newID = FreshIdentifier(name.toString, extractType(b)).setPos(b.pos).setOwner(currentFunDef)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(pat, Some(newID))(pctx)
@@ -968,7 +968,7 @@ trait CodeExtraction extends ASTExtractors {
val res = current match {
case ExEnsuredExpression(body, resVd, contract) =>
- val resId = FreshIdentifier(resVd.symbol.name.toString).setType(extractType(current)).setPos(resVd.pos).setOwner(currentFunDef)
+ val resId = FreshIdentifier(resVd.symbol.name.toString, extractType(current)).setPos(resVd.pos).setOwner(currentFunDef)
val post = extractTree(contract)(dctx.withNewVar(resVd.symbol -> (() => Variable(resId))))
val b = try {
@@ -981,7 +981,7 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(b, resId, post)
case t @ ExHoldsExpression(body) =>
- val resId = FreshIdentifier("holds").setType(BooleanType).setPos(current.pos).setOwner(currentFunDef)
+ val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos).setOwner(currentFunDef)
val post = Variable(resId).setPos(current.pos)
val b = try {
@@ -1069,7 +1069,7 @@ trait CodeExtraction extends ASTExtractors {
case ExValDef(vs, tpt, bdy) =>
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(vs.name.toString, binderTpe).setOwner(currentFunDef)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -1121,7 +1121,7 @@ trait CodeExtraction extends ASTExtractors {
case ExVarDef(vs, tpt, bdy) => {
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString).setType(binderTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(vs.name.toString, binderTpe).setOwner(currentFunDef)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -1260,7 +1260,7 @@ trait CodeExtraction extends ASTExtractors {
val newOracles = oracles map { case (tpt, sym) =>
val aTpe = extractType(tpt)
val oTpe = oracleType(ops.pos, aTpe)
- val newID = FreshIdentifier(sym.name.toString).setType(oTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(sym.name.toString, oTpe).setOwner(currentFunDef)
owners += (newID -> None)
newID
}
@@ -1278,7 +1278,7 @@ trait CodeExtraction extends ASTExtractors {
case chs @ ExChooseExpression(args, body) =>
val vars = args map { case (tpt, sym) =>
val aTpe = extractType(tpt)
- val newID = FreshIdentifier(sym.name.toString).setType(aTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(sym.name.toString, aTpe).setOwner(currentFunDef)
owners += (newID -> None)
newID
}
@@ -1295,7 +1295,7 @@ trait CodeExtraction extends ASTExtractors {
case l @ ExLambdaExpression(args, body) =>
val vds = args map { vd =>
val aTpe = extractType(vd.tpt)
- val newID = FreshIdentifier(vd.symbol.name.toString).setType(aTpe)
+ val newID = FreshIdentifier(vd.symbol.name.toString, aTpe)
owners += (newID -> None)
LeonValDef(newID, aTpe)
}
@@ -1311,7 +1311,7 @@ trait CodeExtraction extends ASTExtractors {
case f @ ExForallExpression(args, body) =>
val vds = args map { case (tpt, sym) =>
val aTpe = extractType(tpt)
- val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
+ val newID = FreshIdentifier(sym.name.toString, aTpe)
owners += (newID -> None)
LeonValDef(newID, aTpe)
}
@@ -1810,7 +1810,7 @@ trait CodeExtraction extends ASTExtractors {
} else {
if (dctx.isExtern) {
unknownsToTP.getOrElse(sym, {
- val tp = TypeParameter(FreshIdentifier(sym.name.toString, true))
+ val tp = TypeParameter(FreshIdentifier(sym.name.toString, Untyped, true)) //FIXME
unknownsToTP += sym -> tp
tp
})
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 626bfe4a4..fa5962176 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -8,7 +8,7 @@ import Definitions.Definition
object Common {
import Trees.Variable
- import TypeTrees.{MutableTyped,Typed}
+ import TypeTrees._
abstract class Tree extends Positioned with Serializable {
def copiedFrom(o: Tree): this.type = {
@@ -30,9 +30,11 @@ object Common {
}
// the type is left blank (Untyped) for Identifiers that are not variables
- class Identifier private[Common](val name: String, val globalId: Int, val id: Int, alwaysShowUniqueID: Boolean = false) extends Tree with MutableTyped {
+ class Identifier private[Common](val name: String, val globalId: Int, val id: Int, val tpe: TypeTree, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
self : Serializable =>
+ val getType = tpe
+
override def equals(other: Any): Boolean = {
if(other == null || !other.isInstanceOf[Identifier])
false
@@ -54,7 +56,7 @@ object Common {
def toVariable : Variable = Variable(this)
- def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
+ def freshen: Identifier = FreshIdentifier(name, tpe, alwaysShowUniqueID).copiedFrom(this)
var owner : Option[Definition] = None
@@ -85,9 +87,11 @@ object Common {
}
object FreshIdentifier {
- def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), alwaysShowUniqueID)
+ def apply(name: String, tpe: TypeTree = Untyped, alwaysShowUniqueID: Boolean = false) : Identifier =
+ new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe: TypeTree, alwaysShowUniqueID)
- def apply(name: String, forceId: Int): Identifier = new Identifier(name, UniqueCounter.nextGlobal, forceId, true)
+ def apply(name: String, forceId: Int, tpe: TypeTree): Identifier =
+ new Identifier(name, UniqueCounter.nextGlobal, forceId, tpe, true)
}
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index a287b3d5f..ceaf8ad37 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -23,7 +23,7 @@ object CompleteAbstractDefinitions extends TransformationPhase {
// We remove methods from class definitions and add corresponding functions
m.defs.foreach {
case fd: FunDef if fd.body.isEmpty =>
- val id = FreshIdentifier("res").setType(fd.returnType)
+ val id = FreshIdentifier("res", fd.returnType)
if (fd.hasPostcondition) {
val (pid, post) = fd.postcondition.get
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 3c74cc29c..f37136d4d 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -220,7 +220,7 @@ object Constructors {
def finiteLambda(dflt: Expr, els: Seq[(Expr, Expr)], tpe: FunctionType): Lambda = {
val args = tpe.from.zipWithIndex.map { case (tpe, idx) =>
- ValDef(FreshIdentifier(s"x${idx + 1}").setType(tpe), tpe)
+ ValDef(FreshIdentifier(s"x${idx + 1}", tpe), tpe)
}
assume(els.isEmpty || !tpe.from.isEmpty, "Can't provide finite mapping for lambda without parameters")
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 2c459bc5f..d01290bbf 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -475,7 +475,7 @@ object Definitions {
val newParams = fd.params.map {
case vd @ ValDef(id, tpe) =>
val newTpe = translated(tpe)
- val newId = FreshIdentifier(id.name, true).setType(newTpe).copiedFrom(id)
+ val newId = FreshIdentifier(id.name, newTpe, true).copiedFrom(id)
ValDef(newId, newTpe).setPos(vd)
}
@@ -512,7 +512,7 @@ object Definitions {
def postcondition = fd.postcondition.map {
case (id, post) if typesMap.nonEmpty =>
postCache.getOrElse((id, post), {
- val nId = FreshIdentifier(id.name).setType(translated(id.getType)).copiedFrom(id)
+ val nId = FreshIdentifier(id.name, translated(id.getType)).copiedFrom(id)
val res = nId -> instantiateType(post, typesMap, paramsMap + (id -> nId))
postCache += ((id,post) -> res)
res
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 7cdfce833..a70de453a 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -50,12 +50,12 @@ object FunctionClosure extends TransformationPhase {
val capturedVars: Set[Identifier] = bindedVars.diff(enclosingLets.map(_._1).toSet)
val capturedConstraints: Set[Expr] = pathConstraints.toSet
- val freshIds: Map[Identifier, Identifier] = capturedVars.map(id => (id, FreshIdentifier(id.name).copiedFrom(id))).toMap
+ val freshIds: Map[Identifier, Identifier] = capturedVars.map(id => (id, id.freshen)).toMap
val freshVars: Map[Expr, Expr] = freshIds.map(p => (p._1.toVariable, p._2.toVariable))
val extraValDefOldIds: Seq[Identifier] = capturedVars.toSeq
val extraValDefFreshIds: Seq[Identifier] = extraValDefOldIds.map(freshIds(_))
- val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map(id => ValDef(id, id.getType))
+ val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map{id => ValDef(id, id.getType)}
val newValDefs: Seq[ValDef] = fd.params ++ extraValDefs
val newBindedVars: Set[Identifier] = bindedVars ++ fd.params.map(_.id)
val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
@@ -69,7 +69,7 @@ object FunctionClosure extends TransformationPhase {
def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {
- val newId = FreshIdentifier(p._1.name).copiedFrom(p._1)
+ val newId = p._1.freshen
val newMap = acc._2 + (p._1 -> newId)
val newBody = functionClosure(acc._1, newBindedVars, freshIds ++ newMap, fd2FreshFd)
(Let(newId, p._2, newBody), newMap)
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 857b2a2d2..b7c766def 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -30,12 +30,12 @@ object MethodLifting extends TransformationPhase {
val recType = classDefToClassType(cd, ctParams.map(_.tp))
val retType = instantiateType(fd.returnType, tparamsMap)
val fdParams = fd.params map { vd =>
- val newId = FreshIdentifier(vd.id.name).setType(instantiateType(vd.id.getType, tparamsMap))
+ val newId = FreshIdentifier(vd.id.name, instantiateType(vd.id.getType, tparamsMap))
ValDef(newId, newId.getType)
}
val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
- val receiver = FreshIdentifier("$this").setType(recType).setPos(cd.id)
+ val receiver = FreshIdentifier("$this", recType).setPos(cd.id)
val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver, recType) +: fdParams, fd.defType)
nfd.copyContentFrom(fd)
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index fed50fe43..e319619e6 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -27,7 +27,7 @@ class ScopeSimplifier extends Transformer {
protected def genId(id: Identifier, scope: Scope): Identifier = {
val existCount = scope.inScope.count(_.name == id.name)
- FreshIdentifier(id.name, existCount).setType(id.getType)
+ FreshIdentifier(id.name, existCount, id.getType)
}
protected def rec(e: Expr, scope: Scope): Expr = e match {
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 857b82fc2..345708fef 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -413,6 +413,7 @@ object TreeOps {
}).setPos(expr)
// rewrites pattern-matching expressions to use fresh variables for the binders
+ // TODO: Unused, and untested
def freshenLocals(expr: Expr) : Expr = {
def rewritePattern(p: Pattern, sm: Map[Identifier,Identifier]) : Pattern = p match {
case InstanceOfPattern(Some(b), ctd) => InstanceOfPattern(Some(sm(b)), ctd)
@@ -425,7 +426,8 @@ object TreeOps {
def freshenCase(cse: MatchCase) : MatchCase = {
val allBinders: Set[Identifier] = cse.pattern.binders
- val subMap: Map[Identifier,Identifier] = Map(allBinders.map(i => (i, FreshIdentifier(i.name, true).setType(i.getType))).toSeq : _*)
+ val subMap: Map[Identifier,Identifier] =
+ Map(allBinders.map(i => (i, FreshIdentifier(i.name, i.getType, true))).toSeq : _*)
val subVarMap: Map[Expr,Expr] = subMap.map(kv => (Variable(kv._1) -> Variable(kv._2)))
MatchCase(
@@ -444,7 +446,7 @@ object TreeOps {
Some(Passes(in, out, cses.map(freshenCase(_))).copiedFrom(p))
case l @ Let(i,e,b) =>
- val newID = FreshIdentifier(i.name, true).copiedFrom(i)
+ val newID = FreshIdentifier(i.name, i.getType, alwaysShowUniqueID = true).copiedFrom(i)
Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
case _ => None
@@ -710,7 +712,7 @@ object TreeOps {
def rec(in: Expr, pattern: Pattern): Seq[(Expr, Expr)] = pattern match {
case InstanceOfPattern(ob, cct: CaseClassType) =>
val pt = CaseClassPattern(ob, cct, cct.fields.map { f =>
- WildcardPattern(Some(FreshIdentifier(f.id.name).setType(f.getType)))
+ WildcardPattern(Some(FreshIdentifier(f.id.name, f.getType)))
})
rec(in, pt)
@@ -915,7 +917,7 @@ object TreeOps {
case l : Literal[_] => LiteralPattern(None, l)
case Variable(i) => WildcardPattern(Some(i))
case other =>
- val id = FreshIdentifier("other", true).setType(other.getType)
+ val id = FreshIdentifier("other", other.getType, true)
guard = and(guard, Equals(Variable(id), other))
WildcardPattern(Some(id))
}
@@ -929,7 +931,7 @@ object TreeOps {
* represent the bindings for intermediate binders (from outermost to innermost)
*/
def patternToExpression(p : Pattern, expectedType : TypeTree) : (Expr, Seq[(Identifier, Expr)]) = {
- def fresh(tp : TypeTree) = FreshIdentifier("binder", true).setType(tp)
+ def fresh(tp : TypeTree) = FreshIdentifier("binder", tp, true)
var ieMap = Seq[(Identifier, Expr)]()
def addBinding(b : Option[Identifier], e : Expr) = b foreach { ieMap +:= (_, e) }
def rec(p : Pattern, expectedType : TypeTree) : Expr = p match {
@@ -1031,7 +1033,7 @@ object TreeOps {
GenericValue(tp, 0)
case FunctionType(from, to) =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", true).setType(tpe), tpe))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true), tpe))
Lambda(args, simplestValue(to))
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
@@ -1311,13 +1313,13 @@ object TreeOps {
val newFD = mapType(funDef.returnType) match {
case None => funDef
case Some(rt) =>
- val fd = new FunDef(FreshIdentifier(funDef.id.name, true), funDef.tparams, rt, funDef.params, funDef.defType)
+ val fd = new FunDef(FreshIdentifier(funDef.id.name, alwaysShowUniqueID = true), funDef.tparams, rt, funDef.params, funDef.defType)
// These will be taken care of in the recursive traversal.
fd.body = funDef.body
fd.precondition = funDef.precondition
funDef.postcondition match {
case Some((id, post)) =>
- val freshId = FreshIdentifier(id.name, true).setType(rt)
+ val freshId = FreshIdentifier(id.name, rt, true)
idMap += id -> freshId
fd.postcondition = Some((freshId, post))
case None =>
@@ -2007,7 +2009,7 @@ object TreeOps {
case _ : Lambda => expr
case _ : Variable => expr
case e =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", true).setType(tpe), tpe))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true), tpe))
val application = apply(expr, args.map(_.toVariable))
Lambda(args, lift(application))
}
@@ -2233,7 +2235,7 @@ object TreeOps {
case _ => "tmp"
}
- val binder = FreshIdentifier(name, true).setType(prefix.getType)
+ val binder = FreshIdentifier(name, prefix.getType, true)
// prefix becomes binder
substMap += prefix -> Variable(binder)
@@ -2244,7 +2246,7 @@ object TreeOps {
if (conditions contains fieldSel) {
computePatternFor(conditions(fieldSel), fieldSel)
} else {
- val b = FreshIdentifier(f.id.name, true).setType(f.tpe)
+ val b = FreshIdentifier(f.id.name, f.tpe, true)
substMap += fieldSel -> Variable(b)
WildcardPattern(Some(b))
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 3ce5566d4..a3ce2caf7 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -234,11 +234,16 @@ object Trees {
// tpe overrides the type of the identifier.
// This is useful for variables that represent class fields with instantiated types.
// E.g. list.head when list: List[Int]
- // @mk: I know this breaks symmetry with the rest of the trees, but it does seem
- // like a natural way to implement this. Feel free to rename the underlying class
- // and define constructor/extractor
+ // @mk: TODO: This breaks symmetry with the rest of the trees and is ugly-ish.
+ // Feel free to rename the underlying class and define constructor/extractor,
+ // or do it some other way
class Variable(val id: Identifier, val tpe: Option[TypeTree]) extends Expr with Terminal {
val getType = tpe getOrElse id.getType
+ override def equals(that: Any) = that match {
+ case Variable(id2) => id == id2
+ case _ => false
+ }
+ override def hashCode: Int = id.hashCode
}
object Variable {
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index f8ca94198..f43465b52 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -196,7 +196,7 @@ object TypeTreeOps {
def rec(idsMap: Map[Identifier, Identifier])(e: Expr): Expr = {
def freshId(id: Identifier, newTpe: TypeTree) = {
if (id.getType != newTpe) {
- FreshIdentifier(id.name).setType(newTpe).copiedFrom(id)
+ FreshIdentifier(id.name, newTpe).copiedFrom(id)
} else {
id
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 31abd59c1..237c129e4 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -224,7 +224,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val args = fd.params.map(_.id)
val argsWrapped = tupleWrap(args.map(_.toVariable))
- val out = fd.postcondition.map(_._1).getOrElse(FreshIdentifier("res", true).setType(fd.returnType))
+ val out = fd.postcondition.map(_._1).getOrElse(FreshIdentifier("res", fd.returnType, true))
val spec = fd.postcondition.map(_._2).getOrElse(BooleanLiteral(true))
@@ -269,7 +269,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
)
def condAsSpec(cond: Expr, inExpr: Expr => Expr) = {
- val newOut = FreshIdentifier("cond", true).setType(BooleanType)
+ val newOut = FreshIdentifier("cond", BooleanType, true)
val newSpec = Let(
out,
inExpr(Variable(newOut)),
diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index f69130658..7948360d3 100644
--- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -52,7 +52,7 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val scrut = scrut0 match {
case v : Variable => v
- case _ => Variable(FreshIdentifier("scrut", true).setType(scrut0.getType))
+ case _ => Variable(FreshIdentifier("scrut", scrut0.getType, true))
}
var scrutCond: Expr = if (scrut == scrut0) BooleanLiteral(true) else Equals(scrut0, scrut)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 7b4668d83..4d1b02ab8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -103,7 +103,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
val tpe @ ArrayType(base) = normalizeType(a.getType)
declareSort(tpe)
- var ar: Term = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
+ var ar: Term = declareVariable(FreshIdentifier("arrayconst", RawArrayType(Int32Type, base)))
for ((i, e) <- elems) {
ar = FunctionApplication(SSymbol("store"), Seq(ar, toSMT(IntLiteral(i)), toSMT(e)))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 8bfc9bc4b..bce269e7a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -330,7 +330,7 @@ trait SMTLIBTarget {
case UnitLiteral() =>
declareSort(UnitType)
- declareVariable(FreshIdentifier("Unit").setType(UnitType))
+ declareVariable(FreshIdentifier("Unit", UnitType))
case InfiniteIntegerLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
case IntLiteral(i) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(i))
@@ -349,7 +349,7 @@ trait SMTLIBTarget {
)
case er @ Error(tpe, _) =>
- val s = declareVariable(FreshIdentifier("error_value").setType(tpe))
+ val s = declareVariable(FreshIdentifier("error_value", tpe))
s
case s @ CaseClassSelector(cct, e, id) =>
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 436220efa..48c029f60 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -26,7 +26,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
return cacheExpr(body);
}
- val fakeFunDef = new FunDef(FreshIdentifier("fake", true),
+ val fakeFunDef = new FunDef(FreshIdentifier("fake", alwaysShowUniqueID = true),
Nil,
body.getType,
variablesOf(body).toSeq.map(id => ValDef(id, id.getType)),
@@ -66,7 +66,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
None
}
- val start : Identifier = FreshIdentifier("start", true).setType(BooleanType)
+ val start : Identifier = FreshIdentifier("start", BooleanType, true)
val pathVar : (Identifier, T) = start -> encoder.encodeId(start)
val funDefArgs : Seq[Identifier] = tfd.params.map(_.id)
@@ -199,7 +199,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
rb
case l @ Let(i, e, b) =>
- val newExpr : Identifier = FreshIdentifier("lt", true).setType(i.getType)
+ val newExpr : Identifier = FreshIdentifier("lt", i.getType, true)
storeExpr(newExpr)
val re = rec(pathVar, e)
storeGuarded(pathVar, Equals(Variable(newExpr), re))
@@ -208,13 +208,13 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
/* TODO: maybe we want this specialization?
case l @ LetTuple(is, e, b) =>
- val tuple : Identifier = FreshIdentifier("t", true).setType(TupleType(is.map(_.getType)))
+ val tuple : Identifier = FreshIdentifier("t", TupleType(is.map(_.getType)), true)
storeExpr(tuple)
val re = rec(pathVar, e)
storeGuarded(pathVar, Equals(Variable(tuple), re))
val mapping = for ((id, i) <- is.zipWithIndex) yield {
- val newId = FreshIdentifier("ti", true).setType(id.getType)
+ val newId = FreshIdentifier("ti", id.getType, true)
storeExpr(newId)
storeGuarded(pathVar, Equals(Variable(newId), TupleSelect(Variable(tuple), i+1)))
@@ -241,9 +241,9 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
if(!requireDecomposition(i)) {
i
} else {
- val newBool1 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
- val newBool2 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
- val newExpr : Identifier = FreshIdentifier("e", true).setType(i.getType)
+ val newBool1 : Identifier = FreshIdentifier("b", BooleanType, true)
+ val newBool2 : Identifier = FreshIdentifier("b", BooleanType, true)
+ val newExpr : Identifier = FreshIdentifier("e", i.getType, true)
storeCond(newBool1)
storeCond(newBool2)
@@ -269,7 +269,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
rec(pathVar, impl)
case c @ Choose(ids, cond, None) =>
- val cid = FreshIdentifier("choose", true).setType(c.getType)
+ val cid = FreshIdentifier("choose", c.getType, true)
storeExpr(cid)
val m: Map[Expr, Expr] = if (ids.size == 1) {
@@ -285,7 +285,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val idArgs : Seq[Identifier] = lambdaArgs(l)
val trArgs : Seq[T] = idArgs.map(encoder.encodeId(_))
- val lid = FreshIdentifier("lambda", true).setType(l.getType)
+ val lid = FreshIdentifier("lambda", l.getType, true)
val clause = appliedEquals(Variable(lid), l)
val localSubst : Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 30ea6d40e..ebc955599 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -292,7 +292,7 @@ object LambdaTemplate {
val freshCount = ids.size - currentVars.size
val typedVars = if (freshCount > 0) {
- val allIds = currentVars ++ List.range(0, freshCount).map(_ => FreshIdentifier("x", true).setType(tpe))
+ val allIds = currentVars ++ List.range(0, freshCount).map(_ => FreshIdentifier("x", tpe, true))
typedIds += tpe -> allIds
allIds
} else {
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 4c7009e0f..c6f9035fe 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -133,7 +133,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
case None =>
val b = appBlockers.get(app) match {
case Some(b) => b
- case None => encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ case None => encoder.encodeId(FreshIdentifier("b_lambda", BooleanType, true))
}
val notB = encoder.mkNot(b)
@@ -145,7 +145,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
private def freshAppBlocks(apps: Traversable[(T, App[T])]) : Seq[T] = {
apps.filter(!appBlockers.isDefinedAt(_)).toSeq.map { case app @ (blocker, App(caller, tpe, _)) =>
- val firstB = encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ val firstB = encoder.encodeId(FreshIdentifier("b_lambda", BooleanType, true))
val freeEq = functionVars(tpe).toSeq.map(t => encoder.mkEquals(t, caller))
val clause = encoder.mkImplies(encoder.mkNot(encoder.mkOr((freeEq :+ firstB) : _*)), encoder.mkNot(blocker))
@@ -159,7 +159,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
assert(appBlockers.isDefinedAt(app), "freshAppBlocks must have been called on app before it can be unlocked")
assert(infos.nonEmpty, "No point in extending blockers if no templates have been unrolled!")
- val nextB = encoder.encodeId(FreshIdentifier("b_lambda", true).setType(BooleanType))
+ val nextB = encoder.encodeId(FreshIdentifier("b_lambda", BooleanType, true))
val extension = encoder.mkOr((infos.map(_.equals).toSeq :+ nextB) : _*)
val clause = encoder.mkEquals(appBlockers(app), extension)
@@ -262,7 +262,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
case None =>
// we need to define this defBlocker and link it to definition
- val defBlocker = encoder.encodeId(FreshIdentifier("d").setType(BooleanType))
+ val defBlocker = encoder.encodeId(FreshIdentifier("d", BooleanType))
defBlockers += info -> defBlocker
val template = templateGenerator.mkTemplate(tfd)
@@ -300,7 +300,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
for ((app @ (b, _), (gen, _, _, _, infos)) <- appInfos; info @ TemplateAppInfo(template, equals, args) <- infos) {
var newCls = Seq.empty[T]
- val nb = encoder.encodeId(FreshIdentifier("b", true).setType(BooleanType))
+ val nb = encoder.encodeId(FreshIdentifier("b", BooleanType, true))
newCls :+= encoder.mkEquals(nb, encoder.mkAnd(equals, b))
val (newExprs, callBlocks, appBlocks) = template.instantiate(nb, args)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index a7051f493..d7a15f584 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -105,18 +105,18 @@ object ConvertHoles extends LeonPhase[Program, Program] {
def toExpr(h: Hole): (Expr, List[Identifier]) = {
h.alts match {
case Seq() =>
- val h1 = FreshIdentifier("hole", true).setType(h.getType)
+ val h1 = FreshIdentifier("hole", h.getType, true)
(h1.toVariable, List(h1))
case Seq(v) =>
- val h1 = FreshIdentifier("hole", true).setType(BooleanType)
- val h2 = FreshIdentifier("hole", true).setType(h.getType)
+ val h1 = FreshIdentifier("hole", BooleanType, true)
+ val h2 = FreshIdentifier("hole", h.getType, true)
(IfExpr(h1.toVariable, h2.toVariable, v), List(h1, h2))
case exs =>
var ids: List[Identifier] = Nil
val ex = exs.init.foldRight(exs.last)({ (e: Expr, r: Expr) =>
- val h = FreshIdentifier("hole", true).setType(BooleanType)
+ val h = FreshIdentifier("hole", BooleanType, true)
ids ::= h
IfExpr(h.toVariable, e, r)
})
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index a9dd5ff9a..5ab60fe9b 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -35,7 +35,7 @@ object LinearEquations {
} else {
val basis: Array[Array[BigInt]] = linearSet(evaluator, as, normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}.toArray)
val (pre, sol) = particularSolution(as, normalizedEquation)
- val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", true).setType(IntegerType))
+ val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", IntegerType, true))
val tbasis = basis.transpose
assert(freshVars.size == tbasis.size)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index f4d839536..a3388ac6c 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -43,7 +43,7 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrust
def project(indices: Seq[Int]): Solution = {
term.getType match {
case TupleType(ts) =>
- val t = FreshIdentifier("t", true).setType(term.getType)
+ val t = FreshIdentifier("t", term.getType, true)
val newTerm = Let(t, term, tupleWrap(indices.map(i => TupleSelect(t.toVariable, i+1))))
Solution(pre, defs, newTerm)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 46ecb4e33..8bc9ee620 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -103,7 +103,7 @@ class Synthesizer(val context : LeonContext,
// Create new fundef for the body
val ret = tupleTypeWrap(problem.xs.map(_.getType))
- val res = Variable(FreshIdentifier("res").setType(ret))
+ val res = Variable(FreshIdentifier("res", ret))
val mapPost: Map[Expr, Expr] =
if (problem.xs.size > 1) {
@@ -116,7 +116,7 @@ class Synthesizer(val context : LeonContext,
}.toMap
}
- val fd = new FunDef(FreshIdentifier(ci.fd.id.name+"_final", true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier(ci.fd.id.name+"_final", alwaysShowUniqueID = true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
fd.precondition = Some(and(problem.pc, sol.pre))
fd.postcondition = Some((res.id, replace(mapPost, problem.phi)))
fd.body = Some(sol.term)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 1f1091786..21d93cb01 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -25,8 +25,8 @@ case object ADTInduction extends Rule("ADT Induction") {
val resType = tupleTypeWrap(p.xs.map(_.getType))
- val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
- val residualArgs = oas.map(id => FreshIdentifier(id.name, true).setType(id.getType))
+ val inductOn = FreshIdentifier(origId.name, origId.getType, true)
+ val residualArgs = oas.map(id => FreshIdentifier(id.name, id.getType, true))
val residualMap = (oas zip residualArgs).map{ case (id, id2) => id -> Variable(id2) }.toMap
val residualArgDefs = residualArgs.map(a => ValDef(a, a.getType))
@@ -49,11 +49,11 @@ case object ADTInduction extends Rule("ADT Induction") {
var recCalls = Map[List[Identifier], List[Expr]]()
var postFs = List[Expr]()
- val newIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, true).setType(vd.tpe)).toList
+ val newIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe, true)).toList
val inputs = (for (id <- newIds) yield {
if (id.getType == origId.getType) {
- val postXs = p.xs map (id => FreshIdentifier("r", true).setType(id.getType))
+ val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
recCalls += postXs -> (Variable(id) +: residualArgs.map(id => Variable(id)))
@@ -80,7 +80,7 @@ case object ADTInduction extends Rule("ADT Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pre, cct, ids, calls)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= and(pre, sol.pre)
@@ -98,7 +98,7 @@ case object ADTInduction extends Rule("ADT Induction") {
} else {
val funPre = substAll(substMap, and(p.pc, orJoin(globalPre)))
val funPost = substAll(substMap, p.phi)
- val idPost = FreshIdentifier("res").setType(resType)
+ val idPost = FreshIdentifier("res", resType)
val outerPre = orJoin(globalPre)
newFun.precondition = Some(funPre)
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 1973dd244..75e4a4ff4 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -26,8 +26,8 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val resType = tupleTypeWrap(p.xs.map(_.getType))
- val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
- val residualArgs = oas.map(id => FreshIdentifier(id.name, true).setType(id.getType))
+ val inductOn = FreshIdentifier(origId.name, origId.getType, true)
+ val residualArgs = oas.map(id => FreshIdentifier(id.name, id.getType, true))
val residualMap = (oas zip residualArgs).map{ case (id, id2) => id -> Variable(id2) }.toMap
val residualArgDefs = residualArgs.map(a => ValDef(a, a.getType))
@@ -68,7 +68,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
(for (id <- ids if isRec(id)) yield {
for (cct <- ct.knownCCDescendents) yield {
- val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, true).setType(vd.tpe)).toList
+ val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe, true)).toList
val newIds = ids.filterNot(_ == id) ++ subIds
val newCalls = if (!subIds.isEmpty) {
@@ -112,7 +112,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
var postFs = List[Expr]()
for (cid <- calls) {
- val postXs = p.xs map (id => FreshIdentifier("r", true).setType(id.getType))
+ val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
postXss = postXss ::: postXs
val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
postFs = substAll(postXsMap + (inductOn -> Variable(cid)), innerPhi) :: postFs
@@ -130,7 +130,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pat, calls, pc)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= and(pc, sol.pre)
@@ -147,7 +147,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
} else {
val funPre = substAll(substMap, and(p.pc, orJoin(globalPre)))
val funPost = substAll(substMap, p.phi)
- val idPost = FreshIdentifier("res").setType(resType)
+ val idPost = FreshIdentifier("res", resType)
val outerPre = orJoin(globalPre)
newFun.precondition = Some(funPre)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index d5b03204d..411cf29f6 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -55,7 +55,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val subInfo = for(ccd <- cases) yield {
val cct = CaseClassType(ccd, act.tps)
- val args = cct.fields.map { vd => FreshIdentifier(vd.id.name, true).setType(vd.tpe) }.toList
+ val args = cct.fields.map { vd => FreshIdentifier(vd.id.name, vd.tpe, true) }.toList
val subPhi = subst(id -> CaseClass(cct, args.map(Variable(_))), p.phi)
val subPC = subst(id -> CaseClass(cct, args.map(Variable(_))), p.pc)
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 75846d3ff..1259a50a7 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -90,7 +90,7 @@ abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
} else {
- val args = gen.subTrees.map(t => FreshIdentifier("arg", true).setType(t.getType))
+ val args = gen.subTrees.map(t => FreshIdentifier("arg", t.getType, true))
val argsV = args.map(_.toVariable)
val expr = gen.builder(argsV)
val ev = evaluator.compile(expr, args).get
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 9c9927f06..f3174b8d3 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -242,16 +242,16 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
- private val bArrayId = FreshIdentifier("bArray", true).setType(ArrayType(BooleanType))
+ private val bArrayId = FreshIdentifier("bArray", ArrayType(BooleanType), true)
- private var cTreeFd = new FunDef(FreshIdentifier("cTree", true),
+ private var cTreeFd = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true),
Seq(),
p.outType,
p.as.map(id => ValDef(id, id.getType)),
DefType.MethodDef
)
- private var phiFd = new FunDef(FreshIdentifier("phiFd", true),
+ private var phiFd = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true),
Seq(),
BooleanType,
p.as.map(id => ValDef(id, id.getType)),
@@ -544,7 +544,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private var slots = Map[T, Int]().withDefaultValue(0)
private def streamOf(t: T): Stream[Identifier] = {
- FreshIdentifier("c", true).setType(t.getType) #:: streamOf(t)
+ FreshIdentifier("c", t.getType, true) #:: streamOf(t)
}
def reset(): Unit = {
@@ -568,7 +568,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
var unfoldedSomething = false;
def freshB() = {
- val id = FreshIdentifier("B", true).setType(BooleanType)
+ val id = FreshIdentifier("B", BooleanType, true)
newBs += id
id
}
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 1157a17ca..4b7eac604 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -23,14 +23,14 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr]) = id.getType match {
case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
- val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, true).setType(vd.tpe) }
+ val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.tpe, true) }
val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> CaseClassSelector(cct, Variable(id), vd.id) }.toMap
(newIds.toList, CaseClass(cct, newIds.map(Variable(_))), map)
case TupleType(ts) =>
- val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), true).setType(t) }
+ val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), t, true) }
val map = (newIds.zipWithIndex).map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index 66dfe0195..fc7d4c8c1 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -27,7 +27,7 @@ case object DetupleOutput extends Rule("Detuple Out") {
if (isDecomposable(x)) {
val ct @ CaseClassType(ccd @ CaseClassDef(name, _, _, _), tpes) = x.getType
- val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, true).setType(vd.tpe) }
+ val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.tpe, true) }
val newCC = CaseClass(ct, newIds.map(Variable(_)))
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index ee9379449..7e1cd1611 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -89,7 +89,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
val res = preMap {
case h @ FunctionInvocation(TypedFunDef(`oracleHead`, Seq(tpe)), Seq(o)) =>
- val x = FreshIdentifier("h", true).setType(tpe)
+ val x = FreshIdentifier("h", tpe, true)
newXs ::= x
Some(x.toVariable)
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index 15c19915d..150686b81 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -18,9 +18,9 @@ case object IntInduction extends Rule("Int Induction") {
case List(IsTyped(origId, IntegerType)) =>
val tpe = tupleTypeWrap(p.xs.map(_.getType))
- val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
+ val inductOn = FreshIdentifier(origId.name, origId.getType, true)
- val postXs = p.xs map (id => FreshIdentifier("r", true).setType(id.getType))
+ val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
@@ -46,8 +46,8 @@ case object IntInduction extends Rule("Int Induction") {
and(LessThan(Variable(inductOn), InfiniteIntegerLiteral(0)), lt.pre))
val preOut = subst(inductOn -> Variable(origId), preIn)
- val newFun = new FunDef(FreshIdentifier("rec", true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)),DefType.MethodDef)
- val idPost = FreshIdentifier("res").setType(tpe)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)),DefType.MethodDef)
+ val idPost = FreshIdentifier("res", tpe)
newFun.precondition = Some(preIn)
newFun.postcondition = Some((idPost, letTuple(p.xs.toSeq, Variable(idPost), p.phi)))
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index a2ebfb9f0..070a4fc39 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -83,7 +83,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
val freshFormula = simplePreTransform({
case d@Division(_, _) => {
assert(variablesOf(d).intersect(problem.xs.toSet).isEmpty)
- val newVar = FreshIdentifier("d", true).setType(Int32Type)
+ val newVar = FreshIdentifier("d", Int32Type, true)
freshInputVariables ::= newVar
equivalenceConstraints += (Variable(newVar) -> d)
Variable(newVar)
@@ -100,7 +100,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
case List(s @ Solution(pre, defs, term)) => {
val freshPre = replace(equivalenceConstraints, pre)
val freshTerm = replace(equivalenceConstraints, term)
- val freshsubxs = subproblemxs.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val freshsubxs = subproblemxs.map(id => FreshIdentifier(id.name, id.getType))
val id2res: Map[Expr, Expr] =
freshsubxs.zip(subproblemxs).map{case (id1, id2) => (Variable(id1), Variable(id2))}.toMap ++
neqxs.map(id => (Variable(id), eqSubstMap(Variable(id)))).toMap
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 20da4b5ac..68cd02b92 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -94,11 +94,11 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
//define max function
- val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b"), Int32Type))
+ val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type), Int32Type))
val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs, DefType.MethodDef)
def maxRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
- val v = FreshIdentifier("m").setType(Int32Type)
+ val v = FreshIdentifier("m", Int32Type)
Let(v, IfExpr(LessThan(x1, x2), x2, x1), maxRec(Variable(v) :: xs))
}
case (x :: Nil) => x
@@ -112,7 +112,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs,DefType.MethodDef)
def minRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
- val v = FreshIdentifier("m").setType(Int32Type)
+ val v = FreshIdentifier("m", Int32Type)
Let(v, IfExpr(LessThan(x1, x2), x1, x2), minRec(Variable(v) :: xs))
}
case (x :: Nil) => x
@@ -162,8 +162,8 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
upperBounds = Nil
}
- val remainderIds: List[Identifier] = upperBounds.map(_ => FreshIdentifier("k", true).setType(Int32Type))
- val quotientIds: List[Identifier] = lowerBounds.map(_ => FreshIdentifier("l", true).setType(Int32Type))
+ val remainderIds: List[Identifier] = upperBounds.map(_ => FreshIdentifier("k", Int32Type, true))
+ val quotientIds: List[Identifier] = lowerBounds.map(_ => FreshIdentifier("l", Int32Type, true))
val newUpperBounds: List[Expr] = upperBounds.map{case (bound, coef) => Times(IntLiteral(L/coef), bound)}
val newLowerBounds: List[Expr] = lowerBounds.map{case (bound, coef) => Times(IntLiteral(L/coef), bound)}
@@ -190,11 +190,11 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
} else {
val k = remainderIds.head
- val loopCounter = Variable(FreshIdentifier("i", true).setType(Int32Type))
+ val loopCounter = Variable(FreshIdentifier("i", Int32Type, true))
val concretePre = replace(Map(Variable(k) -> loopCounter), pre)
val concreteTerm = replace(Map(Variable(k) -> loopCounter), term)
val returnType = tupleTypeWrap(problem.xs.map(_.getType))
- val funDef = new FunDef(FreshIdentifier("rec", true), Nil, returnType, Seq(ValDef(loopCounter.id, Int32Type)),DefType.MethodDef)
+ val funDef = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, returnType, Seq(ValDef(loopCounter.id, Int32Type)),DefType.MethodDef)
val funBody = expandAndSimplifyArithmetic(IfExpr(
LessThan(loopCounter, IntLiteral(0)),
Error(returnType, "No solution exists"),
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 8a0a04832..a0a73caf4 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -50,7 +50,7 @@ abstract class ExpressionGrammar[T <% Typed] {
final def printProductions(printer: String => Unit) {
for ((t, gs) <- cache; g <- gs) {
- val subs = g.subTrees.map { t => FreshIdentifier(Console.BOLD+t.toString+Console.RESET).setType(t.getType).toVariable}
+ val subs = g.subTrees.map { t => FreshIdentifier(Console.BOLD+t.toString+Console.RESET, t.getType).toVariable}
val gen = g.builder(subs)
printer(f"${Console.BOLD}$t%30s${Console.RESET} ::= $gen")
@@ -334,7 +334,7 @@ object ExpressionGrammars {
val res = rec(e, gl)
//for ((t, g) <- res) {
- // val subs = g.subTrees.map { t => FreshIdentifier(t.toString).setType(t.getType).toVariable}
+ // val subs = g.subTrees.map { t => FreshIdentifier(t.toString, t.getType).toVariable}
// val gen = g.builder(subs)
// println(f"$t%30s ::= "+gen)
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 790711ba7..f80977ae6 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -69,7 +69,7 @@ object Helpers {
val res = gs.flatMap {
case Terminating(tfd, args) if isSubtypeOf(tfd.returnType, tpe) =>
- val ids = tfd.params.map(vd => FreshIdentifier("<hole>", true).setType(vd.tpe)).toList
+ val ids = tfd.params.map(vd => FreshIdentifier("<hole>", vd.tpe, true)).toList
for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.tpe);
smaller <- argsSmaller(a, tpe)) yield {
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index f46bd9428..8380bf4d6 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -68,7 +68,7 @@ final case class Chain(relations: List[Relation]) {
}
case xs =>
val params = tfd.params.map(_.id)
- val freshParams = tfd.params.map(arg => FreshIdentifier(arg.id.name, true).setType(arg.tpe))
+ val freshParams = tfd.params.map(arg => FreshIdentifier(arg.id.name, arg.tpe, true))
val bindings = (freshParams.map(_.toVariable) zip newArgs).map(p => Equals(p._1, p._2))
bindings ++ rec(xs, tfd, (params zip freshParams).toMap)
})
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index d0e51f24b..54508cdfc 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -40,7 +40,7 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
val e1 = Tuple(fd.params.map(_.toVariable))
val e2s = fdChains.toSeq.map { chain =>
- val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, true).setType(arg.id.getType))
+ val freshParams = chain.finalParams.map(arg => FreshIdentifier(arg.id.name, arg.id.getType, true))
val finalBindings = (chain.finalParams.map(_.id) zip freshParams).toMap
(chain.loop(finalSubst = finalBindings), Tuple(freshParams.map(_.toVariable)))
}
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index ee9461e2a..99b9d9efc 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -29,7 +29,7 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
reporter.debug("-+> Iteration #" + index)
for (chain <- cs if !nonTerminating.isDefinedAt(chain.funDef) &&
(chain.funDef.params zip chain.finalParams).forall(p => p._1.getType == p._2.getType)) {
- val freshParams = chain.funDef.params.map(arg => FreshIdentifier(arg.id.name, true).setType(arg.tpe))
+ val freshParams = chain.funDef.params.map(arg => FreshIdentifier(arg.id.name, arg.tpe, true))
val finalBindings = (chain.funDef.params.map(_.id) zip freshParams).toMap
val path = chain.loop(finalSubst = finalBindings)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 9d9311ef4..4a06f2a7b 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -40,8 +40,8 @@ trait Solvable extends Processor {
val structDefs = checker.defs
val program : Program = checker.program
val context : LeonContext = checker.context
- val sizeModule : ModuleDef = ModuleDef(FreshIdentifier("$size", false), checker.defs.toSeq, false)
- val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size", false),Seq(sizeModule))
+ val sizeModule : ModuleDef = ModuleDef(FreshIdentifier("$size"), checker.defs.toSeq, false)
+ val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
(new FairZ3Solver(context, newProgram) with TimeoutAssumptionSolver).setTimeout(500L)
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index c0e482c92..5d0395c7b 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -23,7 +23,7 @@ trait Strengthener { self : TerminationChecker with RelationComparator with Rela
def strengthen(cmp: (Expr, Expr) => Expr): Boolean = {
val old = funDef.postcondition
val (res, postcondition) = {
- val (res, post) = old.getOrElse(FreshIdentifier("res").setType(funDef.returnType) -> BooleanLiteral(true))
+ val (res, post) = old.getOrElse(FreshIdentifier("res", funDef.returnType) -> BooleanLiteral(true))
val args = funDef.params.map(_.toVariable)
val sizePost = cmp(Tuple(funDef.params.map(_.toVariable)), res.toVariable)
(res, and(post, sizePost))
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index e1f8f8b3c..6191aa749 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -32,13 +32,13 @@ trait StructuralSize {
sizeCache.get(argumentType) match {
case Some(fd) => fd
case None =>
- val argument = ValDef(FreshIdentifier("x", true).setType(argumentType), argumentType)
+ val argument = ValDef(FreshIdentifier("x", argumentType, true), argumentType)
val formalTParams = typeParams.map(TypeParameterDef(_))
- val fd = new FunDef(FreshIdentifier("size", true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier("size", alwaysShowUniqueID = true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
val body = simplifyLets(matchToIfThenElse(matchExpr(argument.toVariable, cases(argumentType))))
- val postId = FreshIdentifier("res", false).setType(IntegerType)
+ val postId = FreshIdentifier("res", IntegerType)
val postcondition = GreaterThan(Variable(postId), InfiniteIntegerLiteral(0))
fd.body = Some(body)
@@ -49,7 +49,7 @@ trait StructuralSize {
def caseClassType2MatchCase(_c: ClassType): MatchCase = {
val c = _c.asInstanceOf[CaseClassType] // required by leon framework
- val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name).setType(vd.tpe))
+ val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe))
val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
val sizes = arguments.map(id => size(Variable(id)))
val result = sizes.foldLeft[Expr](InfiniteIntegerLiteral(1))(Plus(_,_))
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 61eb37b36..f4c8fb747 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -55,7 +55,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
Some((id, and(CaseClassInstanceOf(cct, Variable(id)).setPos(p), p).setPos(p)))
case None =>
- val resId = FreshIdentifier("res").setType(cct)
+ val resId = FreshIdentifier("res", cct)
Some((resId, CaseClassInstanceOf(cct, Variable(resId))))
}
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 82bb880e3..d32ac6fb3 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -90,7 +90,7 @@ object UnitElimination extends TransformationPhase {
id.getType match {
case TupleType(tpes) if tpes.exists(_ == UnitType) => {
val newTupleType = TupleType(tpes.filterNot(_ == UnitType))
- val freshId = FreshIdentifier(id.name).setType(newTupleType)
+ val freshId = FreshIdentifier(id.name, newTupleType)
id2FreshId += (id -> freshId)
val newBody = removeUnit(b)
id2FreshId -= id
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index c8688cc0f..1d1c7e24d 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -44,16 +44,16 @@ object ArrayTransformation extends TransformationPhase {
case Let(i, v, b) => {
v.getType match {
case ArrayType(_) => {
- val freshIdentifier = FreshIdentifier("t").setType(i.getType)
+ val freshIdentifier = FreshIdentifier("t", i.getType)
id2FreshId += (i -> freshIdentifier)
LetVar(freshIdentifier, transform(v), transform(b))
}
case _ => Let(i, transform(v), transform(b))
}
}
- case Variable(i) => {
+ case v@Variable(i) => {
val freshId = id2FreshId.get(i).getOrElse(i)
- Variable(freshId)
+ Variable(freshId, Some(v.getType))
}
case LetVar(id, e, b) => {
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 7e49ccd27..fec576c08 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -23,9 +23,9 @@ object EpsilonElimination extends TransformationPhase {
val newBody = postMap{
case eps@Epsilon(pred, tpe) =>
val freshName = FreshIdentifier("epsilon")
- val newFunDef = new FunDef(freshName, Nil, eps.getType, Seq(), DefType.MethodDef)
+ val newFunDef = new FunDef(freshName, Nil, tpe, Seq(), DefType.MethodDef)
val epsilonVar = EpsilonVariable(eps.getPos, tpe)
- val resId = FreshIdentifier("res").setType(eps.getType)
+ val resId = FreshIdentifier("res", tpe)
val postcondition = replace(Map(epsilonVar -> Variable(resId)), pred)
newFunDef.postcondition = Some((resId, postcondition))
Some(LetDef(newFunDef, FunctionInvocation(newFunDef.typed, Seq())))
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 93ba69d15..1be1f99ab 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -45,7 +45,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
val res = expr match {
case LetVar(id, e, b) => {
- val newId = FreshIdentifier(id.name).copiedFrom(id)
+ val newId = id.freshen
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
varInScope += id
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
@@ -55,7 +55,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
}
case Assignment(id, e) => {
assert(varInScope.contains(id))
- val newId = FreshIdentifier(id.name).copiedFrom(id)
+ val newId = id.freshen
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
val scope = (body: Expr) => rhsScope(Let(newId, rhsVal, body).copiedFrom(expr))
(UnitLiteral(), scope, rhsFun + (id -> newId))
@@ -69,8 +69,8 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val iteRType = leastUpperBound(tRes.getType, eRes.getType).get
val modifiedVars: Seq[Identifier] = (tFun.keys ++ eFun.keys).toSet.intersect(varInScope).toSeq
- val resId = FreshIdentifier("res").setType(iteRType)
- val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val resId = FreshIdentifier("res", iteRType)
+ val freshIds = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val iteType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
val thenVal = if(modifiedVars.isEmpty) tRes else Tuple(tRes +: modifiedVars.map(vId => tFun.get(vId) match {
@@ -86,7 +86,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val iteExpr = IfExpr(cRes, replaceNames(cFun, tScope(thenVal)), replaceNames(cFun, eScope(elseVal))).copiedFrom(ite)
val scope = ((body: Expr) => {
- val tupleId = FreshIdentifier("t").setType(iteType)
+ val tupleId = FreshIdentifier("t", iteType)
cScope(
Let(tupleId, iteExpr,
if(freshIds.isEmpty)
@@ -108,8 +108,8 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val (scrutRes, scrutScope, scrutFun) = toFunction(scrut)
val modifiedVars: Seq[Identifier] = csesFun.toSet.flatMap((m: Map[Identifier, Identifier]) => m.keys).intersect(varInScope).toSeq
- val resId = FreshIdentifier("res").setType(m.getType)
- val freshIds = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val resId = FreshIdentifier("res", m.getType)
+ val freshIds = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val matchType = if(modifiedVars.isEmpty) resId.getType else TupleType(resId.getType +: freshIds.map(_.getType))
val csesVals = csesRes.zip(csesFun).map{
@@ -127,7 +127,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
}).setPos(m)
val scope = ((body: Expr) => {
- val tupleId = FreshIdentifier("t").setType(matchType)
+ val tupleId = FreshIdentifier("t", matchType)
scrutScope(
Let(tupleId, matchE,
if(freshIds.isEmpty)
@@ -152,7 +152,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
if(modifiedVars.isEmpty)
(UnitLiteral(), (b: Expr) => b, Map())
else {
- val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunValDefs = whileFunVars.map(id => ValDef(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
@@ -172,7 +172,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
condScope(IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase)))
whileFunDef.body = Some(whileFunBody)
- val resVar = Variable(FreshIdentifier("res").setType(whileFunReturnType))
+ val resVar = Variable(FreshIdentifier("res", whileFunReturnType))
val whileFunVars2ResultVars: Map[Expr, Expr] =
if(whileFunVars.size == 1)
Map(whileFunVars.head.toVariable -> resVar)
@@ -194,9 +194,9 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
case None => BooleanLiteral(true)
})))
- val finalVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
+ val finalVars = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val finalScope = ((body: Expr) => {
- val tupleId = FreshIdentifier("t").setType(whileFunReturnType)
+ val tupleId = FreshIdentifier("t", whileFunReturnType)
LetDef(
whileFunDef,
Let(tupleId,
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index ce2c32520..50e87706f 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -21,8 +21,7 @@ object Trees {
case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable with PrettyPrintable {
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
- val Block(args, rest) = this
- Some((args :+ rest, exprs => Block(exprs.init, exprs.last)))
+ Some((exprs :+ last, exprs => Block(exprs.init, exprs.last)))
}
def printWith(implicit pctx: PrinterContext) {
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index b7234f0d7..dc79a820c 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -122,15 +122,15 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
test("eval simple variable") {
- val id = FreshIdentifier("id").setType(Int32Type)
+ val id = FreshIdentifier("id", Int32Type)
expectSuccessful(
defaultEvaluator.eval(Variable(id), Map(id -> IntLiteral(23))),
IntLiteral(23))
}
test("eval with unbound variable should return EvaluatorError") {
- val id = FreshIdentifier("id").setType(Int32Type)
- val foo = FreshIdentifier("foo").setType(Int32Type)
+ val id = FreshIdentifier("id", Int32Type)
+ val foo = FreshIdentifier("foo", Int32Type)
val res = defaultEvaluator.eval(Variable(id), Map(foo -> IntLiteral(23)))
assert(res.isInstanceOf[EvaluationResults.EvaluatorError])
}
@@ -166,7 +166,7 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
}
test("eval variable length of array") {
- val id = FreshIdentifier("id").setType(Int32Type)
+ val id = FreshIdentifier("id", Int32Type)
expectSuccessful(
defaultEvaluator.eval(
ArrayLength(
@@ -176,7 +176,7 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
}
test("eval variable default value of array") {
- val id = FreshIdentifier("id").setType(Int32Type)
+ val id = FreshIdentifier("id", Int32Type)
expectSuccessful(
defaultEvaluator.eval(
finiteArray(Map[Int, Expr](), Some(Variable(id), IntLiteral(7)), Int32Type),
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index b68c1526d..fd5afaef0 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -83,10 +83,10 @@ class DataGen extends LeonTestSuite {
val evaluator = new CodeGenEvaluator(testContext, prog)
- val a = Variable(FreshIdentifier("a").setType(Int32Type))
- val b = Variable(FreshIdentifier("b").setType(Int32Type))
- val x = Variable(FreshIdentifier("x").setType(listType))
- val y = Variable(FreshIdentifier("y").setType(listType))
+ val a = Variable(FreshIdentifier("a", Int32Type))
+ val b = Variable(FreshIdentifier("b", Int32Type))
+ val x = Variable(FreshIdentifier("x", listType))
+ val y = Variable(FreshIdentifier("y", listType))
val sizeX = FunctionInvocation(sizeDef.typed, Seq(x))
val contentX = FunctionInvocation(contentDef.typed, Seq(x))
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index fced5df18..dd72c6795 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -12,11 +12,11 @@ import leon.purescala.TypeTrees._
class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(IntegerType)
+ val xId = FreshIdentifier("x", IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(IntegerType)
+ val yId = FreshIdentifier("y", IntegerType)
val y = Variable(yId)
- val zId = FreshIdentifier("z").setType(IntegerType)
+ val zId = FreshIdentifier("z", IntegerType)
val z = Variable(zId)
test("apply") {
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 75dd10903..90657a52d 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -15,15 +15,15 @@ import leon.purescala.TreeNormalizations._
class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(IntegerType)
+ val xId = FreshIdentifier("x", IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(IntegerType)
+ val yId = FreshIdentifier("y", IntegerType)
val y = Variable(yId)
val xs = Set(xId, yId)
- val aId = FreshIdentifier("a").setType(IntegerType)
+ val aId = FreshIdentifier("a", IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(IntegerType)
+ val bId = FreshIdentifier("b", IntegerType)
val b = Variable(bId)
val as = Set(aId, bId)
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 7137ebd34..68e132d7e 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -43,15 +43,15 @@ class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(IntegerType)
+ val xId = FreshIdentifier("x", IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(IntegerType)
+ val yId = FreshIdentifier("y", IntegerType)
val y = Variable(yId)
val xs = Set(xId, yId)
- val aId = FreshIdentifier("a").setType(IntegerType)
+ val aId = FreshIdentifier("a", IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(IntegerType)
+ val bId = FreshIdentifier("b", IntegerType)
val b = Variable(bId)
val as = Set(aId, bId)
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 73e77f16f..1036fcd88 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -14,7 +14,7 @@ import leon.purescala.TypeTrees._
class TreeTests extends LeonTestSuite {
test("And- and Or- simplifications") {
- val x = Variable(FreshIdentifier("x").setType(BooleanType))
+ val x = Variable(FreshIdentifier("x", BooleanType))
val t = BooleanLiteral(true)
val f = BooleanLiteral(false)
diff --git a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
index b5bfc4466..a2f4b4885 100644
--- a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
@@ -30,14 +30,14 @@ class EnumerationSolverTests extends LeonTestSuite {
test("EnumerationSolver 2 (x == 1)") {
val sf = getSolver
- val x = Variable(FreshIdentifier("x").setType(Int32Type))
+ val x = Variable(FreshIdentifier("x", Int32Type))
val o = IntLiteral(1)
assert(check(sf, Equals(x, o)) === Some(true))
}
test("EnumerationSolver 3 (Limited range for ints)") {
val sf = getSolver
- val x = Variable(FreshIdentifier("x").setType(Int32Type))
+ val x = Variable(FreshIdentifier("x", Int32Type))
val o = IntLiteral(42)
assert(check(sf, Equals(x, o)) === None)
}
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 4f1564619..cb8de56b3 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -56,13 +56,13 @@ class TimeoutSolverTests extends LeonTestSuite {
assert(check(sf, BooleanLiteral(true)) === None)
assert(check(sf, BooleanLiteral(false)) === None)
- val x = Variable(FreshIdentifier("x").setType(IntegerType))
+ val x = Variable(FreshIdentifier("x", IntegerType))
assert(check(sf, Equals(x, x)) === None)
}
test("TimeoutSolver 2") {
val sf = getTOSolver
- val x = Variable(FreshIdentifier("x").setType(IntegerType))
+ val x = Variable(FreshIdentifier("x", IntegerType))
val o = InfiniteIntegerLiteral(1)
assert(check(sf, Equals(Plus(x, o), Plus(o, x))) === None)
assert(check(sf, Equals(Plus(x, o), x)) === None)
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 46f56b4e7..a7f9a4c9d 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -12,8 +12,8 @@ import leon.solvers.combinators._
class UnrollingSolverTests extends LeonTestSuite {
- private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
- private val fres : Identifier = FreshIdentifier("res").setType(IntegerType)
+ private val fx : Identifier = FreshIdentifier("x", IntegerType)
+ private val fres : Identifier = FreshIdentifier("res", IntegerType)
private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
fDef.body = Some(IfExpr(GreaterThan(Variable(fx), InfiniteIntegerLiteral(0)),
Plus(Variable(fx), FunctionInvocation(fDef.typed, Seq(Minus(Variable(fx), InfiniteIntegerLiteral(1))))),
@@ -42,6 +42,6 @@ class UnrollingSolverTests extends LeonTestSuite {
check(BooleanLiteral(true), Some(true), "'true' should always be valid")
check(BooleanLiteral(false), Some(false), "'false' should never be valid")
- check(Not(GreaterThan(FunctionInvocation(fDef.typed, Seq(Variable(FreshIdentifier("toto").setType(IntegerType)))), InfiniteIntegerLiteral(0))),
+ check(Not(GreaterThan(FunctionInvocation(fDef.typed, Seq(Variable(FreshIdentifier("toto", IntegerType)))), InfiniteIntegerLiteral(0))),
Some(false), "unrolling should enable recursive definition verification")
}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index c5662615e..5025f2fbd 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -38,7 +38,7 @@ class FairZ3SolverTests extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fx : Identifier = FreshIdentifier("x", IntegerType)
private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
@@ -50,8 +50,8 @@ class FairZ3SolverTests extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
- private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
+ private val x : Expr = Variable(FreshIdentifier("x", IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y", IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private val solver = SimpleSolverAPI(SolverFactory(() => new FairZ3Solver(testContext, minimalProgram)))
@@ -81,8 +81,8 @@ class FairZ3SolverTests extends LeonTestSuite {
assertValid(solver, unknown1)
test("Check assumptions") {
- val b1 = Variable(FreshIdentifier("b").setType(BooleanType))
- val b2 = Variable(FreshIdentifier("b").setType(BooleanType))
+ val b1 = Variable(FreshIdentifier("b", BooleanType))
+ val b2 = Variable(FreshIdentifier("b", BooleanType))
val f = And(b1, Not(b2))
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 5974d31a1..8eae0d860 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -46,7 +46,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fx : Identifier = FreshIdentifier("x", IntegerType)
private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
@@ -58,8 +58,8 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
- private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
+ private val x : Expr = Variable(FreshIdentifier("x", IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y", IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private val solver = SolverFactory(() => new FairZ3Solver(testContext, minimalProgram))
@@ -89,8 +89,8 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
assertValid(solver, unknown1)
test("Check assumptions") {
- val b1 = Variable(FreshIdentifier("b").setType(BooleanType))
- val b2 = Variable(FreshIdentifier("b").setType(BooleanType))
+ val b1 = Variable(FreshIdentifier("b", BooleanType))
+ val b2 = Variable(FreshIdentifier("b", BooleanType))
val f = And(b1, Not(b2))
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 1c4aadaa5..fad21b759 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -39,7 +39,7 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fx : Identifier = FreshIdentifier("x", IntegerType)
private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
@@ -55,8 +55,8 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
- private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
+ private val x : Expr = Variable(FreshIdentifier("x", IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y", IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private def g(e : Expr) : Expr = FunctionInvocation(gDef.typed, e :: Nil)
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 7e30c3d46..8ac0bdc3d 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -18,16 +18,16 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(IntegerType)
+ val xId = FreshIdentifier("x", IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(IntegerType)
+ val yId = FreshIdentifier("y", IntegerType)
val y = Variable(yId)
- val zId = FreshIdentifier("z").setType(IntegerType)
+ val zId = FreshIdentifier("z", IntegerType)
val z = Variable(zId)
- val aId = FreshIdentifier("a").setType(IntegerType)
+ val aId = FreshIdentifier("a", IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(IntegerType)
+ val bId = FreshIdentifier("b", IntegerType)
val b = Variable(bId)
def toSum(es: Seq[Expr]) = es.reduceLeft(Plus(_, _))
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index 1b6a094a7..085727de4 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -20,15 +20,15 @@ import org.scalatest.FunSuite
class Streams extends LeonTestSuite {
test("Cartesian Product 1") {
- val s1 = FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #:: Stream.empty;
+ val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
- val s2 = FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #:: Stream.empty;
+ val s2 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
val ss = cartesianProduct(List(s1, s2))
@@ -38,15 +38,15 @@ class Streams extends LeonTestSuite {
}
test("Cartesian Product 2") {
- val s1 = FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #:: Stream.empty;
-
- val s2 = FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #::
- FreshIdentifier("B", true) #:: Stream.empty;
+ val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
+
+ val s2 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #::
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
val tmp1 = s1.mkString
val tmp2 = s2.mkString
--
GitLab