From 17699e7ab0bc23f4626cad6b0dd7a2edc02cf83e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 21 Aug 2015 12:24:09 +0200
Subject: [PATCH] Improvements
---
src/main/scala/leon/datagen/SolverDataGen.scala | 7 +------
src/main/scala/leon/datagen/VanuatooDataGen.scala | 10 ++++------
src/main/scala/leon/evaluators/TracingEvaluator.scala | 2 +-
.../scala/leon/frontends/scalac/ASTExtractors.scala | 4 ++--
.../scala/leon/frontends/scalac/ExtractionPhase.scala | 2 --
.../scala/leon/frontends/scalac/SimpleReporter.scala | 1 -
src/main/scala/leon/grammars/SizeBoundedGrammar.scala | 3 ---
src/main/scala/leon/grammars/ValueGrammar.scala | 2 --
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/repair/rules/Focus.scala | 8 --------
src/main/scala/leon/termination/ChainBuilder.scala | 2 +-
src/main/scala/leon/termination/ChainComparator.scala | 4 ++--
.../leon/termination/ComplexTerminationChecker.scala | 1 -
src/main/scala/leon/termination/Processor.scala | 1 -
.../scala/leon/termination/RecursionProcessor.scala | 2 --
.../scala/leon/termination/RelationProcessor.scala | 4 ----
.../scala/leon/termination/SelfCallsProcessor.scala | 1 -
src/main/scala/leon/termination/Strengthener.scala | 5 +----
src/main/scala/leon/termination/StructuralSize.scala | 4 +---
src/main/scala/leon/termination/TerminationPhase.scala | 1 -
src/main/scala/leon/utils/Benchmarks.scala | 4 ++--
src/main/scala/leon/utils/FreeableIterator.scala | 2 +-
src/main/scala/leon/utils/Graphs.scala | 6 +++---
src/main/scala/leon/utils/ModelEnumerator.scala | 8 ++++----
.../leon/verification/VerificationCondition.scala | 2 +-
25 files changed, 25 insertions(+), 63 deletions(-)
diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 78b3753cf..027cc41e0 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -8,12 +8,7 @@ import purescala.Types._
import purescala.Definitions._
import purescala.Common._
import purescala.Constructors._
-import purescala.Extractors._
-import evaluators._
import solvers._
-import solvers.combinators._
-import solvers.smtlib._
-import solvers.z3._
import utils._
@@ -68,7 +63,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
sizeFor(tupleSelect(of, i+1, tps.size))
}
- exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus _)
+ exprs.foldLeft(InfiniteIntegerLiteral(1): Expr)(plus)
case _ =>
InfiniteIntegerLiteral(1)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 1751a1e55..72a905b82 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -280,20 +280,18 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
// Split conjunctions
val TopLevelAnds(ands) = satisfying
- val runners = ands.map(a => compile(a, ins) match {
+ val runners = ands.flatMap(a => compile(a, ins) match {
case Some(runner) => Some(runner)
case None =>
- ctx.reporter.error("Could not compile predicate "+a)
+ ctx.reporter.error("Could not compile predicate " + a)
None
- }).flatten
+ })
val gen = new StubGenerator[Expr, TypeTree]((ints.values ++ bigInts.values ++ booleans.values).toSeq,
Some(getConstructors _),
treatEmptyStubsAsChildless = true)
- var found = Set[Seq[Expr]]()
-
/**
* Gather at most <n> isomoprhic models before skipping them
* - Too little means skipping many excluding patterns
@@ -315,7 +313,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
theNext = computeNext()
}
- theNext != None
+ theNext.isDefined
}
def next() = {
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index d6388822c..ea5ad3e0d 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -14,7 +14,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
def initRC(mappings: Map[Identifier, Expr]) = TracingRecContext(mappings, 2)
- def initGC = new TracingGlobalContext(Nil)
+ def initGC() = new TracingGlobalContext(Nil)
class TracingGlobalContext(var values: List[(Tree, Expr)]) extends GlobalContext
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 919118dd9..3c4818737 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -575,7 +575,7 @@ trait ASTExtractors {
case a @ Apply(
TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "withOracle"), types),
Function(vds, body) :: Nil) =>
- Some(((types zip vds.map(_.symbol)), body))
+ Some((types zip vds.map(_.symbol), body))
case _ => None
}
}
@@ -592,7 +592,7 @@ trait ASTExtractors {
case a @ Apply(
TypeApply(s @ ExSymbol("leon", "lang", "forall"), types),
Function(vds, predicateBody) :: Nil) =>
- Some(((types zip vds.map(_.symbol)), predicateBody))
+ Some((types zip vds.map(_.symbol), predicateBody))
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 461f14501..17503361e 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -4,8 +4,6 @@ package leon
package frontends.scalac
import purescala.Definitions.Program
-import purescala.Common.FreshIdentifier
-
import utils._
import scala.tools.nsc.{Settings,CompilerCommand}
diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index d04cebb3e..c203ee63c 100644
--- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -51,7 +51,6 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
case NoPosition =>
printMessage(msg, LeonNoPosition, severity)
case _ =>
- val buf = new StringBuilder(msg)
val lpos = LeonOffsetPosition(pos.line, pos.column, pos.point, pos.source.file.file)
printMessage(msg, lpos, severity)
}
diff --git a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
index 697120356..8756b136a 100644
--- a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
@@ -4,9 +4,6 @@ package leon
package grammars
import purescala.Types._
-import purescala.Expressions._
-import purescala.TypeOps._
-
import leon.utils.SeqUtils.sumTo
case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
index 2b7bb140b..5442b4ee7 100644
--- a/src/main/scala/leon/grammars/ValueGrammar.scala
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -5,8 +5,6 @@ package grammars
import purescala.Types._
import purescala.Expressions._
-import purescala.Constructors._
-
case object ValueGrammar extends ExpressionGrammar[TypeTree] {
def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index a8a043047..0433affa5 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -93,7 +93,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
bh += be
- bh.write
+ bh.write()
}
if (synth.settings.generateDerivationTrees) {
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 262d40580..8c1694dbd 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -5,25 +5,17 @@ package repair
package rules
import synthesis._
-
-import leon.utils.Simplifiers
-
-import purescala.ScalaPrinter
-
import evaluators._
import purescala.Expressions._
-import purescala.Definitions._
import purescala.Common._
import purescala.Types._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Extractors._
import Witnesses._
-import solvers._
import graph.AndNode
case object Focus extends PreprocessingRule("Focus") {
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 8470a9744..0c6106127 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -90,7 +90,7 @@ final case class Chain(relations: List[Relation]) {
}
*/
- lazy val cycles : Seq[List[Relation]] = (0 to relations.size - 1).map { index =>
+ lazy val cycles : Seq[List[Relation]] = relations.indices.map { index =>
val (start, end) = relations.splitAt(index)
end ++ start
}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index a3ab3f8f4..0c3cbd875 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -37,7 +37,7 @@ trait ChainComparator { self : StructuralSize =>
rec(fieldTpe).map(recons => (e: Expr) => recons(caseClassSelector(cct, e, fieldId)))
})
case TupleType(tpes) =>
- powerSetToFunSet((0 until tpes.length).flatMap { case index =>
+ powerSetToFunSet(tpes.indices.flatMap { case index =>
rec(tpes(index)).map(recons => (e: Expr) => recons(tupleSelect(e, index + 1, true)))
})
case _ => Set((e: Expr) => e)
@@ -53,7 +53,7 @@ trait ChainComparator { self : StructuralSize =>
rec(fieldTpe).map(recons => (e: Expr) => recons(caseClassSelector(cct, e, fieldId)))
}.toSet
case TupleType(tpes) =>
- (0 until tpes.length).flatMap { case index =>
+ tpes.indices.flatMap { case index =>
rec(tpes(index)).map(recons => (e: Expr) => recons(tupleSelect(e, index + 1, true)))
}.toSet
case _ => Set((e: Expr) => e)
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index eef8ddaac..83638aa84 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,6 @@ package leon
package termination
import purescala.Definitions._
-import purescala.Expressions._
import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index db91c8602..91590dd4a 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -10,7 +10,6 @@ import purescala.Definitions._
import scala.concurrent.duration._
import leon.solvers._
-import leon.solvers.z3._
trait Processor {
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 2a93aa853..72c64f62a 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -50,5 +50,3 @@ class RecursionProcessor(val checker: TerminationChecker, val rb: RelationBuilde
}
}
}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 2909d6c4f..d71a6fa3a 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -4,10 +4,6 @@ package leon
package termination
import leon.purescala.Expressions._
-import leon.purescala.ExprOps._
-import leon.purescala.Types._
-import leon.purescala.Common._
-import leon.purescala.Extractors._
import leon.purescala.Constructors._
import leon.purescala.Definitions._
diff --git a/src/main/scala/leon/termination/SelfCallsProcessor.scala b/src/main/scala/leon/termination/SelfCallsProcessor.scala
index 8b53f7cd1..b8fe65f48 100644
--- a/src/main/scala/leon/termination/SelfCallsProcessor.scala
+++ b/src/main/scala/leon/termination/SelfCallsProcessor.scala
@@ -6,7 +6,6 @@ package termination
import purescala.Definitions._
import purescala.Common._
import purescala.Expressions._
-import purescala.Constructors._
class SelfCallsProcessor(val checker: TerminationChecker) extends Processor {
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index 192e78599..dc3d08188 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -20,7 +20,7 @@ trait Strengthener { self : RelationComparator =>
def strengthenPostconditions(funDefs: Set[FunDef])(implicit solver: Processor with Solvable) {
// Strengthen postconditions on all accessible functions by adding size constraints
- val callees : Set[FunDef] = funDefs.map(fd => checker.program.callGraph.transitiveCallees(fd)).flatten
+ val callees : Set[FunDef] = funDefs.flatMap(fd => checker.program.callGraph.transitiveCallees(fd))
val sortedCallees : Seq[FunDef] = callees.toSeq.sortWith((fd1, fd2) => checker.program.callGraph.transitivelyCalls(fd2, fd1))
for (funDef <- sortedCallees if !strengthenedPost(funDef) && funDef.hasBody && checker.terminates(funDef).isGuaranteed) {
@@ -175,6 +175,3 @@ trait Strengthener { self : RelationComparator =>
}
}
}
-
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 99b3c18f6..cb8fa0538 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -90,7 +90,7 @@ trait StructuralSize {
def lexicographicDecreasing(s1: Seq[Expr], s2: Seq[Expr], strict: Boolean, sizeOfOneExpr: Expr => Expr): Expr = {
// Note: The Equal and GreaterThan ASTs work for both BigInt and Bitvector
- val sameSizeExprs = for ((arg1, arg2) <- (s1 zip s2)) yield Equals(sizeOfOneExpr(arg1), sizeOfOneExpr(arg2))
+ val sameSizeExprs = for ((arg1, arg2) <- s1 zip s2) yield Equals(sizeOfOneExpr(arg1), sizeOfOneExpr(arg2))
val greaterBecauseGreaterAtFirstDifferentPos =
orJoin(for (firstDifferent <- 0 until scala.math.min(s1.length, s2.length)) yield and(
@@ -107,5 +107,3 @@ trait StructuralSize {
def defs : Set[FunDef] = Set(sizeCache.values.toSeq : _*)
}
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index b13c109ad..a9f7ef77b 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -4,7 +4,6 @@ package leon
package termination
import purescala.Definitions._
-import purescala.DefOps._
object TerminationPhase extends LeonPhase[Program,TerminationReport] {
val name = "Termination"
diff --git a/src/main/scala/leon/utils/Benchmarks.scala b/src/main/scala/leon/utils/Benchmarks.scala
index c3927ad12..71d948949 100644
--- a/src/main/scala/leon/utils/Benchmarks.scala
+++ b/src/main/scala/leon/utils/Benchmarks.scala
@@ -6,7 +6,7 @@ package utils
import java.io.{File, PrintWriter}
import scala.io.Source
-import com.fasterxml.jackson.databind.{DeserializationFeature, ObjectMapper}
+import com.fasterxml.jackson.databind.ObjectMapper
import com.fasterxml.jackson.module.scala.experimental.ScalaObjectMapper
import com.fasterxml.jackson.module.scala.DefaultScalaModule
@@ -38,7 +38,7 @@ class BenchmarksHistory(file: File) {
try {
pw.write(json)
} finally {
- pw.close
+ pw.close()
}
}
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index a15922640..f6ad42937 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -4,7 +4,7 @@ package utils
abstract class FreeableIterator[T] extends Iterator[T] {
private[this] var nextElem: Option[T] = None
- def hasNext() = {
+ def hasNext = {
nextElem = computeNext()
nextElem.nonEmpty
}
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index 604bef784..b3aeef558 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -172,7 +172,7 @@ object Graphs {
} else {
seen += v
val ins = inEdges(v).map(_.v1)
- ins ++ ins.map(rec).flatten
+ ins ++ ins.flatMap(rec)
}
}
rec(v)
@@ -186,7 +186,7 @@ object Graphs {
} else {
seen += v
val outs = outEdges(v).map(_.v2)
- outs ++ outs.map(rec).flatten
+ outs ++ outs.flatMap(rec)
}
}
rec(v)
@@ -203,7 +203,7 @@ object Graphs {
if (outs(v2)) {
true
} else {
- outs.map(rec).contains(true)
+ outs.exists(rec)
}
}
}
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index d49282639..7494e0c46 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -49,9 +49,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
s.check match {
case Some(true) =>
val model = s.getModel
- val idsModel = (ids.map { id =>
+ val idsModel = ids.map { id =>
id -> model.getOrElse(id, simplestValue(id.getType))
- }).toMap
+ }.toMap
// Vary the model
s.assertCnstr(not(andJoin(idsModel.toSeq.sortBy(_._1).map { case (k, v) => equality(k.toVariable, v) })))
@@ -148,9 +148,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
s.check match {
case Some(true) =>
val sm = s.getModel
- val m = (ids.map { id =>
+ val m = ids.map { id =>
id -> sm.getOrElse(id, simplestValue(id.getType))
- }).toMap
+ }.toMap
evaluator.eval(measure, m).result match {
case Some(InfiniteIntegerLiteral(measureVal)) =>
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 312856790..ba23961e3 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -65,7 +65,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
}
if (strings.nonEmpty) {
- val max = strings.map(_._1.size).max
+ val max = strings.map(_._1.length).max
for ((id, v) <- strings) {
reporter.warning((" %-"+max+"s -> %s").format(id, v))
--
GitLab