From ba97cc0efe84f84ecc0bcdec83b4af7251731a99 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 02:03:34 +0200
Subject: [PATCH] Add UnusedInput
---
src/main/scala/leon/synthesis/Rules.scala | 20 +++++++++++++++++++
.../scala/leon/synthesis/Synthesizer.scala | 10 ++++++----
2 files changed, 26 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 00c8af3a2..e835637a4 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -10,6 +10,7 @@ object Rules {
new OnePoint(synth),
new Ground(synth),
new CaseSplit(synth),
+ new UnusedInput(synth),
new Assert(synth)
)
}
@@ -144,3 +145,22 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
}
}
}
+
+class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
+ def isApplicable(p: Problem, parent: Task): List[Task] = {
+ val unused = p.as.toSet -- variablesOf(p.phi)
+
+ if (!unused.isEmpty) {
+ val sub = p.copy(as = p.as.filterNot(unused))
+
+ val onSuccess: List[Solution] => Solution = {
+ case List(s) => s
+ case _ => Solution.none
+ }
+
+ List(new Task(synth, parent, this, p, List(sub), onSuccess, 300))
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 12da7a5e3..ca8507b85 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -12,7 +12,7 @@ import collection.mutable.PriorityQueue
class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
import r.{error,warning,info,fatalError}
- private[this] var solution: Solution = null
+ private[this] var solution: Option[Solution] = None
def synthesize(p: Problem, rules: List[Rule]): Solution = {
@@ -26,7 +26,9 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
workList += rootTask
- while (!workList.isEmpty) {
+ solution = None
+
+ while (!workList.isEmpty && solution.isEmpty) {
val task = workList.dequeue()
task.subProblems match {
@@ -59,7 +61,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
}
- solution
+ solution.getOrElse(Solution.none)
}
def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
@@ -79,7 +81,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
task match {
case rt: RootTask =>
info(" SUCCESS!")
- this.solution = solution
+ this.solution = Some(solution)
case t: Task =>
info(" => Solved "+task.problem+" ⊢ "+solution)
t.parent.subSucceeded(t.problem, solution)
--
GitLab