From b31f80fb02968eb88d5cb8e6c2f0753ff74eeddb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 12 Feb 2015 17:04:50 +0100
Subject: [PATCH] Always validate up to N programs, even if we got more passing
tests
---
.../leon/synthesis/rules/CegisLike.scala | 45 ++++++++++++-------
.../leon/test/synthesis/SynthesisSuite.scala | 2 +-
2 files changed, 30 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index bdcfb910c..fefec3462 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -59,6 +59,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// Limits the number of programs CEGIS will specifically validate individually
val validateUpTo = 5
+
val useBssFiltering = sctx.settings.cegisUseBssFiltering
val filterThreshold = 1.0/2
@@ -887,23 +888,35 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
if (nPassing == 0 || interruptManager.isInterrupted()) {
// No test passed, we can skip solver and unfold again, if possible
skipCESearch = true;
- } else if (nPassing <= validateUpTo) {
- // Small enough number of programs to try them individually
- ndProgram.validatePrograms(prunedPrograms) match {
- case Left(sols) if sols.nonEmpty =>
- result = Some(RuleClosed(sols))
- case Right(cexs) =>
- // All programs failed verification, we filter everything out and unfold
- //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
- skipCESearch = true;
- }
- } else if (((nPassing < nInitial*filterThreshold)) && useBssFiltering) {
- // We shrink the program to only use the bs mentionned
- val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
- ndProgram.shrinkTo(bssToKeep, unfolding == maxUnfoldings)
} else {
- wrongPrograms.foreach {
- ndProgram.excludeProgram(_)
+ var doFilter = true;
+
+ if (validateUpTo > 0) {
+ // Validate the first N programs individualy
+ ndProgram.validatePrograms(prunedPrograms.take(validateUpTo)) match {
+ case Left(sols) if sols.nonEmpty =>
+ doFilter = false
+ result = Some(RuleClosed(sols))
+ case Right(cexs) =>
+ if (nPassing <= validateUpTo) {
+ // All programs failed verification, we filter everything out and unfold
+ //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
+ doFilter = false
+ skipCESearch = true;
+ }
+ }
+ }
+
+ if (doFilter) {
+ if (((nPassing < nInitial*filterThreshold)) && useBssFiltering) {
+ // We shrink the program to only use the bs mentionned
+ val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
+ ndProgram.shrinkTo(bssToKeep, unfolding == maxUnfoldings)
+ } else {
+ wrongPrograms.foreach {
+ ndProgram.excludeProgram(_)
+ }
+ }
}
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 6d573a147..0296a1e51 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -323,7 +323,7 @@ object SortedList {
Decomp("Ineq. Split on 'head*' and 'v*'", List(
Close("CEGIS"),
Decomp("Equivalent Inputs *", List(
- Decomp("Unused Inputs *", List(
+ Decomp("Unused *", List(
Close("CEGIS")
))
)),
--
GitLab