diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 173e2d5d1c28ecd233b5120bbfe59b90bf345305..c95132d7ebe87cac7c46128c02e2e80950eb4296 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -127,7 +127,7 @@ trait Extractors { self: Trees =>
case FiniteSet(els, base) =>
Some((els, els => FiniteSet(els, base)))
case FiniteBag(els, base) =>
- val subArgs = els.flatMap { case (k, v) => Seq(k, v) }.toSeq
+ val subArgs = els.flatMap { case (k, v) => Seq(k, v) }
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
case Seq(k, v, t @ _*) =>
@@ -139,7 +139,7 @@ trait Extractors { self: Trees =>
}
Some((subArgs, builder))
case FiniteMap(args, f, t) => {
- val subArgs = args.flatMap { case (k, v) => Seq(k, v) }.toSeq
+ val subArgs = args.flatMap { case (k, v) => Seq(k, v) }
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Seq[(Expr, Expr)] = kvs match {
case Seq(k, v, t @ _*) =>
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index d1690fbb3dbf63f0eaff3cadeb78f1f3ec20cfc2..273d2180d2ab2160231a41e9c0feac7a720ab1fe 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -439,7 +439,7 @@ trait GenTreeOps {
case _ =>
}
}
- return None
+ None
}
object Same {
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 9e751eec0c3be889e73b3e0ab0d509e56c63e133..9cab659b588a565d8f01f1708a2bc7d311352751 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -86,7 +86,7 @@ trait Printers { self: Trees =>
case Variable(id, _) =>
p"$id"
- case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd == v2 && v2 == v3 =>
+ case Let(vd, expr, SubString(v2: Variable, start, StringLength(v3: Variable))) if vd.toVariable == v2 && v2 == v3 =>
p"$expr.substring($start)"
case Let(b,d,e) =>
@@ -137,7 +137,7 @@ trait Printers { self: Trees =>
case CaseClassSelector(e, id) => p"$e.$id"
case FunctionInvocation(id, tps, args) =>
- p"${id}${nary(tps, ", ", "[", "]")}"
+ p"$id${nary(tps, ", ", "[", "]")}"
if (args.nonEmpty) {
p"($args)"
}
@@ -146,7 +146,7 @@ trait Printers { self: Trees =>
p"$caller($args)"
case Lambda(Seq(vd), FunctionInvocation(id, Seq(), Seq(arg))) if vd == arg =>
- p"${id}"
+ p"$id"
case Lambda(args, body) =>
optP { p"($args) => $body" }
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 0cc2b401bb6abe54769ad133de338b9eb1599f39..2fa81b40f4d32a9d10a260313b14a0f2677a4edd 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -681,16 +681,16 @@ trait SymbolOps { self: TypeOps =>
case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
fbtpe == tpe &&
elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
- case (FiniteMap(elems, tk, tv), MapType(from, to)) =>
- (tk == from) < s"$tk not equal to $from" && (tv == to) < s"$tv not equal to $to" &&
- (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type ${from}" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
+ case (FiniteMap(elems, default, kt), MapType(from, to)) =>
+ (kt == from) < s"$kt not equal to $from" && (default.getType == to) < s"${default.getType} not equal to $to" &&
+ (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type $from" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
case (CaseClass(ct, args), ct2: ClassType) =>
isSubtypeOf(ct, ct2) < s"$ct not a subtype of $ct2" &&
((args zip ct.tcd.toCase.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2) < s"${argstyped._1} not a value of type ${argstyped._2}" ))
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
variablesOf(e).isEmpty &&
(valdefs zip ins forall (vdin => isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
- (isSubtypeOf(body.getType, out)) < s"${body.getType} is not a subtype of ${out}"
+ isSubtypeOf(body.getType, out) < s"${body.getType} is not a subtype of $out"
case _ => false
}
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 84ae5e3542a819d924530df5138b8744bcb0ec6b..b7019771e53b5968698faed7d8ec0afebba3c704 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -210,7 +210,7 @@ trait TypeOps {
def typeCardinality(tp: Type): Option[Int] = {
def cards(tps: Seq[Type]): Option[Seq[Int]] = {
- val cardinalities = tps.map(typeCardinality).flatten
+ val cardinalities = tps.flatMap(typeCardinality)
if (cardinalities.size == tps.size) {
Some(cardinalities)
} else {
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index fd18f706003ee6df9ebab8149e99b7455736d2de..554f6a44a4bfd55580d32d9b888bc2b4519e5900 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -29,8 +29,8 @@ trait SolvingEvaluator extends Evaluator {
val timer = ctx.timers.evaluators.specs.start()
val sf = getSolver(options.options.collect {
- case o @ InoxOption(opt, _) if opt == optForallCache => o
- }.toSeq : _*)
+ case o@InoxOption(opt, _) if opt == optForallCache => o
+ } : _*)
import SolverResponses._
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 250075f49bfc89dbcf8c0228546b055a0bca3040..a46423abfcedf671f6605c39b443746ee986808b 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -204,7 +204,7 @@ trait QuantificationTemplates { self: Templates =>
quantifications, ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, lambdaAxioms, templates)
private def assumptions: Seq[Encoded] =
- quantifications.collect { case q: GeneralQuantification => q.currentQ2Var }.toSeq
+ quantifications.collect { case q: GeneralQuantification => q.currentQ2Var }
def satisfactionAssumptions = assumptions
def refutationAssumptions = assumptions
@@ -369,7 +369,7 @@ trait QuantificationTemplates { self: Templates =>
q -> (grounds(q).toSet ++ constraints.flatMap { case (key, i) =>
if (correspond(matcherKey(m), key)) Some(bs -> m.args(i)) else None
})
- }).toMap
+ })
/* Transform the map to sequences into a sequence of maps making sure that the current
* matcher is part of the mapping (otherwise, instantiation has already taken place). */
@@ -711,7 +711,7 @@ trait QuantificationTemplates { self: Templates =>
def promoteQuantifications: Unit = {
val optGen = quantificationsManager.unrollGeneration
- if (!optGen.isDefined)
+ if (optGen.isEmpty)
throw FatalError("Attempting to promote inexistent quantifiers")
val diff = (currentGeneration - optGen.get) max 0
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 667e1b8e318a95e45a00ed43065d9292cf483ed2..887e008442e78b99421f3e0470910f94c6e42992 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -385,7 +385,7 @@ trait AbstractUnrollingSolver
}
case InstantiateQuantifiers =>
- if (!templates.quantificationsManager.unrollGeneration.isDefined) {
+ if (templates.quantificationsManager.unrollGeneration.isEmpty) {
reporter.error("Something went wrong. The model is not transitive yet we can't instantiate!?")
CheckResult.cast(Unknown)
} else {
diff --git a/src/main/scala/inox/utils/ASCIIHelpers.scala b/src/main/scala/inox/utils/ASCIIHelpers.scala
index 3737bd97314a62bd6c1d43548abd44003d12b379..162e6b69b0d5aab54ff06cdc72fb19d85e16aa79 100644
--- a/src/main/scala/inox/utils/ASCIIHelpers.scala
+++ b/src/main/scala/inox/utils/ASCIIHelpers.scala
@@ -87,7 +87,7 @@ object ASCIIHelpers {
sb append " "
}
- val size = (i to i+c.spanning-1).map(colSizes).sum + (c.spanning-1) * 2
+ val size = (i until i + c.spanning).map(colSizes).sum + (c.spanning-1) * 2
if (size >= 0) {
if (c.align == Left) {
diff --git a/src/main/scala/inox/utils/GraphPrinters.scala b/src/main/scala/inox/utils/GraphPrinters.scala
index e4c04a8fc5e0e8e12e472f3ee1bb5efe93faa654..1f08143d367a2044f299ff0aec4613571acba663 100644
--- a/src/main/scala/inox/utils/GraphPrinters.scala
+++ b/src/main/scala/inox/utils/GraphPrinters.scala
@@ -113,7 +113,7 @@ object GraphPrinters {
def nextColor = {
_nextColor += 1
- val colornumber: String = if((_nextColor/bgColors.size)%3 == 0) "" else ((_nextColor/bgColors.size)%3)+"";
+ val colornumber: String = if((_nextColor/bgColors.size)%3 == 0) "" else ((_nextColor/bgColors.size)%3)+""
bgColors(_nextColor%bgColors.size)+colornumber
}
@@ -169,7 +169,7 @@ object GraphPrinters {
"turquoise4", "violet", "violetred", "violetred1", "violetred2", "violetred3",
"violetred4", "wheat", "wheat1", "wheat2", "wheat3", "wheat4", "white",
"whitesmoke", "yellow", "yellow1", "yellow2", "yellow3", "yellow4",
- "yellowgreen");
+ "yellowgreen")
def randomColor = {
_nextColor += 1
diff --git a/src/main/scala/inox/utils/SeqUtils.scala b/src/main/scala/inox/utils/SeqUtils.scala
index 659e5291ce23c7728f6b4c401458ec92d8e2d2df..ad0c997cdbd1184791f69accb6f9dc86d6d579d2 100644
--- a/src/main/scala/inox/utils/SeqUtils.scala
+++ b/src/main/scala/inox/utils/SeqUtils.scala
@@ -63,7 +63,7 @@ object SeqUtils {
var res: Seq[Seq[T]] = Nil
var c = es
- while (!c.isEmpty) {
+ while (c.nonEmpty) {
val (span, rest) = c.span(p)
if (span.isEmpty) {
diff --git a/src/main/scala/inox/utils/StreamUtils.scala b/src/main/scala/inox/utils/StreamUtils.scala
index da89263c58d7797e3bd08f99f9340e28d120d184..a70addd071266dd6575cb592dabd40d09bd382ea 100644
--- a/src/main/scala/inox/utils/StreamUtils.scala
+++ b/src/main/scala/inox/utils/StreamUtils.scala
@@ -36,10 +36,10 @@ object StreamUtils {
}
private def reverseCantorPair(z: Int): (Int, Int) = {
- val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt;
- val x = t * (t + 3) / 2 - z;
- val y = z - t * (t + 1) / 2;
- (x, y)
+ val t = Math.floor((-1.0f + Math.sqrt(1.0f + 8.0f * z))/2.0f).toInt
+ val x = t * (t + 3) / 2 - z
+ val y = z - t * (t + 1) / 2
+ (x, y)
}
/** Combines two streams into one using cantor's unpairing function.