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

Handle SIGINT, produce solution on abort.

parent 572cc5a4
No related branches found
No related tags found
No related merge requests found
......@@ -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()
......
......@@ -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)
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment