From c0214950bf6cda75995ec38b09ad49a5cebff807 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sun, 18 Nov 2012 19:37:10 +0100
Subject: [PATCH] Handle SIGINT, produce solution on abort.
---
src/main/scala/leon/synthesis/Synthesizer.scala | 15 ++++++++++++++-
src/main/scala/leon/synthesis/rules/Cegis.scala | 4 ++--
2 files changed, 16 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index c5ae914f2..f33ffe5c9 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -6,6 +6,7 @@ import purescala.Definitions.{Program, FunDef}
import purescala.TreeOps._
import purescala.Trees.{Expr, Not}
import purescala.ScalaPrinter
+import sun.misc.{Signal, SignalHandler}
import solvers.Solver
import java.io.File
@@ -36,7 +37,10 @@ class Synthesizer(val reporter: Reporter,
val worstSolution = Solution.choose(problem)
+ var continue = true
+
def synthesize(): Solution = {
+ continue = true
workList.clear()
workList += rootTask
@@ -51,7 +55,16 @@ class Synthesizer(val reporter: Reporter,
}
}
- var continue = true
+ val sigINT = new Signal("INT")
+ var oldHandler: SignalHandler = null
+ oldHandler = Signal.handle(sigINT, new SignalHandler {
+ def handle(sig: Signal) {
+ reporter.info("Aborting...")
+ continue = false;
+ Signal.handle(sigINT, oldHandler)
+ }
+ })
+
while (!workList.isEmpty && continue) {
val task = workList.dequeue()
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 52691946d..bc992ee80 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -130,7 +130,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
var predicates: Seq[Expr] = Seq()
var continue = true
- while (result.isEmpty && continue) {
+ while (result.isEmpty && continue && synth.continue) {
val basePhi = currentF.entireFormula
val constrainedPhi = And(basePhi +: predicates)
//println("-"*80)
@@ -211,7 +211,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
lastF = currentF
currentF = currentF.unroll
unrolings += 1
- } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty)
+ } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
result.getOrElse(RuleInapplicable)
}
--
GitLab