From f430407992beae25baa7f321f2f17a4bb9c66d3d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Sat, 20 Jul 2013 01:41:03 +0200
Subject: [PATCH] Add rule in --manual to close a branch
---
.../scala/leon/synthesis/SynthesisPhase.scala | 4 ++++
.../scala/leon/synthesis/rules/AsChoose.scala | 16 ++++++++++++++++
2 files changed, 20 insertions(+)
create mode 100644 src/main/scala/leon/synthesis/rules/AsChoose.scala
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 9346b5530..fd210b24b 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -85,6 +85,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case _ =>
}
+ if (options.manualSearch) {
+ options = options.copy(rules = rules.AsChoose +: options.rules)
+ }
+
options
}
diff --git a/src/main/scala/leon/synthesis/rules/AsChoose.scala b/src/main/scala/leon/synthesis/rules/AsChoose.scala
new file mode 100644
index 000000000..e7b1986bd
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/AsChoose.scala
@@ -0,0 +1,16 @@
+/* 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))
+ }
+ })
+ }
+}
+
--
GitLab