From 572cc5a4515a8a6b4e6e3579affcafdc275d5d87 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sat, 17 Nov 2012 13:35:01 +0100
Subject: [PATCH] Reconstruct partial solution, only possible case for now is
in case of timeout
---
src/main/scala/leon/synthesis/Synthesizer.scala | 17 +++++++++++++++--
1 file changed, 15 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 63db3ca0a..c5ae914f2 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -51,7 +51,8 @@ class Synthesizer(val reporter: Reporter,
}
}
- while (!workList.isEmpty) {
+ var continue = true
+ while (!workList.isEmpty && continue) {
val task = workList.dequeue()
val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
@@ -78,7 +79,19 @@ class Synthesizer(val reporter: Reporter,
if (timeoutExpired()) {
warning("Timeout reached")
- workList.clear()
+ continue = false
+ }
+ }
+
+ if (!workList.isEmpty) {
+ // We flush the worklist by solving everything with chooses, that should
+ // rebuild a partial solution
+ while (!workList.isEmpty) {
+ val t = workList.dequeue()
+
+ if (t.parent ne null) {
+ t.parent.partlySolvedBy(t, Solution.choose(t.problem))
+ }
}
}
--
GitLab