diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala index 4cc4750d39e5d9e070929b40dd845a4c2546b58e..45316adff5d64d141f5793e539d3cc1a1dbccefa 100644 --- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala +++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala @@ -183,11 +183,10 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F * Uses default postcondition VC, but can be overriden in the case of non-standard VCs */ def verifyVC(newprog: Program, newroot: FunDef) = { - (newroot.postcondition, newroot.body) match { - case (Some(post), Some(body)) => - val vc = implies(newroot.precOrTrue, application(post, Seq(body))) - solveUsingLeon(ctx.leonContext, newprog, VC(vc, newroot, VCKinds.Postcondition)) - } + val post = newroot.postcondition.get + val body = newroot.body.get + val vc = implies(newroot.precOrTrue, application(post, Seq(body))) + solveUsingLeon(ctx.leonContext, newprog, VC(vc, newroot, VCKinds.Postcondition)) } import leon.solvers._ diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala index da56f3a8ed987505520c3246fd527c9b371dc36b..f760289d554393b9c3fbb82356895d733ffb6bb1 100644 --- a/src/main/scala/leon/invariant/structure/Formula.scala +++ b/src/main/scala/leon/invariant/structure/Formula.scala @@ -3,26 +3,20 @@ 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 java.io._ -import solvers.z3._ import invariant.engine._ import invariant.util._ -import leon.solvers.Model +import solvers.Model import Util._ import PredicateUtil._ import TVarFactory._ import ExpressionTransformer._ -import evaluators._ import invariant.factories._ import evaluators._ import EvaluationResults._ @@ -224,7 +218,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal * 'neweexpr' is required to be in negation normal form and And/Ors have been pulled up */ def conjoinWithDisjunct(guard: Variable, newexpr: Expr, callParents: List[FunDef], inSpec:Boolean) = { - val (exprRoot, newGaurds) = addConstraints(newexpr, callParents, _ => inSpec) + val (exprRoot, newGuards) = addConstraints(newexpr, callParents, _ => inSpec) //add 'newguard' in conjunction with 'disjuncts(guard)' val ctrs = disjuncts(guard) disjuncts -= guard @@ -233,7 +227,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal } def conjoinWithRoot(newexpr: Expr, callParents: List[FunDef], inSpec: Boolean) = { - val (exprRoot, newGaurds) = addConstraints(newexpr, callParents, _ => inSpec) + val (exprRoot, newGuards) = addConstraints(newexpr, callParents, _ => inSpec) roots :+= exprRoot exprRoot } @@ -401,10 +395,10 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal * Functions for stats */ def atomsCount = disjuncts.map(_._2.size).sum + conjuncts.map(i => atomNum(i._2)).sum - def funsCount = disjuncts.map(_._2.filter { + def funsCount = disjuncts.map(_._2.count { case _: Call | _: ADTConstraint => true - case _ => false - }.size).sum + case _ => false + }).sum /** * Functions solely used for debugging @@ -465,14 +459,14 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal def pickSatFromUnflatFormula(unflate: Expr, model: Model, evaluator: DefaultEvaluator): Seq[Expr] = { def rec(e: Expr): Seq[Expr] = e match { case IfExpr(cond, thn, elze) => - evaluator.eval(cond, model) match { + (evaluator.eval(cond, model): @unchecked) match { case Successful(BooleanLiteral(true)) => cond +: rec(thn) case Successful(BooleanLiteral(false)) => Not(cond) +: rec(elze) } case And(args) => args flatMap rec case Or(args) => rec(args.find(evaluator.eval(_, model) == Successful(BooleanLiteral(true))).get) case Equals(b: Variable, rhs) if b.getType == BooleanType => - evaluator.eval(b, model) match { + (evaluator.eval(b, model): @unchecked) match { case Successful(BooleanLiteral(true)) => rec(b) ++ rec(rhs) case Successful(BooleanLiteral(false)) => diff --git a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala index 2ad934ed1994e2876a8392a28e6a54c39b3f88fa..d5c0ccc0d1f65d6cab2438bb27ae61e44b37453e 100644 --- a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala +++ b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala @@ -78,7 +78,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) { } // an weaker property whose equality is necessary for mayAlias val hashcode = - key match { + (key: @unchecked) match { case Left(TypedFunDef(fd, _)) => fd.id.hashCode() case Right(ct: CaseClassType) => ct.classDef.id.hashCode() case Right(tp @ TupleType(tps)) => (tps.hashCode() << 3) ^ tp.dimension diff --git a/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala b/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala index 580af747f0e4a399a86158945e07c11df2a9bcc0..920e1a9885bfe9bbf45039ab8c91ed3cf98b8c8a 100644 --- a/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala +++ b/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala @@ -4,9 +4,7 @@ package leon.regression.orb import leon.test._ import leon._ -import purescala.Definitions._ import invariant.engine._ -import transformations._ import laziness._ import verification._ @@ -35,14 +33,14 @@ class LazyEvalRegressionSuite extends LeonRegressionSuite { } report.resourceVeri match { case None => fail(s"No resource verification report found!") - case Some(rep: VerificationReport) => - val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc } - if (!fails.isEmpty) - fail(s"Resource verification failed for functions ${fails.map(_.fd).mkString("\n")}") case Some(rep: InferenceReport) => val fails = rep.conditions.filterNot(_.prettyInv.isDefined) if (!fails.isEmpty) fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}") + case Some(rep: VerificationReport) => + val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc } + if (!fails.isEmpty) + fail(s"Resource verification failed for functions ${fails.map(_.fd).mkString("\n")}") } }