diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index c57a1e4514b00372033c7e19242b7782e40b8c56..c9f6af1681735ad3e1b1b176a2b16e178caf9ecf 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -1,6 +1,7 @@
package leon
// typically these settings can be changed through some command-line switch.
+// TODO this global object needs to die (or at least clean out of its var's)
object Settings {
var experimental : Boolean = false
var showIDs: Boolean = false
@@ -10,7 +11,6 @@ object Settings {
var runDefaultExtensions: Boolean = true
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
- var zeroInlining : Boolean = true
var useBAPA: Boolean = false
var impureTestcases: Boolean = false
var nbTestcases: Int = 1
diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
index 500606ac05704ded8282625301e2d9353cb30b02..504016d9dfcf842a7e0e05990e16003a5b522cc8 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -220,116 +220,3 @@ class Analysis(val program : Program, val reporter: Reporter) {
}
}
}
-
-object Analysis {
- private val keepCallWhenInlined: Boolean = true
-
- private def defineOneInlining(f : FunctionInvocation) : (Expr, Expr) = {
- val FunctionInvocation(fd, args) = f
- val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
- val newFunctionCall = FunctionInvocation(fd, newLetIDs.map(Variable(_))).setType(f.getType)
- val callID = FreshIdentifier("call_" + fd.id.name, true).setType(newBody.getType)
- val callTree = Let(callID, (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)), Variable(callID))
-
- (Equals(newFunctionCall, Variable(callID)), callTree)
- }
-
- private def inlineFunctionCall(f : FunctionInvocation) : Expr = {
- val FunctionInvocation(fd, args) = f
- val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
- simplifyLets((newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)))
- }
-
- def inlineNonRecursiveFunctions(program: Program, expression: Expr) : Expr = {
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && !program.isRecursive(fd) => Some(inlineFunctionCall(f))
- case _ => None
- }
-
- var change: Boolean = true
- var toReturn: Expr = expression
- while(change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = t
- }
- toReturn
- }
-
- def unrollRecursiveFunctions(program: Program, expression: Expr, times: Int) : Expr = {
- def urf1(expression: Expr, times: Int) : Expr = {
- var newEqs: List[Expr] = Nil
-
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
- val (newEq, bdy) = defineOneInlining(f)
- newEqs = newEq :: newEqs
- Some(bdy)
- }
- case _ => None
- }
-
- var remaining = if(times < 0) 0 else times
- var change: Boolean = true
- var toReturn: Expr = expression
- while(remaining > 0 && change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = inlineNonRecursiveFunctions(program, t)
- remaining = remaining - 1
- }
- liftLets(Implies(And(newEqs.reverse), toReturn))
- }
-
- def urf2(expression: Expr, times: Int) : Expr = {
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => Some(inlineFunctionCall(f))
- case _ => None
- }
-
- var remaining = if(times < 0) 0 else times
- var change: Boolean = true
- var toReturn: Expr = expression
- while(remaining > 0 && change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = inlineNonRecursiveFunctions(program, t)
- remaining = remaining - 1
- }
- toReturn
- }
-
- if(keepCallWhenInlined)
- urf1(expression, times)
- else
- urf2(expression, times)
- }
-
- def inlineContracts(expression: Expr) : Expr = {
- var trueThings: List[Expr] = Nil
-
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasPostcondition => {
- val argsAsLet = fd.args.map(a => FreshIdentifier("parg_" + a.id.name, true).setType(a.tpe)).toList
- val argsAsLetVars = argsAsLet.map(Variable(_))
- val resultAsLet = FreshIdentifier("call_" + fd.id.name, true).setType(f.getType)
- val newFunCall = FunctionInvocation(fd, argsAsLetVars)
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip argsAsLetVars) : _*) + (ResultVariable() -> Variable(resultAsLet))
- // this thing is full of let variables! We will need to lift the let
- // defs. later to make sure they capture this
- val trueFact = replace(substMap, freshenLocals(fd.postcondition.get))
- val defList: Seq[(Identifier,Expr)] = ((argsAsLet :+ resultAsLet) zip (args :+ newFunCall))
- trueThings = trueFact :: trueThings
- // again: these let defs. need eventually to capture the "true thing"
- Some(defList.foldRight[Expr](Variable(resultAsLet))((iap, e) => Let(iap._1, iap._2, e)))
- }
- case _ => None
- }
- val result = searchAndReplaceDFS(applyToCall)(expression)
- liftLets(Implies(And(trueThings.reverse), result))
- }
-}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index a3f4374ccbce324214b4c437429b3910ef1e6936..69d5cf6c4636e912f0cff1baca6b1dd354748e3f 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -44,41 +44,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
import Analysis._
- if(Settings.zeroInlining) {
- withPrec
- } else {
- if(Settings.experimental) {
- reporter.info("Raw:")
- reporter.info(withPrec)
- reporter.info("Raw, expanded:")
- reporter.info(expandLets(withPrec))
- }
- reporter.info(" - inlining...")
- val expr0 = inlineNonRecursiveFunctions(program, withPrec)
- if(Settings.experimental) {
- reporter.info("Inlined:")
- reporter.info(expr0)
- reporter.info("Inlined, expanded:")
- reporter.info(expandLets(expr0))
- }
- reporter.info(" - unrolling...")
- val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
- if(Settings.experimental) {
- reporter.info("Unrolled:")
- reporter.info(expr1)
- reporter.info("Unrolled, expanded:")
- reporter.info(expandLets(expr1))
- }
- reporter.info(" - inlining contracts...")
- val expr2 = inlineContracts(expr1)
- if(Settings.experimental) {
- reporter.info("Contract'ed:")
- reporter.info(expr2)
- reporter.info("Contract'ed, expanded:")
- reporter.info(expandLets(expr2))
- }
- expr2
- }
+ withPrec
}
if(functionDefinition.fromLoop)
Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))