diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala index b41835e1a8b762223e84e5ede72ced36b59784eb..864f3ff285df43a9d49452c183b40b3874980f30 100644 --- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala +++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala @@ -199,7 +199,6 @@ object LazyVerificationPhase { def checkVCs(vcs: List[VC], checkCtx: LeonContext, p: Program) = { val timeout: Option[Long] = None - val reporter = checkCtx.reporter // Solvers selection and validation val baseSolverF = SolverFactory.getFromSettings(checkCtx, p) val solverF = timeout match { @@ -208,7 +207,7 @@ object LazyVerificationPhase { case None => baseSolverF } - val vctx = VerificationContext(checkCtx, p, solverF, reporter) + val vctx = new VerificationContext(checkCtx, p, solverF) try { VerificationPhase.checkVCs(vctx, vcs) //println("Resource Verification Results: \n" + veriRep.summaryString) diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala index 919a8c458de6a418a59518f7f269cd7feb106d7c..4b6d0ce83121e26e775ff4f4397f7e44acbe4d67 100644 --- a/src/main/scala/leon/repair/Repairman.scala +++ b/src/main/scala/leon/repair/Repairman.scala @@ -201,7 +201,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou def getVerificationCExs(fd: FunDef): Seq[Example] = { val timeoutMs = verifTimeoutMs.getOrElse(3000L) val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs) - val vctx = VerificationContext(ctx, program, solverf, reporter) + val vctx = new VerificationContext(ctx, program, solverf) val vcs = VerificationPhase.generateVCs(vctx, Seq(fd)) try { diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 0a668a05951c8a3b9237b1ea69a8eb5e6d5e99c7..3a2a1df7f9f837ebfee2aab53d43d0d77028a129 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -144,7 +144,7 @@ class Synthesizer(val context : LeonContext, val solverf = SolverFactory.default(context, npr).withTimeout(timeout) try { - val vctx = VerificationContext(context, npr, solverf, context.reporter) + val vctx = new VerificationContext(context, npr, solverf) val vcs = generateVCs(vctx, fds) val vcreport = checkVCs(vctx, vcs, stopWhen = _.isInvalid) diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala index 008a03f5aca8d737b2e46de4e3b3ce42a83ead40..75910e625432dce2b4084c93a95b8c8ce8d3638b 100644 --- a/src/main/scala/leon/verification/Tactic.scala +++ b/src/main/scala/leon/verification/Tactic.scala @@ -9,7 +9,7 @@ import purescala.Expressions._ abstract class Tactic(vctx: VerificationContext) { val description : String - implicit protected val ctx = vctx.context + implicit val ctx = vctx def generateVCs(fd: FunDef): Seq[VC] = { generatePostconditions(fd) ++ diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala index 1cbbf2103913f07a490a5641040abd3927c71bf2..d7850d079e88ce3d8cc37dc4338a817d42d4b40a 100644 --- a/src/main/scala/leon/verification/VerificationCondition.scala +++ b/src/main/scala/leon/verification/VerificationCondition.scala @@ -49,7 +49,6 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option def report(vctx: VerificationContext) { import vctx.reporter - import vctx.context status match { case VCStatus.Valid => @@ -64,7 +63,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option // is free to simplify val strings = cex.toSeq.sortBy(_._1.name).map { case (id, v) => - (id.asString(context), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx.context, vctx.program)) + (id.asString(vctx), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx, vctx.program)) } if (strings.nonEmpty) { diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala index be8f9efe56480b44c47aebc7c4eabeb4d3190975..87811eb8955cf2b1e1e1ac91c4c4c14adae01a4d 100644 --- a/src/main/scala/leon/verification/VerificationContext.scala +++ b/src/main/scala/leon/verification/VerificationContext.scala @@ -6,11 +6,17 @@ package verification import purescala.Definitions.Program import solvers._ -case class VerificationContext ( +class VerificationContext( context: LeonContext, - program: Program, - solverFactory: SolverFactory[Solver], - reporter: Reporter + val program: Program, + val solverFactory: SolverFactory[Solver] +) extends LeonContext( + context.reporter, + context.interruptManager, + context.options, + context.files, + context.classDir, + context.timers ) { - val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs) + lazy val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs) } diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala index 39ed875a056d3dcc189ab526302abc7569550085..01df60771b9c602272a28f3967e338c5f8f2ac34 100644 --- a/src/main/scala/leon/verification/VerificationPhase.scala +++ b/src/main/scala/leon/verification/VerificationPhase.scala @@ -36,7 +36,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] { baseSolverF } - val vctx = VerificationContext(ctx, program, solverF, reporter) + val vctx = new VerificationContext(ctx, program, solverF) reporter.debug("Generating Verification Conditions...") @@ -97,7 +97,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] { vcs: Seq[VC], stopWhen: VCResult => Boolean = _ => false ): VerificationReport = { - val interruptManager = vctx.context.interruptManager + val interruptManager = vctx.interruptManager var stop = false @@ -126,7 +126,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] { import vctx.reporter import vctx.solverFactory - val interruptManager = vctx.context.interruptManager + val interruptManager = vctx.interruptManager val vcCond = vc.condition @@ -135,7 +135,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] { try { reporter.synchronized { reporter.info(s" - Now considering '${vc.kind}' VC for ${vc.fd.id} @${vc.getPos}...") - reporter.debug(simplifyLets(vcCond).asString(vctx.context)) + reporter.debug(simplifyLets(vcCond).asString(vctx)) reporter.debug("Solving with: " + s.name) }