diff --git a/src/main/scala/leon/invariant/datastructure/DisjointSet.scala b/src/main/scala/leon/invariant/datastructure/DisjointSets.scala
similarity index 94%
rename from src/main/scala/leon/invariant/datastructure/DisjointSet.scala
rename to src/main/scala/leon/invariant/datastructure/DisjointSets.scala
index 4cab7291bfa58dd3d79993233251d7dd589e0019..003bb31d1233ce7ab3ad1fe0dbe775008ae7f806 100644
--- a/src/main/scala/leon/invariant/datastructure/DisjointSet.scala
+++ b/src/main/scala/leon/invariant/datastructure/DisjointSets.scala
@@ -1,8 +1,6 @@
package leon
package invariant.datastructure
-import scala.collection.mutable.{ Map => MutableMap }
-import scala.annotation.migration
import scala.collection.mutable.{Map => MutableMap}
class DisjointSets[T] {
diff --git a/src/main/scala/leon/invariant/datastructure/Graph.scala b/src/main/scala/leon/invariant/datastructure/Graph.scala
index 484f04668c08a6b02f8acfd2db12b343e4b4c303..7262b4b4ef4932a89f76406ed49e4d5e00ee9be1 100644
--- a/src/main/scala/leon/invariant/datastructure/Graph.scala
+++ b/src/main/scala/leon/invariant/datastructure/Graph.scala
@@ -66,7 +66,7 @@ class DirectedGraph[T] {
}
})
}
- if (!queue.isEmpty) {
+ if (queue.nonEmpty) {
val (head :: tail) = queue
queue = tail
BFSReachRecur(head)
diff --git a/src/main/scala/leon/invariant/datastructure/Maps.scala b/src/main/scala/leon/invariant/datastructure/Maps.scala
index 777a79375d874588f3be108d702aa6dc8118df79..ca2dcb98e99f247651dfd1b8632c570630fce7f0 100644
--- a/src/main/scala/leon/invariant/datastructure/Maps.scala
+++ b/src/main/scala/leon/invariant/datastructure/Maps.scala
@@ -1,13 +1,6 @@
package leon
-package invariant.util
+package invariant.datastructure
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
import scala.annotation.tailrec
class MultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.Set[B]] with scala.collection.mutable.MultiMap[A, B] {
diff --git a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
similarity index 92%
rename from src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
rename to src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
index 647616fce1bab0eb01182ad50d75c060ce4ff737..7a9605c922e21373abb6df06fe9d585a104da2ba 100644
--- a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala
@@ -1,16 +1,13 @@
package leon
package invariant.engine
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import invariant.templateSolvers._
import transformations._
import invariant.structure.FunctionUtils._
-import transformations.InstUtil._
import leon.invariant.structure.Formula
import leon.invariant.structure.Call
import leon.invariant.util._
@@ -20,7 +17,6 @@ import leon.solvers.Model
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd: FunDef)
extends FunctionTemplateSolver {
@@ -183,23 +179,21 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd:
var timeTmpl: Option[Expr] = None
var recTmpl: Option[Expr] = None
var othersTmpls: Seq[Expr] = Seq[Expr]()
- tmplConjuncts.foreach(conj => {
- conj match {
- case Operator(Seq(lhs, _), _) if (tupleSelectToInst.contains(lhs)) =>
- tupleSelectToInst(lhs) match {
- case n if n == TPR.name =>
- tprTmpl = Some(conj)
- case n if n == Time.name =>
- timeTmpl = Some(conj)
- case n if n == Rec.name =>
- recTmpl = Some(conj)
- case _ =>
- othersTmpls = othersTmpls :+ conj
- }
- case _ =>
- othersTmpls = othersTmpls :+ conj
- }
- })
+ tmplConjuncts.foreach {
+ case conj@Operator(Seq(lhs, _), _) if (tupleSelectToInst.contains(lhs)) =>
+ tupleSelectToInst(lhs) match {
+ case n if n == TPR.name =>
+ tprTmpl = Some(conj)
+ case n if n == Time.name =>
+ timeTmpl = Some(conj)
+ case n if n == Rec.name =>
+ recTmpl = Some(conj)
+ case _ =>
+ othersTmpls = othersTmpls :+ conj
+ }
+ case conj =>
+ othersTmpls = othersTmpls :+ conj
+ }
(tprTmpl, recTmpl, timeTmpl, othersTmpls)
}
}
diff --git a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
index 3058a267eceef7c5ec1aa537c4766bee15a93204..95927a66ad3bda803a329b61e284f854a94bfcb4 100644
--- a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
+++ b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
@@ -1,19 +1,8 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import evaluators._
-import java.io._
-
-import invariant.factories._
-import invariant.util._
import invariant.structure._
class ConstraintTracker(ctx : InferenceContext, program: Program, rootFun : FunDef/*, temFactory: TemplateFactory*/) {
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index e79926e62158a095b755b48db43c8f3e46c41590..3ef178a03095a74dc8233dfd1ec3739abbdb3cef 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -1,21 +1,7 @@
package leon
package invariant.engine
-import purescala.Common._
import purescala.Definitions._
-import purescala.ExprOps._
-import purescala.Expressions._
-import purescala.Extractors._
-import purescala.Types._
-import verification.VerificationReport
-import invariant.templateSolvers._
-import invariant.factories._
-import invariant.util._
-import invariant.structure.FunctionUtils._
-import invariant.structure._
-import transformations._
-import leon.purescala.ScalaPrinter
-import leon.purescala.PrettyPrinter
/**
* @author ravi
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index b735cb8de7101f3bf109c6318cc7a05c571ba4b7..a6cdc317d1fcd17aba9abaa5199975e664ada9bf 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -12,7 +12,6 @@ import invariant.util._
import verification._
import verification.VCKinds
import InferInvariantsPhase._
-import Util._
import ProgramUtil._
/**
@@ -71,13 +70,13 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
instrumentedProg.definedFunctions.foreach((fd) => {
if (!foundStrongest && fd.hasPostcondition) {
val cond = fd.postcondition.get
- postTraversal((e) => e match {
+ postTraversal {
case Equals(_, _) => {
rel = Equals.apply _
foundStrongest = true
}
case _ => ;
- })(cond)
+ }(cond)
}
})
rel
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index 85491acf1924560e5fe020a38176b513da989690..6ca6ef6327d00465bbbe5141bd69b6ce1e6338a6 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -1,31 +1,18 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala.Common._
import purescala.Definitions._
-import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import solvers._
import java.io._
-import verification.VerificationReport
import verification.VC
import scala.util.control.Breaks._
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.util.Util._
-import invariant.structure._
import invariant.structure.FunctionUtils._
-import leon.invariant.factories.TemplateFactory
import transformations._
import leon.utils._
import Util._
-import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
/**
* @author ravi
@@ -85,13 +72,13 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
} else {
var remFuncs = functionsToAnalyze
var b = 200
- var maxCegisBound = 200
+ val maxCegisBound = 200
breakable {
while (b <= maxCegisBound) {
Stats.updateCumStats(1, "CegisBoundsTried")
val succeededFuncs = analyseProgram(program, remFuncs, progressCallback)
remFuncs = remFuncs.filterNot(succeededFuncs.contains _)
- if (remFuncs.isEmpty) break;
+ if (remFuncs.isEmpty) break
b += 5 //increase bounds in steps of 5
}
//println("Inferrence did not succeeded for functions: " + remFuncs.map(_.id))
@@ -200,7 +187,7 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
first = false
ic
}
- progressCallback.map(cb => cb(inferCond))
+ progressCallback.foreach(cb => cb(inferCond))
}
val funsWithTemplates = inferredFuns.filter { fd =>
val origFd = functionByName(fd.id.name, startProg).get
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index d5f0196278d04489f657940caf74e30009fd02b9..4b0fb349f591780da0856e4ccbbe7e49f30c8d83 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -9,8 +9,6 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Definitions._
import purescala.Common._
-import invariant.templateSolvers._
-import invariant.factories._
import invariant.util._
import invariant.structure._
import leon.transformations.InstUtil
@@ -18,7 +16,6 @@ import leon.purescala.PrettyPrinter
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
import FunctionUtils._
import purescala._
@@ -64,7 +61,7 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
"║ └─────────┘" + (" " * (size - 12)) + "║"
private def infoLine(str: String, size: Int): String = {
- "║ " + str + (" " * (size - str.size - 2)) + " ║"
+ "║ " + str + (" " * (size - str.length - 2)) + " ║"
}
private def fit(str: String, maxLength: Int): String = {
@@ -77,11 +74,11 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
private def funName(fd: FunDef) = InstUtil.userFunctionName(fd)
- override def summaryString: String = if (conditions.size > 0) {
- val maxTempSize = (conditions.map(_.status.size).max + 3)
+ override def summaryString: String = if (conditions.nonEmpty) {
+ val maxTempSize = (conditions.map(_.status.length).max + 3)
val outputStrs = conditions.map(vc => {
val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
- "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" " * (maxTempSize - vc.status.size)), timeStr)
+ "%-15s %s %-4s".format(fit(funName(vc.fd), 15), vc.status + (" " * (maxTempSize - vc.status.length)), timeStr)
})
val summaryStr = {
val totalTime = conditions.foldLeft(0.0)((a, ic) => a + ic.time.getOrElse(0.0))
@@ -89,7 +86,7 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
"total: %-4d inferred: %-4d unknown: %-4d time: %-3.3f".format(
conditions.size, inferredConds, conditions.size - inferredConds, totalTime)
}
- val entrySize = (outputStrs :+ summaryStr).map(_.size).max + 2
+ val entrySize = (outputStrs :+ summaryStr).map(_.length).max + 2
infoHeader(entrySize) +
outputStrs.map(str => infoLine(str, entrySize)).mkString("\n", "\n", "\n") +
@@ -129,7 +126,7 @@ object InferenceReportUtil {
def fullNameWoInst(fd: FunDef) = {
val splits = DefOps.fullName(fd)(ctx.inferProgram).split("-")
- if (!splits.isEmpty) splits(0)
+ if (splits.nonEmpty) splits(0)
else ""
}
@@ -148,8 +145,8 @@ object InferenceReportUtil {
}
def mapExpr(ine: Expr): Expr = {
- val replaced = simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(TypedFunDef(fd, targs), args) =>
+ val replaced = simplePostTransform {
+ case e@FunctionInvocation(TypedFunDef(fd, targs), args) =>
if (initToOutput.contains(fd)) {
FunctionInvocation(TypedFunDef(initToOutput(fd), targs), args)
} else {
@@ -159,8 +156,8 @@ object InferenceReportUtil {
case _ => e
}
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
replaced
}
// copy bodies and specs
diff --git a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
similarity index 100%
rename from src/main/scala/leon/invariant/engine/SpecInstatiator.scala
rename to src/main/scala/leon/invariant/engine/SpecInstantiator.scala
diff --git a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
index c568910684e89d78862a516583eb0baf31174888..1e717dbc1a23723680ecdffeb27b3f78553d1747 100644
--- a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
+++ b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
@@ -1,26 +1,15 @@
package leon
package invariant.engine
-import z3.scala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet }
-import java.io._
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ Set => MutableSet }
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.structure._
-import Util._
-import PredicateUtil._
import ProgramUtil._
+import scala.collection.mutable.{Set => MutableSet}
/**
* An enumeration based template generator.
* Enumerates all numerical terms in some order (this enumeration is incomplete for termination).
@@ -126,7 +115,7 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr, Expr
if (fun != rootFun && !callGraph.transitivelyCalls(fun, rootFun)) {
//check if every argument has at least one satisfying assignment?
- if (fun.params.filter((vardecl) => !ttCurrent.contains(vardecl.getType)).isEmpty) {
+ if (!fun.params.exists((vardecl) => !ttCurrent.contains(vardecl.getType))) {
//here compute all the combinations
val newcalls = generateFunctionCalls(fun)
@@ -153,7 +142,7 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr, Expr
//return all the integer valued terms of newTerms
//++ newTerms.getOrElse(Int32Type, Seq[Expr]()) (for now not handling int 32 terms)
val numericTerms = (newTerms.getOrElse(RealType, Seq[Expr]()) ++ newTerms.getOrElse(IntegerType, Seq[Expr]())).toSeq
- if (!numericTerms.isEmpty) {
+ if (numericTerms.nonEmpty) {
//create a linear combination of intTerms
val newTemp = numericTerms.foldLeft(null: Expr)((acc, t: Expr) => {
val summand = Times(t, TemplateIdFactory.freshTemplateVar(): Expr)
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 4bb5bbc3d76a341151ff9478b139f2ad8157485d..a53456e73f72d323aca3597623ab9998c106bf94 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -1,31 +1,24 @@
package leon
package invariant.engine
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
import purescala.DefOps._
-import solvers._
-import solvers.z3.FairZ3Solver
-import java.io._
import purescala.ScalaPrinter
+
+import solvers._
import verification._
-import scala.reflect.runtime.universe
-import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
import invariant.structure._
import transformations._
import FunctionUtils._
-import leon.invariant.templateSolvers.ExtendedUFSolver
import Util._
import PredicateUtil._
import ProgramUtil._
-import SolverUtil._
/**
* @author ravi
@@ -119,7 +112,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
case (Some(model), callsInPath) =>
toRefineCalls = callsInPath
//Validate the model here
- instantiateAndValidateModel(model, constTracker.getFuncs.toSeq)
+ instantiateAndValidateModel(model, constTracker.getFuncs)
Some(InferResult(true, Some(model),
constTracker.getFuncs.toList))
case (None, callsInPath) =>
@@ -129,7 +122,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
}
}
}
- } while (!infRes.isDefined)
+ } while (infRes.isEmpty)
infRes
}
diff --git a/src/main/scala/leon/invariant/factories/AxiomFactory.scala b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
index 6fdf7fa633def45017de8df5fbab4250ce70928e..907db46ab1cf1fbd4efcc19f58ae5867142575f6 100644
--- a/src/main/scala/leon/invariant/factories/AxiomFactory.scala
+++ b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
@@ -1,24 +1,13 @@
package leon
package invariant.factories
-import z3.scala._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
-import scala.concurrent._
-import scala.concurrent.duration._
import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
-import Util._
import PredicateUtil._
class AxiomFactory(ctx : InferenceContext) {
@@ -85,7 +74,6 @@ class AxiomFactory(ctx : InferenceContext) {
//this is applicable only to binary operations
def undistributeCalls(call1: Call, call2: Call): (Expr,Expr) = {
- val fd = call1.fi.tfd.fd
val tfd = call1.fi.tfd
val Seq(a1,b1) = call1.fi.args
@@ -93,9 +81,7 @@ class AxiomFactory(ctx : InferenceContext) {
val r1 = call1.retexpr
val r2 = call2.retexpr
- val dret1 = TVarFactory.createTemp("dt", IntegerType).toVariable
val dret2 = TVarFactory.createTemp("dt", IntegerType).toVariable
- val dcall1 = Call(dret1, FunctionInvocation(tfd,Seq(a2,Plus(b1,b2))))
val dcall2 = Call(dret2, FunctionInvocation(tfd,Seq(Plus(a1,a2),b2)))
(LessEquals(b1,b2), And(LessEquals(Plus(r1,r2),dret2), dcall2.toExpr))
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateFactory.scala b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
index ab1f51359151de13ef8cd506f4f1c9da9472c208..b44fcfa684d66168cad5de3e0cca7d8df5d11f50 100644
--- a/src/main/scala/leon/invariant/factories/TemplateFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
@@ -1,23 +1,16 @@
package leon
package invariant.factories
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
-import scala.collection.mutable.{ Map => MutableMap }
-import invariant._
import scala.collection.mutable.{Map => MutableMap}
-import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
-import Util._
import PredicateUtil._
import ProgramUtil._
@@ -28,7 +21,7 @@ object TemplateIdFactory {
def getTemplateIds : Set[Identifier] = ids
def freshIdentifier(name : String = "", idType: TypeTree = RealType) : Identifier = {
- val idname = if(name.isEmpty()) "a?"
+ val idname = if(name.isEmpty) "a?"
else name + "?"
val freshid = FreshIdentifier(idname, idType, true)
ids += freshid
@@ -72,7 +65,7 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
//a mapping from function definition to the template
private var templateMap = {
//initialize the template map with predefined user maps
- var muMap = MutableMap[FunDef, Expr]()
+ val muMap = MutableMap[FunDef, Expr]()
functionsWOFields(prog.definedFunctions).foreach { fd =>
val tmpl = fd.template
if (tmpl.isDefined) {
@@ -114,7 +107,7 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
//initialize the template for the function
if (!templateMap.contains(fd)) {
- if(!tempGen.isDefined) templateMap += (fd -> getDefaultTemplate(fd))
+ if(tempGen.isEmpty) templateMap += (fd -> getDefaultTemplate(fd))
else {
templateMap += (fd -> tempGen.get.getNextTemplate(fd))
refinementSet += fd
diff --git a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
index ccaabc57aabecb9fa22fd94a5972c1a554196729..dbcdc4c5e1a2de62fb5a1c1e81ebe17b4449a584 100644
--- a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
@@ -1,23 +1,15 @@
package leon
package invariant.factories
-import z3.scala._
-import purescala._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import invariant.engine._
import invariant.util._
import invariant.structure._
import leon.solvers.Model
import leon.invariant.util.RealValuedExprEvaluator
-import Util._
import PredicateUtil._
-import ProgramUtil._
object TemplateInstantiator {
/**
@@ -51,17 +43,17 @@ object TemplateInstantiator {
*/
def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
//do a simple post transform and replace the template vars by their values
- val inv = simplePostTransform((tempExpr: Expr) => tempExpr match {
- case e @ Operator(Seq(lhs, rhs), op) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
+ val inv = simplePostTransform {
+ case tempExpr@(e@Operator(Seq(lhs, rhs), op)) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals])
&&
- !getTemplateVars(tempExpr).isEmpty) => {
+ getTemplateVars(tempExpr).nonEmpty) => {
val linearTemp = LinearConstraintUtil.exprToTemplate(tempExpr)
instantiateTemplate(linearTemp, tempVarMap, prettyInv)
}
- case _ => tempExpr
- })(expr)
+ case tempExpr => tempExpr
+ }(expr)
inv
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
index 469317998a98f979a9a90770fd9c902544eee584..96c8d212a59cfc39c8cc428dc521f8e4a278a004 100644
--- a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
@@ -1,12 +1,8 @@
package leon
package invariant.factories
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
import invariant._
import invariant.engine._
import invariant.util._
diff --git a/src/main/scala/leon/invariant/structure/Constraint.scala b/src/main/scala/leon/invariant/structure/Constraint.scala
index 9d2490fe5f8b61b6847636007c61d6ba3c0dba34..39fd20bca11971ba0feadf26e20331970f9a9ca7 100644
--- a/src/main/scala/leon/invariant/structure/Constraint.scala
+++ b/src/main/scala/leon/invariant/structure/Constraint.scala
@@ -1,23 +1,10 @@
package leon
package invariant.structure
-import z3.scala._
-import purescala._
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import solvers.{ Solver, TimeoutSolver }
-import solvers.z3.FairZ3Solver
-import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{ Map => MutableMap }
-import evaluators._
-import java.io._
-import solvers.z3.UninterpretedZ3Solver
import invariant.util._
-import Util._
import PredicateUtil._
trait Constraint {
@@ -42,9 +29,7 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
}
val coeffTemplate = {
//assert if the coefficients are templated expressions
- assert(coeffTemp.values.foldLeft(true)((acc, e) => {
- acc && isTemplateExpr(e)
- }))
+ assert(coeffTemp.values.forall(e => isTemplateExpr(e)))
coeffTemp
}
@@ -110,7 +95,7 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
rhsExprs :+= InfiniteIntegerLiteral(-v)
case Some(c) =>
lhsExprs :+= c
- case _ => Nil
+ case _ =>
}
val lhsExprOpt = ((None: Option[Expr]) /: lhsExprs) {
case (acc, minterm) =>
@@ -175,9 +160,7 @@ class LinearConstraint(opr: Seq[Expr] => Expr, cMap: Map[Expr, Expr], constant:
val coeffMap = {
//assert if the coefficients are only constant expressions
- assert(cMap.values.foldLeft(true)((acc, e) => {
- acc && variablesOf(e).isEmpty
- }))
+ assert(cMap.values.forall(e => variablesOf(e).isEmpty))
//TODO: here we should try to simplify the constant expressions
cMap
}
diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala
index daed61ff679cba61666a6c227005c103a31d8d01..c17711e102877861010359256ff902ad7d51d70b 100644
--- a/src/main/scala/leon/invariant/structure/Formula.scala
+++ b/src/main/scala/leon/invariant/structure/Formula.scala
@@ -22,8 +22,7 @@ import PredicateUtil._
/**
* Data associated with a call
*/
-class CallData(val guard : Variable, val parents: List[FunDef]) {
-}
+class CallData(val guard : Variable, val parents: List[FunDef])
/**
* Representation of an expression as a set of implications.
@@ -81,13 +80,13 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
})
}
- val f1 = simplePostTransform((e: Expr) => e match {
- case Or(args) => {
- val newargs = args.map(arg => arg match {
- case v: Variable if (disjuncts.contains(v)) => arg
- case v: Variable if (conjuncts.contains(v)) => throw new IllegalStateException("or gaurd inside conjunct: "+e+" or-guard: "+v)
- case _ => {
- val atoms = arg match {
+ val f1 = simplePostTransform {
+ case e@Or(args) => {
+ val newargs = args.map {
+ case arg@(v: Variable) if (disjuncts.contains(v)) => arg
+ case v: Variable if (conjuncts.contains(v)) => throw new IllegalStateException("or gaurd inside conjunct: " + e + " or-guard: " + v)
+ case arg => {
+ val atoms = arg match {
case And(atms) => atms
case _ => Seq(arg)
}
@@ -98,14 +97,14 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
disjuncts += (g -> ctrs)
g
}
- })
+ }
//create a temporary for Or
val gor = TVarFactory.createTemp("b", BooleanType).toVariable
val newor = createOr(newargs)
conjuncts += (gor -> newor)
gor
}
- case And(args) => {
+ case e@And(args) => {
val newargs = args.map(arg => if (getTemplateVars(e).isEmpty) {
arg
} else {
@@ -118,8 +117,8 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
})
createAnd(newargs)
}
- case _ => e
- })(ExpressionTransformer.simplify(simplifyArithmetic(
+ case e => e
+ }(ExpressionTransformer.simplify(simplifyArithmetic(
//TODO: this is a hack as of now. Fix this.
//Note: it is necessary to convert real literals to integers since the linear constraint cannot handle real literals
if(ctx.usereals) ExpressionTransformer.FractionalLiteralToInt(ine)
@@ -151,7 +150,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
val e @ Or(guards) = conjuncts(gd)
//pick one guard that is true
val guard = guards.collectFirst { case g @ Variable(id) if (model(id) == tru) => g }
- if (!guard.isDefined)
+ if (guard.isEmpty)
throw new IllegalStateException("No satisfiable guard found: " + e)
guard.get +: traverseAnds(guard.get, model)
}
@@ -236,16 +235,16 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
//replace all conjunct guards in disjuncts by their mapping
val disjs : Map[Expr,Expr] = disjuncts.map((entry) => {
val (g,ctrs) = entry
- val newctrs = ctrs.map(_ match {
+ val newctrs = ctrs.map {
case BoolConstraint(g@Variable(_)) if conjuncts.contains(g) => conjuncts(g)
case ctr@_ => ctr.toExpr
- })
+ }
(g, createAnd(newctrs))
})
- val rootexprs = roots.map(_ match {
- case g@Variable(_) if conjuncts.contains(g) => conjuncts(g)
- case e@_ => e
- })
+ val rootexprs = roots.map {
+ case g@Variable(_) if conjuncts.contains(g) => conjuncts(g)
+ case e@_ => e
+ }
//replace every guard in the 'disjs' by its disjunct. DO this as long as every guard is replaced in every disjunct
var unpackedDisjs = disjs
var replacedGuard = true
diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index 7910df7230e82f7ac8b695bc8089fcd64c005e3a..5ed3316a44bb6d0baaec32dd1962fbe7f78af0f5 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -3,23 +3,15 @@ package invariant.structure
import purescala._
import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet }
import scala.collection.mutable.{ Map => MutableMap }
-import java.io._
import invariant.util._
import BigInt._
-import Constructors._
-import Util._
import PredicateUtil._
-class NotImplementedException(message: String) extends RuntimeException(message) {
-
-}
+class NotImplementedException(message: String) extends RuntimeException(message)
//a collections of utility methods that manipulate the templates
object LinearConstraintUtil {
@@ -31,14 +23,14 @@ object LinearConstraintUtil {
//some utility methods
def getFIs(ctr: LinearConstraint): Set[FunctionInvocation] = {
- val fis = ctr.coeffMap.keys.collect((e) => e match {
+ val fis = ctr.coeffMap.keys.collect {
case fi: FunctionInvocation => fi
- })
+ }
fis.toSet
}
def evaluate(lt: LinearTemplate): Option[Boolean] = lt match {
- case lc: LinearConstraint if (lc.coeffMap.size == 0) =>
+ case lc: LinearConstraint if lc.coeffMap.isEmpty =>
ExpressionTransformer.simplify(lt.toExpr) match {
case BooleanLiteral(v) => Some(v)
case _ => None
@@ -74,7 +66,7 @@ object LinearConstraintUtil {
}
} else coeffMap += (term -> simplifyArithmetic(coeff))
- if (!variablesOf(coeff).isEmpty) {
+ if (variablesOf(coeff).nonEmpty) {
isTemplate = true
}
}
@@ -86,7 +78,7 @@ object LinearConstraintUtil {
} else
constant = Some(simplifyArithmetic(coeff))
- if (!variablesOf(coeff).isEmpty) {
+ if (variablesOf(coeff).nonEmpty) {
isTemplate = true
}
}
@@ -341,7 +333,6 @@ object LinearConstraintUtil {
//now consider each constraint look for (a) equality involving the elimVar or (b) check if all bounds are lower
//or (c) if all bounds are upper.
var elimExpr : Option[Expr] = None
- var bestExpr = false
var elimCtr : Option[LinearConstraint] = None
var allUpperBounds : Boolean = true
var allLowerBounds : Boolean = true
@@ -354,7 +345,7 @@ object LinearConstraintUtil {
foundEquality = true
//here, sometimes we replace an existing expression with a better one if available
- if (!elimExpr.isDefined || shouldReplace(elimExpr.get, lc, elimVar)) {
+ if (elimExpr.isEmpty || shouldReplace(elimExpr.get, lc, elimVar)) {
//if the coeffcient of elimVar is +ve the the sign of the coeff of every other term should be changed
val InfiniteIntegerLiteral(elimCoeff) = lc.coeffMap(elimVar.toVariable)
//make sure the value of the coefficient is 1 or -1
diff --git a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index 98f162fea4b2974702c4672274ed6d8f86075690..15ae673019e9c50eb3ff257fc88114c935230342 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -1,23 +1,17 @@
package leon
package invariant.templateSolvers
-import z3.scala._
+
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import scala.util.control.Breaks._
import solvers._
-import solvers.z3._
import invariant.engine._
import invariant.factories._
import invariant.util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.util.RealValuedExprEvaluator._
-import Util._
import PredicateUtil._
import SolverUtil._
@@ -95,7 +89,7 @@ class CegisCore(ctx: InferenceContext,
val tempVarSum = if (minimizeSum) {
//compute the sum of the tempIds
val rootTempIds = getTemplateVars(cegisSolver.rootFun.getTemplate)
- if (rootTempIds.size >= 1) {
+ if (rootTempIds.nonEmpty) {
rootTempIds.tail.foldLeft(rootTempIds.head.asInstanceOf[Expr])((acc, tvar) => Plus(acc, tvar))
} else zero
} else zero
@@ -126,7 +120,7 @@ class CegisCore(ctx: InferenceContext,
//sanity checks
val spuriousTempIds = variablesOf(instFormula).intersect(TemplateIdFactory.getTemplateIds)
- if (!spuriousTempIds.isEmpty)
+ if (spuriousTempIds.nonEmpty)
throw new IllegalStateException("Found a template variable in instFormula: " + spuriousTempIds)
if (hasReals(instFormula))
throw new IllegalStateException("Reals in instFormula: " + instFormula)
@@ -144,21 +138,21 @@ class CegisCore(ctx: InferenceContext,
//simplify the tempctrs, evaluate every atom that does not involve a template variable
//this should get rid of all functions
val satctrs =
- simplePreTransform((e) => e match {
+ simplePreTransform {
//is 'e' free of template variables ?
- case _ if (variablesOf(e).filter(TemplateIdFactory.IsTemplateIdentifier _).isEmpty) => {
+ case e if !variablesOf(e).exists(TemplateIdFactory.IsTemplateIdentifier _) => {
//evaluate the term
val value = solver1.evalExpr(e)
if (value.isDefined) value.get
else throw new IllegalStateException("Cannot evaluate expression: " + e)
}
- case _ => e
- })(Not(formula))
+ case e => e
+ }(Not(formula))
solver1.free()
//sanity checks
val spuriousProgIds = variablesOf(satctrs).filterNot(TemplateIdFactory.IsTemplateIdentifier _)
- if (!spuriousProgIds.isEmpty)
+ if (spuriousProgIds.nonEmpty)
throw new IllegalStateException("Found a progam variable in tempctrs: " + spuriousProgIds)
val tempctrs = if (!solveAsInt) ExpressionTransformer.IntLiteralToReal(satctrs) else satctrs
@@ -201,7 +195,7 @@ class CegisCore(ctx: InferenceContext,
println("2: " + (if (res1.isDefined) "solved" else "timed out") + "... in " + (t4 - t3) / 1000.0 + "s")
if (res1.isDefined) {
- if (res1.get == false) {
+ if (!res1.get) {
//there exists no solution for templates
(Some(false), newctr, Model.empty)
diff --git a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
index 805f09a941139d817309a3a10df0b07cd57a21aa..9a9c1b0b4290b07408adb33c0e174813de831a29 100644
--- a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
@@ -4,16 +4,9 @@ package leon
package invariant.templateSolvers
import z3.scala._
-import leon.solvers._
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.Extractors._
-import purescala.ExprOps._
-import purescala.Types._
-import leon.LeonContext
import leon.solvers.z3.UninterpretedZ3Solver
-import leon.solvers.smtlib.SMTLIBZ3Solver
/**
* A uninterpreted solver extended with additional functionalities.
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 19dee9ab4be261cd2378d2146864fb9566912ca3..a4e20f61a7424ee59724b8cf4374cecbcaf84f9f 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -1,26 +1,19 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import java.io._
import solvers.SimpleSolverAPI
-import scala.collection.mutable.{ Map => MutableMap }
import invariant.engine._
-import invariant.factories._
import invariant.util._
import Util._
-import ProgramUtil._
import SolverUtil._
import PredicateUtil._
-import TimerUtil._
import invariant.structure._
+import invariant.datastructure._
import leon.solvers.TimeoutSolver
import leon.solvers.SolverFactory
import leon.solvers.TimeoutSolverFactory
@@ -83,8 +76,8 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
println("#" * 20)
//Optimization 1: Check if ants are unsat (already handled)
- val pathVC = createAnd(antsSimple.map(_.toExpr).toSeq ++ conseqsSimple.map(_.toExpr).toSeq)
- val notPathVC = And(createAnd(antsSimple.map(_.toExpr).toSeq), Not(createAnd(conseqsSimple.map(_.toExpr).toSeq)))
+ val pathVC = createAnd(antsSimple.map(_.toExpr) ++ conseqsSimple.map(_.toExpr))
+ val notPathVC = And(createAnd(antsSimple.map(_.toExpr)), Not(createAnd(conseqsSimple.map(_.toExpr))))
val (satVC, _) = uisolver.solveSAT(pathVC)
val (satNVC, _) = uisolver.solveSAT(notPathVC)
@@ -135,7 +128,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
strictCtrLambdas :+= l
GreaterEquals(l, zero)
}
- }).toSeq :+ GreaterEquals(lambda0, zero))
+ }) :+ GreaterEquals(lambda0, zero))
//add the constraints on constant terms
val sumConst = ants.foldLeft(UMinus(lambda0): Expr)((acc, ant) => ant.constTemplate match {
@@ -206,7 +199,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
// factor out common nonlinear terms and create an equiv-satisfiable constraint
def reduceCommonNLTerms(ctrs: Expr) = {
- var nlUsage = new CounterMap[Expr]()
+ val nlUsage = new CounterMap[Expr]()
postTraversal{
case t: Times => nlUsage.inc(t)
case e => ;
@@ -223,7 +216,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
// try eliminate nonlinearity to whatever extent possible
var elimMap = Map[Identifier, (Identifier, Identifier)]() // maps the fresh identifiers to the product of the identifiers they represent.
def reduceNonlinearity(farkasctrs: Expr): Expr = {
- var varCounts = new CounterMap[Identifier]()
+ val varCounts = new CounterMap[Identifier]()
// collect # of uses of each variable
postTraversal {
case Variable(id) => varCounts.inc(id)
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 41d672fe5a94861197430a69c9516985e46f2511..90cffa3f181d11deb499a06ec538a515ed164ac1 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -9,7 +9,6 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import evaluators._
-import scala.collection.mutable.{ Map => MutableMap }
import java.io._
import solvers._
import solvers.combinators._
@@ -369,7 +368,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val cegisSolver = new CegisCore(ctx, program, timeout.toInt, this)
val (res, ctr, model) = cegisSolver.solve(tempIds, expr, precond, solveAsInt = false, initModel)
- if (!res.isDefined)
+ if (res.isEmpty)
reporter.info("cegis timed-out on the disjunct...")
(res, ctr, model)
}
@@ -508,7 +507,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val InfiniteIntegerLiteral(v) = model(id)
v
}
- def eval: (Expr => Boolean) = e => e match {
+ def eval: (Expr => Boolean) = {
case And(args) => args.forall(eval)
// case Iff(Variable(id1), Variable(id2)) => model(id1) == model(id2)
case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
@@ -516,7 +515,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
case GreaterEquals(Variable(id1), Variable(id2)) => modelVal(id1) >= modelVal(id2)
case GreaterThan(Variable(id1), Variable(id2)) => modelVal(id1) > modelVal(id2)
case LessThan(Variable(id1), Variable(id2)) => modelVal(id1) < modelVal(id2)
- case _ => throw new IllegalStateException("Predicate not handled: " + e)
+ case e => throw new IllegalStateException("Predicate not handled: " + e)
}
eval
}
@@ -526,14 +525,14 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
//println("Identifier: "+id)
model(id).asInstanceOf[FractionalLiteral]
}
- (e: Expr) => e match {
+ {
case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
- case Operator(Seq(Variable(id1), Variable(id2)), op) if (e.isInstanceOf[LessThan]
+ case e@Operator(Seq(Variable(id1), Variable(id2)), op) if (e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals]) => {
evaluateRealPredicate(op(Seq(modelVal(id1), modelVal(id2))))
}
- case _ => throw new IllegalStateException("Predicate not handled: " + e)
+ case e => throw new IllegalStateException("Predicate not handled: " + e)
}
}
@@ -587,11 +586,11 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
var calls = Set[Call]()
var cons = Set[Expr]()
- satCtrs.foreach(ctr => ctr match {
+ satCtrs.foreach {
case t: Call => calls += t
case t: ADTConstraint if (t.cons.isDefined) => cons += t.cons.get
case _ => ;
- })
+ }
val callExprs = calls.map(_.toExpr)
var t1 = System.currentTimeMillis()
@@ -617,11 +616,11 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
//exclude guards, separate calls and cons from the rest
var lnctrs = Set[LinearConstraint]()
var temps = Set[LinearTemplate]()
- (satCtrs ++ callCtrs ++ axiomCtrs ++ theoryCtrs).foreach(ctr => ctr match {
+ (satCtrs ++ callCtrs ++ axiomCtrs ++ theoryCtrs).foreach {
case t: LinearConstraint => lnctrs += t
case t: LinearTemplate => temps += t
case _ => ;
- })
+ }
if (this.debugChooseDisjunct) {
lnctrs.map(_.toExpr).foreach((ctr) => {
@@ -693,7 +692,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
var elimRems = Set[Identifier]()
elimLnctrs.foreach((lc) => {
val evars = variablesOf(lc.toExpr).intersect(elimVars)
- if (!evars.isEmpty) {
+ if (evars.nonEmpty) {
elimCtrs :+= lc
elimCtrCount += 1
elimRems ++= evars
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
index a2a6524c6d6f52ffa232129b4adb2ff0f794ee42..d67955ff9efd38dd9c5c70b0684b04b5cda1661b 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
@@ -1,15 +1,9 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
-import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
import solvers._
import invariant.engine._
@@ -18,7 +12,6 @@ import invariant.util._
import invariant.structure._
import Util._
import PredicateUtil._
-import SolverUtil._
class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun: FunDef,
ctrTracker: ConstraintTracker, minimizer: Option[(Expr, Model) => Model])
@@ -42,10 +35,10 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun
//in the sequel we instantiate axioms for multiplication
val inst1 = unaryMultAxioms(formula, calls, predEval(model))
val inst2 = binaryMultAxioms(formula,calls, predEval(model))
- val multCtrs = (inst1 ++ inst2).flatMap(_ match {
+ val multCtrs = (inst1 ++ inst2).flatMap {
case And(args) => args.map(ConstraintUtil.createConstriant _)
case e => Seq(ConstraintUtil.createConstriant(e))
- })
+ }
Stats.updateCounterStats(multCtrs.size, "MultAxiomBlowup", "disjuncts")
ctx.reporter.info("Number of multiplication induced predicates: "+multCtrs.size)
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index dceed68279e089122875d19c86664425df49aa22..a85a7d4f5b9f55af812da50d577ec36d350b7ce5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -1,18 +1,11 @@
package leon
package invariant.templateSolvers
-import z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
import java.io._
-import leon.invariant._
-import scala.util.control.Breaks._
-import scala.concurrent._
-import scala.concurrent.duration._
import invariant.engine._
import invariant.factories._
import invariant.util._
diff --git a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
index f41ec7e8963a45978fb4a9ac3fe091de48140d10..6b2aa300b2792f7f86b5f01565ee783731f8d863 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
@@ -1,20 +1,14 @@
package leon
package invariant.templateSolvers
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import java.io._
import invariant.datastructure.UndirectedGraph
-import scala.util.control.Breaks._
import invariant.util._
import leon.purescala.TypeOps
import PredicateUtil._
-import SolverUtil._
-import Util._
class UFADTEliminator(ctx: LeonContext, program: Program) {
@@ -113,7 +107,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
lhs :+ rhs
}
//remove self equalities.
- val preds = eqs.filter(_ match {
+ val preds = eqs.filter {
case Operator(Seq(Variable(lid), Variable(rid)), _) => {
if (lid == rid) false
else {
@@ -121,8 +115,8 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
else false
}
}
- case e @ _ => throw new IllegalStateException("Not an equality or Iff: " + e)
- })
+ case e@_ => throw new IllegalStateException("Not an equality or Iff: " + e)
+ }
preds
}
@@ -134,21 +128,21 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
axiomatizeADTCons(call1, call2)
}
- if (makeEfficient && ants.exists(_ match {
+ if (makeEfficient && ants.exists {
case Equals(l, r) if (l.getType != RealType && l.getType != BooleanType && l.getType != IntegerType) => true
case _ => false
- })) {
+ }) {
Seq()
} else {
var unsatIntEq: Option[Expr] = None
var unsatOtherEq: Option[Expr] = None
ants.foreach(eq =>
- if (!unsatOtherEq.isDefined) {
+ if (unsatOtherEq.isEmpty) {
eq match {
case Equals(lhs @ Variable(_), rhs @ Variable(_)) if !predEval(Equals(lhs, rhs)) => {
if (lhs.getType != Int32Type && lhs.getType != RealType && lhs.getType != IntegerType)
unsatOtherEq = Some(eq)
- else if (!unsatIntEq.isDefined)
+ else if (unsatIntEq.isEmpty)
unsatIntEq = Some(eq)
}
case _ => ;
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index 6750bd59c144fa656b2d820516d6691e3e169862..9bf2889ed103f0e14083a031e5b80c700e5c89d0 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -8,10 +8,7 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import java.io._
-import java.io._
import purescala.ScalaPrinter
-import invariant.structure.Call
-import invariant.structure.FunctionUtils._
import leon.invariant.factories.TemplateIdFactory
import PredicateUtil._
import Util._
@@ -185,7 +182,7 @@ object ExpressionTransformer {
}
}
val (nexp, ncjs) = transform(inexpr, false)
- val res = if (!ncjs.isEmpty) {
+ val res = if (ncjs.nonEmpty) {
createAnd(nexp +: ncjs.toSeq)
} else nexp
res
@@ -283,31 +280,30 @@ object ExpressionTransformer {
def flattenArgs(args: Seq[Expr], insideFunction: Boolean): (Seq[Expr], Set[Expr]) = {
var newConjuncts = Set[Expr]()
- val newargs = args.map((arg) =>
- arg match {
- case v: Variable => v
- case r: ResultVariable => r
- case _ => {
- val (nexpr, ncjs) = flattenFunc(arg, insideFunction)
-
- newConjuncts ++= ncjs
-
- nexpr match {
- case v: Variable => v
- case r: ResultVariable => r
- case _ => {
- val freshArgVar = Variable(TVarFactory.createTemp("arg", arg.getType))
- newConjuncts += Equals(freshArgVar, nexpr)
- freshArgVar
- }
+ val newargs = args.map {
+ case v: Variable => v
+ case r: ResultVariable => r
+ case arg => {
+ val (nexpr, ncjs) = flattenFunc(arg, insideFunction)
+
+ newConjuncts ++= ncjs
+
+ nexpr match {
+ case v: Variable => v
+ case r: ResultVariable => r
+ case _ => {
+ val freshArgVar = Variable(TVarFactory.createTemp("arg", arg.getType))
+ newConjuncts += Equals(freshArgVar, nexpr)
+ freshArgVar
}
}
- })
+ }
+ }
(newargs, newConjuncts)
}
val (nexp, ncjs) = flattenFunc(inExpr, false)
- if (!ncjs.isEmpty) {
+ if (ncjs.nonEmpty) {
createAnd(nexp +: ncjs.toSeq)
} else nexp
}
@@ -387,7 +383,7 @@ object ExpressionTransformer {
*/
def pullAndOrs(expr: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case Or(args) => {
val newArgs = args.foldLeft(Seq[Expr]())((acc, arg) => arg match {
case Or(inArgs) => acc ++ inArgs
@@ -402,8 +398,8 @@ object ExpressionTransformer {
})
createAnd(newArgs)
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
}
def classSelToCons(e: Expr): Expr = {
@@ -466,15 +462,15 @@ object ExpressionTransformer {
*/
def unFlatten(ine: Expr, freevars: Set[Identifier]): Expr = {
var tempMap = Map[Expr, Expr]()
- val newinst = simplePostTransform((e: Expr) => e match {
- case Equals(v @ Variable(id), rhs @ _) if !freevars.contains(id) =>
+ val newinst = simplePostTransform {
+ case e@Equals(v@Variable(id), rhs@_) if !freevars.contains(id) =>
if (tempMap.contains(v)) e
else {
tempMap += (v -> rhs)
tru
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
val closure = (e: Expr) => replace(tempMap, e)
fix(closure)(newinst)
}
@@ -510,11 +506,11 @@ object ExpressionTransformer {
def isSubExpr(key: Expr, expr: Expr): Boolean = {
var found = false
- simplePostTransform((e: Expr) => e match {
- case _ if (e == key) =>
+ simplePostTransform {
+ case e if (e == key) =>
found = true; e
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
found
}
@@ -524,7 +520,7 @@ object ExpressionTransformer {
def simplify(expr: Expr): Expr = {
//Note: some simplification are already performed by the class constructors (see Tree.scala)
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case Equals(lhs, rhs) if (lhs == rhs) => tru
case LessEquals(lhs, rhs) if (lhs == rhs) => tru
case GreaterEquals(lhs, rhs) if (lhs == rhs) => tru
@@ -536,8 +532,8 @@ object ExpressionTransformer {
case LessThan(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 < v2)
case GreaterEquals(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 >= v2)
case GreaterThan(InfiniteIntegerLiteral(v1), InfiniteIntegerLiteral(v2)) => BooleanLiteral(v1 > v2)
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
}
/**
@@ -545,7 +541,7 @@ object ExpressionTransformer {
* Note: (a) Not(Equals()) and Not(Variable) is allowed
*/
def isDisjunct(e: Expr): Boolean = e match {
- case And(args) => args.foldLeft(true)((acc, arg) => acc && isDisjunct(arg))
+ case And(args) => args.forall(arg => isDisjunct(arg))
case Not(Equals(_, _)) | Not(Variable(_)) => true
case Or(_) | Implies(_, _) | Not(_) | Equals(_, _) => false
case _ => true
@@ -556,7 +552,7 @@ object ExpressionTransformer {
* Note: (a) Not(Equals()) and Not(Variable) is allowed
*/
def isConjunct(e: Expr): Boolean = e match {
- case Or(args) => args.foldLeft(true)((acc, arg) => acc && isConjunct(arg))
+ case Or(args) => args.forall(arg => isConjunct(arg))
case Not(Equals(_, _)) | Not(Variable(_)) => true
case And(_) | Implies(_, _) | Not(_) | Equals(_, _) => false
case _ => true
@@ -568,17 +564,17 @@ object ExpressionTransformer {
case And(args) => {
//have we seen an or ?
if (seen == 2) false
- else args.foldLeft(true)((acc, arg) => acc && uniOP(arg, 1))
+ else args.forall(arg => uniOP(arg, 1))
}
case Or(args) => {
//have we seen an And ?
if (seen == 1) false
- else args.foldLeft(true)((acc, arg) => acc && uniOP(arg, 2))
+ else args.forall(arg => uniOP(arg, 2))
}
case t: Terminal => true
/*case u @ UnaryOperator(e1, op) => uniOP(e1, seen)
case b @ BinaryOperator(e1, e2, op) => uniOP(e1, seen) && uniOP(e2, seen)*/
- case n @ Operator(args, op) => args.foldLeft(true)((acc, arg) => acc && uniOP(arg, seen))
+ case n @ Operator(args, op) => args.forall(arg => uniOP(arg, seen))
}
def printRec(e: Expr, indent: Int): Unit = {
@@ -588,7 +584,7 @@ object ExpressionTransformer {
e match {
case And(args) => {
var start = true
- args.map((arg) => {
+ args.foreach((arg) => {
wr.print(" " * (indent + 1))
if (!start) wr.print("^")
printRec(arg, indent + 1)
@@ -597,7 +593,7 @@ object ExpressionTransformer {
}
case Or(args) => {
var start = true
- args.map((arg) => {
+ args.foreach((arg) => {
wr.print(" " * (indent + 1))
if (!start) wr.print("v")
printRec(arg, indent + 1)
@@ -627,8 +623,8 @@ object ExpressionTransformer {
}
def distribute(e: Expr): Expr = {
- simplePreTransform(_ match {
- case e @ FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if isMultFunctions(fd) =>
+ simplePreTransform {
+ case e@FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if isMultFunctions(fd) =>
val newe = (e1, e2) match {
case (Plus(sum1, sum2), _) =>
// distribute e2 over e1
@@ -655,7 +651,7 @@ object ExpressionTransformer {
}
newe
case other => other
- })(e)
+ }(e)
}
distribute(e)
}
diff --git a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
similarity index 92%
rename from src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
rename to src/main/scala/leon/invariant/util/LetTupleSimplification.scala
index bd99992014bd94ab29c099b7a03eb7e452e154c0..83b7b0cba056c0c7f377caa2c4f76134bab81e24 100644
--- a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
+++ b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
@@ -7,14 +7,8 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
-import java.io._
-import java.io._
-import purescala.ScalaPrinter
import leon.utils._
import PredicateUtil._
-
-import invariant.structure.Call
-import invariant.structure.FunctionUtils._
import leon.transformations.InstUtil._
/**
@@ -31,13 +25,13 @@ object LetTupleSimplification {
val bone = BigInt(1)
def letSanityChecks(ine: Expr) = {
- simplePostTransform(_ match {
- case letExpr @ Let(binderId, letValue, body)
- if (binderId.getType != letValue.getType) =>
- throw new IllegalStateException("Binder and value type mismatch: "+
- s"(${binderId.getType},${letValue.getType})")
+ simplePostTransform {
+ case letExpr@Let(binderId, letValue, body)
+ if (binderId.getType != letValue.getType) =>
+ throw new IllegalStateException("Binder and value type mismatch: " +
+ s"(${binderId.getType},${letValue.getType})")
case e => e
- })(ine)
+ }(ine)
}
/**
@@ -130,11 +124,11 @@ object LetTupleSimplification {
(arg1, arg2) match {
case (_: TupleSelect, _) => error = true
case (_, _: TupleSelect) => error = true
- case _ => { ; }
+ case _ =>
}
}
- case _ => { ; }
+ case _ =>
}
}
@@ -172,8 +166,8 @@ object LetTupleSimplification {
// in the sequel, we are using the fact that 'depth' is positive and
// 'ine' contains only 'depth' variables
- val simpe = simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(tfd, args) if (tfd.fd == maxFun) => {
+ val simpe = simplePostTransform {
+ case e@FunctionInvocation(tfd, args) if (tfd.fd == maxFun) => {
if (debugMaxSimplify) {
println("Simplifying: " + e)
}
@@ -183,20 +177,20 @@ object LetTupleSimplification {
import invariant.structure.LinearConstraintUtil._
val lt = exprToTemplate(LessEquals(Minus(arg1, arg2), InfiniteIntegerLiteral(0)))
//now, check if all the variables in 'lt' have only positive coefficients
- val allPositive = lt.coeffTemplate.forall(entry => entry match {
+ val allPositive = lt.coeffTemplate.forall {
case (k, IntLiteral(v)) if (v >= 0) => true
case _ => false
- }) && (lt.constTemplate match {
+ } && (lt.constTemplate match {
case None => true
case Some(IntLiteral(v)) if (v >= 0) => true
case _ => false
})
if (allPositive) arg1
else {
- val allNegative = lt.coeffTemplate.forall(entry => entry match {
+ val allNegative = lt.coeffTemplate.forall {
case (k, IntLiteral(v)) if (v <= 0) => true
case _ => false
- }) && (lt.constTemplate match {
+ } && (lt.constTemplate match {
case None => true
case Some(IntLiteral(v)) if (v <= 0) => true
case _ => false
@@ -222,14 +216,14 @@ object LetTupleSimplification {
// case FunctionInvocation(tfd, args) if(tfd.fd.id.name == "max") => {
// throw new IllegalStateException("Found just max in expression " + e + "\n")
// }
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
simpe
}
def inlineMax(ine: Expr): Expr = {
//inline 'max' operations here
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(tfd, args) if (tfd.fd == maxFun) =>
val Seq(arg1, arg2) = args
val bindWithLet = (value: Expr, body: (Expr with Terminal) => Expr) => {
@@ -245,8 +239,8 @@ object LetTupleSimplification {
}
bindWithLet(arg1, a1 => bindWithLet(arg2, a2 =>
IfExpr(GreaterEquals(a1, a2), a1, a2)))
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def removeLetsFromLetValues(ine: Expr): Expr = {
@@ -317,10 +311,10 @@ object LetTupleSimplification {
Tuple(args :+ e2)
}))
}
- replaceLetBody(transLet, (e: Expr) => e match {
+ replaceLetBody(transLet, {
case Tuple(args) =>
op(args)
- case _ => op(Seq(e)) //here, there was only one argument
+ case e => op(Seq(e)) //here, there was only one argument
})
}
transe
@@ -378,7 +372,7 @@ object LetTupleSimplification {
res
}
- val transforms = removeLetsFromLetValues _ andThen fixpoint(postMap(simplerLet)) _ andThen simplifyArithmetic
+ val transforms = removeLetsFromLetValues _ andThen fixpoint(postMap(simplerLet)) andThen simplifyArithmetic
transforms(ine)
}
@@ -398,7 +392,7 @@ object LetTupleSimplification {
val allLeaves = getLeaves(e, true)
// Here the expression is not of the form we are currently simplifying
- if (allLeaves.size == 0) e
+ if (allLeaves.isEmpty) e
else {
// fold constants here
val allConstantsOpped = allLeaves.foldLeft(identity)((acc, e) => e match {
@@ -406,17 +400,17 @@ object LetTupleSimplification {
case _ => acc
})
- val allNonConstants = allLeaves.filter((e) => e match {
+ val allNonConstants = allLeaves.filter {
case _: InfiniteIntegerLiteral => false
case _ => true
- })
+ }
// Reconstruct the expressin tree with the non-constants and the result of constant evaluation above
if (allConstantsOpped != identity) {
allNonConstants.foldLeft(InfiniteIntegerLiteral(allConstantsOpped): Expr)((acc: Expr, currExpr) => makeTree(acc, currExpr))
}
else {
- if (allNonConstants.size == 0) InfiniteIntegerLiteral(identity)
+ if (allNonConstants.isEmpty) InfiniteIntegerLiteral(identity)
else {
allNonConstants.tail.foldLeft(allNonConstants.head)((acc: Expr, currExpr) => makeTree(acc, currExpr))
}
@@ -455,10 +449,11 @@ object LetTupleSimplification {
((a: BigInt, b: BigInt) => if (a > b) a else b),
getAllMaximands,
0,
- ((e1, e2) => {
+ (e1, e2) => {
val typedMaxFun = TypedFunDef(maxFun, Seq())
FunctionInvocation(typedMaxFun, Seq(e1, e2))
- }))
+ }
+ )
maxSimplifiedExpr
})(e)
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index e39378f267c0970d85797d19eef468c3a35f1db4..3794f55463490ae048574f3613f720ba092d0ff2 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -1,22 +1,15 @@
package leon
package invariant.util
-import z3.scala._
-import purescala.Common._
+
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
-import purescala.Types._
import solvers._
-import solvers.z3._
import solvers.smtlib.SMTLIBZ3Solver
-import leon.invariant._
-import scala.util.control.Breaks._
import invariant.engine.InferenceContext
import invariant.factories._
-import leon.invariant.templateSolvers.ExtendedUFSolver
import leon.invariant.util.RealValuedExprEvaluator._
-import invariant.util.TimerUtil._
class Minimizer(ctx: InferenceContext, program: Program) {
diff --git a/src/main/scala/leon/invariant/util/RealToIntExpr.scala b/src/main/scala/leon/invariant/util/RealToInt.scala
similarity index 96%
rename from src/main/scala/leon/invariant/util/RealToIntExpr.scala
rename to src/main/scala/leon/invariant/util/RealToInt.scala
index 54650b2c4111b32e127070cdc23889708a81b6fd..6c1860160f2bebc5bf0cb574b9c9934985246f45 100644
--- a/src/main/scala/leon/invariant/util/RealToIntExpr.scala
+++ b/src/main/scala/leon/invariant/util/RealToInt.scala
@@ -2,12 +2,9 @@ package leon
package invariant.util
import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import leon.invariant._
import invariant.factories._
import solvers._
diff --git a/src/main/scala/leon/invariant/util/RealExprEvaluator.scala b/src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
similarity index 100%
rename from src/main/scala/leon/invariant/util/RealExprEvaluator.scala
rename to src/main/scala/leon/invariant/util/RealValuedExprEvaluator.scala
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
index e67385c435ea94b24ef63ed8fe8bdbf41f602570..466ec1d2def3831b42c1f0b4bc6eaad3351ef716 100644
--- a/src/main/scala/leon/invariant/util/SolverUtil.scala
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -1,21 +1,13 @@
package leon
package invariant.util
-import utils._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
-import leon.invariant._
import solvers.z3._
import solvers._
-import invariant.engine._
-import invariant.factories._
-import invariant.structure._
-import FunctionUtils._
import leon.invariant.templateSolvers.ExtendedUFSolver
import java.io._
import Util._
@@ -55,7 +47,7 @@ object SolverUtil {
case id @ _ if (id.name.toString == "c?") => id.toVariable -> InfiniteIntegerLiteral(2)
}.toMap
//println("found ids: " + idmap.keys)
- if (!idmap.keys.isEmpty) {
+ if (idmap.keys.nonEmpty) {
val newpathcond = replace(idmap, expr)
//check if this is solvable
val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
@@ -76,8 +68,8 @@ object SolverUtil {
var controlVars = Map[Variable, Expr]()
var newEqs = Map[Expr, Expr]()
val solver = new ExtendedUFSolver(ctx, prog)
- val newe = simplePostTransform((e: Expr) => e match {
- case And(_) | Or(_) => {
+ val newe = simplePostTransform {
+ case e@(And(_) | Or(_)) => {
val v = TVarFactory.createTemp("a", BooleanType).toVariable
newEqs += (v -> e)
val newe = Equals(v, e)
@@ -88,8 +80,8 @@ object SolverUtil {
solver.assertCnstr(Or(newe, cvar))
v
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
//create new variable and add it in disjunction
val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
controlVars += (cvar -> newe)
diff --git a/src/main/scala/leon/invariant/util/Stats.scala b/src/main/scala/leon/invariant/util/Stats.scala
index 76a1f12ee4eede0ba631969ebb7bf3076bb3bf08..72239ac32227122c5f65c1ea73ac231d04014a11 100644
--- a/src/main/scala/leon/invariant/util/Stats.scala
+++ b/src/main/scala/leon/invariant/util/Stats.scala
@@ -1,19 +1,11 @@
package leon
package invariant.util
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
-import purescala.Types._
-import scala.collection.mutable.{ Map => MutableMap }
-import java.io._
-import leon.invariant._
import java.io._
import scala.collection.mutable.{Map => MutableMap}
-
/**
* A generic statistics object that provides:
* (a) Temporal variables that change over time. We track the total sum and max of the values the variable takes over time
diff --git a/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala b/src/main/scala/leon/invariant/util/TVarFactory.scala
similarity index 81%
rename from src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
rename to src/main/scala/leon/invariant/util/TVarFactory.scala
index c85c7837b1c4dbf35e2a90b87d93bccca929a6c9..6743e802b27ef44b1b966555d6965130373b5f8b 100644
--- a/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
+++ b/src/main/scala/leon/invariant/util/TVarFactory.scala
@@ -2,11 +2,8 @@ package leon
package invariant.util
import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+import scala.collection.mutable.{ Set => MutableSet}
object TVarFactory {
diff --git a/src/main/scala/leon/invariant/util/TimerUtil.scala b/src/main/scala/leon/invariant/util/TimerUtil.scala
index 1284951709d4c374c56f1115b8b946f1a796855d..77e9b520116234e1d4bb6fee6ddf7563deed1640 100644
--- a/src/main/scala/leon/invariant/util/TimerUtil.scala
+++ b/src/main/scala/leon/invariant/util/TimerUtil.scala
@@ -2,9 +2,6 @@ package leon
package invariant.util
import utils._
-import solvers._
-import invariant.engine._
-import purescala.Expressions._
object TimerUtil {
/**
@@ -12,13 +9,13 @@ object TimerUtil {
*/
def scheduleTask(callBack: () => Unit, timeOut: Long): Option[java.util.Timer] = {
if (timeOut > 0) {
- val timer = new java.util.Timer();
+ val timer = new java.util.Timer()
timer.schedule(new java.util.TimerTask() {
def run() {
callBack()
timer.cancel() //the timer will be cancelled after it runs
}
- }, timeOut);
+ }, timeOut)
Some(timer)
} else None
}
@@ -30,7 +27,6 @@ class InterruptOnSignal(it: Interruptible) {
private var keepRunning = true
override def run(): Unit = {
- val startTime: Long = System.currentTimeMillis
while (!signal && keepRunning) {
Thread.sleep(100) // a relatively infrequent poll
}
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 6e3e45f22a49bc3ef70d0d18e3d0371fedac2654..4494787081ace61dfe1e1c086a702da6b2be15c4 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -33,8 +33,8 @@ object ProgramUtil {
*/
def copyProgram(prog: Program, mapdefs: (Seq[Definition] => Seq[Definition])): Program = {
prog.copy(units = prog.units.collect {
- case unit if (!unit.defs.isEmpty) => unit.copy(defs = unit.defs.collect {
- case module : ModuleDef if (!module.defs.isEmpty) =>
+ case unit if unit.defs.nonEmpty => unit.copy(defs = unit.defs.collect {
+ case module : ModuleDef if module.defs.nonEmpty =>
module.copy(defs = mapdefs(module.defs))
case other => other
})
@@ -71,11 +71,11 @@ object ProgramUtil {
}
def mapFunctionsInExpr(funmap: Map[FunDef, FunDef])(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(tfd, args) if funmap.contains(tfd.fd) =>
FunctionInvocation(TypedFunDef(funmap(tfd.fd), tfd.tps), args)
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
/**
@@ -161,7 +161,7 @@ object ProgramUtil {
}
def translateExprToProgram(ine: Expr, currProg: Program, newProg: Program): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(TypedFunDef(fd, tps), args) =>
functionByName(fullName(fd)(currProg), newProg) match {
case Some(nfd) =>
@@ -169,8 +169,8 @@ object ProgramUtil {
case _ =>
throw new IllegalStateException(s"Cannot find translation for ${fd.id.name}")
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def getFunctionReturnVariable(fd: FunDef) = {
@@ -205,18 +205,18 @@ object PredicateUtil {
*/
def isTemplateExpr(expr: Expr): Boolean = {
var foundVar = false
- simplePostTransform((e: Expr) => e match {
- case Variable(id) => {
+ simplePostTransform {
+ case e@Variable(id) => {
if (!TemplateIdFactory.IsTemplateIdentifier(id))
foundVar = true
e
}
- case ResultVariable(_) => {
+ case e@ResultVariable(_) => {
foundVar = true
e
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
!foundVar
}
@@ -234,13 +234,13 @@ object PredicateUtil {
*/
def hasReals(expr: Expr): Boolean = {
var foundReal = false
- simplePostTransform((e: Expr) => e match {
- case _ => {
+ simplePostTransform {
+ case e => {
if (e.getType == RealType)
- foundReal = true;
+ foundReal = true
e
}
- })(expr)
+ }(expr)
foundReal
}
@@ -252,13 +252,13 @@ object PredicateUtil {
*/
def hasInts(expr: Expr): Boolean = {
var foundInt = false
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) => {
- foundInt = true;
+ foundInt = true
e
}
- case _ => e
- })(expr)
+ case e => e
+ }(expr)
foundInt
}
@@ -268,29 +268,29 @@ object PredicateUtil {
def atomNum(e: Expr): Int = {
var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case And(args) => {
+ simplePostTransform {
+ case e@And(args) => {
count += args.size
e
}
- case Or(args) => {
+ case e@Or(args) => {
count += args.size
e
}
- case _ => e
- })(e)
+ case e => e
+ }(e)
count
}
def numUIFADT(e: Expr): Int = {
var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_) => {
+ simplePostTransform {
+ case e@(FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_)) => {
count += 1
e
}
- case _ => e
- })(e)
+ case e => e
+ }(e)
count
}
@@ -327,12 +327,12 @@ object PredicateUtil {
//replaces occurrences of mult by Times
def multToTimes(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
+ simplePostTransform {
case FunctionInvocation(TypedFunDef(fd, _), args) if isMultFunctions(fd) => {
Times(args(0), args(1))
}
- case _ => e
- })(ine)
+ case e => e
+ }(ine)
}
def createAnd(exprs: Seq[Expr]): Expr = {
diff --git a/src/main/scala/leon/invariant/util/Util.scala b/src/main/scala/leon/invariant/util/Util.scala
index f8358dec14f22f420a2b19b90dcf9dd9d308d80d..a792f1586479d5989773cdeee7e322eaa66983a6 100644
--- a/src/main/scala/leon/invariant/util/Util.scala
+++ b/src/main/scala/leon/invariant/util/Util.scala
@@ -1,19 +1,16 @@
package leon
package invariant.util
-import purescala.Common._
-import purescala.Definitions._
import purescala.Expressions._
-import purescala.ExprOps._
import purescala.Types._
-import leon.purescala.PrettyPrintable
-import leon.purescala.PrinterContext
+import purescala.PrettyPrintable
+import purescala.PrinterContext
import purescala.PrinterHelpers._
object FileCountGUID {
var fileCount = 0
def getID: Int = {
- var oldcnt = fileCount
+ val oldcnt = fileCount
fileCount += 1
oldcnt
}
@@ -32,7 +29,7 @@ case class ResultVariable(tpe: TypeTree) extends Expr with Terminal with PrettyP
val getType = tpe
override def toString: String = "#res"
- def printWith(implicit pctx: PrinterContext) {
+ def printWith(implicit pctx: PrinterContext) = {
p"#res"
}
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 3dd72ad613023fe5e9a30a7375aa34926de2c586..4959ae799c8f34b25dbdf1cac812ef8d954b4717 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -3,13 +3,11 @@
package leon
package repair
-import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Types._
import purescala.DefOps._
-import purescala.Quantification._
import purescala.Constructors._
import purescala.Extractors.unwrapTuple