From 7e8f60bf6e5c6e893924196d1c2bfad5ad49e96e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 18 Mar 2016 17:19:16 +0100
Subject: [PATCH] Refactor checkVC stopping parameter, use it in Synthesizer
---
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 3 ++-
src/main/scala/leon/verification/VerificationPhase.scala | 6 +++---
3 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index d941f1c0e..919a8c458 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -208,7 +208,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val report = VerificationPhase.checkVCs(
vctx,
vcs,
- stopAfter = Some({ (vc, vr) => vr.isInvalid })
+ stopWhen = _.isInvalid
)
val vrs = report.vrs
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 50f2da1af..467ed7376 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -3,6 +3,7 @@
package leon
package synthesis
+import leon.purescala.Expressions.Choose
import purescala.Definitions._
import purescala.ExprOps._
import purescala.DefOps._
@@ -145,7 +146,7 @@ class Synthesizer(val context : LeonContext,
try {
val vctx = VerificationContext(context, npr, solverf, context.reporter)
val vcs = generateVCs(vctx, fds)
- val vcreport = checkVCs(vctx, vcs)
+ val vcreport = checkVCs(vctx, vcs, stopWhen = _.isInvalid)
if (vcreport.totalValid == vcreport.totalConditions) {
(sol, Some(true))
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index e9a9fe601..39ed875a0 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -95,7 +95,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
def checkVCs(
vctx: VerificationContext,
vcs: Seq[VC],
- stopAfter: Option[(VC, VCResult) => Boolean] = None
+ stopWhen: VCResult => Boolean = _ => false
): VerificationReport = {
val interruptManager = vctx.context.interruptManager
@@ -107,14 +107,14 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
for (vc <- vcs.par if !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter.exists(_(vc, r))
+ stop = stopWhen(r)
vc -> Some(r)
}
} else {
for (vc <- vcs.toSeq.sortWith((a,b) => a.fd.getPos < b.fd.getPos) if !interruptManager.isInterrupted && !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter.exists(_(vc, r))
+ stop = stopWhen(r)
vc -> Some(r)
}
}
--
GitLab