diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java
index d7f3d90fbfa7a50111d914e03371dfa2bdbfe1d2..3b1c35922c943d14db7dbbde4fc10591e0ac1eea 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeHashing.java
@@ -4,24 +4,24 @@ package leon.codegen.runtime;
// MurmurHash3, reproduced from std. Scala lib.
public final class LeonCodeGenRuntimeHashing {
- public static final int seqHash(Object[] elements, int seed) {
+ public static int seqHash(Object[] elements, int seed) {
// I feel good about this line.
int h = avalanche(seed ^ 0xcafebabe);
int sz = elements.length;
if(sz == 0) return h;
- for(int i = 0; i < sz; i++) {
- h = mix(h, elements[i].hashCode());
- }
+ for (Object element : elements) {
+ h = mix(h, element.hashCode());
+ }
return finalizeHash(h, sz);
}
- private static final int mix(int hash, int data) {
+ private static int mix(int hash, int data) {
int h = mixLast(hash, data);
h = Integer.rotateLeft(h, 13);
return h * 5 + 0xe6546b64;
}
- private static final int mixLast(int hash, int data) {
+ private static int mixLast(int hash, int data) {
int k = data;
k *= 0xcc9e2d51;
k = Integer.rotateLeft(k, 15);
@@ -29,11 +29,11 @@ public final class LeonCodeGenRuntimeHashing {
return hash ^ k;
}
- private static final int finalizeHash(int hash, int length) {
+ private static int finalizeHash(int hash, int length) {
return avalanche(hash ^ length);
}
- private static final int avalanche(int hash) {
+ private static int avalanche(int hash) {
int h = hash;
h ^= h >>> 16;
h *= 0x85ebca6b;
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
index 65454c0b0dd656c7d5f8fd0c54cc1db841a5a27d..bcae3f89f468d2795f1628178eff43432697cb1d 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeMonitor.java
@@ -12,12 +12,10 @@ public class LeonCodeGenRuntimeMonitor {
}
public void onInvoke() throws LeonCodeGenEvaluationException {
- if(invocationsLeft < 0) {
- return;
+ if(invocationsLeft > 0) {
+ invocationsLeft--;
} else if(invocationsLeft == 0) {
throw new LeonCodeGenEvaluationException("Maximum number of invocations reached.");
- } else {
- invocationsLeft--;
}
}
}
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index e5e1db5846cdae5ce95e241d3ca26ab0675ca0a0..ce7582e355795a84a4d41c1bfabd730cbfee6e94 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -84,9 +84,7 @@ public final class Set {
Set other = (Set)that;
- if(this.size() != other.size()) return false;
-
- return this.subsetOf(other);
+ return this.size() == other.size() && this.subsetOf(other);
}
@Override
diff --git a/src/main/java/leon/codegen/runtime/Tuple.java b/src/main/java/leon/codegen/runtime/Tuple.java
index c83048dd2d5f59482d94c01551786baa913f83c2..a27a2e00e97fe8c74a7749d80921f02ac1a4b6a4 100644
--- a/src/main/java/leon/codegen/runtime/Tuple.java
+++ b/src/main/java/leon/codegen/runtime/Tuple.java
@@ -49,7 +49,7 @@ public final class Tuple {
@Override
final public int hashCode() {
if(_hash != 0) return _hash;
- int seed = (new String("Tuple" + getArity())).hashCode();
+ int seed = ("Tuple" + getArity()).hashCode();
int h = LeonCodeGenRuntimeHashing.seqHash(elements, seed);
_hash = h;
return h;
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 78f887914eb8224b053be19c2481905e32100b25..5516506dfbafa65fc6b0fc2489c469d0eac704ec 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -9,7 +9,7 @@ sealed abstract class LeonOption {
/** Boolean (on/off) options. Present means "on". */
case class LeonFlagOption(name: String, value: Boolean) extends LeonOption {
- override def toString() : String = {
+ override def toString: String = {
if (value) {
"--" + name
} else {
@@ -38,7 +38,7 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
None
}
- override def toString() : String = "--%s=%s".format(name, value)
+ override def toString: String = "--%s=%s".format(name, value)
}
sealed abstract class LeonOptionDef {
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 4877a7d342772f0a073ff69cde9118fa6873cbfb..31baa4a3363406822a1653295a762ac5ad18196b 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -29,7 +29,7 @@ abstract class UnitPhase[T] extends LeonPhase[T, T] {
}
case class NoopPhase[T]() extends LeonPhase[T, T] {
- val name = "noop";
+ val name = "noop"
val description = "no-op"
override def run(ctx: LeonContext)(v: T) = v
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index dd177e7e20dab7ee8baafe06cb4a6f8b434f5df2..e8ca95a69b8d8a7e370531f28c11f2637fe22741 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -54,7 +54,7 @@ object Main {
reporter.info("")
reporter.info("Additional options, by component:")
- for (c <- allComponents.toSeq.sortBy(_.name) if !c.definedOptions.isEmpty) {
+ for (c <- allComponents.toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
reporter.info("%s (%s)".format(c.name, c.description))
for(opt <- c.definedOptions.toSeq.sortBy(_.name)) {
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 9bd1a983f6096d68cbb870097db16ac386209bcc..c2295e0d1502d635886053e218e13c9d772a1e84 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -14,7 +14,7 @@ abstract class Reporter(settings: Settings) {
case object INTERNAL extends Severity
case class DEBUG(section: DebugSection) extends Severity
- case class Message(severity: Severity, position: Position, msg: Any);
+ case class Message(severity: Severity, position: Position, msg: Any)
private var _errorCount : Int = 0
private var _warningCount : Int = 0
@@ -155,7 +155,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
val carret = if (bp.line == ep.line) {
val width = Math.max(ep.col - bp.col, 1)
- ("^" * width)
+ "^" * width
} else {
val width = Math.max(line.length+1-bp.col, 1)
("^" * width)+"..."
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index ad77182a864910fa69c06f9467e83b349f6e4d99..5032acb94ba854fbbfb1a6f4b5c7e2eb7111f44c 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -5,13 +5,13 @@ package leon
import utils.DebugSection
case class Settings(
- val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
- val terminateAfterEachPhase: Boolean = true, // Terminates Leon after each phase if an error occured
- val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
- val termination: Boolean = false,
- val repair: Boolean = false,
- val synthesis: Boolean = false,
- val xlang: Boolean = false,
- val verify: Boolean = true,
- val selectedSolvers: Set[String] = Set("fairz3")
+ strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
+ terminateAfterEachPhase: Boolean = true, // Terminates Leon after each phase if an error occured
+ debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
+ termination: Boolean = false,
+ repair: Boolean = false,
+ synthesis: Boolean = false,
+ xlang: Boolean = false,
+ verify: Boolean = true,
+ selectedSolvers: Set[String] = Set("fairz3")
)
diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
index 714531f785c68310e8cd09237633feeeaf9e8dbd..3e0e7d84d4fa66ed1bdfc16cd9ed3b75b344f313 100644
--- a/src/main/scala/leon/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -39,7 +39,7 @@ class Stopwatch(name: String = "Stopwatch") {
this
}
- def stop {
+ def stop() {
end = System.currentTimeMillis
acc += (end - beginning)
beginning = 0L
diff --git a/src/main/scala/leon/codegen/CodeGenPhase.scala b/src/main/scala/leon/codegen/CodeGenPhase.scala
index 8acf1fa619d7b8b4642f82babc149149965e6ecf..6339a43054ba79afb5c65f1f56e841ccbceee4af 100644
--- a/src/main/scala/leon/codegen/CodeGenPhase.scala
+++ b/src/main/scala/leon/codegen/CodeGenPhase.scala
@@ -13,7 +13,7 @@ object CodeGenPhase extends LeonPhase[Program,CompilationResult] {
def run(ctx : LeonContext)(p : Program) : CompilationResult = {
try {
- val unit = new CompilationUnit(ctx, p);
+ val unit = new CompilationUnit(ctx, p)
unit.writeClassFiles("./")
CompilationResult(successful = true)
} catch {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 95d1e0d954d2c2df0516c344603de20d9fd215b1..7dd3d3dd40585fdf24d7527fc4898f7339b88a82 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -790,7 +790,7 @@ trait CodeGeneration {
case choose @ Choose(_, None) =>
val prob = synthesis.Problem.fromChoose(choose)
- val id = runtime.ChooseEntryPoint.register(prob, this);
+ val id = runtime.ChooseEntryPoint.register(prob, this)
ch << Ldc(id)
@@ -810,7 +810,7 @@ trait CodeGeneration {
mkUnbox(choose.getType, ch)
case gv @ GenericValue(tp, int) =>
- val id = runtime.GenericValues.register(gv);
+ val id = runtime.GenericValues.register(gv)
ch << Ldc(id)
ch << InvokeStatic(GenericValuesClass, "get", "(I)Ljava/lang/Object;")
@@ -1502,7 +1502,7 @@ trait CodeGeneration {
ech << ALoad(1) << InstanceOf(cName) << IfEq(notEq)
// ...finally, we compare fields one by one, shortcircuiting on disequalities.
- if(!ccd.fields.isEmpty) {
+ if(ccd.fields.nonEmpty) {
ech << ALoad(1) << CheckCast(cName) << AStore(castSlot)
for(vd <- ccd.fields) {
@@ -1532,7 +1532,7 @@ trait CodeGeneration {
// definition of hashcode
locally {
val hashFieldName = "$leon$hashCode"
- cf.addField("I", hashFieldName).setFlags((FIELD_ACC_PRIVATE).asInstanceOf[U2])
+ cf.addField("I", hashFieldName).setFlags(FIELD_ACC_PRIVATE)
val hmh = cf.addMethod("I", "hashCode", "")
hmh.setFlags((
METHOD_ACC_PUBLIC |
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 759af0eaf0e745e062a0c06d01f86ba240ccdf8e..70f9342dd17380bc5191a577f5be872f183dcb8c 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -102,8 +102,8 @@ class CompilationUnit(val ctx: LeonContext,
case Some(cf) =>
val klass = loader.loadClass(cf.className)
// This is a hack: we pick the constructor with the most arguments.
- val conss = klass.getConstructors().sortBy(_.getParameterTypes().length)
- assert(!conss.isEmpty)
+ val conss = klass.getConstructors.sortBy(_.getParameterTypes.length)
+ assert(conss.nonEmpty)
val cons = conss.last
ccdConstructors += ccd -> cons
@@ -116,8 +116,8 @@ class CompilationUnit(val ctx: LeonContext,
private[this] lazy val tupleConstructor: Constructor[_] = {
val tc = loader.loadClass("leon.codegen.runtime.Tuple")
- val conss = tc.getConstructors().sortBy(_.getParameterTypes().length)
- assert(!conss.isEmpty)
+ val conss = tc.getConstructors.sortBy(_.getParameterTypes.length)
+ assert(conss.nonEmpty)
conss.last
}
@@ -138,12 +138,12 @@ class CompilationUnit(val ctx: LeonContext,
e
case Tuple(elems) =>
- tupleConstructor.newInstance(elems.map(exprToJVM _).toArray).asInstanceOf[AnyRef]
+ tupleConstructor.newInstance(elems.map(exprToJVM).toArray).asInstanceOf[AnyRef]
case CaseClass(cct, args) =>
caseClassConstructor(cct.classDef) match {
case Some(cons) =>
- val realArgs = if (params.requireMonitor) monitor +: args.map(exprToJVM _) else args.map(exprToJVM _)
+ val realArgs = if (params.requireMonitor) monitor +: args.map(exprToJVM) else args.map(exprToJVM)
cons.newInstance(realArgs.toArray : _*).asInstanceOf[AnyRef]
case None =>
ctx.reporter.fatalError("Case class constructor not found?!?")
@@ -174,7 +174,7 @@ class CompilationUnit(val ctx: LeonContext,
for ((k,v) <- els) {
val ks = unwrapTuple(k, f.getType.asInstanceOf[FunctionType].from.size)
// Force tuple even with 1/0 elems.
- val kJvm = tupleConstructor.newInstance(ks.map(exprToJVM _).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
+ val kJvm = tupleConstructor.newInstance(ks.map(exprToJVM).toArray).asInstanceOf[leon.codegen.runtime.Tuple]
val vJvm = exprToJVM(v)
l.add(kJvm,vJvm)
}
@@ -216,7 +216,7 @@ class CompilationUnit(val ctx: LeonContext,
CaseClass(cct, (fields zip cct.fieldsTypes).map { case (e, tpe) => jvmToExpr(e, tpe) })
case (tpl: runtime.Tuple, tpe) =>
- val stpe = unwrapTupleType(tpe, tpl.getArity())
+ val stpe = unwrapTupleType(tpe, tpl.getArity)
val elems = stpe.zipWithIndex.map { case (tpe, i) =>
jvmToExpr(tpl.get(i), tpe)
}
@@ -227,12 +227,12 @@ class CompilationUnit(val ctx: LeonContext,
else GenericValue(tp, id).copiedFrom(gv)
case (set : runtime.Set, SetType(b)) =>
- finiteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSet, b)
+ finiteSet(set.getElements.asScala.map(jvmToExpr(_, b)).toSet, b)
case (map : runtime.Map, MapType(from, to)) =>
- val pairs = map.getElements().asScala.map { entry =>
- val k = jvmToExpr(entry.getKey(), from)
- val v = jvmToExpr(entry.getValue(), to)
+ val pairs = map.getElements.asScala.map { entry =>
+ val k = jvmToExpr(entry.getKey, from)
+ val v = jvmToExpr(entry.getValue, to)
(k, v)
}
finiteMap(pairs.toSeq, from, to)
@@ -241,7 +241,7 @@ class CompilationUnit(val ctx: LeonContext,
throw CompilationException("Unsupported return value : " + e.getClass +" while expecting "+tpe)
}
- var compiledN = 0;
+ var compiledN = 0
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
if(e.getType == Untyped) {
@@ -421,7 +421,7 @@ class CompilationUnit(val ctx: LeonContext,
}
- classes.values.foreach(loader.register _)
+ classes.values.foreach(loader.register)
}
def writeClassFiles(prefix: String) {
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 78cca61d102e038cef7e6172738b318d12e2dd2b..e75c9b0bb9a709790f7b7d9d7cc3a3901d94a878 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -47,7 +47,7 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
try {
unit.jvmToExpr(evalToJVM(args, monitor), exprType)
} catch {
- case ite : InvocationTargetException => throw ite.getCause()
+ case ite : InvocationTargetException => throw ite.getCause
}
}
@@ -57,7 +57,7 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
new LM(params.maxFunctionInvocations)
evalFromJVM(argsToJVM(args, monitor),monitor)
} catch {
- case ite : InvocationTargetException => throw ite.getCause()
+ case ite : InvocationTargetException => throw ite.getCause
}
}
}
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 2835a8f41d1683e5f40fe3b8b34bd7f639430344..0f8762d4eb605a9761cec88642b846eeb9aada24 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -46,7 +46,7 @@ object ChooseEntryPoint {
if (cache contains (i, is)) {
cache((i, is))
} else {
- val tStart = System.currentTimeMillis;
+ val tStart = System.currentTimeMillis
val solver = (new FairZ3Solver(ctx, program) with TimeoutSolver).setTimeout(10000L)
@@ -60,14 +60,14 @@ object ChooseEntryPoint {
try {
solver.check match {
case Some(true) =>
- val model = solver.getModel;
+ val model = solver.getModel
val valModel = valuateWithModel(model) _
val res = p.xs.map(valModel)
val leonRes = tupleWrap(res)
- val total = System.currentTimeMillis-tStart;
+ val total = System.currentTimeMillis-tStart
ctx.reporter.debug("Synthesis took "+total+"ms")
ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala
index dee6b18503b843873ae68aa2747f49e0d3d2fe9f..0bf7b27ae34efd56225e63c3442ac2fde567b392 100644
--- a/src/main/scala/leon/codegen/runtime/GenericValues.scala
+++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala
@@ -7,7 +7,7 @@ import purescala.Trees.GenericValue
import scala.collection.immutable.{Map => ScalaMap}
object GenericValues {
- private[this] var counter = 0;
+ private[this] var counter = 0
private[this] var gvToI = ScalaMap[GenericValue, Int]()
private[this] var iTogv = ScalaMap[Int, GenericValue]()
@@ -16,7 +16,7 @@ object GenericValues {
if (gvToI contains gv) {
gvToI(gv)
} else {
- counter += 1;
+ counter += 1
gvToI += gv -> counter
iTogv += counter -> gv
counter
diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index e97321053accebe5ecbb14756e48f3bafaef3d77..3a34af97f7cc4d7bfcb658795e8b219fc07a0c6c 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -12,7 +12,7 @@ import java.util.concurrent.atomic.AtomicBoolean
trait DataGenerator extends Interruptible {
implicit val debugSection = DebugSectionDataGen
- def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]];
+ def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]]
protected val interrupted: AtomicBoolean = new AtomicBoolean(false)
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index b447778728d90730833b63a8fba3251c09e6c49e..91238109ab5e14f8ea80c72403ed345509f2f49f 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -48,7 +48,7 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
tpStream(tp)
case TupleType(bses) =>
- cartesianProduct(bses.map(generate(_))).map(Tuple)
+ cartesianProduct(bses.map(generate)).map(Tuple)
case act : AbstractClassType =>
// We prioritize base cases among the children.
@@ -76,7 +76,7 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
Stream.cons(CaseClass(cct, Nil), Stream.empty)
} else {
val fieldTypes = cct.fieldsTypes
- cartesianProduct(fieldTypes.map(generate(_))).map(CaseClass(cct, _))
+ cartesianProduct(fieldTypes.map(generate)).map(CaseClass(cct, _))
}
case _ => Stream.empty
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 5858407944a4c228c9c6f65d5122c9c423ad2690..daec365e46bc61d851c426bbd4ab7deaec912466 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -199,7 +199,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case (t: codegen.runtime.Tuple, tpe) =>
val r = t.__getRead()
- val parts = unwrapTupleType(tpe, t.getArity())
+ val parts = unwrapTupleType(tpe, t.getArity)
val c = getConstructors(tpe)(0)
@@ -231,7 +231,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val ttype = tupleTypeWrap(argorder.map(_.getType))
val tid = FreshIdentifier("tup", ttype)
- val map = argorder.zipWithIndex.map{ case (id, i) => (id -> tupleSelect(Variable(tid), i+1, argorder.size)) }.toMap
+ val map = argorder.zipWithIndex.map{ case (id, i) => id -> tupleSelect(Variable(tid), i + 1, argorder.size) }.toMap
val newExpr = replaceFromIDs(map, expression)
@@ -270,7 +270,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
})
} catch {
case t: Throwable =>
- ctx.reporter.warning("Error while compiling expression: "+t.getMessage); t.printStackTrace
+ ctx.reporter.warning("Error while compiling expression: "+t.getMessage); t.printStackTrace()
None
}
}
@@ -299,17 +299,17 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
* - Too large means repetitive (and not useful models) before reaching maxEnumerated
*/
- val maxIsomorphicModels = maxValid+1;
+ val maxIsomorphicModels = maxValid+1
val it = gen.enumerate(tupleTypeWrap(ins.map(_.getType)))
- return new Iterator[Seq[Expr]] {
+ new Iterator[Seq[Expr]] {
var total = 0
var found = 0
var theNext: Option[Seq[Expr]] = None
- def hasNext() = {
+ def hasNext = {
if (total == 0) {
theNext = computeNext()
}
@@ -327,20 +327,20 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
def computeNext(): Option[Seq[Expr]] = {
//return None
while(total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) {
- val model = it.next
+ val model = it.next()
if (model eq null) {
total = maxEnumerated
} else {
total += 1
- var failed = false;
+ var failed = false
for (r <- runners) r(model) match {
case (EvaluationResults.Successful(BooleanLiteral(true)), _) =>
case (_, Some(pattern)) =>
- failed = true;
+ failed = true
it.exclude(pattern)
case (_, None) =>
@@ -359,7 +359,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
it.skipIsomorphic()
}
- return Some(unwrapTuple(model, ins.size));
+ return Some(unwrapTuple(model, ins.size))
}
//if (total % 1000 == 0) {
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index b350aafc54e16779b021d99a8046d1ef11074806..bef203c064a75c68eab2c61e6ae47783af872850 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -39,12 +39,12 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
val allArgs = if (params.requireMonitor) monitor +: args else args
- ctx.reporter.debug(s"Calling ${className}.${methodName}(${args.mkString(",")})")
+ ctx.reporter.debug(s"Calling $className.$methodName(${args.mkString(",")})")
try {
val cl = unit.loader.loadClass(className)
- val meth = cl.getMethods().find(_.getName() == methodName).get
+ val meth = cl.getMethods.find(_.getName == methodName).get
val res = if (allArgs.isEmpty) {
meth.invoke(null)
@@ -67,12 +67,12 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
val (className, fieldName, _) = unit.leonFunDefToJVMInfo(fd).get
- ctx.reporter.debug(s"Retrieving ${className}.${fieldName}")
+ ctx.reporter.debug(s"Retrieving $className.$fieldName")
try {
val cl = unit.loader.loadClass(className)
- val field = cl.getFields().find(_.getName() == fieldName).get
+ val field = cl.getFields.find(_.getName == fieldName).get
val res = field.get(null)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 7bac62443527f46f673cd3d74d0bf55ca0177f03..e52d12904bcab37413283a273e1896cc9ce2a85c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -32,7 +32,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
trait RecContext {
def mappings: Map[Identifier, Expr]
- def newVars(news: Map[Identifier, Expr]): RC;
+ def newVars(news: Map[Identifier, Expr]): RC
def withNewVar(id: Identifier, v: Expr): RC = {
newVars(mappings + (id -> v))
@@ -76,7 +76,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
rctx.mappings.get(id) match {
- case Some(v) if (v != expr) =>
+ case Some(v) if v != expr =>
e(v)
case Some(v) =>
v
@@ -222,7 +222,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
case CaseClass(cd, args) =>
- CaseClass(cd, args.map(e(_)))
+ CaseClass(cd, args.map(e))
case CaseClassInstanceOf(cct, expr) =>
val le = e(expr)
@@ -289,14 +289,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case Division(l,r) =>
(e(l), e(r)) match {
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
- if(i2 != 0) InfiniteIntegerLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
+ if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
}
case Modulo(l,r) =>
(e(l), e(r)) match {
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
- if(i2 != 0) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
+ if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
}
@@ -395,7 +395,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetIntersection(s1,s2) =>
(e(s1), e(s2)) match {
case (f @ FiniteSet(els1), FiniteSet(els2)) => {
- val newElems = (els1 intersect els2)
+ val newElems = els1 intersect els2
val SetType(tpe) = f.getType
finiteSet(newElems, tpe)
}
@@ -429,7 +429,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case f @ FiniteSet(els) =>
val SetType(tp) = f.getType
- finiteSet(els.map(e(_)), tp)
+ finiteSet(els.map(e), tp)
case i @ IntLiteral(_) => i
case i @ InfiniteIntegerLiteral(_) => i
case b @ BooleanLiteral(_) => b
@@ -517,9 +517,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
if (clpCache contains (choose, ins)) {
clpCache((choose, ins))
} else {
- val tStart = System.currentTimeMillis;
+ val tStart = System.currentTimeMillis
- val solver = SolverFactory.getFromSettings(ctx, program).getNewSolver
+ val solver = SolverFactory.getFromSettings(ctx, program).getNewSolver()
val eqs = p.as.map {
case id =>
@@ -532,13 +532,13 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
try {
solver.check match {
case Some(true) =>
- val model = solver.getModel;
+ val model = solver.getModel
val valModel = valuateWithModel(model) _
val res = p.xs.map(valModel)
val leonRes = tupleWrap(res)
- val total = System.currentTimeMillis-tStart;
+ val total = System.currentTimeMillis-tStart
ctx.reporter.debug("Synthesis took "+total+"ms")
ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index ea6309c8cc901fac3718981fb8f3f3797b1be6dc..a66f16300a7ecaafbc08538d8a3c07461ed140f8 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -266,7 +266,7 @@ trait ASTExtractors {
* visibility. Does not match on the automatically generated companion
* objects of case classes (or any synthetic class). */
def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
- case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
+ case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic => {
Some((name.toString, impl))
}
case _ => None
@@ -279,7 +279,7 @@ trait ASTExtractors {
* no abstract members. */
def unapply(cd: ClassDef): Option[(String, Symbol, Template)] = cd match {
// abstract class
- case ClassDef(_, name, tparams, impl) if (cd.symbol.isAbstractClass) => Some((name.toString, cd.symbol, impl))
+ case ClassDef(_, name, tparams, impl) if cd.symbol.isAbstractClass => Some((name.toString, cd.symbol, impl))
case _ => None
}
@@ -287,11 +287,11 @@ trait ASTExtractors {
object ExCaseClass {
def unapply(cd: ClassDef): Option[(String,Symbol,Seq[(Symbol,ValDef)], Template)] = cd match {
- case ClassDef(_, name, tparams, impl) if (cd.symbol.isCase && !cd.symbol.isAbstractClass && impl.body.size >= 8) => {
- val constructor: DefDef = impl.children.find(child => child match {
+ case ClassDef(_, name, tparams, impl) if cd.symbol.isCase && !cd.symbol.isAbstractClass && impl.body.size >= 8 => {
+ val constructor: DefDef = impl.children.find {
case ExConstructorDef() => true
case _ => false
- }).get.asInstanceOf[DefDef]
+ }.get.asInstanceOf[DefDef]
val args = constructor.vparamss.flatten.map(vd => ( vd.symbol, vd))
Some((name.toString, cd.symbol, args, impl))
@@ -324,21 +324,21 @@ trait ASTExtractors {
object ExCaseClassSyntheticJunk {
def unapply(cd: ClassDef): Boolean = cd match {
- case ClassDef(_, _, _, _) if (cd.symbol.isSynthetic) => true
+ case ClassDef(_, _, _, _) if cd.symbol.isSynthetic => true
case _ => false
}
}
object ExConstructorDef {
def unapply(dd: DefDef): Boolean = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name == nme.CONSTRUCTOR && tparams.isEmpty) => true
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if name == nme.CONSTRUCTOR && tparams.isEmpty => true
case _ => false
}
}
object ExMainFunctionDef {
def unapply(dd: DefDef): Boolean = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 1) => {
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 1 => {
true
}
case _ => false
@@ -707,7 +707,7 @@ trait ASTExtractors {
object ExSomeConstruction {
def unapply(tree: Apply) : Option[(Type,Tree)] = tree match {
- case Apply(s @ Select(New(tpt), n), arg) if (arg.size == 1 && n == nme.CONSTRUCTOR && tpt.symbol.name.toString == "Some") => tpt.tpe match {
+ case Apply(s @ Select(New(tpt), n), arg) if arg.size == 1 && n == nme.CONSTRUCTOR && tpt.symbol.name.toString == "Some" => tpt.tpe match {
case TypeRef(_, sym, tpe :: Nil) => Some((tpe, arg(0)))
case _ => None
}
@@ -717,7 +717,7 @@ trait ASTExtractors {
object ExCaseClassConstruction {
def unapply(tree: Apply): Option[(Tree,Seq[Tree])] = tree match {
- case Apply(s @ Select(New(tpt), n), args) if (n == nme.CONSTRUCTOR) => {
+ case Apply(s @ Select(New(tpt), n), args) if n == nme.CONSTRUCTOR => {
Some((tpt, args))
}
case _ => None
@@ -747,7 +747,7 @@ trait ASTExtractors {
object ExAnd {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(s @ Select(lhs, _), List(rhs)) if (s.symbol == Boolean_and) =>
+ case Apply(s @ Select(lhs, _), List(rhs)) if s.symbol == Boolean_and =>
Some((lhs,rhs))
case _ => None
}
@@ -755,7 +755,7 @@ trait ASTExtractors {
object ExOr {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(s @ Select(lhs, _), List(rhs)) if (s.symbol == Boolean_or) =>
+ case Apply(s @ Select(lhs, _), List(rhs)) if s.symbol == Boolean_or =>
Some((lhs,rhs))
case _ => None
}
@@ -763,42 +763,42 @@ trait ASTExtractors {
object ExNot {
def unapply(tree: Select): Option[Tree] = tree match {
- case Select(t, n) if (n == nme.UNARY_!) => Some(t)
+ case Select(t, n) if n == nme.UNARY_! => Some(t)
case _ => None
}
}
object ExEquals {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(Select(lhs, n), List(rhs)) if (n == nme.EQ) => Some((lhs,rhs))
+ case Apply(Select(lhs, n), List(rhs)) if n == nme.EQ => Some((lhs,rhs))
case _ => None
}
}
object ExNotEquals {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
- case Apply(Select(lhs, n), List(rhs)) if (n == nme.NE) => Some((lhs,rhs))
+ case Apply(Select(lhs, n), List(rhs)) if n == nme.NE => Some((lhs,rhs))
case _ => None
}
}
object ExUMinus {
def unapply(tree: Select): Option[Tree] = tree match {
- case Select(t, n) if (n == nme.UNARY_- && hasBigIntType(t)) => Some(t)
+ case Select(t, n) if n == nme.UNARY_- && hasBigIntType(t) => Some(t)
case _ => None
}
}
object ExBVUMinus {
def unapply(tree: Select): Option[Tree] = tree match {
- case Select(t, n) if (n == nme.UNARY_- && hasIntType(t)) => Some(t)
+ case Select(t, n) if n == nme.UNARY_- && hasIntType(t) => Some(t)
case _ => None
}
}
object ExBVNot {
def unapply(tree: Select): Option[Tree] = tree match {
- case Select(t, n) if (n == nme.UNARY_~ && hasIntType(t)) => Some(t)
+ case Select(t, n) if n == nme.UNARY_~ && hasIntType(t) => Some(t)
case _ => None
}
}
@@ -938,7 +938,7 @@ trait ASTExtractors {
def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
case Apply(
s @ Select(lhs, update),
- index :: newValue :: Nil) if(s.symbol.fullName.endsWith("Array.update")) =>
+ index :: newValue :: Nil) if s.symbol.fullName.endsWith("Array.update") =>
Some((lhs, index, newValue))
case _ => None
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 630f688a52ea01ecd3e370d375157228451f3a1b..bfbcd41afe0a1b94165c3a3d9d0826d783172da5 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -213,41 +213,41 @@ trait CodeExtraction extends ASTExtractors {
var standaloneDefs = List[Tree]()
- val modules = lst.flatMap { _ match {
-
+ val modules = lst.flatMap {
+
case t if isIgnored(t.symbol) =>
None
-
- case po@ExObjectDef(n, templ) if n == "package" =>
+
+ case po@ExObjectDef(n, templ) if n == "package" =>
outOfSubsetError(po, "No other definitions are allowed in a file with a package object.")
-
+
case ExObjectDef(n, templ) if n != "package" =>
Some(TempModule(FreshIdentifier(n), templ.body, false))
/*
- case d @ ExCompanionObjectSynthetic(_, sym, templ) =>
+ case d @ ExCompanionObjectSynthetic(_, sym, templ) =>
// Find default param. implementations
- templ.body foreach {
+ templ.body foreach {
case ExDefaultValueFunction(sym, _, _, _, owner, index, _) =>
val namePieces = sym.toString.reverse.split("\\$", 3).reverse map { _.reverse }
assert(namePieces.length == 3 && namePieces(0)== "$lessinit$greater" && namePieces(1) == "default") // FIXME : maybe $lessinit$greater?
val index = namePieces(2).toInt
val theParam = sym.companionClass.paramss.head(index - 1)
paramsToDefaultValues += theParam -> body
- case _ =>
- }
- None
+ case _ =>
+ }
+ None
*/
- case d @ ExAbstractClass(_, _, _) =>
+ case d@ExAbstractClass(_, _, _) =>
standaloneDefs ::= d
None
- case d @ ExCaseClass(_, _, _, _) =>
+ case d@ExCaseClass(_, _, _, _) =>
standaloneDefs ::= d
None
-
- case d @ ExCaseClassSyntheticJunk() =>
+
+ case d@ExCaseClassSyntheticJunk() =>
None
case cd: ClassDef =>
@@ -257,7 +257,7 @@ trait CodeExtraction extends ASTExtractors {
case other =>
outOfSubsetError(other, "Expected: top-level object/class.")
None
- }}
+ }
// File name without extension
val unitName = u.source.file.name.replaceFirst("[.][^.]+$", "")
@@ -359,7 +359,7 @@ trait CodeExtraction extends ASTExtractors {
val allSels = sels map { prefix :+ _.name.toString }
// Make a different import for each selector at the end of the chain
allSels flatMap { selectors =>
- assert(!selectors.isEmpty)
+ assert(selectors.nonEmpty)
val (thePath, isWild) = selectors.last match {
case "_" => (selectors.dropRight(1), true)
case _ => (selectors, false)
@@ -1015,7 +1015,7 @@ trait CodeExtraction extends ASTExtractors {
val nil = CaseClassPattern(None, CaseClassType(nilClass, Seq(CharType)), Seq())
val consType = CaseClassType(consClass, Seq(CharType))
def mkCons(hd: Pattern, tl: Pattern) = CaseClassPattern(None, consType, Seq(hd,tl))
- val chars = s.toCharArray()//.asInstanceOf[Seq[Char]]
+ val chars = s.toCharArray//.asInstanceOf[Seq[Char]]
def charPat(ch : Char) = LiteralPattern(None, CharLiteral(ch))
(chars.foldRight(nil)( (ch: Char, p : Pattern) => mkCons( charPat(ch), p)), dctx)
@@ -1105,7 +1105,7 @@ trait CodeExtraction extends ASTExtractors {
case ExPasses(in, out, cases) =>
val ine = extractTree(in)
val oute = extractTree(out)
- val rc = cases.map(extractMatchCase(_))
+ val rc = cases.map(extractMatchCase)
// @mk: FIXME: this whole sanity checking is very dodgy at best.
val ines = unwrapTuple(ine, ine.isInstanceOf[Tuple]) // @mk We untuple all tuples
@@ -1122,7 +1122,7 @@ trait CodeExtraction extends ASTExtractors {
case ExGives(sel, cses) =>
val rs = extractTree(sel)
- val rc = cses.map(extractMatchCase(_))
+ val rc = cses.map(extractMatchCase)
gives(rs, rc)
case ExArrayLiteral(tpe, args) =>
@@ -1404,7 +1404,7 @@ trait CodeExtraction extends ASTExtractors {
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt) match {
case cct: CaseClassType =>
- val nargs = args.map(extractTree(_))
+ val nargs = args.map(extractTree)
CaseClass(cct, nargs)
case _ =>
@@ -1456,14 +1456,14 @@ trait CodeExtraction extends ASTExtractors {
case ExFiniteSet(tt, args) =>
val underlying = extractType(tt)
- finiteSet(args.map(extractTree(_)).toSet, underlying)
+ finiteSet(args.map(extractTree).toSet, underlying)
case ExEmptySet(tt) =>
val underlying = extractType(tt)
EmptySet(underlying)
case ExFiniteMultiset(tt, args) =>
val underlying = extractType(tt)
- finiteMultiset(args.map(extractTree(_)),underlying)
+ finiteMultiset(args.map(extractTree),underlying)
case ExEmptyMultiset(tt) =>
val underlying = extractType(tt)
@@ -1538,7 +1538,7 @@ trait CodeExtraction extends ASTExtractors {
case pm @ ExPatternMatching(sel, cses) =>
val rs = extractTree(sel)
- val rc = cses.map(extractMatchCase(_))
+ val rc = cses.map(extractMatchCase)
matchExpr(rs, rc)
case t: This =>
@@ -1558,8 +1558,8 @@ trait CodeExtraction extends ASTExtractors {
case l @ ExListLiteral(tpe, elems) =>
val rtpe = extractType(tpe)
- val cons = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Cons"), Seq(rtpe));
- val nil = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Nil"), Seq(rtpe));
+ val cons = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Cons"), Seq(rtpe))
+ val nil = CaseClassType(libraryCaseClass(l.pos, "leon.collection.Nil"), Seq(rtpe))
elems.foldRight(CaseClass(nil, Seq())) {
case (e, ls) => CaseClass(cons, Seq(extractTree(e), ls))
@@ -1569,10 +1569,10 @@ trait CodeExtraction extends ASTExtractors {
CharLiteral(c)
case str @ ExStringLiteral(s) =>
- val chars = s.toList.map(CharLiteral(_))
+ val chars = s.toList.map(CharLiteral)
- val consChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Cons"), Seq(CharType));
- val nilChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Nil"), Seq(CharType));
+ val consChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Cons"), Seq(CharType))
+ val nilChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Nil"), Seq(CharType))
val charList = chars.foldRight(CaseClass(nilChar, Seq())) {
case (c, s) => CaseClass(consChar, Seq(c, s))
@@ -1933,9 +1933,9 @@ trait CodeExtraction extends ASTExtractors {
}
def containsLetDef(expr: LeonExpr): Boolean = {
- exists { _ match {
+ exists {
case (l: LetDef) => true
case _ => false
- }}(expr)
+ }(expr)
}
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 7e1f75dfd59ee391481019b654af3c8569b89334..d7d9e53bcc08a0c7818cc4f8167352c767033d9b 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -23,7 +23,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val settings = new NSCSettings
- val scalaLib = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource()).map{
+ val scalaLib = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource).map{
_.getLocation.getPath
}.orElse( for {
// We are in Eclipse. Look in Eclipse plugins to find scala lib
diff --git a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
index e3f6817b5f75892b9f8953ed95107a4bd439d1e4..121e84f791d74494d77e458ab58b7ac3f1431efe 100644
--- a/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
+++ b/src/main/scala/leon/frontends/scalac/SimpleReporter.scala
@@ -26,7 +26,7 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
}
private def getCountString(severity: Severity): String =
- StringOps.countElementsAsString((severity).count, label(severity))
+ StringOps.countElementsAsString(severity.count, label(severity))
/** Prints the message. */
def printMessage(msg: String, pos: LeonPosition, severity: Severity) {
@@ -81,5 +81,5 @@ class SimpleReporter(val settings: Settings, reporter: leon.Reporter) extends Ab
print(pos, msg, severity)
}
- def displayPrompt: Unit = {}
+ def displayPrompt(): Unit = {}
}
diff --git a/src/main/scala/leon/purescala/CallGraph.scala b/src/main/scala/leon/purescala/CallGraph.scala
index a6ffa8980fa8833de57440f3ec2f7801e7caab8b..77fa4cfa87f53f9c3493fcde2c11c8772f609736 100644
--- a/src/main/scala/leon/purescala/CallGraph.scala
+++ b/src/main/scala/leon/purescala/CallGraph.scala
@@ -68,7 +68,7 @@ class CallGraph(p: Program) {
}
private def transitiveClosure() {
- var changed = true;
+ var changed = true
while(changed) {
val newCalls = _transitiveCalls.flatMap {
case (from, to) => _transitiveCallees.getOrElse(to, Set()).map((from, _))
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 2112689c675b74c337a1e1b0af21b7cf1b40cca7..7c6d32e04705dae3eaf2acd0be89e2b8517d6e49 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -96,7 +96,7 @@ object Common {
def aliased(ids1 : Set[Identifier], ids2 : Set[Identifier]) = {
val s1 = ids1.groupBy{ _.toString }.keySet
val s2 = ids2.groupBy{ _.toString }.keySet
- !(s1 & s2).isEmpty
+ (s1 & s2).nonEmpty
}
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 8f1b5f57ff5aa810def235999063225ec3146b58..3d316f8d8088b433239dfcd6e1f67b59e641970c 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -132,10 +132,10 @@ object Constructors {
def and(exprs: Expr*): Expr = {
- val flat = exprs.flatMap(_ match {
+ val flat = exprs.flatMap {
case And(es) => es
case o => Seq(o)
- })
+ }
var stop = false
val simpler = for(e <- flat if !stop && e != BooleanLiteral(true)) yield {
@@ -153,10 +153,10 @@ object Constructors {
def andJoin(es: Seq[Expr]) = and(es :_*)
def or(exprs: Expr*): Expr = {
- val flat = exprs.flatMap(_ match {
+ val flat = exprs.flatMap {
case Or(es) => es
case o => Seq(o)
- })
+ }
var stop = false
val simpler = for(e <- flat if !stop && e != BooleanLiteral(false)) yield {
@@ -204,7 +204,7 @@ object Constructors {
}
def finiteArray(els: Seq[Expr]): Expr = {
- require(!els.isEmpty)
+ require(els.nonEmpty)
finiteArray(els, None, Untyped) // Untyped is not correct, but will not be used anyway
}
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index ce8785768bdf889dbd23ffa2199b93fc0029767d..96acd8f225ffa827f7eaeecc992f58f46b75514c 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -125,7 +125,7 @@ object DefOps {
val index = rootPath lastIndexWhere { isImportedBy(_, unitOf(base).toSeq.flatMap { _.imports }) }
val pathFromImport = rootPath drop scala.math.max(index, 0)
val finalPath = if (pathFromAncestor.length <= pathFromImport.length) pathFromAncestor else pathFromImport
- assert(!finalPath.isEmpty)
+ assert(finalPath.nonEmpty)
// Package
val pack = if (finalPath.head.isInstanceOf[UnitDef]) {
@@ -167,7 +167,7 @@ object DefOps {
require(programOf(base).isDefined)
val fullNameList = fullName.split("\\.").toList map scala.reflect.NameTransformer.encode
- require(!fullNameList.isEmpty)
+ require(fullNameList.nonEmpty)
def onCondition[A](cond:Boolean)(body : => Option[A]) : Option[A] = {
if (cond) body else None
@@ -199,7 +199,7 @@ object DefOps {
val visible = visibleDefsFrom(base).toList
val defs : List[Definition] =
if(exploreStandalones)
- visible ++ (visible.collect{ case ModuleDef(_,subs,true) => subs }.flatten)
+ visible ++ visible.collect { case ModuleDef(_, subs, true) => subs}.flatten
else visible
defs find { _.id.toString == fullNameList.head }
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 95942afe54d2468aa958afcbde291bcf68d15880..2dbeb4f436b1f84737568e8235bbddad63351c42 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -184,7 +184,7 @@ object Definitions {
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
- case class ModuleDef(id: Identifier, defs : Seq[Definition], val isStandalone : Boolean) extends Definition {
+ case class ModuleDef(id: Identifier, defs : Seq[Definition], isStandalone : Boolean) extends Definition {
def subDefinitions = defs
@@ -288,9 +288,9 @@ object Definitions {
}
/** Abstract classes. */
- case class AbstractClassDef(val id: Identifier,
- val tparams: Seq[TypeParameterDef],
- val parent: Option[AbstractClassType]) extends ClassDef {
+ case class AbstractClassDef(id: Identifier,
+ tparams: Seq[TypeParameterDef],
+ parent: Option[AbstractClassType]) extends ClassDef {
val fields = Nil
val isAbstract = true
@@ -301,10 +301,10 @@ object Definitions {
}
/** Case classes/objects. */
- case class CaseClassDef(val id: Identifier,
- val tparams: Seq[TypeParameterDef],
- val parent: Option[AbstractClassType],
- val isCaseObject: Boolean) extends ClassDef {
+ case class CaseClassDef(id: Identifier,
+ tparams: Seq[TypeParameterDef],
+ parent: Option[AbstractClassType],
+ isCaseObject: Boolean) extends ClassDef {
private var _fields = Seq[ValDef]()
@@ -461,8 +461,8 @@ object Definitions {
}
}
- private lazy val typesMap = {
- (fd.tparams zip tps).toMap.filter(tt => tt._1 != tt._2)
+ private lazy val typesMap: Map[TypeParameterDef, TypeTree] = {
+ (fd.tparams zip tps).toMap.filter(tt => tt._1.tp != tt._2)
}
def translated(t: TypeTree): TypeTree = instantiateType(t, typesMap)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 3ec5fcf2a79758e74d46047ab081f53e94dd773d..7077cf9f83227d0b3871f971efa86b31005d854c 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -37,7 +37,7 @@ object Extractors {
}
trait UnaryExtractable {
- def extract: Option[(Expr, (Expr)=>Expr)];
+ def extract: Option[(Expr, (Expr)=>Expr)]
}
object BinaryOperator {
@@ -95,7 +95,7 @@ object Extractors {
}
trait BinaryExtractable {
- def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)];
+ def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)]
}
object NAryOperator {
@@ -104,9 +104,9 @@ object Extractors {
case Seq(pred) => Choose(pred, None)
case Seq(pred, impl) => Choose(pred, Some(impl))
}))
- case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPos(fi))))
- case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, (as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi))))
- case fa @ Application(caller, args) => Some((caller +: args), (as => application(as.head, as.tail).setPos(fa)))
+ case fi @ FunctionInvocation(fd, args) => Some((args, as => FunctionInvocation(fd, as).setPos(fi)))
+ case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi)))
+ case fa @ Application(caller, args) => Some(caller +: args, as => application(as.head, as.tail).setPos(fa))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
@@ -177,7 +177,7 @@ object Extractors {
}
trait NAryExtractable {
- def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)];
+ def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)]
}
object StringLiteral {
@@ -217,7 +217,7 @@ object Extractors {
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Let(i, e, TopLevelOrs(bs)) => Some(bs map (let(i,e,_)))
case Or(exprs) =>
- Some(exprs.flatMap(unapply(_)).flatten)
+ Some(exprs.flatMap(unapply).flatten)
case e =>
Some(Seq(e))
}
@@ -226,7 +226,7 @@ object Extractors {
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Let(i, e, TopLevelAnds(bs)) => Some(bs map (let(i,e,_)))
case And(exprs) =>
- Some(exprs.flatMap(unapply(_)).flatten)
+ Some(exprs.flatMap(unapply).flatten)
case e =>
Some(Seq(e))
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 10ee5d41eba9ce2624d509e2daf5013d5ce3d6d1..7fcfb683e9ceb5a8ae3da4ba3038b31f0ffb272d 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -180,7 +180,7 @@ object FunctionClosure extends TransformationPhase {
constraints = pathConstraints.filterNot(filteredConstraints.contains(_))
constraints.foreach(expr => {
val vs = variablesOf(expr)
- if(!vs.intersect(allVars).isEmpty) {
+ if(vs.intersect(allVars).nonEmpty) {
filteredConstraints ::= expr
newVars ++= vs.diff(allVars)
}
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index d8a9096f3cb88fe6e600a065703d5f71e70add0f..dc6ce8aea94635b7d68ce7c4eeee8b6086279789 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -85,10 +85,10 @@ object MethodLifting extends TransformationPhase {
// We remove methods from class definitions and add corresponding functions
val newDefs = m.defs.flatMap {
case acd: AbstractClassDef if acd.methods.nonEmpty =>
- acd +: acd.methods.map(translateMethod(_))
+ acd +: acd.methods.map(translateMethod)
case ccd: CaseClassDef if ccd.methods.nonEmpty =>
- ccd +: ccd.methods.map(translateMethod(_))
+ ccd +: ccd.methods.map(translateMethod)
case fd: FunDef =>
List(translateMethod(fd))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b82f1e71ed5115d5ca6f86fe49eeb73b6323dc49..fd881faa5c86ba1ca1b18e2dd02b3e6b7f8d54fc 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -36,8 +36,8 @@ object PrinterHelpers {
var strings = sc.parts.iterator
var expressions = args.iterator
- var extraInd = 0;
- var firstElem = true;
+ var extraInd = 0
+ var firstElem = true
while(strings.hasNext) {
val s = strings.next.stripMargin
@@ -45,7 +45,7 @@ object PrinterHelpers {
// Compute indentation
var start = s.lastIndexOf('\n')
if(start >= 0 || firstElem) {
- var i = start+1;
+ var i = start+1
while(i < s.length && s(i) == ' ') {
i += 1
}
@@ -160,7 +160,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
val alphaNumDollar = "[\\w\\$]"
// FIXME this does not account for class names with operator symbols
def isLegalScalaId(id : String) = id.matches(
- s"${alphaNumDollar}+|[${alphaNumDollar}+_]?[!@#%^&*+-\\|~/?><:]+"
+ s"$alphaNumDollar+|[$alphaNumDollar+_]?[!@#%^&*+-\\|~/?><:]+"
)
// Replace $opname with operator symbols
val candidate = scala.reflect.NameTransformer.decode(name)
@@ -238,7 +238,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
if (chars.length == elems.length) {
// String literal
val str = chars mkString ""
- val q = '"';
+ val q = '"'
p"$q$str$q"
}
@@ -274,7 +274,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case UnitLiteral() => p"()"
case GenericValue(tp, id) => p"$tp#$id"
case Tuple(exprs) => p"($exprs)"
- case TupleSelect(t, i) => p"${t}._$i"
+ case TupleSelect(t, i) => p"$t._$i"
case NoTree(tpe) => p"???($tpe)"
case Choose(pred, oimpl) =>
oimpl match {
@@ -310,11 +310,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
case BinaryMethodCall(a, op, b) =>
- optP { p"${a} $op ${b}" }
+ optP { p"$a $op $b" }
case FcallMethodInvocation(rec, fd, id, tps, args) =>
- p"${rec}.${id}"
+ p"$rec.$id"
if (tps.nonEmpty) {
p"[$tps]"
}
@@ -542,7 +542,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"""${nary(units filter {_.isMainUnit}, "\n\n")}"""
case UnitDef(id,modules,pack,imports,_) =>
- if (!pack.isEmpty){
+ if (pack.nonEmpty){
p"""|package ${pack mkString "."}
|"""
}
@@ -631,7 +631,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
if (fd.canBeField) {
p"""|${fd.defType} ${fd.id} : ${fd.returnType} = {
|"""
- } else if (!fd.tparams.isEmpty) {
+ } else if (fd.tparams.nonEmpty) {
p"""|def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): ${fd.returnType} = {
|"""
} else {
@@ -697,7 +697,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
object BinaryMethodCall {
- val makeBinary = Set("+", "-", "*", "::", "++", "--", "&&", "||", "/");
+ val makeBinary = Set("+", "-", "*", "::", "++", "--", "&&", "||", "/")
def unapply(fi: FunctionInvocation): Option[(Expr, String, Expr)] = fi match {
case FcallMethodInvocation(rec, _, name, Nil, List(a)) =>
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 73bc15aef2a6a47b5d31dda4365e5a84e1ec5ca8..554d3268e2c7c771536f3d55a6a5bbdd26be6091 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -31,7 +31,7 @@ object TreeNormalizations {
}
rec(e)
- assert(!id.isEmpty)
+ assert(id.isDefined)
(InfiniteIntegerLiteral(coef), id.get)
}
@@ -62,7 +62,7 @@ object TreeNormalizations {
res(index+1) = coef
}}
- res(0) = simplifyArithmetic(exprs.foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus(_, _)))
+ res(0) = simplifyArithmetic(exprs.foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus))
res
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 5cc4796c211311803f83ecd966a6dad9d0bde70e..0003474dba82edeb9821cf7d7c19a4bfee74d1c4 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -329,7 +329,7 @@ object TreeOps {
}
def count(matcher: Expr => Int)(e: Expr): Int = {
- foldRight[Int]({ (e, subs) => matcher(e) + subs.foldLeft(0)(_ + _) } )(e)
+ foldRight[Int]({ (e, subs) => matcher(e) + subs.sum } )(e)
}
def replace(substs: Map[Expr,Expr], expr: Expr) : Expr = {
@@ -439,10 +439,10 @@ object TreeOps {
postMap({
case m @ MatchLike(s, cses, builder) =>
- Some(builder(s, cses.map(freshenCase(_))).copiedFrom(m))
+ Some(builder(s, cses.map(freshenCase)).copiedFrom(m))
case p @ Passes(in, out, cses) =>
- Some(Passes(in, out, cses.map(freshenCase(_))).copiedFrom(p))
+ Some(Passes(in, out, cses.map(freshenCase)).copiedFrom(p))
case l @ Let(i,e,b) =>
val newID = FreshIdentifier(i.name, i.getType, alwaysShowUniqueID = true).copiedFrom(i)
@@ -560,10 +560,10 @@ object TreeOps {
//we replace, so we drop old
false
case (id, value) =>
- val occurences = count{ (e: Expr) => e match {
+ val occurences = count {
case Variable(x) if x == id => 1
case _ => 0
- }}(body)
+ }(body)
if(occurences == 0) {
false
@@ -1186,7 +1186,7 @@ object TreeOps {
}
def simplifyPaths(sf: SolverFactory[Solver]): Expr => Expr = {
- new SimplifierWithPaths(sf).transform _
+ new SimplifierWithPaths(sf).transform
}
trait Traverser[T] {
@@ -1281,7 +1281,7 @@ object TreeOps {
formulaSize(e1)+formulaSize(e2)+1
case NAryOperator(es, _) =>
- es.map(formulaSize).foldRight(0)(_ + _)+1
+ es.map(formulaSize).sum+1
}
def collectChooses(e: Expr): List[Choose] = {
@@ -1443,7 +1443,7 @@ object TreeOps {
}
def idHomo(i1: Identifier, i2: Identifier)(implicit map: Map[Identifier, Identifier]) = {
- i1 == i2 || map.get(i1).map(_ == i2).getOrElse(false)
+ i1 == i2 || map.get(i1).exists(_ == i2)
}
def fdHomo(fd1: FunDef, fd2: FunDef)(implicit map: Map[Identifier, Identifier]) = {
@@ -1671,7 +1671,7 @@ object TreeOps {
case UnitType =>
// Anything matches ()
- !ps.isEmpty
+ ps.nonEmpty
case Int32Type =>
// Can't possibly pattern match against all Ints one by one
@@ -1778,7 +1778,7 @@ object TreeOps {
val expr0 = try {
val freeVars: Array[Identifier] = variablesOf(expr).toArray
val coefs: Array[Expr] = TreeNormalizations.linearArithmeticForm(expr, freeVars)
- coefs.toList.zip(InfiniteIntegerLiteral(1) :: freeVars.toList.map(Variable(_))).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, t) => {
+ coefs.toList.zip(InfiniteIntegerLiteral(1) :: freeVars.toList.map(Variable)).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, t) => {
if(t._1 == InfiniteIntegerLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
})
} catch {
@@ -2038,7 +2038,7 @@ object TreeOps {
val TopLevelOrs(orcases) = cond
if (orcases.exists{ case TopLevelAnds(ands) => ands.exists(_.isInstanceOf[CaseClassInstanceOf]) } ) {
- if (!orcases.tail.isEmpty) {
+ if (orcases.tail.nonEmpty) {
pre(IfExpr(orcases.head, thenn, IfExpr(orJoin(orcases.tail), thenn, elze)))
} else {
val TopLevelAnds(andcases) = orcases.head
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 57e85d91ff30735202eb1b3059af9542b7d6d5cd..197fc891f882dd0e7d312642665557db9aee1946 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -258,7 +258,7 @@ object Trees {
val getType = BooleanType
}
- case class Variable(val id: Identifier) extends Expr with Terminal {
+ case class Variable(id: Identifier) extends Expr with Terminal {
val getType = id.getType
}
@@ -491,7 +491,7 @@ object Trees {
case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr {
val getType = array.getType match {
case ArrayType(base) =>
- leastUpperBound(base, newValue.getType).map(ArrayType(_)).getOrElse(Untyped).unveilUntyped
+ leastUpperBound(base, newValue.getType).map(ArrayType).getOrElse(Untyped).unveilUntyped
case _ =>
Untyped
}
@@ -514,7 +514,7 @@ object Trees {
// Provide an oracle (synthesizable, all-seeing choose)
case class WithOracle(oracles: List[Identifier], body: Expr) extends Expr with UnaryExtractable {
- require(!oracles.isEmpty)
+ require(oracles.nonEmpty)
val getType = body.getType
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 451291d7d970f6202e9a90cc4a2b0ad35f3bc0c8..dd6597e8fc5c26d4e82c691f93b60c9c854ef3e4 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -140,7 +140,7 @@ object TypeTreeOps {
case (TupleType(args1), TupleType(args2)) =>
val args = (args1 zip args2).map(p => leastUpperBound(p._1, p._2))
if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
- case (o1, o2) if (o1 == o2) => Some(o1)
+ case (o1, o2) if o1 == o2 => Some(o1)
case _ => None
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 4ca362592b7aab3478c4c9014a72843340cd1c8c..5119582455ba3ee6e91df4e7440099364366a286 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -13,7 +13,7 @@ object TypeTrees {
trait Typed {
def getType: TypeTree
- def isTyped : Boolean = (getType != Untyped)
+ def isTyped : Boolean = getType != Untyped
}
class TypeErrorException(msg: String) extends Exception(msg)
@@ -58,7 +58,7 @@ object TypeTrees {
* If you are not sure about the requirement,
* you should use tupleTypeWrap in purescala.Constructors
*/
- case class TupleType (val bases: Seq[TypeTree]) extends TypeTree {
+ case class TupleType (bases: Seq[TypeTree]) extends TypeTree {
lazy val dimension: Int = bases.length
require(dimension >= 2)
}
@@ -129,7 +129,7 @@ object TypeTrees {
def unapply(t: TypeTree): Option[(Seq[TypeTree], Seq[TypeTree] => TypeTree)] = t match {
case CaseClassType(ccd, ts) => Some((ts, ts => CaseClassType(ccd, ts)))
case AbstractClassType(acd, ts) => Some((ts, ts => AbstractClassType(acd, ts)))
- case TupleType(ts) => Some((ts, Constructors.tupleTypeWrap(_)))
+ case TupleType(ts) => Some((ts, Constructors.tupleTypeWrap _))
case ArrayType(t) => Some((Seq(t), ts => ArrayType(ts.head)))
case SetType(t) => Some((Seq(t), ts => SetType(ts.head)))
case MultisetType(t) => Some((Seq(t), ts => MultisetType(ts.head)))
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index a2ed84fd7b6d46d09ad6a948fbcf7876a01e3ab9..da65e5c1fa2c27400812149a1ca4274d20174d40 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -63,11 +63,11 @@ class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr
Try {
treat(e => e)
}.getOrElse {
- treat( postMap{
+ treat( postMap {
// Use reference equality, just in case cond appears again in the program
case c if c eq cond => Some(not(cond))
case _ => None
- } _)
+ })
}
case _ => super.e(expr)
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index d030327b5e52f7a0835bf6fc95ef6a397ce66c66..3d4ca1c15cc0dd39857978b1155bda9ae4605c1a 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -37,7 +37,7 @@ object RepairPhase extends LeonPhase[Program, Program] {
filterInclusive(repairFuns.map(fdMatcher), None)
}
- val toRepair = funDefsFromMain(program).toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter).filter{ _.hasPostcondition }
+ val toRepair = funDefsFromMain(program).toList.filter(fdFilter).filter{ _.hasPostcondition }.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
if (toRepair.isEmpty) reporter.warning("No functions found with the given names")
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 76656acdf44a819b97be4d9be71089fe62bd1f79..9e234643c7966db1923411b653113e92d12db199 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -126,7 +126,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
ci.ch.impl = Some(expr)
getVerificationCounterExamples(ci.fd, program) match {
- case NotValid(_, ces) if !ces.isEmpty =>
+ case NotValid(_, ces) if ces.nonEmpty =>
reporter.error("I ended up finding this counter example:\n"+ces.mkString(" | "))
case NotValid(_, _) =>
@@ -156,7 +156,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
for ((sol, i) <- solutions.reverse.zipWithIndex) {
reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
val expr = sol.toSimplifiedExpr(ctx, program)
- reporter.info(ScalaPrinter(expr));
+ reporter.info(ScalaPrinter(expr))
}
reporter.info(ASCIIHelpers.title("In context:"))
@@ -164,13 +164,13 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
for ((sol, i) <- solutions.reverse.zipWithIndex) {
reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
val expr = sol.toSimplifiedExpr(ctx, program)
- val nfd = fd.duplicate;
-
+ val nfd = fd.duplicate
+
nfd.body = fd.body.map { b =>
replace(Map(ci.source -> expr), b)
}
- reporter.info(ScalaPrinter(nfd));
+ reporter.info(ScalaPrinter(nfd))
}
}
@@ -197,7 +197,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val guide = Guide(replacedExpr)
// Return synthesizer for this choose
- val soptions0 = SynthesisPhase.processOptions(ctx);
+ val soptions0 = SynthesisPhase.processOptions(ctx)
val soptions = soptions0.copy(
functionsToIgnore = soptions0.functionsToIgnore + fd,
@@ -208,7 +208,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
CEGLESS
//TEGLESS
)) diff Seq(ADTInduction, TEGIS, IntegerInequalities, IntegerEquation)
- );
+ )
// extract chooses from fd
val Seq(ci) = ChooseInfo.extractFromFunction(program, fd)
@@ -411,7 +411,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val maxValid = 400
val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams(checkContracts = true))
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions _)
+ val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
val inputs = enum.iterator(tupleTypeWrap(fd.params map { _.getType})).map(unwrapTuple(_, fd.params.size))
diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index 7948360d3919ae272e22d584684a47b277b6303f..2546dd4e5a595bbffb72c2d45f526b66ecf1fa51 100644
--- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -23,7 +23,7 @@ import solvers._
case object GuidedDecomp extends Rule("Guided Decomp") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
if (hctx.searchDepth > 0) {
- return Nil;
+ return Nil
}
val TopLevelAnds(clauses) = p.ws
@@ -66,7 +66,7 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val subs = for ((c, cond) <- cs zip matchCasePathConditions(fullMatch, List(p.pc))) yield {
- val localScrut = c.pattern.binder.map( Variable(_) ) getOrElse scrut
+ val localScrut = c.pattern.binder.map( Variable ) getOrElse scrut
val scrutConstraint = if (localScrut == scrut) BooleanLiteral(true) else Equals(localScrut, scrut)
val substs = patternSubstitutions(localScrut, c.pattern)
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 6f87389c4c79c21b830f01c427bff8c01b9dbc45..9ec495e88ef2b6dfcfd3764d79cedb271ba8fa12 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -18,11 +18,11 @@ import datagen._
class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible with IncrementalSolver with NaiveAssumptionSolver {
def name = "Enum"
- val maxTried = 10000;
+ val maxTried = 10000
var datagen: Option[DataGenerator] = None
- private var interrupted = false;
+ private var interrupted = false
var freeVars = List[List[Identifier]](Nil)
var constraints = List[List[Expr]](Nil)
@@ -86,7 +86,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
}
def interrupt(): Unit = {
- interrupted = true;
+ interrupted = true
datagen.foreach{ s =>
s.interrupt
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
index f7344aa9b225da325ce92756a55460c716b1661f..c888f38df1a447031059f11a7697773213125196 100644
--- a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -18,7 +18,7 @@ trait NaiveAssumptionSolver extends AssumptionSolver {
var lastBs = Set[Expr]()
def checkAssumptions(bs: Set[Expr]): Option[Boolean] = {
push()
- lastBs = bs;
+ lastBs = bs
assertCnstr(andJoin(bs.toSeq))
val res = check
pop()
@@ -26,7 +26,7 @@ trait NaiveAssumptionSolver extends AssumptionSolver {
res
}
- def getUnsatCore(): Set[Expr] = {
+ def getUnsatCore: Set[Expr] = {
lastBs
}
}
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
index 5d7b8982a5902ee2b5ed2bd009b230cd3e3776ab..b8053b7658b26dc3dd37289c6c392dd4edcde623 100644
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
@@ -9,7 +9,7 @@ import purescala.Trees._
class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {
def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
- val s = sf.getNewSolver
+ val s = sf.getNewSolver()
try {
s.assertCnstr(expression)
s.checkAssumptions(assumptions) match {
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index 097ba58d6e225ab4ec5af6ef489d9667b70740c6..eafd3fbd32cb2e9898266d7b807f6e0534ce766e 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -8,7 +8,7 @@ import purescala.Trees._
class SimpleSolverAPI(sf: SolverFactory[Solver]) {
def solveVALID(expression: Expr): Option[Boolean] = {
- val s = sf.getNewSolver
+ val s = sf.getNewSolver()
try {
s.assertCnstr(Not(expression))
s.check.map(r => !r)
@@ -18,7 +18,7 @@ class SimpleSolverAPI(sf: SolverFactory[Solver]) {
}
def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
- val s = sf.getNewSolver
+ val s = sf.getNewSolver()
try {
s.assertCnstr(expression)
s.check match {
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index eacfbb77e2ce6c0e63ef11100dd4a16500ec7525..360c48d6ce4efb9b4eb8c30be93ff9a95c897967 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -19,7 +19,7 @@ object SolverFactory {
}
}
- val definedSolvers = Set("fairz3", "unrollz3", "enum", "smt", "smt-z3", "smt-cvc4");
+ val definedSolvers = Set("fairz3", "unrollz3", "enum", "smt", "smt-z3", "smt-cvc4")
def getFromSettings[S](ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
import combinators._
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 1198e0d728b460cf20757e27373b6da7a94933a7..d0c928af375ec07387c033f85b71d76f43189eaa 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -9,7 +9,7 @@ trait TimeoutSolver extends Solver with Interruptible {
val ti = new TimeoutFor(this)
- protected var optTimeout: Option[Long] = None;
+ protected var optTimeout: Option[Long] = None
def setTimeout(timeout: Long): this.type = {
optTimeout = Some(timeout)
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 1fc16886f2304c2b62e70c09fa34166c11037b15..0b06aeb966d1a0a030d03b78c0a8d5607ec499c0 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -14,7 +14,7 @@ class DNFSolver(val context: LeonContext,
def name = "DNF("+underlyings.name+")"
- def free {}
+ def free() {}
private var theConstraint : Option[Expr] = None
private var theModel : Option[Map[Identifier,Expr]] = None
@@ -22,7 +22,7 @@ class DNFSolver(val context: LeonContext,
import context.reporter._
def assertCnstr(expression : Expr) {
- if(!theConstraint.isEmpty) { fatalError("Multiple assertCnstr(...).") }
+ if(theConstraint.isDefined) { fatalError("Multiple assertCnstr(...).") }
theConstraint = Some(expression)
}
@@ -73,7 +73,7 @@ class DNFSolver(val context: LeonContext,
}
def getModel : Map[Identifier,Expr] = {
- val vs : Set[Identifier] = theConstraint.map(variablesOf(_)).getOrElse(Set.empty)
+ val vs : Set[Identifier] = theConstraint.map(variablesOf).getOrElse(Set.empty)
theModel.getOrElse(Map.empty).filter(p => vs(p._1))
}
@@ -100,7 +100,7 @@ class DNFSolver(val context: LeonContext,
private def dnf(expr : Expr) : Expr = expr match {
case And(es) =>
val (ors, lits) = es.partition(_.isInstanceOf[Or])
- if(!ors.isEmpty) {
+ if(ors.nonEmpty) {
val orHead = ors.head.asInstanceOf[Or]
val orTail = ors.tail
orJoin(orHead.exprs.map(oe => dnf(andJoin(filterObvious(lits ++ (oe +: orTail))))))
@@ -109,7 +109,7 @@ class DNFSolver(val context: LeonContext,
}
case Or(es) =>
- orJoin(es.map(dnf(_)))
+ orJoin(es.map(dnf))
case _ => expr
}
@@ -125,7 +125,7 @@ class DNFSolver(val context: LeonContext,
}
val both : Set[Identifier] = pos.toSet intersect neg.toSet
- if(!both.isEmpty) {
+ if(both.nonEmpty) {
Seq(BooleanLiteral(false))
} else {
exprs
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 942f7519169dbbfbf60dea3281628a84a0fd454d..4e9a28045aa84875087e65964050130831478ea5 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -21,7 +21,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
var constraints = List[Expr]()
protected var modelMap = Map[Identifier, Expr]()
- protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver)
+ protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver())
def assertCnstr(expression: Expr): Unit = {
solversInsts.foreach(_.assertCnstr(expression))
@@ -44,14 +44,14 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
case Some((s, r, m)) =>
modelMap = m
context.reporter.debug("Solved with "+s.name)
- solversInsts.foreach(_.interrupt)
+ solversInsts.foreach(_.interrupt())
r
case None =>
None
}
// Block until all solvers finished
- Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days);
+ Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days)
res
}
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 3239bdd9794875141f65cd941da85cc7ea5570ef..59ac92e7a11221bb02cacd51bfc75161311a5532 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -48,8 +48,8 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
def name = "U:"+underlying.name
- def free {
- underlying.free
+ def free() {
+ underlying.free()
}
val templateGenerator = new TemplateGenerator(new TemplateEncoder[Expr] {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index ed5559a4173c7e73fb66ea855b22a61a8c2886cd..2f9e4423395dd7479949c887a1253d7099864bf8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -120,7 +120,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
} else {
val selems = elems.toSeq.map(toSMT)
- val sgt = FunctionApplication(SSymbol("singleton"), Seq(selems.head));
+ val sgt = FunctionApplication(SSymbol("singleton"), Seq(selems.head))
if (selems.size > 1) {
FunctionApplication(SSymbol("insert"), selems.tail :+ sgt)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 96b8f34dd31a64f64af3c21ee469de82720e5382..4da09b251abfdda9f6855ff18fa0ac5a112308c5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -20,7 +20,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected var interrupted = false
- override def interrupt: Unit = {
+ override def interrupt(): Unit = {
interrupted = true
interpreter.interrupt()
}
@@ -38,7 +38,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
override def free() = {
interpreter.free()
- reporter.ifDebug { _ => out.close }
+ reporter.ifDebug { _ => out.close() }
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 74cf6d03106e57433153bce6e745e595af470ea7..938dd2667f1b67863b4cab35326f4bc5187811b9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -36,7 +36,7 @@ trait SMTLIBTarget {
val file = context.files.headOption.map(_.getName).getOrElse("NA")
val n = VCNumbers.getNext(targetName+file)
- val dir = new java.io.File("vcs");
+ val dir = new java.io.File("vcs")
if (!dir.isDirectory) {
dir.mkdir
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 1015b4a924c10f03882cdcc46656a57bbd68db82..ef7a58f1c0850d8155937140946100c6da29c124 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -23,7 +23,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
def mkTemplate(body: Expr): FunctionTemplate[T] = {
if (cacheExpr contains body) {
- return cacheExpr(body);
+ return cacheExpr(body)
}
val fakeFunDef = new FunDef(FreshIdentifier("fake", alwaysShowUniqueID = true),
@@ -162,7 +162,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
var c = l
- while(!c.isEmpty) {
+ while(c.nonEmpty) {
val (span, rest) = c.span(p)
if (span.isEmpty) {
@@ -276,7 +276,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
case l @ Lambda(args, body) =>
val idArgs : Seq[Identifier] = lambdaArgs(l)
- val trArgs : Seq[T] = idArgs.map(encoder.encodeId(_))
+ val trArgs : Seq[T] = idArgs.map(encoder.encodeId)
val lid = FreshIdentifier("lambda", l.getType, true)
val clause = appliedEquals(Variable(lid), l)
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index 4d6716c6b8a337461de95a797f7b1a9af4951fa0..ddf513b8c5b01cc8bd131186342dfbe24c7ac357 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -142,13 +142,13 @@ object Template {
lambdas.map { case (idT, template) => template.id -> idT }
}
- val encodeExpr : Expr => T = encoder.encodeExpr(idToTrId) _
+ val encodeExpr : Expr => T = encoder.encodeExpr(idToTrId)
val clauses : Seq[T] = (for ((b,es) <- guardedExprs; e <- es) yield {
encodeExpr(Implies(Variable(b), e))
}).toSeq
- val extractInfos : Expr => (Set[TemplateCallInfo[T]], Set[App[T]]) = functionCallInfos(encodeExpr) _
+ val extractInfos : Expr => (Set[TemplateCallInfo[T]], Set[App[T]]) = functionCallInfos(encodeExpr)
val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 4fad725d9a914f6abd80c0eda8d887bdb50f3984..015dc2ada44ddd862106990a8f16eee515389265 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -76,7 +76,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
appBlockersStack = appBlockersStack.drop(lvl)
}
- def dumpBlockers = {
+ def dumpBlockers() = {
val generations = (callInfo.map(_._2._1).toSet ++ appInfo.map(_._2._1).toSet).toSeq.sorted
generations.foreach { generation =>
@@ -92,7 +92,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
}
}
- def canUnroll = !callInfo.isEmpty || !appInfo.isEmpty
+ def canUnroll = callInfo.nonEmpty || appInfo.nonEmpty
def currentBlockers = callInfo.map(_._2._3).toSeq ++ appInfo.map(_._2._4).toSeq
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index b1626ec6c908958ed7b69fb09f01ba7e39f0dbc7..6237fde6a01ff5a1c14d73a2d6c2c8618a1d169d 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -55,11 +55,11 @@ trait AbstractZ3Solver
freed = true
if (z3 ne null) {
z3.delete()
- z3 = null;
+ z3 = null
}
}
- protected[z3] var interrupted = false;
+ protected[z3] var interrupted = false
override def interrupt() {
interrupted = true
@@ -89,7 +89,7 @@ trait AbstractZ3Solver
object LeonType {
def unapply(a: Z3Sort): Option[(TypeTree)] = {
- sorts.getLeon(a).map(tt => (tt))
+ sorts.getLeon(a).map(tt => tt)
}
}
@@ -340,7 +340,7 @@ trait AbstractZ3Solver
val resultingZ3Info = z3.mkADTSorts(defs)
- for ((z3Inf, (root, childrenList)) <- (resultingZ3Info zip newHierarchies)) {
+ for ((z3Inf, (root, childrenList)) <- resultingZ3Info zip newHierarchies) {
sorts += (root -> z3Inf._1)
assert(childrenList.size == z3Inf._2.size)
for ((child, (consFun, testFun)) <- childrenList zip (z3Inf._2 zip z3Inf._3)) {
@@ -351,7 +351,7 @@ trait AbstractZ3Solver
}
for ((child, fieldFuns) <- childrenList zip z3Inf._4) {
assert(child.fields.size == fieldFuns.size)
- for ((fid, selFun) <- (child.fields.map(_.id) zip fieldFuns)) {
+ for ((fid, selFun) <- child.fields.map(_.id) zip fieldFuns) {
adtFieldSelectors += ((child, fid) -> selFun)
reverseADTFieldSelectors += (selFun -> (child, fid))
}
@@ -364,7 +364,7 @@ trait AbstractZ3Solver
}
// Prepares some of the Z3 sorts, but *not* the tuple sorts; these are created on-demand.
- private def prepareSorts: Unit = {
+ private def prepareSorts(): Unit = {
import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
val Seq((us, Seq(unitCons), Seq(unitTester), _)) = z3.mkADTSorts(
@@ -490,7 +490,7 @@ trait AbstractZ3Solver
val varsInformula: Set[Identifier] = variablesOf(expr)
- var z3Vars: Map[Identifier,Z3AST] = if(!initialMap.isEmpty) {
+ var z3Vars: Map[Identifier,Z3AST] = if(initialMap.nonEmpty) {
initialMap
} else {
// FIXME TODO pleeeeeeeease make this cleaner. Ie. decide what set of
@@ -504,7 +504,7 @@ trait AbstractZ3Solver
case LetTuple(ids, e, b) => {
var ix = 1
z3Vars = z3Vars ++ ids.map((id) => {
- val entry = (id -> rec(tupleSelect(e, ix, ids.size)))
+ val entry = id -> rec(tupleSelect(e, ix, ids.size))
ix += 1
entry
})
@@ -526,7 +526,7 @@ trait AbstractZ3Solver
typeToSort(tu.getType) // Make sure we generate sort & meta info
val meta = tupleMetaDecls(normalizeType(tu.getType))
- meta.cons(args.map(rec(_)): _*)
+ meta.cons(args.map(rec): _*)
case ts @ TupleSelect(tu, i) =>
typeToSort(tu.getType) // Make sure we generate sort & meta info
@@ -560,8 +560,8 @@ trait AbstractZ3Solver
}
case ite @ IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e))
- case And(exs) => z3.mkAnd(exs.map(rec(_)): _*)
- case Or(exs) => z3.mkOr(exs.map(rec(_)): _*)
+ case And(exs) => z3.mkAnd(exs.map(rec): _*)
+ case Or(exs) => z3.mkOr(exs.map(rec): _*)
case Implies(l, r) => z3.mkImplies(rec(l), rec(r))
case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
case Not(e) => z3.mkNot(rec(e))
@@ -609,7 +609,7 @@ trait AbstractZ3Solver
case c @ CaseClass(ct, args) =>
typeToSort(ct) // Making sure the sort is defined
val constructor = adtConstructors(ct)
- constructor(args.map(rec(_)): _*)
+ constructor(args.map(rec): _*)
case c @ CaseClassSelector(cct, cc, sel) =>
typeToSort(cct) // Making sure the sort is defined
@@ -622,7 +622,7 @@ trait AbstractZ3Solver
tester(rec(e))
case f @ FunctionInvocation(tfd, args) =>
- z3.mkApp(functionDefToDecl(tfd), args.map(rec(_)): _*)
+ z3.mkApp(functionDefToDecl(tfd), args.map(rec): _*)
case fa @ Application(caller, args) =>
z3.mkSelect(rec(caller), rec(tupleWrap(args)))
@@ -797,7 +797,7 @@ trait AbstractZ3Solver
case IntLiteral(index) => index
case _ => throw new CantTranslateException(t)
}
- (index -> rec(v))
+ index -> rec(v)
}
finiteArray(valuesMap, Some(elseValue, IntLiteral(length)), dt)
@@ -837,7 +837,7 @@ trait AbstractZ3Solver
case _ =>
import Z3DeclKind._
- val rargs = args.map(rec(_))
+ val rargs = args.map(rec)
z3.getDeclKind(decl) match {
case OpTrue => BooleanLiteral(true)
case OpFalse => BooleanLiteral(false)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 9a0f7a92869a53806b1a62c3da3c595e01350ada..b9852dfe9fefe54576404d163793b57d7735e2dc 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -279,7 +279,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
case Some(true) => // SAT
- val z3model = solver.getModel
+ val z3model = solver.getModel()
if (this.checkModels) {
val (isValid, model) = validateModel(z3model, entireFormula, allVars, silenceErrors = false)
@@ -303,7 +303,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
case Some(false) if !unrollingBank.canUnroll =>
- val core = z3CoreToCore(solver.getUnsatCore)
+ val core = z3CoreToCore(solver.getUnsatCore())
foundAnswer(Some(false), core = core)
@@ -333,7 +333,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
for (c <- solver.getUnsatCore) {
val (z3ast, pol) = coreElemToBlocker(c)
- assert(pol == true)
+ assert(pol)
unrollingBank.promoteBlocker(z3ast)
}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index b903921a2af79fcd4e2a47d5b5514212dc0dfb3b..1ee010c4f71fef31cadc4fabcfc9c2f302c31fb1 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -41,7 +41,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
val solver = z3.mkSolver
def push() {
- solver.push
+ solver.push()
}
def pop(lvl: Int = 1) {
@@ -54,10 +54,10 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
solver.assertCnstr(toZ3Formula(expression).getOrElse(scala.sys.error("Failed to compile to Z3: "+expression)))
}
- override def check: Option[Boolean] = solver.check
+ override def check: Option[Boolean] = solver.check()
override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
- freeVariables ++= assumptions.flatMap(variablesOf(_))
+ freeVariables ++= assumptions.flatMap(variablesOf)
solver.checkAssumptions(assumptions.toSeq.map(toZ3Formula(_).get) : _*)
}
@@ -66,7 +66,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program)
}
def getUnsatCore = {
- solver.getUnsatCore.map(ast => fromZ3Formula(null, ast) match {
+ solver.getUnsatCore().map(ast => fromZ3Formula(null, ast) match {
case n @ Not(Variable(_)) => n
case v @ Variable(_) => v
case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index bb290cd89f8ef808b7561120d4e0325c57a189e2..5558c745ff5af705a582b13c08012a3edd2370b8 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -22,9 +22,9 @@ trait Z3ModelReconstruction {
variables.getZ3(id.toVariable).flatMap { z3ID =>
expectedType match {
- case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral(_))
+ case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral)
case Int32Type =>
- model.evalAs[Int](z3ID).map(IntLiteral(_)).orElse{
+ model.evalAs[Int](z3ID).map(IntLiteral).orElse{
model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t))
}
case IntegerType => model.evalAs[Int](z3ID).map(InfiniteIntegerLiteral(_))
@@ -40,16 +40,16 @@ trait Z3ModelReconstruction {
var asMap = Map.empty[Identifier,Expr]
def completeID(id : Identifier) : Unit = {
- asMap = asMap + ((id -> simplestValue(id.getType)))
+ asMap = asMap + (id -> simplestValue(id.getType))
reporter.debug("Completing variable '" + id + "' to simplest value")
}
for(id <- ids) {
modelValue(model, id) match {
- case None if (AUTOCOMPLETEMODELS) => completeID(id)
+ case None if AUTOCOMPLETEMODELS => completeID(id)
case None => ;
- case Some(v @ Variable(exprId)) if (AUTOCOMPLETEMODELS && exprId == id) => completeID(id)
- case Some(ex) => asMap = asMap + ((id -> ex))
+ case Some(v @ Variable(exprId)) if AUTOCOMPLETEMODELS && exprId == id => completeID(id)
+ case Some(ex) => asMap = asMap + (id -> ex)
}
}
asMap
diff --git a/src/main/scala/leon/synthesis/Algebra.scala b/src/main/scala/leon/synthesis/Algebra.scala
index 474d6e90e2bd4b2277cad21ca22ce7cea8705ac9..f63a7fec20036bb41c0c3fa90910e86b01ce24da 100644
--- a/src/main/scala/leon/synthesis/Algebra.scala
+++ b/src/main/scala/leon/synthesis/Algebra.scala
@@ -64,7 +64,7 @@ object Algebra {
val (na, nb) = (a.abs, b.abs)
def gcd0(a: BigInt, b: BigInt): BigInt = {
require(a >= b)
- if(b == 0) a else gcd0(b, a % b)
+ if(b == BigInt(0)) a else gcd0(b, a % b)
}
if(na > nb) gcd0(na, nb) else gcd0(nb, na)
}
@@ -176,7 +176,7 @@ object Algebra {
def extendedEuclid(a: BigInt, b: BigInt): (BigInt, BigInt) = {
def rec(a: BigInt, b: BigInt): (BigInt, BigInt) = {
require(a >= 0 && b >= 0)
- if(b == 0) (1, 0) else {
+ if(b == BigInt(0)) (1, 0) else {
val (q, r) = divide(a, b)
val (s, t) = extendedEuclid(b, r)
(t, s - q * t)
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
similarity index 100%
rename from src/main/scala/leon/synthesis/ConvertWithOracles.scala
rename to src/main/scala/leon/synthesis/ConvertWithOracle.scala
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index fe8be1a7c34f1a0b07a08bb58fb6ce618b300553..b6a0db402bd0796db54b1a33db7970b9661da23b 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -20,7 +20,7 @@ abstract class CostModel(val name: String) {
}
}
-case class Cost(val minSize: Int) extends AnyVal with Ordered[Cost] {
+case class Cost(minSize: Int) extends AnyVal with Ordered[Cost] {
def compare(that: Cost): Int = {
this.minSize-that.minSize
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 91f21e4ee6a05eac42e462492ec76c890722cb2d..16edbd4ab05643bf350a6aa240e2b2e8b4023222 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -150,7 +150,7 @@ class ExamplesFinder(ctx: LeonContext, program: Program) {
} else {
// If the input contains free variables, it does not provide concrete examples.
// We will instantiate them according to a simple grammar to get them.
- val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions _)
+ val enum = new MemoizedEnumerator[TypeTree, Expr](ValueGrammar.getProductions)
val values = enum.iterator(tupleTypeWrap(freeVars.map{ _.getType }))
val instantiations = values.map {
v => freeVars.zip(unwrapTuple(v, freeVars.size)).toMap
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 0e81f6f6c19f8ea6c27e5b35d8a19f90aaaa9f2e..11bd6e704a1216ceeef3d1de3ba7655057006991 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -19,18 +19,18 @@ class FileInterface(reporter: Reporter) {
import java.io.{File, BufferedWriter, FileWriter}
val FileExt = """^(.+)\.([^.]+)$""".r
- origFile.getAbsolutePath() match {
+ origFile.getAbsolutePath match {
case FileExt(path, "scala") =>
var i = 0
def savePath = path+".scala."+i
- while (new File(savePath).isFile()) {
+ while (new File(savePath).isFile) {
i += 1
}
val origCode = readFile(origFile)
val backup = new File(savePath)
- val newFile = new File(origFile.getAbsolutePath())
+ val newFile = new File(origFile.getAbsolutePath)
origFile.renameTo(backup)
var newCode = origCode
@@ -40,7 +40,7 @@ class FileInterface(reporter: Reporter) {
val out = new BufferedWriter(new FileWriter(newFile))
out.write(newCode)
- out.close
+ out.close()
case _ =>
}
diff --git a/src/main/scala/leon/synthesis/Histogram.scala b/src/main/scala/leon/synthesis/Histogram.scala
index 2614704ea824066da4d6caae5171b724b7b10a42..9d3a33cd73c5992bdf79d1ccb5b244dc2986ca3a 100644
--- a/src/main/scala/leon/synthesis/Histogram.scala
+++ b/src/main/scala/leon/synthesis/Histogram.scala
@@ -11,12 +11,12 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
*/
def and(that: Histogram): Histogram = {
val a = Array.fill(bound)(0d)
- var i = 0;
+ var i = 0
while(i < bound) {
- var j = 0;
+ var j = 0
while(j <= i) {
- val v1 = (this.values(j) * that.values(i-j))
+ val v1 = this.values(j) * that.values(i - j)
val v2 = a(i)
a(i) = v1+v2 - (v1*v2)
@@ -39,7 +39,7 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
*/
def or(that: Histogram): Histogram = {
val a = Array.fill(bound)(0d)
- var i = 0;
+ var i = 0
while(i < bound) {
val v1 = this.values(i)
val v2 = that.values(i)
@@ -57,27 +57,27 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
}
lazy val mode = {
- var max = 0d;
- var argMax = -1;
- var i = 0;
+ var max = 0d
+ var argMax = -1
+ var i = 0
while(i < bound) {
if ((argMax < 0) || values(i) > max) {
- argMax = i;
+ argMax = i
max = values(i)
}
- i += 1;
+ i += 1
}
(max, argMax)
}
lazy val firstNonZero = {
- var i = 0;
+ var i = 0
var mini = -1
while(i < bound && mini < 0) {
if (values(i) > 0) {
- mini = i;
+ mini = i
}
- i += 1;
+ i += 1
}
if (mini >= 0) {
(values(mini), mini)
@@ -87,9 +87,9 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
}
lazy val moment = {
- var i = 0;
- var moment = 0d;
- var allV = 0d;
+ var i = 0
+ var moment = 0d
+ var allV = 0d
while(i < bound) {
val v = values(i)
moment += v*i
@@ -122,11 +122,11 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
def rescaled(by: Double): Histogram = {
val a = new Array[Double](bound)
- var i = 0;
+ var i = 0
while(i < bound) {
val v = values(i)
- val nv = 1-Math.pow(1-v, by);
+ val nv = 1-Math.pow(1-v, by)
a(i) = nv
@@ -153,8 +153,8 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
}
override def toString: String = {
- var lastv = -1d;
- var fromi = -1;
+ var lastv = -1d
+ var fromi = -1
val entries = new scala.collection.mutable.ArrayBuffer[((Int, Int), Double)]()
@@ -162,7 +162,7 @@ class Histogram(val bound: Int, val values: Array[Double]) extends Ordered[Histo
val v = values(i)
if (lastv < 0) {
lastv = v
- fromi = i;
+ fromi = i
}
if (lastv != v) {
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index c68590fbd6a9004ff0a4dcb6b4b7637be3eb03ca..d3a7663e94dfbf9f1c3cd7e2385f8be2cdea1ca6 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -7,7 +7,7 @@ import purescala.Trees._
import leon.utils.ASCIIHelpers._
class Example(val ins: Seq[Expr])
-case class InOutExample(is: Seq[Expr], val outs: Seq[Expr]) extends Example(is)
+case class InOutExample(is: Seq[Expr], outs: Seq[Expr]) extends Example(is)
case class InExample(is: Seq[Expr]) extends Example(is)
class ExamplesTable(title: String, ts: Seq[Example]) {
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 5ab60fe9b561b6c7702ca615af7f08b103746662..684bae5c616591c2d8c6a4ef768687ce94b7ceb3 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -17,7 +17,7 @@ object LinearEquations {
//return a mapping for each of the n variables in (pre, map, freshVars)
def elimVariable(evaluator: Evaluator, as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
require(normalizedEquation.size > 1)
- require(normalizedEquation.tail.forall{case InfiniteIntegerLiteral(i) if i != 0 => true case _ => false})
+ require(normalizedEquation.tail.forall{case InfiniteIntegerLiteral(i) if i != BigInt(0) => true case _ => false})
val t: Expr = normalizedEquation.head
val coefsVars: List[BigInt] = normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}
val orderedParams: Array[Identifier] = as.toArray
@@ -30,7 +30,7 @@ object LinearEquations {
(Equals(Modulo(t, InfiniteIntegerLiteral(coef)), InfiniteIntegerLiteral(0)), List(UMinus(Division(t, InfiniteIntegerLiteral(coef)))), List())
} else if(d > 1) {
val newCoefsParams: List[Expr] = coefsParams.map(i => InfiniteIntegerLiteral(i/d) : Expr)
- val newT = newCoefsParams.zip(InfiniteIntegerLiteral(1)::orderedParams.map(Variable(_)).toList).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
+ val newT = newCoefsParams.zip(InfiniteIntegerLiteral(1)::orderedParams.map(Variable).toList).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
elimVariable(evaluator, as, newT :: normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(i/d) : Expr})
} else {
val basis: Array[Array[BigInt]] = linearSet(evaluator, as, normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}.toArray)
@@ -71,7 +71,7 @@ object LinearEquations {
}
}
for(j <- 0 until K.size - 1) {
- val (_, sols) = particularSolution(as, InfiniteIntegerLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(InfiniteIntegerLiteral(_)).toList)
+ val (_, sols) = particularSolution(as, InfiniteIntegerLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(InfiniteIntegerLiteral).toList)
var i = 0
while(i < sols.size) {
// seriously ???
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index 2f05eb1a723f2005b36a0dbf4a6edcee391fbdd0..187ec4d059086b17e684d4a1a63dd59dffcd733d 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -49,7 +49,7 @@ class PartialSolution(g: Graph, includeUntrusted: Boolean = false) {
}
- def getSolution(): Solution = {
+ def getSolution: Solution = {
getSolutionFor(g.root)
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index a4a0686c1c6e3a4e63893c5f29bc46558c5e60e7..90f3eb4ff546db143eb06d6222bed298ba98b1ac 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -84,7 +84,7 @@ abstract class SolutionBuilder {
def apply(sols: List[Solution]): Option[Solution]
}
-case class SolutionBuilderDecomp(val types: Seq[TypeTree], recomp: List[Solution] => Option[Solution]) extends SolutionBuilder {
+case class SolutionBuilderDecomp(types: Seq[TypeTree], recomp: List[Solution] => Option[Solution]) extends SolutionBuilder {
def apply(sols: List[Solution]): Option[Solution] = {
assert(types.size == sols.size)
recomp(sols)
@@ -95,7 +95,7 @@ case class SolutionBuilderDecomp(val types: Seq[TypeTree], recomp: List[Solution
* Used by rules expected to close, no decomposition but maybe we already know
* the solution when instantiating
*/
-case class SolutionBuilderCloser(val osol: Option[Solution] = None) extends SolutionBuilder {
+case class SolutionBuilderCloser(osol: Option[Solution] = None) extends SolutionBuilder {
val types = Nil
def apply(sols: List[Solution]) = {
assert(sols.isEmpty)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index a6f794ca73faff97ea4bd303455dab5258253421..de1916639622a7a5b009ccf46476821f0ca31532 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -117,7 +117,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def run(ctx: LeonContext)(p: Program): Program = {
val options = processOptions(ctx)
- def excludeByDefault(fd: FunDef): Boolean = (fd.annotations contains "library")
+ def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
val fdFilter = {
import OptionsHelpers._
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 6898a685f8e9a2b15960d6a4d1ef88d574f1dcb5..44246404e9f35f0080c39975444ee45e2514ce45 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -29,7 +29,7 @@ class Synthesizer(val context : LeonContext,
lazy val sctx = SynthesisContext.fromSynthesizer(this)
- def getSearch(): Search = {
+ def getSearch: Search = {
if (settings.manualSearch.isDefined) {
new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
} else if (settings.searchWorkers > 1) {
@@ -41,7 +41,7 @@ class Synthesizer(val context : LeonContext,
}
def synthesize(): (Search, Stream[Solution]) = {
- val s = getSearch();
+ val s = getSearch
val t = context.timers.synthesis.search.start()
diff --git a/src/main/scala/leon/synthesis/graph/DotGenerator.scala b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
index c4ee0d758c7012bf8e442f7087c8b472227fb825..8d71ffabafbe0c6cb0373670ca726852f63140b3 100644
--- a/src/main/scala/leon/synthesis/graph/DotGenerator.scala
+++ b/src/main/scala/leon/synthesis/graph/DotGenerator.scala
@@ -57,7 +57,7 @@ class DotGenerator(g: Graph) {
""
}
- res append " "+nodesToNames(f)+" -> "+nodesToNames(t) +" [label=\""+label+"\""+style+"]\n";
+ res append " "+nodesToNames(f)+" -> "+nodesToNames(t) +" [label=\""+label+"\""+style+"]\n"
}
res append "}\n"
@@ -104,7 +104,7 @@ class DotGenerator(g: Graph) {
res append "<TR><TD BORDER=\"0\">"+escapeHTML(n.cost.asString)+"</TD></TR>"
}
- res append "<TR><TD BORDER=\"1\" BGCOLOR=\""+color+"\">"+escapeHTML(limit(nodeDesc(n)))+"</TD></TR>";
+ res append "<TR><TD BORDER=\"1\" BGCOLOR=\""+color+"\">"+escapeHTML(limit(nodeDesc(n)))+"</TD></TR>"
if (n.isSolved) {
res append "<TR><TD BGCOLOR=\""+color+"\">"+escapeHTML(limit(n.generateSolutions().head.toString))+"</TD></TR>"
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 76e161b1b7a105c059ace1d6e26db4768a68228e..349a4afbfce56a0128d62f6054ed630dc6175de2 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -96,7 +96,7 @@ sealed abstract class Node(cm: CostModel, val parent: Option[Node]) {
class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) extends Node(cm, parent) {
val p = ri.problem
- override def toString = "\u2227 "+ri;
+ override def toString = "\u2227 "+ri
def expand(hctx: SearchContext): Unit = {
require(!isExpanded)
@@ -111,7 +111,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
ri.apply(hctx) match {
case RuleClosed(sols) =>
solutions = Some(sols)
- selectedSolution = 0;
+ selectedSolution = 0
updateCost()
@@ -159,7 +159,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
// Everything is solved correctly
if (solveds.size == descendents.size) {
- isSolved = true;
+ isSolved = true
parents.foreach(_.onSolved(this))
}
}
@@ -168,7 +168,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(cm, parent) {
- override def toString = "\u2228 "+p;
+ override def toString = "\u2228 "+p
def getInstantiations(hctx: SearchContext): List[RuleInstantiation] = {
val rules = hctx.sctx.rules
@@ -183,7 +183,7 @@ class OrNode(cm: CostModel, parent: Option[Node], val p: Problem) extends Node(c
}.toList
if (results.nonEmpty) {
- return results;
+ return results
}
}
Nil
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index b5f37629f5fdd987e73e4aaf1a46739c0131e72f..9611593f04ffeb8e643cc3001d8946b551f2df2a 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -9,11 +9,11 @@ import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
abstract class Search(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: CostModel) extends Interruptible {
- val g = new Graph(costModel, p);
+ val g = new Graph(costModel, p)
def findNodeToExpandFrom(n: Node): Option[Node]
- val interrupted = new AtomicBoolean(false);
+ val interrupted = new AtomicBoolean(false)
def doStep(n: Node, sctx: SynthesisContext): Unit = {
ctx.timers.synthesis.step.timed {
@@ -100,7 +100,8 @@ class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: Cost
}
}
- var counter = 0;
+ var counter = 0
+
def findNodeToExpandFrom(from: Node): Option[Node] = {
counter += 1
ctx.timers.synthesis.search.find.timed {
@@ -183,7 +184,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
}
override def doStep(n: Node, sctx: SynthesisContext) = {
- super.doStep(n, sctx);
+ super.doStep(n, sctx)
// Backtrack view to a point where node is neither closed nor solved
if (n.isDeadEnd || n.isSolved) {
@@ -309,7 +310,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
continue = false
case e: Throwable =>
- error("Woops: "+e.getMessage())
+ error("Woops: "+e.getMessage)
e.printStackTrace()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index f99c8916e67e929f60b48d8885db9bd3e685aa5c..5bb9d6f5d8b70649d8f1e606cacd08ed460921a0 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -18,14 +18,14 @@ case object ADTDual extends NormalizingRule("ADTDual") {
val (toRemove, toAdd) = exprs.collect {
- case eq @ Equals(cc @ CaseClass(ct, args), e) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
+ case eq @ Equals(cc @ CaseClass(ct, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
(eq, CaseClassInstanceOf(ct, e) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, CaseClassSelector(ct, e, vd.id)) } )
- case eq @ Equals(e, cc @ CaseClass(ct, args)) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
+ case eq @ Equals(e, cc @ CaseClass(ct, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
(eq, CaseClassInstanceOf(ct, e) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, CaseClassSelector(ct, e, vd.id)) } )
}.unzip
- if (!toRemove.isEmpty) {
+ if (toRemove.nonEmpty) {
val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
Some(decomp(List(sub), forward, "ADTDual"))
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 6dcb79d5e64f250aada4a997cc6f146e3d414093..6c12864c5f41b5afe186975a6f4fc4494f5a0a70 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -57,7 +57,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
CaseClassPattern(None, cct, withIds.map(id => WildcardPattern(Some(id))))
case CaseClassPattern(binder, sccd, sub) =>
- CaseClassPattern(binder, sccd, sub.map(unrollPattern(id, cct, withIds) _))
+ CaseClassPattern(binder, sccd, sub.map(unrollPattern(id, cct, withIds)))
case _ => on
}
@@ -71,7 +71,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType, true)).toList
val newIds = ids.filterNot(_ == id) ++ subIds
- val newCalls = if (!subIds.isEmpty) {
+ val newCalls = if (subIds.nonEmpty) {
List(subIds.find(isRec)).flatten
} else {
List()
@@ -81,7 +81,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
//println(subIds)
val newPattern = unrollPattern(id, cct, subIds)(pat)
- val newMap = trMap.mapValues(v => substAll(Map(id -> CaseClass(cct, subIds.map(Variable(_)))), v))
+ val newMap = trMap.mapValues(v => substAll(Map(id -> CaseClass(cct, subIds.map(Variable))), v))
InductCase(newIds, newCalls, newPattern, and(pc, CaseClassInstanceOf(cct, Variable(id))), newMap)
}
@@ -91,7 +91,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
}
}
- val cases = unroll(init).flatMap(unroll(_))
+ val cases = unroll(init).flatMap(unroll)
val innerPhi = substAll(substMap, p.phi)
val innerPC = substAll(substMap, p.pc)
@@ -114,7 +114,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
for (cid <- calls) {
val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
postXss = postXss ::: postXs
- val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
+ val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable)
postFs = substAll(postXsMap + (inductOn -> Variable(cid)), innerPhi) :: postFs
recCalls += postXs -> (Variable(cid) +: residualArgs.map(id => Variable(id)))
@@ -132,7 +132,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
- val cases = for ((sol, (problem, pat, calls, pc)) <- (sols zip subProblemsInfo)) yield {
+ val cases = for ((sol, (problem, pat, calls, pc)) <- sols zip subProblemsInfo) yield {
globalPre ::= and(pc, sol.pre)
SimpleCase(pat, calls.foldLeft(sol.term){ case (t, (binders, callargs)) => letTuple(binders, FunctionInvocation(newFun.typed, callargs), t) })
@@ -157,7 +157,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
Some(Solution(orJoin(globalPre),
sols.flatMap(_.defs).toSet+newFun,
- FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))),
+ FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable)),
sols.forall(_.isTrusted)
))
}
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index d88016265df5c2312acb7410238e3b2fc5896cfa..a836f884322556380bdf0134ad9522d6785a83be 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -41,7 +41,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val cases = optCases.flatten
- if (!cases.isEmpty) {
+ if (cases.nonEmpty) {
Some((id, act, cases))
} else {
None
@@ -57,9 +57,9 @@ case object ADTSplit extends Rule("ADT Split.") {
val args = cct.fields.map { vd => FreshIdentifier(vd.id.name, vd.getType, true) }.toList
- val subPhi = subst(id -> CaseClass(cct, args.map(Variable(_))), p.phi)
- val subPC = subst(id -> CaseClass(cct, args.map(Variable(_))), p.pc)
- val subWS = subst(id -> CaseClass(cct, args.map(Variable(_))), p.ws)
+ val subPhi = subst(id -> CaseClass(cct, args.map(Variable)), p.phi)
+ val subPC = subst(id -> CaseClass(cct, args.map(Variable)), p.pc)
+ val subWS = subst(id -> CaseClass(cct, args.map(Variable)), p.ws)
val subProblem = Problem(args ::: oas, subWS, subPC, subPhi, p.xs)
val subPattern = CaseClassPattern(None, cct, args.map(id => WildcardPattern(Some(id))))
@@ -71,7 +71,7 @@ case object ADTSplit extends Rule("ADT Split.") {
case sols =>
var globalPre = List[Expr]()
- val cases = for ((sol, (cct, problem, pattern)) <- (sols zip subInfo)) yield {
+ val cases = for ((sol, (cct, problem, pattern)) <- sols zip subInfo) yield {
if (sol.pre != BooleanLiteral(true)) {
val substs = (for ((field,arg) <- cct.fields zip problem.as ) yield {
(arg, CaseClassSelector(cct, id.toVariable, field.id))
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index eff8465aa0b921d3e28aac64ea9945b42cbcf58a..4d6dcca5c9c8786a1d266acdef0fb8bc1b4742f4 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -15,7 +15,7 @@ case object Assert extends NormalizingRule("Assert") {
val xsSet = p.xs.toSet
val (exprsA, others) = exprs.partition(e => (variablesOf(e) & xsSet).isEmpty)
- if (!exprsA.isEmpty) {
+ if (exprsA.nonEmpty) {
if (others.isEmpty) {
Some(solve(Solution(andJoin(exprsA), Set(), tupleWrap(p.xs.map(id => simplestValue(id.getType))))))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index d08a1e07724800020f76e692f33e169128aba8b5..46fd17233ac07d0df0fa5cf610392913063c0da6 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -119,12 +119,12 @@ abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
)
- val timers = sctx.context.timers.synthesis.rules.tegis;
+ val timers = sctx.context.timers.synthesis.rules.tegis
val matches = enum.iterator(getRootLabel(targetType))
if (matches.hasNext) {
- RuleClosed(Solution(BooleanLiteral(true), Set(), matches.next, isTrusted = false))
+ RuleClosed(Solution(BooleanLiteral(true), Set(), matches.next(), isTrusted = false))
} else {
RuleFailed()
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
similarity index 100%
rename from src/main/scala/leon/synthesis/rules/Cegis.scala
rename to src/main/scala/leon/synthesis/rules/CEGIS.scala
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
similarity index 95%
rename from src/main/scala/leon/synthesis/rules/CegisLike.scala
rename to src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 6eeb98f8f89e3bab7919a2e8bde73b3657ee5c22..f3191fdfce3346187be49e7089bc5153013ecf46 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -37,7 +37,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
grammar: ExpressionGrammar[T],
rootLabel: TypeTree => T,
maxUnfoldings: Int = 3
- );
+ )
def getParams(sctx: SynthesisContext, p: Problem): CegisParams
@@ -46,7 +46,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val cexSolverTo = 2000L
// Track non-deterministic programs up to 50'000 programs, or give up
- val nProgramsLimit = 100000;
+ val nProgramsLimit = 100000
val sctx = hctx.sctx
val ctx = sctx.context
@@ -213,17 +213,17 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// We order the lets base don dependencies
def defFor(c: Identifier): Expr = {
- cDeps(c).filter(lets contains _).foldLeft(lets(c)) {
+ cDeps(c).filter(lets.contains).foldLeft(lets(c)) {
case (e, c) => Let(c, defFor(c), e)
}
}
- val resLets = p.xs.map(defFor(_))
+ val resLets = p.xs.map(defFor)
val res = tupleWrap(p.xs.map(defFor))
- val substMap : Map[Expr,Expr] = (bsOrdered.zipWithIndex.map {
- case (b,i) => Variable(b) -> ArraySelect(bArrayId.toVariable, IntLiteral(i))
- }).toMap
+ val substMap : Map[Expr,Expr] = bsOrdered.zipWithIndex.map {
+ case (b, i) => Variable(b) -> ArraySelect(bArrayId.toVariable, IntLiteral(i))
+ }.toMap
val simplerRes = simplifyLets(res)
@@ -460,8 +460,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val initialBs = remainingBs ++ (if (finalUnfolding) Set() else closedBs.keySet)
- var cParent = Map[Identifier, Identifier]();
- var cOfB = Map[Identifier, Identifier]();
+ var cParent = Map[Identifier, Identifier]()
+ var cOfB = Map[Identifier, Identifier]()
var underBs = Map[Identifier, Set[Identifier]]()
for ((cparent, alts) <- cTree;
@@ -565,7 +565,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
def unfold(finalUnfolding: Boolean): Boolean = {
var newBs = Set[Identifier]()
- var unfoldedSomething = false;
+ var unfoldedSomething = false
def freshB() = {
val id = FreshIdentifier("B", BooleanType, true)
@@ -607,7 +607,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val cs = cToLabel.map(_._1)
val ex = gen.builder(cs.map(_.toVariable))
- if (!cs.isEmpty) {
+ if (cs.nonEmpty) {
closedBs += b -> cs.toSet
}
@@ -630,7 +630,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
sctx.reporter.ifDebug { printer =>
- printer("Grammar so far:");
+ printer("Grammar so far:")
grammar.printProductions(printer)
}
@@ -660,7 +660,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val activeBs = alts.map(_._1).filter(isBActive)
if (activeBs.nonEmpty) {
- val oneOf = orJoin(activeBs.map(_.toVariable));
+ val oneOf = orJoin(activeBs.map(_.toVariable))
//println(" - "+oneOf)
solver.assertCnstr(oneOf)
}
@@ -677,7 +677,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
case Some(true) =>
val model = solver.getModel
- val bModel = bs.filter(b => model.get(b).map(_ == BooleanLiteral(true)).getOrElse(false))
+ val bModel = bs.filter(b => model.get(b).contains(BooleanLiteral(true)))
//println("Found potential expr: "+getExpr(bModel)+" under inputs: "+model)
Some(Some(bModel))
@@ -803,14 +803,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
i
}
- def hasNext() = inputIterator.hasNext
+ def hasNext = inputIterator.hasNext
}
val failedTestsStats = new MutableMap[Seq[Expr], Int]().withDefaultValue(0)
- def hasInputExamples() = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
+ def hasInputExamples = baseExampleInputs.size > 0 || cachedInputIterator.hasNext
- var n = 1;
+ var n = 1
def allInputExamples() = {
if (n % 1000 == 0) {
baseExampleInputs = baseExampleInputs.sortBy(e => -failedTestsStats(e))
@@ -849,11 +849,11 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// }
//}
- var wrongPrograms = Set[Set[Identifier]]();
+ var wrongPrograms = Set[Set[Identifier]]()
// We further filter the set of working programs to remove those that fail on known examples
- if (hasInputExamples()) {
- for (bs <- prunedPrograms if !interruptManager.isInterrupted()) {
+ if (hasInputExamples) {
+ for (bs <- prunedPrograms if !interruptManager.isInterrupted) {
var valid = true
val examples = allInputExamples()
while(valid && examples.hasNext) {
@@ -864,7 +864,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
wrongPrograms += bs
prunedPrograms -= bs
- valid = false;
+ valid = false
}
}
@@ -885,11 +885,11 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
}
- if (nPassing == 0 || interruptManager.isInterrupted()) {
+ if (nPassing == 0 || interruptManager.isInterrupted) {
// No test passed, we can skip solver and unfold again, if possible
- skipCESearch = true;
+ skipCESearch = true
} else {
- var doFilter = true;
+ var doFilter = true
if (validateUpTo > 0) {
// Validate the first N programs individualy
@@ -902,7 +902,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// All programs failed verification, we filter everything out and unfold
//ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
doFilter = false
- skipCESearch = true;
+ skipCESearch = true
}
}
}
@@ -914,20 +914,20 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
ndProgram.shrinkTo(bssToKeep, unfolding == maxUnfoldings)
} else {
wrongPrograms.foreach {
- ndProgram.excludeProgram(_)
+ ndProgram.excludeProgram
}
}
}
}
// CEGIS Loop at a given unfolding level
- while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted()) {
+ while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted) {
ndProgram.solveForTentativeProgram() match {
case Some(Some(bs)) =>
// Should we validate this program with Z3?
- val validateWithZ3 = if (useCETests && hasInputExamples()) {
+ val validateWithZ3 = if (useCETests && hasInputExamples) {
if (allInputExamples().forall(ndProgram.testForProgram(bs))) {
// All valid inputs also work with this, we need to
@@ -981,14 +981,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
}
unfolding += 1
- } while(unfolding <= maxUnfoldings && result.isEmpty && !interruptManager.isInterrupted())
+ } while(unfolding <= maxUnfoldings && result.isEmpty && !interruptManager.isInterrupted)
result.getOrElse(RuleFailed())
} catch {
case e: Throwable =>
sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
- e.printStackTrace
+ e.printStackTrace()
RuleFailed()
} finally {
ndProgram.free()
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
similarity index 100%
rename from src/main/scala/leon/synthesis/rules/Cegless.scala
rename to src/main/scala/leon/synthesis/rules/CEGLESS.scala
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index be9f77b61c6e6b821fed2cd16e539b2a3b24ba1c..71f4ea75580a8d8a68a5494faeb39b64d049ec2d 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -27,14 +27,14 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
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)
+ (newIds.toList, CaseClass(cct, newIds.map(Variable)), map)
case TupleType(ts) =>
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
+ val map = newIds.zipWithIndex.map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
- (newIds.toList, tupleWrap(newIds.map(Variable(_))), map)
+ (newIds.toList, tupleWrap(newIds.map(Variable)), map)
case _ => sys.error("woot")
}
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index 1ec3858fc1a2c291199cb2b3bd7b40b161e16766..b6e57333c9c86624b26ac8ea2a4b418b743eb827 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") {
val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
- val newCC = CaseClass(ct, newIds.map(Variable(_)))
+ val newCC = CaseClass(ct, newIds.map(Variable))
subProblem = subst(x -> newCC, subProblem)
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 812a0c11901cdbb017d2d64f58e8ba01209013dd..89da1b14d520c17b509b3133adcc2edcf034e786 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -24,7 +24,7 @@ object Disunification {
}
}.unzip
- if (!toRemove.isEmpty) {
+ if (toRemove.nonEmpty) {
val sub = p.copy(phi = orJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
Some(decomp(List(sub), forward, this.name))
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index 087c9d9d14889386f79edab803a468c509605fbf..d331b492892a33ad08687f4d84584059b428ec32 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -37,15 +37,15 @@ case object EqualitySplit extends Rule("Eq. Split") {
case _ => false
}).values.flatten
- candidates.flatMap(_ match {
+ candidates.flatMap {
case List(a1, a2) =>
val sub1 = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc))
val sub2 = p.copy(pc = and(not(Equals(Variable(a1), Variable(a2))), p.pc))
- val onSuccess: List[Solution] => Option[Solution] = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(s1, s2) =>
- Some(Solution(or(s1.pre, s2.pre), s1.defs++s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
+ Some(Solution(or(s1.pre, s2.pre), s1.defs ++ s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term), s1.isTrusted && s2.isTrusted))
case _ =>
None
}
@@ -53,6 +53,6 @@ case object EqualitySplit extends Rule("Eq. Split") {
Some(decomp(List(sub1, sub2), onSuccess, s"Eq. Split on '$a1' and '$a2'"))
case _ =>
None
- })
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index f6edb6bb2a5f3403575a30f67f342beec18ad344..86ccb02adf9e582bd12a137c30aaf71bab142fe7 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -50,23 +50,27 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
}
- candidates.flatMap(_ match {
+ candidates.flatMap {
case List(a1, a2) =>
val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc))
val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc))
val subGT = p.copy(pc = and(GreaterThan(Variable(a1), Variable(a2)), p.pc))
- val onSuccess: List[Solution] => Option[Solution] = {
- case sols @ List(sLT, sEQ, sGT) =>
- val pre = orJoin(sols.map(_.pre))
+ val onSuccess: List[Solution] => Option[Solution] = {
+ case sols@List(sLT, sEQ, sGT) =>
+ val pre = orJoin(sols.map(_.pre))
val defs = sLT.defs ++ sEQ.defs ++ sGT.defs
- val term = IfExpr(LessThan(Variable(a1), Variable(a2)),
- sLT.term,
- IfExpr(Equals(Variable(a1), Variable(a2)),
- sEQ.term,
- sGT.term))
+ val term = IfExpr(
+ LessThan(Variable(a1), Variable(a2)),
+ sLT.term,
+ IfExpr(
+ Equals(Variable(a1), Variable(a2)),
+ sEQ.term,
+ sGT.term
+ )
+ )
Some(Solution(pre, defs, term, sols.forall(_.isTrusted)))
case _ =>
@@ -76,6 +80,6 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
Some(decomp(List(subLT, subEQ, subGT), onSuccess, s"Ineq. Split on '$a1' and '$a2'"))
case _ =>
None
- })
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index de4c61916c0b86b337c90a02d3a409253695038d..249c62f3084c4cd8bbd587f012b4f732827bf2fd 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -23,7 +23,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
val discreteHoles = sctx.settings.distreteHoles
if (!discreteHoles) {
- return Nil;
+ return Nil
}
val Some(oracleHead) = sctx.program.definedFunctions.find(_.id.name == "Oracle.head")
@@ -51,7 +51,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
case None =>
cache += fd -> false
- val res = fd.body.map(callsHolesExpr _).getOrElse(false)
+ val res = fd.body.exists(callsHolesExpr)
cache += fd -> res
res
@@ -118,7 +118,7 @@ case object InlineHoles extends Rule("Inline-Holes") {
val newProblem1 = p.copy(phi = newPhi)
Some(decomp(List(newProblem1), {
- case List(s) if (s.pre != BooleanLiteral(false)) => Some(s)
+ case List(s) if s.pre != BooleanLiteral(false) => Some(s)
case _ => None
}, "Avoid Holes"))
} else {
diff --git a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
index f87751e0d60421e14eb8ae67dae1a8bdaf580578..47851103139cd63ba67b760c2d08822675046bbb 100644
--- a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
@@ -17,10 +17,10 @@ case object InnerCaseSplit extends Rule("Inner-Case-Split"){
var phi = p.phi
phi match {
case Not(And(es)) =>
- phi = orJoin(es.map(not(_)))
+ phi = orJoin(es.map(not))
case Not(Or(es)) =>
- phi = andJoin(es.map(not(_)))
+ phi = andJoin(es.map(not))
case _ =>
}
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index 5a611320f8ee8b0ae819efb411be29dcde353cce..abf2545d56f708bdc50781c65341051ae4128e71 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -22,7 +22,7 @@ case object IntInduction extends Rule("Int Induction") {
val postXs = p.xs map (id => FreshIdentifier("r", id.getType, true))
- val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
+ val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable)
val newPhi = subst(origId -> Variable(inductOn), p.phi)
val newPc = subst(origId -> Variable(inductOn), p.pc)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 070a4fc392065278b09fb9f08aa559eaac9a0deb..d943fb072ebabcd2bb470083dab6840d072f4dee 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -30,7 +30,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
var eqxs: List[Identifier] = List()
var optionNormalizedEq: Option[List[Expr]] = None
- while(!candidates.isEmpty && optionNormalizedEq == None) {
+ while(candidates.nonEmpty && optionNormalizedEq == None) {
val eq@Equals(_,_) = candidates.head
candidates = candidates.tail
@@ -104,7 +104,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
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
- Some(Solution(and(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(letTuple(subproblemxs, freshTerm, replace(id2res, tupleWrap(problem.xs.map(Variable(_))))))), s.isTrusted))
+ Some(Solution(and(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(letTuple(subproblemxs, freshTerm, replace(id2res, tupleWrap(problem.xs.map(Variable)))))), s.isTrusted))
}
case _ =>
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index b043d069b108cfd00d7357f3b808d27cf8c37ea2..69217a3369e5610b24b5006c4d2fc61ddc233549 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -35,7 +35,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
- val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains(_))
+ val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains)
val processedVars: Set[(Identifier, Int)] = candidateVars.flatMap(v => {
try {
@@ -104,7 +104,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
case (x :: Nil) => x
case Nil => sys.error("cannot build a max expression with no argument")
}
- if(!lowerBounds.isEmpty)
+ if(lowerBounds.nonEmpty)
maxFun.body = Some(maxRec(maxValDefs.map(vd => Variable(vd.id)).toList))
def max(xs: Seq[Expr]): Expr = FunctionInvocation(maxFun.typed, xs)
//define min function
@@ -118,7 +118,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
case (x :: Nil) => x
case Nil => sys.error("cannot build a min expression with no argument")
}
- if(!upperBounds.isEmpty)
+ if(upperBounds.nonEmpty)
minFun.body = Some(minRec(minValDefs.map(vd => Variable(vd.id)).toList))
def min(xs: Seq[Expr]): Expr = FunctionInvocation(minFun.typed, xs)
val floorFun = new FunDef(FreshIdentifier("floorDiv"), Nil, Int32Type, Seq(
@@ -184,7 +184,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
Some(Solution(And(newPre, pre), defs,
letTuple(subProblemxs, term,
Let(processedVar, witness,
- tupleWrap(problem.xs.map(Variable(_))))), isTrusted=s.isTrusted))
+ tupleWrap(problem.xs.map(Variable)))), isTrusted=s.isTrusted))
} else if(remainderIds.size > 1) {
sys.error("TODO")
} else {
@@ -202,7 +202,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
concretePre,
letTuple(subProblemxs, concreteTerm,
Let(processedVar, witness,
- tupleWrap(problem.xs.map(Variable(_))))
+ tupleWrap(problem.xs.map(Variable)))
),
FunctionInvocation(funDef.typed, Seq(Minus(loopCounter, IntLiteral(1))))
)
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 54484206b5f4797b24343745811ab488e6be862a..5ad58a0a467da3941da81e64f279208c17222bc0 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -25,7 +25,7 @@ case object OnePoint extends NormalizingRule("One-point") {
(x, e, eq)
}
- if (!candidates.isEmpty) {
+ if (candidates.nonEmpty) {
val (x, e, eq) = candidates.head
val others = exprs.filter(_ != eq)
@@ -35,7 +35,7 @@ case object OnePoint extends NormalizingRule("One-point") {
val onSuccess: List[Solution] => Option[Solution] = {
case List(s @ Solution(pre, defs, term)) =>
- Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, tupleWrap(p.xs.map(Variable(_))))), s.isTrusted))
+ Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, tupleWrap(p.xs.map(Variable)))), s.isTrusted))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 13d79428e78ca1ea7a2474a3c545033b5fe30307..28256da4e9ea2c46b07074c73e00e99450da0996 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -12,7 +12,7 @@ import solvers._
case object OptimisticGround extends Rule("Optimistic Ground") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- if (!p.as.isEmpty && !p.xs.isEmpty) {
+ if (p.as.nonEmpty && p.xs.nonEmpty) {
val res = new RuleInstantiation(this.name) {
def apply(hctx: SearchContext) = {
@@ -23,8 +23,8 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
val tpe = tupleTypeWrap(p.xs.map(_.getType))
- var i = 0;
- var maxTries = 3;
+ var i = 0
+ var maxTries = 3
var result: Option[RuleApplication] = None
var continue = true
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
index 299bdeb0f75e2e3a893e9da1de384cdd0247290b..e329de9d16ced9fa07a334accfd84d53b97dbf28 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
@@ -20,7 +20,7 @@ case object OptimisticInjection extends Rule("Opt. Injection") {
}
val candidates = eqfuncalls.groupBy(_._1).filter(_._2.size > 1)
- if (!candidates.isEmpty) {
+ if (candidates.nonEmpty) {
var newExprs = exprs
for (cands <- candidates.values) {
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
index b8877d78356021d189d4f562403982f82309e7c9..f1356c77d3493882441cae0c583a06d9455cd3cd 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
@@ -20,7 +20,7 @@ case object SelectiveInlining extends Rule("Sel. Inlining") {
}
val candidates = eqfuncalls.groupBy(_._1).filter(_._2.size > 1)
- if (!candidates.isEmpty) {
+ if (candidates.nonEmpty) {
var newExprs = exprs
for (cands <- candidates.values) {
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala
similarity index 100%
rename from src/main/scala/leon/synthesis/rules/Tegis.scala
rename to src/main/scala/leon/synthesis/rules/TEGIS.scala
diff --git a/src/main/scala/leon/synthesis/rules/TegisLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
similarity index 95%
rename from src/main/scala/leon/synthesis/rules/TegisLike.scala
rename to src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 864f5302b2797a7b511ead9f0633585ca0561711..48ca570c2a6c86f54699f0947c3c4a4fad51e0ad 100644
--- a/src/main/scala/leon/synthesis/rules/TegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -21,7 +21,7 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
rootLabel: TypeTree => T,
enumLimit: Int = 10000,
reorderInterval: Int = 50
- );
+ )
def getParams(sctx: SynthesisContext, p: Problem): TegisParams
@@ -43,18 +43,18 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
val interruptManager = sctx.context.interruptManager
- val enum = new MemoizedEnumerator[T, Expr](grammar.getProductions _)
+ val enum = new MemoizedEnumerator[T, Expr](grammar.getProductions)
val targetType = tupleTypeWrap(p.xs.map(_.getType))
- val timers = sctx.context.timers.synthesis.rules.tegis;
+ val timers = sctx.context.timers.synthesis.rules.tegis
val allExprs = enum.iterator(params.rootLabel(targetType))
var failStat = Map[Seq[Expr], Int]().withDefaultValue(0)
var candidate: Option[Expr] = None
- var n = 1;
+ var n = 1
def findNext(): Option[Expr] = {
candidate = None
@@ -92,16 +92,16 @@ abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
candidate
}
- def toStream(): Stream[Solution] = {
+ def toStream: Stream[Solution] = {
findNext() match {
case Some(e) =>
- Stream.cons(Solution(BooleanLiteral(true), Set(), e, isTrusted = false), toStream())
+ Stream.cons(Solution(BooleanLiteral(true), Set(), e, isTrusted = false), toStream)
case None =>
Stream.empty
}
}
- RuleClosed(toStream())
+ RuleClosed(toStream)
} else {
sctx.reporter.debug("No test available")
RuleFailed()
diff --git a/src/main/scala/leon/synthesis/rules/Tegless.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
similarity index 100%
rename from src/main/scala/leon/synthesis/rules/Tegless.scala
rename to src/main/scala/leon/synthesis/rules/TEGLESS.scala
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 3b42bf379b6fa8c1f717f7a5added8e5c5bd5b4b..5311caf122d3ad02887f079f307e91c63928edd9 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -12,7 +12,7 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val unconstr = p.xs.toSet -- variablesOf(p.phi)
- if (!unconstr.isEmpty) {
+ if (unconstr.nonEmpty) {
val sub = p.copy(xs = p.xs.filterNot(unconstr))
val onSuccess: List[Solution] => Option[Solution] = {
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index db2e8b6d163ed103b81f8ef493c950bb93a772be..3c304c1fdefeccb9c5cb73a27932df0ef81ab027 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -25,7 +25,7 @@ object Unification {
}
}.unzip
- if (!toRemove.isEmpty) {
+ if (toRemove.nonEmpty) {
val sub = p.copy(phi = andJoin((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
List(decomp(List(sub), forward, this.name))
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 467a106436b2b8c3765117ed59bd8469463fa7ec..077003e82f9e13104164db13ce2e88c299924c6d 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -10,7 +10,7 @@ case object UnusedInput extends NormalizingRule("UnusedInput") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc) -- variablesOf(p.ws)
- if (!unused.isEmpty) {
+ if (unused.nonEmpty) {
val sub = p.copy(as = p.as.filterNot(unused))
List(decomp(List(sub), forward, s"Unused inputs ${p.as.filter(unused).mkString(", ")}"))
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index f44f23717a7109ed1c65eeb9951c10d121aee950..b2f5ced92cbade68ae90d05ca6f506ce266f092d 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -37,7 +37,7 @@ abstract class ExpressionGrammar[T <% Typed] {
def computeProductions(t: T): Seq[Gen]
def filter(f: Gen => Boolean) = {
- val that = this;
+ val that = this
new ExpressionGrammar[T] {
def computeProductions(t: T) = that.computeProductions(t).filter(f)
}
@@ -218,9 +218,10 @@ object ExpressionGrammars {
type L = Label[String]
- private var counter = -1;
+ private var counter = -1
+
def getNext(): Int = {
- counter += 1;
+ counter += 1
counter
}
@@ -353,7 +354,7 @@ object ExpressionGrammars {
val isRecursiveCall = (prog.callGraph.transitiveCallers(cfd) + cfd) contains fd
- val isDet = fd.body.map(isDeterministic).getOrElse(false)
+ val isDet = fd.body.exists(isDeterministic)
if (!isRecursiveCall && isDet) {
val free = fd.tparams.map(_.tp)
@@ -416,7 +417,7 @@ object ExpressionGrammars {
case g: Generator[Label[T], Expr] =>
if (l.depth == Some(bound) && g.subTrees.nonEmpty) {
None
- } else if (l.depth.map(_ > bound).getOrElse(false)) {
+ } else if (l.depth.exists(_ > bound)) {
None
} else {
Some(Generator(g.subTrees.map(sl => sl.copy(depth = l.depth.map(_+1).orElse(Some(1)))), g.builder))
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 617ae9462543a93888beba3f3c277e951ee4fe4c..77634ff76e49b1ffa3616674c317d8267ed98fe9 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -49,10 +49,10 @@ object Helpers {
case _ => None
}
- val knownSmallers = (clauses.collect {
- case Equals(v: Variable, s @ CaseClassSelector(cct, r, _)) => subExprsOf(s, v)
- case Equals(s @ CaseClassSelector(cct, r, _), v: Variable) => subExprsOf(s, v)
- }).flatten.groupBy(_._1).mapValues(v => v.map(_._2))
+ val knownSmallers = clauses.collect {
+ case Equals(v: Variable, s@CaseClassSelector(cct, r, _)) => subExprsOf(s, v)
+ case Equals(s@CaseClassSelector(cct, r, _), v: Variable) => subExprsOf(s, v)
+ }.flatten.groupBy(_._1).mapValues(v => v.map(_._2))
def argsSmaller(e: Expr, tpe: TypeTree): Seq[Expr] = e match {
case CaseClass(cct, args) =>
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index c5e99812590222f259ac73decfc61a1c59e1c30d..e73470f2a91239cec2edbd5f9ab113689e12e465 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -24,7 +24,7 @@ final case class Chain(relations: List[Relation]) {
case _ => false
}
- override def hashCode(): Int = identifier.hashCode
+ override def hashCode(): Int = identifier.hashCode()
lazy val funDef : FunDef = relations.head.funDef
lazy val funDefs : Set[FunDef] = relations.map(_.funDef).toSet
@@ -34,7 +34,7 @@ final case class Chain(relations: List[Relation]) {
private lazy val inlining : Seq[(Seq[ValDef], Expr)] = {
def rec(list: List[Relation], funDef: TypedFunDef, args: Seq[Expr]): Seq[(Seq[ValDef], Expr)] = list match {
case Relation(_, _, fi @ FunctionInvocation(fitfd, nextArgs), _) :: xs =>
- val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated(_)))
+ val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
val subst = (tfd.params.map(_.id) zip args).toMap
val expr = replaceFromIDs(subst, hoistIte(expandLets(matchToIfThenElse(tfd.body.get))))
val mappedArgs = nextArgs.map(e => replaceFromIDs(subst, tfd.translated(e)))
@@ -58,11 +58,11 @@ final case class Chain(relations: List[Relation]) {
}
val Relation(_, path, fi @ FunctionInvocation(fitfd, args), _) = relations.head
- val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated(_)))
+ val tfd = TypedFunDef(fitfd.fd, fitfd.tps.map(funDef.translated))
- lazy val newArgs = args.map(translate(_))
+ lazy val newArgs = args.map(translate)
- path.map(translate(_)) ++ (relations.tail match {
+ path.map(translate) ++ (relations.tail match {
case Nil => if (finalSubst.isEmpty) Seq.empty else {
(tfd.params.map(vd => finalSubst(vd.id).toVariable) zip newArgs).map(p => Equals(p._1, p._2))
}
@@ -115,7 +115,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
protected type ChainSignature = (FunDef, Set[RelationSignature])
protected def funDefChainSignature(funDef: FunDef): ChainSignature = {
- funDef -> (self.program.callGraph.transitiveCallees(funDef) + funDef).map(funDefRelationSignature(_))
+ funDef -> (self.program.callGraph.transitiveCallees(funDef) + funDef).map(funDefRelationSignature)
}
private val chainCache : MutableMap[FunDef, (Set[FunDef], Set[Chain], ChainSignature)] = MutableMap.empty
@@ -126,7 +126,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
val relationConstraints : MutableMap[Relation, SizeConstraint] = MutableMap.empty
def decreasing(relations: List[Relation]): Boolean = {
- val constraints = relations.map(relation => relationConstraints.get(relation).getOrElse {
+ val constraints = relations.map(relation => relationConstraints.getOrElse(relation, {
val Relation(funDef, path, FunctionInvocation(fd, args), _) = relation
val (e1, e2) = (tupleWrap(funDef.params.map(_.toVariable)), tupleWrap(args))
val constraint = if (solver.definitiveALL(implies(andJoin(path), self.softDecreasing(e1, e2)))) {
@@ -141,7 +141,7 @@ trait ChainBuilder extends RelationBuilder { self: TerminationChecker with Stren
relationConstraints(relation) = constraint
constraint
- }).toSet
+ })).toSet
!constraints(NoConstraint) && constraints(StrongDecreasing)
}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 58e04d4237fb4387868ca482190f41cde17a7fe9..4a3e8270c4fe5f3d193269d4d09a2388968820ae 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -157,8 +157,8 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
}
def matches(expr: Expr) : NumericEndpoint = expr match {
- case And(es) => es.map(matches(_)).foldLeft[NumericEndpoint](AnyEndpoint)(_ min _)
- case Or(es) => es.map(matches(_)).foldLeft[NumericEndpoint](NoEndpoint)(_ max _)
+ case And(es) => es.map(matches).foldLeft[NumericEndpoint](AnyEndpoint)(_ min _)
+ case Or(es) => es.map(matches).foldLeft[NumericEndpoint](NoEndpoint)(_ max _)
case Not(e) => matches(e).inverse
case GreaterThan(Value(), e) if variablesOf(e).isEmpty => LowerBoundEndpoint
case GreaterThan(e, Value()) if variablesOf(e).isEmpty => UpperBoundEndpoint
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 6570865e95dfbda481d090c8453fad06db95aedf..817aec03d9f819c6fe0d61af9208ef4a98c90383 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -67,7 +67,7 @@ class ChainProcessor(val checker: TerminationChecker with ChainBuilder with Chai
}
if (structuralDecreasing || numericDecreasing) {
- (problem.funDefs.map(Cleared(_)), Nil)
+ (problem.funDefs.map(Cleared), Nil)
} else {
(Nil, List(problem))
}
diff --git a/src/main/scala/leon/termination/ComponentProcessor.scala b/src/main/scala/leon/termination/ComponentProcessor.scala
index 6fd32320cd82a4496b4761a6dc1f81f21abf1908..fb8109fca5123de167e2c85b370ca8bbb9d8dec5 100644
--- a/src/main/scala/leon/termination/ComponentProcessor.scala
+++ b/src/main/scala/leon/termination/ComponentProcessor.scala
@@ -22,14 +22,14 @@ class ComponentProcessor(val checker: TerminationChecker with ComponentBuilder)
val terminationCache : MutableMap[FunDef, Boolean] = MutableMap()
def terminates(fd: FunDef) : Boolean = terminationCache.getOrElse(fd, {
val scc = fdToSCC.getOrElse(fd, Set()) // functions that aren't called and don't call belong to no SCC
- val result = if (scc(fd)) false else scc.forall(terminates(_))
+ val result = if (scc(fd)) false else scc.forall(terminates)
terminationCache(fd) = result
result
})
- val terminating = problem.funDefs.filter(terminates(_))
+ val terminating = problem.funDefs.filter(terminates)
assert(components.forall(scc => (scc subsetOf terminating) || (scc intersect terminating).isEmpty))
- val newProblems = components.filter(scc => (scc intersect terminating).isEmpty).map(Problem(_))
- (terminating.map(Cleared(_)), newProblems)
+ val newProblems = components.filter(scc => (scc intersect terminating).isEmpty).map(Problem)
+ (terminating.map(Cleared), newProblems)
}
}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 4a06f2a7bd10be277dbf2f11750438f08fc369a9..f4fe5c65e9547d7fbc7d654365a7f08c1161eb32 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -70,7 +70,7 @@ trait Solvable extends Processor {
def definitiveALL(problem: Expr): Boolean = {
withoutPosts {
- SimpleSolverAPI(solver).solveSAT(Not(problem))._1.map(!_) getOrElse false
+ SimpleSolverAPI(solver).solveSAT(Not(problem))._1.exists(!_)
}
}
@@ -95,7 +95,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
private val problems : MutableQueue[(Problem,Int)] = MutableQueue((initialProblem, 0))
private var unsolved : Set[Problem] = Set()
- private def printQueue {
+ private def printQueue() {
val sb = new StringBuilder()
sb.append("- Problems in Queue:\n")
for((problem, index) <- problems) {
@@ -137,7 +137,7 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
// }).flatten.toSet(fd)))
def hasNext : Boolean = problems.nonEmpty
- def next : (String, List[Result]) = {
+ def next() : (String, List[Result]) = {
printQueue
val (problem, index) = problems.head
val processor : Processor = processors(index)
@@ -148,15 +148,15 @@ class ProcessingPipeline(program: Program, context: LeonContext, _processors: Pr
// dequeue and enqueue atomically to make sure the queue always
// makes sense (necessary for calls to clear(fd))
- problems.dequeue
+ problems.dequeue()
nextProblems match {
case x :: xs if x == problem =>
assert(xs.isEmpty)
if (index == processors.size - 1) unsolved += x
else problems.enqueue(x -> (index + 1))
case list @ x :: xs =>
- problems.enqueue(list.map(p => (p -> 0)) : _*)
- problems.enqueue(unsolved.map(p => (p -> 0)).toSeq : _*)
+ problems.enqueue(list.map(p => p -> 0) : _*)
+ problems.enqueue(unsolved.map(p => p -> 0).toSeq : _*)
unsolved = Set()
case Nil => // no problem => do nothing!
}
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index a4f871ead9ab465e10e818c6f4d166c6734facd8..33f7c9da0d0aa7df5b36c27ac33dae53c4c5d9f9 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -75,7 +75,7 @@ class RelationProcessor(
assert(terminating ++ nonTerminating == problem.funDefs)
- val results = terminating.map(Cleared(_)).toList
+ val results = terminating.map(Cleared).toList
val newProblems = if ((problem.funDefs intersect nonTerminating).nonEmpty) List(Problem(nonTerminating)) else Nil
(results, newProblems)
}
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index caeb10e36a4a859de35de7524dabc8301b5ede8d..ada2df4a3cddb46e14711f283795bdcde65027f9 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -113,7 +113,7 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
private def isSubTreeOfArg(expr: Expr, args: Set[Identifier]): Boolean = {
@tailrec
def rec(e: Expr, fst: Boolean): Boolean = e match {
- case Variable(id) if (args(id)) => !fst
+ case Variable(id) if args(id) => !fst
case CaseClassSelector(_, cc, _) => rec(cc, false)
case _ => false
}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index b255c58b64aa20623a27b9637b41fc47cdfd596e..206e4ac444927a59b4d368ae7be2e4c3e9b70dde 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -33,7 +33,7 @@ trait StructuralSize {
case Some(fd) => fd
case None =>
val argument = ValDef(FreshIdentifier("x", argumentType, true))
- val formalTParams = typeParams.map(TypeParameterDef(_))
+ val formalTParams = typeParams.map(TypeParameterDef)
val fd = new FunDef(FreshIdentifier("size", alwaysShowUniqueID = true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
@@ -52,20 +52,20 @@ trait StructuralSize {
val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType))
val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
val sizes = arguments.map(id => size(Variable(id)))
- val result = sizes.foldLeft[Expr](InfiniteIntegerLiteral(1))(Plus(_,_))
+ val result = sizes.foldLeft[Expr](InfiniteIntegerLiteral(1))(Plus)
purescala.Extractors.SimpleCase(CaseClassPattern(None, c, argumentPatterns), result)
}
expr.getType match {
case (ct: ClassType) =>
- val fd = funDef(ct, _ match {
+ val fd = funDef(ct, {
case (act: AbstractClassType) => act.knownCCDescendents map caseClassType2MatchCase
case (cct: CaseClassType) => Seq(caseClassType2MatchCase(cct))
})
FunctionInvocation(TypedFunDef(fd, ct.tps), Seq(expr))
case TupleType(argTypes) => argTypes.zipWithIndex.map({
case (_, index) => size(tupleSelect(expr, index + 1, true))
- }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus(_,_))
+ }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
case _ => InfiniteIntegerLiteral(0)
}
}
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index eeba3a0ad0bd3eb2a6444bd7842f065df69c6fae..5f80f57266048b7b188892b13b05bab093352bb4 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -19,7 +19,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
tc.initialize()
val results = visibleFunDefsFromMain(program).toList.sortWith(_.getPos < _.getPos).map { funDef =>
- (funDef -> tc.terminates(funDef))
+ funDef -> tc.terminates(funDef)
}
val endTime = System.currentTimeMillis
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index 12dfa4757747ad793be6ff29d45de389e177e121..5acdef237ae770da8a942b18a9125e94b18b32fc 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -5,7 +5,7 @@ package termination
import purescala.Definitions._
-case class TerminationReport(val results : Seq[(FunDef,TerminationGuarantee)], val time : Double) {
+case class TerminationReport(results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
def summaryString : String = {
val sb = new StringBuilder
sb.append("─────────────────────\n")
diff --git a/src/main/scala/leon/utils/ASCIIHelpers.scala b/src/main/scala/leon/utils/ASCIIHelpers.scala
index cf8f78c3100befda7eaa6043ede9c60858fd8d8a..64ae274d87b066465ec67b0789be32777ed43a56 100644
--- a/src/main/scala/leon/utils/ASCIIHelpers.scala
+++ b/src/main/scala/leon/utils/ASCIIHelpers.scala
@@ -129,7 +129,7 @@ object ASCIIHelpers {
def line(str: String, sep: String, width: Int = 80): String = {
val middle = " "+str+" "
- val remSize = (width-middle.length)
+ val remSize = width - middle.length
sep*math.floor(remSize/2).toInt+middle+sep*math.ceil(remSize/2).toInt
}
diff --git a/src/main/scala/leon/utils/GraphOps.scala b/src/main/scala/leon/utils/GraphOps.scala
index 33fcb73f20d9045471783e096fcef7b303d8faa5..f7ad5646ac96ed11798a28366da7f8eee45cf590 100644
--- a/src/main/scala/leon/utils/GraphOps.scala
+++ b/src/main/scala/leon/utils/GraphOps.scala
@@ -27,7 +27,7 @@ object GraphOps {
def transitiveClosure[A](graph: Map[A,Set[A]]) : Map[A,Set[A]] = {
def step(graph : Map[A, Set[A]]) : Map[A,Set[A]] = graph map {
case (k, vs) => (k, vs ++ (vs flatMap { v =>
- graph.get(v).getOrElse(Set())
+ graph.getOrElse(v, Set())
}))
}
leon.purescala.TreeOps.fixpoint(step, -1)(graph)
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index b5bb18977ae464639511559ce317abaf417260f3..0f6a75fed63e25617dc40f29c76ea25d75b424d0 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -149,8 +149,8 @@ object Graphs {
def union(that: This): This = copy(
vertices = this.V ++ that.V,
edges = this.E ++ that.E,
- ins = ((this.ins.keySet ++ that.ins.keySet) map { k => (k -> (this.ins(k) ++ that.ins(k))) }).toMap.withDefaultValue(Set()),
- outs = ((this.outs.keySet ++ that.outs.keySet) map { k => (k -> (this.outs(k) ++ that.outs(k))) }).toMap.withDefaultValue(Set())
+ ins = ((this.ins.keySet ++ that.ins.keySet) map { k => k -> (this.ins(k) ++ that.ins(k)) }).toMap.withDefaultValue(Set()),
+ outs = ((this.outs.keySet ++ that.outs.keySet) map { k => k -> (this.outs(k) ++ that.outs(k)) }).toMap.withDefaultValue(Set())
)
def stronglyConnectedComponents: Seq[Set[Vertex]] = ???
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index e4aa86b3a35a8836a0d9a5cf5ca00a9cdc622c43..753edf9a944c793e4f876002a2e6d1c8d6b28421 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -17,7 +17,7 @@ class InterruptManager(reporter: Reporter) extends Interruptible {
val interrupted: AtomicBoolean = new AtomicBoolean(false)
@inline
- def isInterrupted() = interrupted.get()
+ def isInterrupted = interrupted.get()
def interrupt() = synchronized {
if (!interrupted.get()) {
diff --git a/src/main/scala/leon/utils/SCC.scala b/src/main/scala/leon/utils/SCC.scala
index f82b6262ea8785f828306adcba82afae3e3b720d..109137a0c2f08886d5536e9182b6522a6dbdf6d9 100644
--- a/src/main/scala/leon/utils/SCC.scala
+++ b/src/main/scala/leon/utils/SCC.scala
@@ -38,8 +38,8 @@ object SCC {
val x :: xs = s
c = c + x
s = xs
- stop = (x == v)
- } while(!stop);
+ stop = x == v
+ } while(!stop)
components = c :: components
}
}
diff --git a/src/main/scala/leon/utils/SeqUtils.scala b/src/main/scala/leon/utils/SeqUtils.scala
index c3b17b82b15277366acd2ff62a11e0895350af09..47a6e678da6383549e1d5c6410aa82bb8b3d00e7 100644
--- a/src/main/scala/leon/utils/SeqUtils.scala
+++ b/src/main/scala/leon/utils/SeqUtils.scala
@@ -12,13 +12,13 @@ object SeqUtils {
val max = sizes.product
val result = new ArrayBuffer[Tuple[T]](max)
- var i = 0;
-
+ var i = 0
+
while (i < max) {
- var c = i;
- var sel = -1;
+ var c = i
+ var sel = -1
val elem = for (s <- sizes) yield {
- val index = c % s;
+ val index = c % s
c = c / s
sel += 1
seqs(sel)(index)
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 1659f481168941cef3d55fc13f7cebf8687741da..86d71130396bdd4297c033c0b8e10314f5c94bea 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -15,11 +15,11 @@ object Simplifiers {
val simplifiers = List[Expr => Expr](
simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
+ simplifyLets,
simplifyPaths(uninterpretedZ3)(_),
- simplifyArithmetic _,
+ simplifyArithmetic,
evalGround(ctx, p),
- normalizeExpression _
+ normalizeExpression
)
val simple = { expr: Expr =>
@@ -40,9 +40,9 @@ object Simplifiers {
val simplifiers = List[Expr => Expr](
simplifyTautologies(uninterpretedZ3)(_),
- simplifyArithmetic _,
+ simplifyArithmetic,
evalGround(ctx, p),
- normalizeExpression _
+ normalizeExpression
)
val simple = { expr: Expr =>
diff --git a/src/main/scala/leon/utils/StreamUtils.scala b/src/main/scala/leon/utils/StreamUtils.scala
index 3af285528e0243cb6858336e3048a48e6c5cf98f..8e1caa684f7516faca0fa16d1a541725bd09aa2b 100644
--- a/src/main/scala/leon/utils/StreamUtils.scala
+++ b/src/main/scala/leon/utils/StreamUtils.scala
@@ -5,7 +5,7 @@ package leon.utils
object StreamUtils {
def interleave[T](streams : Seq[Stream[T]]) : Stream[T] = {
var ss = streams
- while(!ss.isEmpty && ss.head.isEmpty) {
+ while(ss.nonEmpty && ss.head.isEmpty) {
ss = ss.tail
}
if(ss.isEmpty) return Stream.empty
@@ -54,13 +54,13 @@ object StreamUtils {
while(continue && d < dimensions) {
var i = is.head
- if(bounds(d).map(i > _).getOrElse(false)) {
+ if(bounds(d).exists(i > _)) {
continue = false
} else try {
// TODO can we speed up by caching the random access into
// the stream in an indexedSeq? After all, `i` increases
// slowly.
- tuple = (ss.head)(i) :: tuple
+ tuple = ss.head(i) :: tuple
is = is.tail
ss = ss.tail
d += 1
diff --git a/src/main/scala/leon/utils/TemporaryInputPhase.scala b/src/main/scala/leon/utils/TemporaryInputPhase.scala
index b5c5f18b1561d016918343ffab22da5221ec4fe4..eed93a673a6a45e0df7edfc80b58221d8c3b24f6 100644
--- a/src/main/scala/leon/utils/TemporaryInputPhase.scala
+++ b/src/main/scala/leon/utils/TemporaryInputPhase.scala
@@ -14,12 +14,12 @@ object TemporaryInputPhase extends LeonPhase[(String, List[String]), List[String
val (content, opts) = data
val file : File = File.createTempFile("leon", ".scala")
- file.deleteOnExit
+ file.deleteOnExit()
val out = new BufferedWriter(new FileWriter(file))
out.write(content)
- out.close
+ out.close()
- (file.getAbsolutePath() :: opts)
+ file.getAbsolutePath :: opts
}
}
diff --git a/src/main/scala/leon/utils/TimeoutFor.scala b/src/main/scala/leon/utils/TimeoutFor.scala
index a92f011a9809497a6b322e7e2ca3e496054d3d04..fad71ac27e54e5f29cf29c1d3d6873273c65caf9 100644
--- a/src/main/scala/leon/utils/TimeoutFor.scala
+++ b/src/main/scala/leon/utils/TimeoutFor.scala
@@ -4,7 +4,7 @@ package utils
class TimeoutFor(it: Interruptible) {
private class Countdown(timeout: Long, onTimeout: => Unit) extends Thread {
private var keepRunning = true
- override def run : Unit = {
+ override def run() : Unit = {
val startTime : Long = System.currentTimeMillis
var exceeded : Boolean = false
@@ -20,7 +20,7 @@ class TimeoutFor(it: Interruptible) {
}
}
- def finishedRunning : Unit = {
+ def finishedRunning() : Unit = {
keepRunning = false
}
}
@@ -33,7 +33,7 @@ class TimeoutFor(it: Interruptible) {
reachedTimeout = true
})
- timer.start
+ timer.start()
val res = body
timer.finishedRunning
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index b2c8b38222836b8c05c4d3e88d4956c3f539fc1c..cc8b07a41108168483326871e13cc6b2caee2af1 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -86,7 +86,7 @@ class TimerStorage extends Dynamic {
}
def timed[T](b: => T): T = {
- start
+ start()
val res = b
stop
res
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index c853744008b2c0596046acef2f9f292afd52d753..e5672bd5128f8fabc7f64b4f04038ff78b39f307 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -70,7 +70,7 @@ object UnitElimination extends TransformationPhase {
val TupleType(tpes) = t.getType
val simpleTypes = tpes map simplifyType
val newArity = tpes.count(_ != UnitType)
- val newIndex = simpleTypes.take(index).filter(_ != UnitType).size
+ val newIndex = simpleTypes.take(index).count(_ != UnitType)
tupleSelect(removeUnit(t), newIndex, newArity)
}
case Let(id, e, b) => {
@@ -78,7 +78,7 @@ object UnitElimination extends TransformationPhase {
removeUnit(b)
else {
id.getType match {
- case TupleType(tpes) if tpes.exists(_ == UnitType) => {
+ case TupleType(tpes) if tpes.contains(UnitType) => {
val newTupleType = tupleTypeWrap(tpes.filterNot(_ == UnitType))
val freshId = FreshIdentifier(id.name, newTupleType)
id2FreshId += (id -> freshId)
@@ -120,7 +120,7 @@ object UnitElimination extends TransformationPhase {
IfExpr(removeUnit(cond), thenRec, elseRec)
}
case n @ NAryOperator(args, recons) => {
- recons(args.map(removeUnit(_)))
+ recons(args.map(removeUnit))
}
case b @ BinaryOperator(a1, a2, recons) => {
recons(removeUnit(a1), removeUnit(a2))
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 57482f7a8c7d6a0e191fcfceaf234801fb5d736e..4d590e40aab5e6acb0b61e124710d4d902d2fe2e 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -48,7 +48,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
filterInclusive(filterFuns.map(fdMatcher), Some(excludeByDefault _))
}
- val toVerify = program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter)
+ val toVerify = program.definedFunctions.toList.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
for(funDef <- toVerify) {
if (excludeByDefault(funDef)) {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index e2c3af95ffdd738ce7e00d0bb26cac79784590a0..474d7a2b9d26527b44b865c27330ba085040633c 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -85,16 +85,16 @@ 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 scope = (body: Expr) => {
val tupleId = FreshIdentifier("t", iteType)
- cScope( Let(tupleId, iteExpr, Let(
- resId,
+ cScope(Let(tupleId, iteExpr, Let(
+ resId,
tupleSelect(tupleId.toVariable, 1, modifiedVars.nonEmpty),
- freshIds.zipWithIndex.foldLeft(body)((b, id) =>
+ freshIds.zipWithIndex.foldLeft(body)((b, id) =>
Let(id._1, tupleSelect(tupleId.toVariable, id._2 + 2, true), b)
))
).copiedFrom(expr))
- })
+ }
(resId.toVariable, scope, cFun ++ modifiedVars.zip(freshIds).toMap)
}
@@ -123,18 +123,18 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
case (mc @ MatchCase(pat, guard, _), newRhs) => MatchCase(pat, guard map { replaceNames(scrutFun, _)}, newRhs).setPos(mc)
}).setPos(m)
- val scope = ((body: Expr) => {
+ val scope = (body: Expr) => {
val tupleId = FreshIdentifier("t", matchType)
scrutScope(
- Let(tupleId, matchE,
+ Let(tupleId, matchE,
Let(resId, tupleSelect(tupleId.toVariable, 1, freshIds.nonEmpty),
- freshIds.zipWithIndex.foldLeft(body)((b, id) =>
+ freshIds.zipWithIndex.foldLeft(body)((b, id) =>
Let(id._1, tupleSelect(tupleId.toVariable, id._2 + 2, true), b)
)
)
)
)
- })
+ }
(resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
}
@@ -159,7 +159,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val whileFunRecursiveCall = replaceNames(condFun,
bodyScope(FunctionInvocation(whileFunDef.typed, modifiedVars.map(id => condBodyFun(id).toVariable)).setPos(wh)))
val whileFunBaseCase =
- tupleWrap(modifiedVars.map(id => condFun.get(id).getOrElse(modifiedVars2WhileFunVars(id)).toVariable))
+ tupleWrap(modifiedVars.map(id => condFun.getOrElse(id, modifiedVars2WhileFunVars(id)).toVariable))
val whileFunBody = replaceNames(modifiedVars2WhileFunVars,
condScope(IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase)))
whileFunDef.body = Some(whileFunBody)
@@ -174,7 +174,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
//the mapping of the trivial post condition variables depends on whether the condition has had some side effect
val trivialPostcondition: Option[Expr] = Some(Not(replace(
- modifiedVars.map(id => (condFun.get(id).getOrElse(id).toVariable, modifiedVars2ResultVars(id.toVariable))).toMap,
+ modifiedVars.map(id => (condFun.getOrElse(id, id).toVariable, modifiedVars2ResultVars(id.toVariable))).toMap,
whileFunCond)))
val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replaceNames(modifiedVars2WhileFunVars, expr))
val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
@@ -186,16 +186,16 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
})))
val finalVars = modifiedVars.map(_.freshen)
- val finalScope = ((body: Expr) => {
+ val finalScope = (body: Expr) => {
val tupleId = FreshIdentifier("t", whileFunReturnType)
- LetDef( whileFunDef, Let(
- tupleId,
- FunctionInvocation(whileFunDef.typed, modifiedVars.map(_.toVariable)).setPos(wh),
- finalVars.zipWithIndex.foldLeft(body){(b, id) =>
+ LetDef(whileFunDef, Let(
+ tupleId,
+ FunctionInvocation(whileFunDef.typed, modifiedVars.map(_.toVariable)).setPos(wh),
+ finalVars.zipWithIndex.foldLeft(body) { (b, id) =>
Let(id._1, tupleSelect(tupleId.toVariable, id._2 + 1, finalVars.size), b)
}
))
- })
+ }
(UnitLiteral(), finalScope, modifiedVars.zip(finalVars).toMap)
}
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index ff8e5a34cba848fcc1c1cbe8c4e1f13973d2bbf8..400716980b850f29252435bf6e213643072c72da 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -55,7 +55,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
- completeVerificationReport(vr, functionWasLoop _)
+ completeVerificationReport(vr, functionWasLoop)
}
def completeVerificationReport(vr: VerificationReport, functionWasLoop: FunDef => Boolean): VerificationReport = {
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index d3e5321e58f9c3b91c51a4592af7e0553800e0ce..a5c94e9ab4bea038e51b8fe3e3d131263325ed2d 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -3,7 +3,7 @@
package leon.test
import leon._
-import leon.{LeonContext,Settings}
+import leon.LeonContext
import leon.utils._
import scala.io.Source
@@ -16,8 +16,8 @@ import java.io.File
trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
// Hard-code resource directory, for Eclipse purposes
- val resourceDirHard = "src/test/resources/regression/"
-
+ val resourceDirHard = "src/test/resources/"
+
def now() = {
System.currentTimeMillis
}
@@ -32,7 +32,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
true
} else {
val msd = ms.toDouble
- (msd < avg + 3*stddev + 20)
+ msd < avg + 3*stddev + 20
}
}
@@ -62,7 +62,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
def bookKeepingFile(id: String) = {
import java.io.File
- val f = new File(System.getProperty("user.dir")+"/.test-history/"+id+".log");
+ val f = new File(System.getProperty("user.dir")+"/.test-history/"+id+".log")
f.getParentFile.mkdirs()
@@ -72,8 +72,8 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
def getStats(id: String): Statistics = {
val f = bookKeepingFile(id)
- if (f.canRead()) {
- Statistics(Source.fromFile(f).getLines.flatMap{ line =>
+ if (f.canRead) {
+ Statistics(Source.fromFile(f).getLines().flatMap{ line =>
val l = line.trim
if (l.length > 0) {
Some(line.toLong)
@@ -93,7 +93,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
val fw = new FileWriter(f, true)
fw.write(stats.values.head+"\n")
- fw.close
+ fw.close()
}
override implicit val defaultInterruptor = new Interruptor {
@@ -137,7 +137,6 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
def resourceDir(dir : String) : File = {
- import scala.collection.JavaConversions._
val d = this.getClass.getClassLoader.getResource(dir)
@@ -146,7 +145,7 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
new File(resourceDirHard + dir)
}
else {
- new File(d.toURI())
+ new File(d.toURI)
}
}
@@ -154,15 +153,14 @@ trait LeonTestSuite extends FunSuite with Timeouts with BeforeAndAfterEach {
def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {
- import scala.collection.JavaConversions._
val d = this.getClass.getClassLoader.getResource(dir)
val asFile = if(d == null || d.getProtocol != "file") {
// We are in Eclipse. The only way we are saved is by hard-coding the path
new File(resourceDirHard + dir)
- } else new File(d.toURI())
+ } else new File(d.toURI)
- asFile.listFiles().filter(f => filter(f.getPath()))
+ asFile.listFiles().filter(f => filter(f.getPath))
}
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 22cbcf472b40b8eefd9a118df3070c9144ab6c78..b0ea6159d9160f118fa55002b18c9c7593aaf993 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -85,10 +85,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
def asIntSet(e : Expr) : Option[Set[Int]] = e match {
case FiniteSet(es) =>
- val ois = es.map(_ match {
+ val ois = es.map {
case IntLiteral(v) => Some(v)
case _ => None
- })
+ }
if(ois.forall(_.isDefined))
Some(ois.map(_.get).toSet)
else
@@ -110,10 +110,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
def asIntMap(e : Expr) : Option[Map[Int,Int]] = e match {
case FiniteMap(ss) =>
- val oips : Seq[Option[(Int,Int)]] = ss.map(_ match {
- case (IntLiteral(f),IntLiteral(t)) => Some(f -> t)
+ val oips : Seq[Option[(Int,Int)]] = ss.map {
+ case (IntLiteral(f), IntLiteral(t)) => Some(f -> t)
case _ => None
- })
+ }
if(oips.forall(_.isDefined))
Some(oips.map(_.get).toMap)
else
diff --git a/src/test/scala/leon/test/frontends/FrontEndsTest.scala b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
index 90335806c2eb597b31becd36e78d609267a49373..5a4d74f475e23ac36b63f88e4d28efcee8851c29 100644
--- a/src/test/scala/leon/test/frontends/FrontEndsTest.scala
+++ b/src/test/scala/leon/test/frontends/FrontEndsTest.scala
@@ -18,10 +18,10 @@ class FrontEndsTest extends LeonTestSuite {
val ctx = createLeonContext()
if (forError) {
intercept[LeonFatalError]{
- pipeline.run(ctx)(List(f.getAbsolutePath()))
+ pipeline.run(ctx)(List(f.getAbsolutePath))
}
} else {
- pipeline.run(ctx)(List(f.getAbsolutePath()))
+ pipeline.run(ctx)(List(f.getAbsolutePath))
}
}
diff --git a/src/test/scala/leon/test/frontends/Imports.scala b/src/test/scala/leon/test/frontends/ImportsTests.scala
similarity index 100%
rename from src/test/scala/leon/test/frontends/Imports.scala
rename to src/test/scala/leon/test/frontends/ImportsTests.scala
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 90657a52d5a6c0467392126ffbce6de92ba838e6..61a7bbe9aa4d54c328aa93256403aa8aa6532420 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -34,8 +34,8 @@ class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
)
}
- def toSum(es: Seq[Expr]) = es.reduceLeft(Plus(_, _))
- def coefToSum(es: Array[Expr], vs: Array[Expr]) = (es.zip(Array[Expr](InfiniteIntegerLiteral(1)) ++ vs)).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
+ def toSum(es: Seq[Expr]) = es.reduceLeft(Plus)
+ def coefToSum(es: Array[Expr], vs: Array[Expr]) = es.zip(Array[Expr](InfiniteIntegerLiteral(1)) ++ vs).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
test("checkSameExpr") {
checkSameExpr(Plus(x, y), Plus(y, x), xs)
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/WithLikelyEq.scala
similarity index 100%
rename from src/test/scala/leon/test/purescala/LikelyEq.scala
rename to src/test/scala/leon/test/purescala/WithLikelyEq.scala
diff --git a/src/test/scala/leon/test/repair/RepairSuite.scala b/src/test/scala/leon/test/repair/RepairSuite.scala
index e34c9fb1d1fa4ddd9cfa149943f497dfe74abf17..fecf891b84209b8e9a0300775ce4720baedaf0e7 100644
--- a/src/test/scala/leon/test/repair/RepairSuite.scala
+++ b/src/test/scala/leon/test/repair/RepairSuite.scala
@@ -20,8 +20,8 @@ class RepairSuite extends LeonTestSuite {
)
for (file <- filesInResourceDir("regression/repair/")) {
- val path = file.getAbsoluteFile().toString
- val name = file.getName()
+ val path = file.getAbsoluteFile.toString
+ val name = file.getName
val reporter = new TestSilentReporter
diff --git a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
index a2f4b488590d2b9e2a3265bfc8ae4dbf642bfe95..f784faea2fc5d90dcd47775e0e933c20827b3bbd 100644
--- a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
@@ -14,7 +14,7 @@ import leon.purescala.TypeTrees._
class EnumerationSolverTests extends LeonTestSuite {
private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
- val s = sf.getNewSolver
+ val s = sf.getNewSolver()
s.assertCnstr(e)
s.check
}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 54740f920a651ddf2c07b7bad0f5325bb480295a..e5816f5b13cd8d6d0bd9df1d4d4fce1a97daa1c1 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -18,7 +18,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
testCounter += 1
test("Solver test #" + testCounter) {
- val sub = solver.getNewSolver
+ val sub = solver.getNewSolver()
try {
sub.assertCnstr(Not(expr))
@@ -105,7 +105,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
}
locally {
- val sub = solver.getNewSolver
+ val sub = solver.getNewSolver()
try {
sub.assertCnstr(f)
val result = sub.checkAssumptions(Set(b1))
@@ -118,7 +118,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
}
locally {
- val sub = solver.getNewSolver
+ val sub = solver.getNewSolver()
try {
sub.assertCnstr(f)
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 8ac0bdc3d40de48feb4a76e89ee3b6a0d45a0835..dfa2b2ac77f4ff156ce1f8b427c4f96446e18588 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -30,7 +30,7 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
val bId = FreshIdentifier("b", IntegerType)
val b = Variable(bId)
- def toSum(es: Seq[Expr]) = es.reduceLeft(Plus(_, _))
+ def toSum(es: Seq[Expr]) = es.reduceLeft(Plus)
def checkSameExpr(e1: Expr, e2: Expr, vs: Set[Identifier], prec: Expr, defaultMap: Map[Identifier, Expr] = Map()) {
assert( //this outer assert should not be needed because of the nested one
@@ -226,7 +226,7 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def check(t: Expr, c: List[Expr], prec: Expr, witnesses: List[Expr], freshVars: List[Identifier]) {
enumerate(freshVars.size, (vals: Array[Int]) => {
- val mapping: Map[Expr, Expr] = (freshVars.zip(vals.toList).map(t => (Variable(t._1), i(t._2))).toMap)
+ val mapping: Map[Expr, Expr] = freshVars.zip(vals.toList).map(t => (Variable(t._1), i(t._2))).toMap
val cWithVars: Expr = c.zip(witnesses).foldLeft[Expr](i(0)){ case (acc, (coef, wit)) => Plus(acc, Times(coef, replace(mapping, wit))) }
checkSameExpr(Plus(t, cWithVars), i(0), as, prec)
})
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index a933080a960196ed98c3e34a8362c1772eb86f44..1a2f205d381ed1eac9d4d51fa1d623dec73c693e 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -6,21 +6,16 @@ package synthesis
import leon._
import leon.purescala.Definitions._
-import leon.purescala.Common._
-import leon.purescala.Trees._
import leon.purescala.ScalaPrinter
import leon.purescala.PrinterContext
import leon.purescala.PrinterOptions
-import leon.purescala.TreeOps._
-import leon.solvers.z3._
-import leon.solvers.Solver
import leon.synthesis._
-import leon.synthesis.utils._
+import scala.collection.mutable
import scala.collection.mutable.Stack
import scala.io.Source
-import java.io.{File, BufferedWriter, FileWriter}
+import java.io.File
class StablePrintingSuite extends LeonTestSuite {
private def forEachFileIn(path : String)(block : File => Unit) {
@@ -50,7 +45,7 @@ class StablePrintingSuite extends LeonTestSuite {
def info(task: String): String = {
val r = if (rules.isEmpty) "<init>" else "after "+rules.head
- val indent = " "*(rules.size)+" "
+ val indent = " "* rules.size +" "
f"${indent+r}%-40s [$task%s]"
}
@@ -62,7 +57,7 @@ class StablePrintingSuite extends LeonTestSuite {
val workList = Stack[Job](Job(res, Set(), Nil))
- while(!workList.isEmpty) {
+ while(workList.nonEmpty) {
val reporter = new TestSilentReporter
val ctx = createLeonContext("--synthesis").copy(reporter = reporter)
val j = workList.pop()
@@ -86,7 +81,7 @@ class StablePrintingSuite extends LeonTestSuite {
for ((ci, i) <- chooses.zipWithIndex if j.choosesToProcess(i) || j.choosesToProcess.isEmpty) {
val synthesizer = new Synthesizer(ctx, pgm, ci, opts)
val sctx = SynthesisContext.fromSynthesizer(synthesizer)
- val search = synthesizer.getSearch()
+ val search = synthesizer.getSearch
val hctx = SearchContext(sctx, ci, search.g.root, search)
val problem = ci.problem
info(j.info("synthesis "+problem))
@@ -96,7 +91,7 @@ class StablePrintingSuite extends LeonTestSuite {
a.apply(hctx) match {
case RuleClosed(sols) =>
case RuleExpanded(sub) =>
- a.onSuccess(sub.map(Solution.choose(_))) match {
+ a.onSuccess(sub.map(Solution.choose)) match {
case Some(sol) =>
val result = sol.toSimplifiedExpr(ctx, pgm)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 9ad67c8a03240cded8e0843370dca3743c85e44b..16091cd8eb7cf881aec2db865f60e2519fd0632e 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -30,7 +30,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
var ctx: LeonContext = null
var opts: SynthesisSettings = null
- test(cat+": "+f.getName()+" Compilation") {
+ test(cat+": "+f.getName+" Compilation") {
ctx = createLeonContext("--synthesis")
opts = SynthesisSettings(searchBound = Some(bound), allSeeing = true)
@@ -43,7 +43,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
}
for (ci <- chooses) {
- test(cat+": "+f.getName()+" - "+ci.fd.id.name) {
+ test(cat+": "+f.getName+" - "+ci.fd.id.name) {
val synthesizer = new Synthesizer(ctx, program, ci, opts)
val (search, sols) = synthesizer.synthesize()
if (sols.isEmpty) {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 30fc1a4d7336d881859b2af6e5e0e0283d2d1bc2..9f3a3aa5d2e5dd54b60940ec1448d77cd581c4cb 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -3,20 +3,11 @@
package leon.test.synthesis
import leon.test._
import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.solvers.z3._
-import leon.solvers.Solver
import leon.synthesis._
import leon.synthesis.graph._
import leon.synthesis.utils._
import leon.utils.PreprocessingPhase
-import org.scalatest.matchers.ShouldMatchers._
-
-import java.io.{BufferedWriter, FileWriter, File}
-
class SynthesisSuite extends LeonTestSuite {
private var counter : Int = 0
private def nextInt() : Int = {
@@ -24,9 +15,11 @@ class SynthesisSuite extends LeonTestSuite {
counter
}
- abstract class SynStrat(val ruleName: String);
- case class Decomp(n: String, sub: Seq[SynStrat]) extends SynStrat(n);
- case class Close(n: String) extends SynStrat(n);
+ abstract class SynStrat(val ruleName: String)
+
+ case class Decomp(n: String, sub: Seq[SynStrat]) extends SynStrat(n)
+
+ case class Close(n: String) extends SynStrat(n)
class TestSearch(ctx: LeonContext,
@@ -81,7 +74,7 @@ class SynthesisSuite extends LeonTestSuite {
}
def matchingDesc(app: RuleInstantiation, n: String): Boolean = {
- import java.util.regex.Pattern;
+ import java.util.regex.Pattern
val pattern = Pattern.quote(n).replace("*", "\\E.*\\Q")
app.toString.matches(pattern)
}
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index 085727de4f1a20aa22669a3a51710057d82f05bf..e75af01ef08dc726897be657786f9bdbed8d2b65 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -23,12 +23,12 @@ class Streams extends LeonTestSuite {
val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
FreshIdentifier("B", alwaysShowUniqueID = true) #::
FreshIdentifier("B", alwaysShowUniqueID = true) #::
- FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
+ 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;
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
val ss = cartesianProduct(List(s1, s2))
@@ -41,12 +41,12 @@ class Streams extends LeonTestSuite {
val s1 = FreshIdentifier("B", alwaysShowUniqueID = true) #::
FreshIdentifier("B", alwaysShowUniqueID = true) #::
FreshIdentifier("B", alwaysShowUniqueID = true) #::
- FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty;
+ 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;
+ FreshIdentifier("B", alwaysShowUniqueID = true) #:: Stream.empty
val tmp1 = s1.mkString
val tmp2 = s2.mkString
@@ -61,12 +61,12 @@ class Streams extends LeonTestSuite {
val s1 = 1 #::
2 #::
3 #::
- 4 #:: Stream.empty;
+ 4 #:: Stream.empty
val s2 = 5 #::
6 #::
7 #::
- 8 #:: Stream.empty;
+ 8 #:: Stream.empty
val tmp1 = s1.mkString
val tmp2 = s2.mkString
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
index 700c1b193d77e15ab531ea0dde04d86a8069d5cd..b945059b8a20ffa470259a35e50cd8516e4d23ac 100644
--- a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -22,6 +22,6 @@ class LibraryVerificationRegression extends LeonTestSuite {
val report = pipeline.run(ctx)(Nil)
- assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions);
+ assert(report.totalConditions === report.totalValid, "Only "+report.totalValid+" valid out of "+report.totalConditions)
}
}
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 83e89516991052b4d83103461941631fe6d74065..c315794aa9a9239d131562e9710a983512eae078 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -28,7 +28,7 @@ class XLangVerificationRegression extends LeonTestSuite {
XLangAnalysisPhase
private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
- val fullName = file.getPath()
+ val fullName = file.getPath
val start = fullName.indexOf("regression")
val displayName = if(start != -1) {