From caab8799a7c3f64b329e95d2378194d66de2fc26 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 17 Dec 2015 16:26:19 +0100
Subject: [PATCH] Respect --timeout in synthesis
---
.../scala/leon/synthesis/SynthesisPhase.scala | 33 ++++++++++---------
.../leon/synthesis/SynthesisSettings.scala | 1 -
.../leon/synthesis/rules/CEGISLike.scala | 7 +---
3 files changed, 19 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 72cfffec3..b9ba6df1f 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -6,6 +6,7 @@ package synthesis
import purescala.ExprOps._
import purescala.ScalaPrinter
+import leon.utils._
import purescala.Definitions.{Program, FunDef}
import leon.utils.ASCIIHelpers
@@ -20,12 +21,11 @@ object SynthesisPhase extends TransformationPhase {
val optDerivTrees = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
// CEGIS options
- val optCEGISShrink = LeonFlagOptionDef( "cegis:shrink", "Shrink non-det programs when tests pruning works well", true)
val optCEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
val optCEGISVanuatoo = LeonFlagOptionDef( "cegis:vanuatoo", "Generate inputs using new korat-style generator", false)
override val definedOptions : Set[LeonOptionDef[Any]] =
- Set(optManual, optCostModel, optDerivTrees, optCEGISShrink, optCEGISOptTimeout, optCEGISVanuatoo)
+ Set(optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISVanuatoo)
def processOptions(ctx: LeonContext): SynthesisSettings = {
val ms = ctx.findOption(optManual)
@@ -57,7 +57,6 @@ object SynthesisPhase extends TransformationPhase {
manualSearch = ms,
functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
- cegisUseShrink = ctx.findOption(optCEGISShrink),
cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo)
)
}
@@ -74,21 +73,25 @@ object SynthesisPhase extends TransformationPhase {
val synthesizer = new Synthesizer(ctx, program, ci, options)
- val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+ val to = new TimeoutFor(ctx.interruptManager)
- try {
- if (options.generateDerivationTrees) {
- val dot = new DotGenerator(search.g)
- dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
- }
+ to.interruptAfter(options.timeoutMs) {
+ val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+
+ try {
+ if (options.generateDerivationTrees) {
+ val dot = new DotGenerator(search.g)
+ dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
+ }
- val (sol, _) = solutions.head
+ val (sol, _) = solutions.head
- val expr = sol.toSimplifiedExpr(ctx, program)
- fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
- functions += fd
- } finally {
- synthesizer.shutdown()
+ val expr = sol.toSimplifiedExpr(ctx, program)
+ fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
+ functions += fd
+ } finally {
+ synthesizer.shutdown()
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 9d227bdb6..5202818e1 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -17,7 +17,6 @@ case class SynthesisSettings(
// Cegis related options
cegisUseOptTimeout: Option[Boolean] = None,
- cegisUseShrink: Option[Boolean] = None,
cegisUseVanuatoo: Option[Boolean] = None
)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 09ee7dd30..4f03c9bed 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,14 +45,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// CEGIS Flags to activate or deactivate features
val useOptTimeout = sctx.settings.cegisUseOptTimeout.getOrElse(true)
val useVanuatoo = sctx.settings.cegisUseVanuatoo.getOrElse(false)
- val useShrink = sctx.settings.cegisUseShrink.getOrElse(false)
// Limits the number of programs CEGIS will specifically validate individually
val validateUpTo = 3
- // Shrink the program when the ratio of passing cases is less than the threshold
- val shrinkThreshold = 1.0/2
-
val interruptManager = sctx.context.interruptManager
val params = getParams(sctx, p)
@@ -827,14 +823,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
if (nPassing <= validateUpTo) {
// All programs failed verification, we filter everything out and unfold
- //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
doFilter = false
skipCESearch = true
}
}
}
- if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+ if (doFilter) {
sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
wrongPrograms.foreach {
ndProgram.excludeProgram(_, true)
--
GitLab