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

Add rule in --manual to close a branch

parent 501e9663
No related branches found
No related tags found
No related merge requests found
...@@ -85,6 +85,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] { ...@@ -85,6 +85,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case _ => case _ =>
} }
if (options.manualSearch) {
options = options.copy(rules = rules.AsChoose +: options.rules)
}
options options
} }
......
/* Copyright 2009-2013 EPFL, Lausanne */
package leon
package synthesis
package rules
case object AsChoose extends Rule("As Choose") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
Some(new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
def apply(sctx: SynthesisContext) = {
RuleSuccess(Solution.choose(p))
}
})
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment