From 73d58d51a9e6817b58a9bb2c07c33f64537c4a9f Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 16 Dec 2014 17:44:15 +0100
Subject: [PATCH] Shortcut test discovery
---
src/main/scala/leon/repair/Repairman.scala | 22 +++++++++++++++-------
1 file changed, 15 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 68abb20c5..d14db9d35 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -296,7 +296,12 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val vctx = VerificationContext(ctx, prog, solver, reporter)
val vcs = AnalysisPhase.generateVerificationConditions(vctx, Some(List(fd.id.name)))
- AnalysisPhase.checkVerificationConditions(vctx, vcs, checkInParallel = true)
+ AnalysisPhase.checkVerificationConditions(
+ vctx,
+ vcs,
+ checkInParallel = true,
+ interruptOn = _.counterExample.isDefined
+ )
var invalid = false;
var ces = List[Seq[Expr]]()
@@ -357,7 +362,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
new InExample(ins)
}
}
-
+
val generatedTests = inputs
.take(maxEnumerated)
.filter(filtering)
@@ -370,14 +375,17 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case _ => false
}
- // Try to verify, if it fails, we have at least one CE
- val ces = getVerificationCounterExamples(fd, program) getOrElse Nil
-
// Extract passing/failing from the passes in POST
val ef = new ExamplesFinder(ctx, program)
- val (userPassing, userFailing) = ef.extractTests(fd)
+ val (userPassing, userFailing) = ef.extractTests(fd)
+
+ // If we have no ce yet, try to verify, if it fails, we have at least one CE
+ val ces = (generatedFailing ++ userFailing) match {
+ case Seq() => getVerificationCounterExamples(fd, program) getOrElse Nil
+ case nonEmpty => nonEmpty
+ }
- (generatedPassing ++ userPassing, generatedFailing ++ ces ++ userFailing)
+ (generatedPassing ++ userPassing, ces.toList )
}
--
GitLab