From ea31f269705348aea170e981199379688fdaebdd Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 19 Jan 2015 15:06:27 +0100
Subject: [PATCH] Unknown during validation yields optimistic solution
---
src/main/scala/leon/repair/Repairman.scala | 8 ++++++--
src/main/scala/leon/synthesis/rules/CegisLike.scala | 9 ++++++++-
2 files changed, 14 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e80100f78..f72b88920 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -78,9 +78,13 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case NotValid(_, ces) if !ces.isEmpty =>
reporter.error("I ended up finding this counter example:\n"+ces.mkString(" | "))
- case _ =>
+ case NotValid(_, _) =>
solutions ::= sol
- reporter.info("Solution was not trusted but verification passed!")
+ reporter.warning("Solution is not trusted!")
+
+ case Valid =>
+ solutions ::= sol
+ reporter.info("Solution was not trusted but post-validation passed!")
}
} else {
reporter.info("Found trusted solution!")
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index dcc7cad3f..622ab658d 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -403,7 +403,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
return Left(Stream(Solution(BooleanLiteral(true), Set(), sol, true)))
case None =>
- None
+ if (useOptTimeout) {
+ // Interpret timeout in CE search as "the candidate is valid"
+ sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
+ // Optimistic valid solution
+ return Left(Stream(Solution(BooleanLiteral(true), Set(), sol, false)))
+ } else {
+ None
+ }
}
} finally {
solver.free
--
GitLab