Skip to content
Snippets Groups Projects
Commit caab8799 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Respect --timeout in synthesis

parent 79020284
Branches
Tags
No related merge requests found
......@@ -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()
}
}
}
......
......@@ -17,7 +17,6 @@ case class SynthesisSettings(
// Cegis related options
cegisUseOptTimeout: Option[Boolean] = None,
cegisUseShrink: Option[Boolean] = None,
cegisUseVanuatoo: Option[Boolean] = None
)
......@@ -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)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment