Provide reliable way to shutdown long-lasting rules

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -432,7 +432,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
             reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
 
             if (!forceStop) {
-              if (Settings.luckyTest) {
+              if (Settings.luckyTest && false) {
                 // we need the model to perform the additional test
                 reporter.info(" - Running search without blocked literals (w/ lucky test)")
               } else {
@@ -447,7 +447,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
                   foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
                 case Some(true) =>
                   //reporter.info("SAT WITHOUT Blockers")
-                  if (Settings.luckyTest && !forceStop) {
+                  if (Settings.luckyTest && !forceStop && false) {
                     // we might have been lucky :D
                     val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
                     if(wereWeLucky) {

src/main/scala/leon/synthesis/ParallelSearch.scala

@@ -20,7 +20,7 @@ class ParallelSearch(synth: Synthesizer,
 
     solver.initZ3
 
-    SynthesisContext(solver = solver, reporter = synth.reporter)
+    SynthesisContext(solver = solver, reporter = synth.reporter, shouldStop = synth.shouldStop)
   }
 
   def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {

src/main/scala/leon/synthesis/SynthesisContext.scala

@@ -3,12 +3,15 @@ package synthesis
 
 import solvers.Solver
 
+import java.util.concurrent.atomic.AtomicBoolean
+
 case class SynthesisContext(
   solver: Solver,
-  reporter: Reporter
+  reporter: Reporter,
+  shouldStop: AtomicBoolean
 )
 
 object SynthesisContext {
-  def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter)
+  def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter, new AtomicBoolean(false))
 }
 

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -15,6 +15,8 @@ import collection.mutable.PriorityQueue
 
 import synthesis.search._
 
+import java.util.concurrent.atomic.AtomicBoolean
+
 class Synthesizer(val context : LeonContext,
                   val solver: Solver,
                   val program: Program,
@@ -26,7 +28,7 @@ class Synthesizer(val context : LeonContext,
 
   import reporter.{error,warning,info,fatalError}
 
-  var continue = true
+  var shouldStop = new AtomicBoolean(false)
 
   def synthesize(): (Solution, Boolean) = {
 
@@ -43,7 +45,7 @@ class Synthesizer(val context : LeonContext,
         println
         reporter.info("Aborting...")
 
-        continue = false
+        shouldStop.set(true)
         search.stop()
 
         Signal.handle(sigINT, oldHandler)

src/main/scala/leon/synthesis/rules/Cegis.scala

@@ -163,7 +163,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
 
               //println("Unrolling #"+unrolings+" bss size: "+bss.size)
 
-              while (result.isEmpty && continue) {
+              while (result.isEmpty && continue && !sctx.shouldStop.get) {
                 //println("Looking for CE...")
                 //println("-"*80)
                 //println(basePhi)
@@ -262,7 +262,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
               }
 
               unrolings += 1
-            } while(unrolings < maxUnrolings && result.isEmpty)
+            } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
 
             result.getOrElse(RuleApplicationImpossible)
 

src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala

@@ -4,6 +4,7 @@ import akka.actor._
 import akka.util.duration._
 import akka.util.Timeout
 import akka.pattern.ask
+import akka.pattern.AskTimeoutException
 import akka.dispatch.Await
 
 abstract class AndOrGraphParallelSearch[WC,
@@ -27,7 +28,11 @@ abstract class AndOrGraphParallelSearch[WC,
       system.actorOf(Props(new Worker(master)), name = "Worker"+i)
     }
 
-    Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+    try {
+      Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+    } catch {
+      case e: AskTimeoutException =>
+    }
 
     if (system ne null) {
       system.shutdown
@@ -92,8 +97,6 @@ abstract class AndOrGraphParallelSearch[WC,
                 w ! RequestOrTask(ol.task)
             }
           }
-
-
       }
     }