From 685d25bab24420a8a7643cfed497a5e28f778628 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 2 May 2016 16:33:38 +0200
Subject: [PATCH] CEGIS should reject crashing examples early
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 1247edf33..60cc1ca5e 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -866,7 +866,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val examples = allInputExamples()
var badExamples = List[Example]()
var stop = false
- for (e <- examples if !stop) {
+ for (e <- examples if !stop && !badExamples.contains(e)) {
ndProgram.testForProgram(bs)(e) match {
case Some(true) => // ok, passes
case Some(false) =>
@@ -936,8 +936,9 @@ abstract class CEGISLike(name: String) extends Rule(name) {
failedTestsStats(ce) += 1
ndProgram.excludeProgram(bs, false)
+ var bad = false
// Retest whether the newly found C-E invalidates some programs
- ndProgram.prunedPrograms.foreach { p =>
+ for (p <- ndProgram.prunedPrograms if !bad) {
ndProgram.testForProgram(p)(ce) match {
case Some(true) =>
case Some(false) =>
@@ -947,6 +948,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
case None =>
debug(s" Test $ce failed, removing...")
gi -= ce
+ bad = true
}
}
--
GitLab